| Step | Hyp | Ref
| Expression |
| 1 | | simp3 1139 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴)) |
| 2 | | rexr 11307 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
| 3 | 2 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈
ℝ*) |
| 4 | | iccssxr 13470 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
| 5 | | volf 25564 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
| 6 | 5 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
| 7 | 4, 6 | sselid 3981 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
| 8 | 7 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈
ℝ*) |
| 9 | | xrltnle 11328 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘𝐴) ∈
ℝ*) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵)) |
| 10 | 3, 8, 9 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵)) |
| 11 | 1, 10 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ (vol‘𝐴) ≤ 𝐵) |
| 12 | | negeq 11500 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → -𝑚 = -𝑛) |
| 13 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
| 14 | 12, 13 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (-𝑚[,]𝑚) = (-𝑛[,]𝑛)) |
| 15 | 14 | ineq2d 4220 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-𝑛[,]𝑛))) |
| 16 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) |
| 17 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (-𝑛[,]𝑛) ∈ V |
| 18 | 17 | inex2 5318 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-𝑛[,]𝑛)) ∈ V |
| 19 | 15, 16, 18 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛))) |
| 20 | 19 | iuneq2i 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛)) |
| 21 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛)) = (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
| 22 | 20, 21 | eqtri 2765 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
| 23 | | simpl1 1192 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol) |
| 24 | | nnre 12273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
| 26 | 25 | renegcld 11690 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -𝑛 ∈ ℝ) |
| 27 | | iccmbl 25601 |
. . . . . . . . . . . . . 14
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol) |
| 28 | 26, 25, 27 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ∈ dom vol) |
| 29 | | inmbl 25577 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
| 30 | 23, 28, 29 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
| 31 | 15 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑛 ∈ ℕ ↦ (𝐴 ∩ (-𝑛[,]𝑛))) |
| 32 | 30, 31 | fmptd 7134 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol) |
| 33 | 32 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ) |
| 34 | | fniunfv 7267 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) |
| 36 | | mblss 25566 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ⊆ ℝ) |
| 38 | 37 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
| 39 | | recn 11245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 40 | 39 | abscld 15475 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
| 41 | | arch 12523 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘𝑥)
∈ ℝ → ∃𝑛 ∈ ℕ (abs‘𝑥) < 𝑛) |
| 42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
(abs‘𝑥) < 𝑛) |
| 43 | | ltle 11349 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝑥)
∈ ℝ ∧ 𝑛
∈ ℝ) → ((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛)) |
| 44 | 40, 24, 43 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛)) |
| 45 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛)) |
| 46 | 45 | 3expib 1123 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛) → (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 48 | | absle 15354 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) →
((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 49 | 24, 48 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 50 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℝ) |
| 51 | 50 | renegcld 11690 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → -𝑛 ∈
ℝ) |
| 52 | | elicc2 13452 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 53 | 51, 50, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛))) |
| 54 | 47, 49, 53 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) ≤ 𝑛 → 𝑥 ∈ (-𝑛[,]𝑛))) |
| 55 | 44, 54 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) →
((abs‘𝑥) < 𝑛 → 𝑥 ∈ (-𝑛[,]𝑛))) |
| 56 | 55 | reximdva 3168 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(∃𝑛 ∈ ℕ
(abs‘𝑥) < 𝑛 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))) |
| 57 | 42, 56 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
𝑥 ∈ (-𝑛[,]𝑛)) |
| 58 | 38, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥 ∈ 𝐴) → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)) |
| 59 | 58 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥 ∈ 𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))) |
| 60 | | eliun 4995 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)) |
| 61 | 59, 60 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛))) |
| 62 | 61 | ssrdv 3989 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ⊆ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) |
| 63 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ∪ 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴) |
| 64 | 62, 63 | sylib 218 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐴 ∩ ∪
𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴) |
| 65 | 22, 35, 64 | 3eqtr3a 2801 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = 𝐴) |
| 66 | 65 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = (vol‘𝐴)) |
| 67 | | peano2re 11434 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) |
| 68 | 25, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
| 69 | 68 | renegcld 11690 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ∈ ℝ) |
| 70 | 25 | lep1d 12199 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
| 71 | 25, 68 | lenegd 11842 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 ≤ (𝑛 + 1) ↔ -(𝑛 + 1) ≤ -𝑛)) |
| 72 | 70, 71 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ≤ -𝑛) |
| 73 | | iccss 13455 |
. . . . . . . . . . . 12
⊢
(((-(𝑛 + 1) ∈
ℝ ∧ (𝑛 + 1)
∈ ℝ) ∧ (-(𝑛
+ 1) ≤ -𝑛 ∧ 𝑛 ≤ (𝑛 + 1))) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1))) |
| 74 | 69, 68, 72, 70, 73 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1))) |
| 75 | | sslin 4243 |
. . . . . . . . . . 11
⊢ ((-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1)) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
| 77 | 19 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛))) |
| 78 | | peano2nn 12278 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
| 80 | | negeq 11500 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → -𝑚 = -(𝑛 + 1)) |
| 81 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → 𝑚 = (𝑛 + 1)) |
| 82 | 80, 81 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (-𝑚[,]𝑚) = (-(𝑛 + 1)[,](𝑛 + 1))) |
| 83 | 82 | ineq2d 4220 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
| 84 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (-(𝑛 + 1)[,](𝑛 + 1)) ∈ V |
| 85 | 84 | inex2 5318 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))) ∈ V |
| 86 | 83, 16, 85 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
| 87 | 79, 86 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1)))) |
| 88 | 76, 77, 87 | 3sstr4d 4039 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) |
| 89 | 88 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) |
| 90 | | volsup 25591 |
. . . . . . . 8
⊢ (((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
((𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
| 91 | 32, 89, 90 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
| 92 | 66, 91 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, <
)) |
| 93 | 92 | breq1d 5153 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵)) |
| 94 | | imassrn 6089 |
. . . . . . 7
⊢ (vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆ ran vol |
| 95 | | frn 6743 |
. . . . . . . . 9
⊢ (vol:dom
vol⟶(0[,]+∞) → ran vol ⊆
(0[,]+∞)) |
| 96 | 5, 95 | ax-mp 5 |
. . . . . . . 8
⊢ ran vol
⊆ (0[,]+∞) |
| 97 | 96, 4 | sstri 3993 |
. . . . . . 7
⊢ ran vol
⊆ ℝ* |
| 98 | 94, 97 | sstri 3993 |
. . . . . 6
⊢ (vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆
ℝ* |
| 99 | | supxrleub 13368 |
. . . . . 6
⊢ (((vol
“ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))) ⊆ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵)) |
| 100 | 98, 3, 99 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (sup((vol “ ran
(𝑚 ∈ ℕ ↦
(𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵)) |
| 101 | | ffn 6736 |
. . . . . . . 8
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
| 102 | 5, 101 | ax-mp 5 |
. . . . . . 7
⊢ vol Fn
dom vol |
| 103 | 32 | frnd 6744 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol) |
| 104 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑛 = (vol‘𝑧) → (𝑛 ≤ 𝐵 ↔ (vol‘𝑧) ≤ 𝐵)) |
| 105 | 104 | ralima 7257 |
. . . . . . 7
⊢ ((vol Fn
dom vol ∧ ran (𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚))) ⊆ dom vol) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵)) |
| 106 | 102, 103,
105 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵)) |
| 107 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → (vol‘𝑧) = (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛))) |
| 108 | 107 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → ((vol‘𝑧) ≤ 𝐵 ↔ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
| 109 | 108 | ralrn 7108 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
| 110 | 33, 109 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵)) |
| 111 | 19 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(vol‘((𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))‘𝑛)) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
| 112 | 111 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((vol‘((𝑚 ∈
ℕ ↦ (𝐴 ∩
(-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 113 | 112 | ralbiia 3091 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (vol‘((𝑚
∈ ℕ ↦ (𝐴
∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
| 114 | 110, 113 | bitrdi 287 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 115 | 106, 114 | bitrd 279 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 116 | 93, 100, 115 | 3bitrd 305 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 117 | 11, 116 | mtbid 324 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ ∀𝑛 ∈ ℕ
(vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
| 118 | | rexnal 3100 |
. . 3
⊢
(∃𝑛 ∈
ℕ ¬ (vol‘(𝐴
∩ (-𝑛[,]𝑛))) ≤ 𝐵 ↔ ¬ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
| 119 | 117, 118 | sylibr 234 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ ¬
(vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵) |
| 120 | 3 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) |
| 121 | 5 | ffvelcdmi 7103 |
. . . . . 6
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞)) |
| 122 | 4, 121 | sselid 3981 |
. . . . 5
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
| 123 | 30, 122 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
| 124 | | xrltnle 11328 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘(𝐴 ∩
(-𝑛[,]𝑛))) ∈ ℝ*) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 125 | 120, 123,
124 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 126 | 125 | rexbidva 3177 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)) |
| 127 | 119, 126 | mpbird 257 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |