Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴)) |
2 | | rexr 9964 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
3 | 2 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈
ℝ*) |
4 | | iccssxr 12127 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
5 | | volf 23104 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
6 | 5 | ffvelrni 6266 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
7 | 4, 6 | sseldi 3566 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
8 | 7 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈
ℝ*) |
9 | | xrltnle 9984 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘𝐴) ∈
ℝ*) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵)) |
10 | 3, 8, 9 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵)) |
11 | 1, 10 | mpbid 221 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ (vol‘𝐴) ≤ 𝐵) |
12 | | negeq 10152 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → -𝑚 = -𝑛) |
13 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
14 | 12, 13 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (-𝑚[,]𝑚) = (-𝑛[,]𝑛)) |
15 | 14 | ineq2d 3776 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-𝑛[,]𝑛))) |
16 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) |
17 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (-𝑛[,]𝑛) ∈ V |
18 | 17 | inex2 4728 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-𝑛[,]𝑛)) ∈ V |
19 | 15, 16, 18 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛))) |
20 | 19 | iuneq2i 4475 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛)) |
21 | | iunin2 4520 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛)) = (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
22 | 20, 21 | eqtri 2632 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
23 | | simpl1 1057 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol) |
24 | | nnre 10904 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
26 | 25 | renegcld 10336 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -𝑛 ∈ ℝ) |
27 | | iccmbl 23141 |
. . . . . . . . . . . . . 14
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol) |
28 | 26, 25, 27 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ∈ dom vol) |
29 | | inmbl 23117 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
30 | 23, 28, 29 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
31 | 15 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑛 ∈ ℕ ↦ (𝐴 ∩ (-𝑛[,]𝑛))) |
32 | 30, 31 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol) |
33 | | ffn 5958 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ) |
35 | | fniunfv 6409 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) |
37 | | mblss 23106 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ⊆ ℝ) |
39 | 38 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
40 | | recn 9905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
41 | 40 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
42 | | arch 11166 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘𝑥)
∈ ℝ → ∃𝑛 ∈ ℕ (abs‘𝑥) < 𝑛) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
(abs‘𝑥) < 𝑛) |
44 | | ltle 10005 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝑥)
∈ ℝ ∧ 𝑛
∈ ℝ) → ((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛)) |
45 | 41, 24, 44 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛)) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛)) |
47 | 46 | 3expib 1260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
49 | | absle 13903 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) →
((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
50 | 24, 49 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
51 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℝ) |
52 | 51 | renegcld 10336 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → -𝑛 ∈
ℝ) |
53 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
54 | 52, 51, 53 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
55 | 48, 50, 54 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) ≤ 𝑛 → 𝑥 ∈ (-𝑛[,]𝑛))) |
56 | 45, 55 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) < 𝑛 → 𝑥 ∈ (-𝑛[,]𝑛))) |
57 | 56 | reximdva 3000 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(∃𝑛 ∈ ℕ
(abs‘𝑥) < 𝑛 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))) |
58 | 43, 57 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
𝑥 ∈ (-𝑛[,]𝑛)) |
59 | 39, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥 ∈ 𝐴) → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)) |
60 | 59 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥 ∈ 𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))) |
61 | | eliun 4460 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)) |
62 | 60, 61 | syl6ibr 241 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛))) |
63 | 62 | ssrdv 3574 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ⊆ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
64 | | df-ss 3554 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ∪ 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴) |
65 | 63, 64 | sylib 207 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴) |
66 | 22, 36, 65 | 3eqtr3a 2668 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = 𝐴) |
67 | 66 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = (vol‘𝐴)) |
68 | | peano2re 10088 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) |
69 | 25, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
70 | 69 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ∈ ℝ) |
71 | 25 | lep1d 10834 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
72 | 25, 69 | lenegd 10485 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 ≤ (𝑛 + 1) ↔ -(𝑛 + 1) ≤ -𝑛)) |
73 | 71, 72 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ≤ -𝑛) |
74 | | iccss 12112 |
. . . . . . . . . . . 12
⊢
(((-(𝑛 + 1) ∈
ℝ ∧ (𝑛 + 1)
∈ ℝ) ∧ (-(𝑛
+ 1) ≤ -𝑛 ∧ 𝑛 ≤ (𝑛 + 1))) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1))) |
75 | 70, 69, 73, 71, 74 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1))) |
76 | | sslin 3801 |
. . . . . . . . . . 11
⊢ ((-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1)) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
78 | 19 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛))) |
79 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
80 | 79 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
81 | | negeq 10152 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → -𝑚 = -(𝑛 + 1)) |
82 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → 𝑚 = (𝑛 + 1)) |
83 | 81, 82 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (-𝑚[,]𝑚) = (-(𝑛 + 1)[,](𝑛 + 1))) |
84 | 83 | ineq2d 3776 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
85 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (-(𝑛 + 1)[,](𝑛 + 1)) ∈ V |
86 | 85 | inex2 4728 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))) ∈ V |
87 | 84, 16, 86 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
88 | 80, 87 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
89 | 77, 78, 88 | 3sstr4d 3611 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) |
90 | 89 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) |
91 | | volsup 23131 |
. . . . . . . 8
⊢ (((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
((𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
92 | 32, 90, 91 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
93 | 67, 92 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
94 | 93 | breq1d 4593 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵)) |
95 | | imassrn 5396 |
. . . . . . 7
⊢ (vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆ ran vol |
96 | | frn 5966 |
. . . . . . . . 9
⊢ (vol:dom
vol⟶(0[,]+∞) → ran vol ⊆
(0[,]+∞)) |
97 | 5, 96 | ax-mp 5 |
. . . . . . . 8
⊢ ran vol
⊆ (0[,]+∞) |
98 | 97, 4 | sstri 3577 |
. . . . . . 7
⊢ ran vol
⊆ ℝ* |
99 | 95, 98 | sstri 3577 |
. . . . . 6
⊢ (vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆
ℝ* |
100 | | supxrleub 12028 |
. . . . . 6
⊢ (((vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵)) |
101 | 99, 3, 100 | sylancr 694 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (sup((vol “ ran
(𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵)) |
102 | | ffn 5958 |
. . . . . . . 8
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
103 | 5, 102 | ax-mp 5 |
. . . . . . 7
⊢ vol Fn
dom vol |
104 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol) |
105 | 32, 104 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol) |
106 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑛 = (vol‘𝑧) → (𝑛 ≤ 𝐵 ↔ (vol‘𝑧) ≤ 𝐵)) |
107 | 106 | ralima 6402 |
. . . . . . 7
⊢ ((vol Fn
dom vol ∧ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚))) ⊆ dom vol) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵)) |
108 | 103, 105,
107 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵)) |
109 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → (vol‘𝑧) = (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛))) |
110 | 109 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → ((vol‘𝑧) ≤ 𝐵 ↔ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
111 | 110 | ralrn 6270 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
112 | 34, 111 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
113 | 19 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(vol‘((𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))‘𝑛)) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
114 | 113 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((vol‘((𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
115 | 114 | ralbiia 2962 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (vol‘((𝑚
∈ ℕ ↦ (𝐴
∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
116 | 112, 115 | syl6bb 275 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
117 | 108, 116 | bitrd 267 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
118 | 94, 101, 117 | 3bitrd 293 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
119 | 11, 118 | mtbid 313 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ ∀𝑛 ∈ ℕ
(vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
120 | | rexnal 2978 |
. . 3
⊢
(∃𝑛 ∈
ℕ ¬ (vol‘(𝐴
∩ (-𝑛[,]𝑛))) ≤ 𝐵 ↔ ¬ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
121 | 119, 120 | sylibr 223 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ ¬
(vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
122 | 3 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) |
123 | 5 | ffvelrni 6266 |
. . . . . 6
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞)) |
124 | 4, 123 | sseldi 3566 |
. . . . 5
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
125 | 30, 124 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
126 | | xrltnle 9984 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘(𝐴 ∩
(-𝑛[,]𝑛))) ∈ ℝ*) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
127 | 122, 125,
126 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
128 | 127 | rexbidva 3031 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
129 | 121, 128 | mpbird 246 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |