MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  volsup2 Structured version   Visualization version   GIF version

Theorem volsup2 23367
Description: The volume of 𝐴 is the supremum of the sequence vol*‘(𝐴 ∩ (-𝑛[,]𝑛)) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014.)
Assertion
Ref Expression
volsup2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛

Proof of Theorem volsup2
Dummy variables 𝑚 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 1062 . . . . 5 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴))
2 rexr 10082 . . . . . . 7 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
323ad2ant2 1082 . . . . . 6 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ*)
4 iccssxr 12253 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
5 volf 23291 . . . . . . . . 9 vol:dom vol⟶(0[,]+∞)
65ffvelrni 6356 . . . . . . . 8 (𝐴 ∈ dom vol → (vol‘𝐴) ∈ (0[,]+∞))
74, 6sseldi 3599 . . . . . . 7 (𝐴 ∈ dom vol → (vol‘𝐴) ∈ ℝ*)
873ad2ant1 1081 . . . . . 6 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈ ℝ*)
9 xrltnle 10102 . . . . . 6 ((𝐵 ∈ ℝ* ∧ (vol‘𝐴) ∈ ℝ*) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵))
103, 8, 9syl2anc 693 . . . . 5 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐵 < (vol‘𝐴) ↔ ¬ (vol‘𝐴) ≤ 𝐵))
111, 10mpbid 222 . . . 4 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ (vol‘𝐴) ≤ 𝐵)
12 negeq 10270 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → -𝑚 = -𝑛)
13 id 22 . . . . . . . . . . . . . 14 (𝑚 = 𝑛𝑚 = 𝑛)
1412, 13oveq12d 6665 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (-𝑚[,]𝑚) = (-𝑛[,]𝑛))
1514ineq2d 3812 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-𝑛[,]𝑛)))
16 eqid 2621 . . . . . . . . . . . 12 (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))
17 ovex 6675 . . . . . . . . . . . . 13 (-𝑛[,]𝑛) ∈ V
1817inex2 4798 . . . . . . . . . . . 12 (𝐴 ∩ (-𝑛[,]𝑛)) ∈ V
1915, 16, 18fvmpt 6280 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛)))
2019iuneq2i 4537 . . . . . . . . . 10 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛))
21 iunin2 4582 . . . . . . . . . 10 𝑛 ∈ ℕ (𝐴 ∩ (-𝑛[,]𝑛)) = (𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛))
2220, 21eqtri 2643 . . . . . . . . 9 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛))
23 simpl1 1063 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol)
24 nnre 11024 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
2524adantl 482 . . . . . . . . . . . . . . 15 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
2625renegcld 10454 . . . . . . . . . . . . . 14 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -𝑛 ∈ ℝ)
27 iccmbl 23328 . . . . . . . . . . . . . 14 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
2826, 25, 27syl2anc 693 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ∈ dom vol)
29 inmbl 23304 . . . . . . . . . . . . 13 ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol)
3023, 28, 29syl2anc 693 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol)
3115cbvmptv 4748 . . . . . . . . . . . 12 (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = (𝑛 ∈ ℕ ↦ (𝐴 ∩ (-𝑛[,]𝑛)))
3230, 31fmptd 6383 . . . . . . . . . . 11 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol)
33 ffn 6043 . . . . . . . . . . 11 ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ)
3432, 33syl 17 . . . . . . . . . 10 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ)
35 fniunfv 6502 . . . . . . . . . 10 ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))
3634, 35syl 17 . . . . . . . . 9 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))
37 mblss 23293 . . . . . . . . . . . . . . . 16 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
38373ad2ant1 1081 . . . . . . . . . . . . . . 15 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ⊆ ℝ)
3938sselda 3601 . . . . . . . . . . . . . 14 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥𝐴) → 𝑥 ∈ ℝ)
40 recn 10023 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4140abscld 14169 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
42 arch 11286 . . . . . . . . . . . . . . . 16 ((abs‘𝑥) ∈ ℝ → ∃𝑛 ∈ ℕ (abs‘𝑥) < 𝑛)
4341, 42syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ (abs‘𝑥) < 𝑛)
44 ltle 10123 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛))
4541, 24, 44syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((abs‘𝑥) < 𝑛 → (abs‘𝑥) ≤ 𝑛))
46 id 22 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛) → (𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛))
47463expib 1267 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ((-𝑛𝑥𝑥𝑛) → (𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛)))
4847adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((-𝑛𝑥𝑥𝑛) → (𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛)))
49 absle 14049 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛𝑥𝑥𝑛)))
5024, 49sylan2 491 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((abs‘𝑥) ≤ 𝑛 ↔ (-𝑛𝑥𝑥𝑛)))
5124adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
5251renegcld 10454 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → -𝑛 ∈ ℝ)
53 elicc2 12235 . . . . . . . . . . . . . . . . . . 19 ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛)))
5452, 51, 53syl2anc 693 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ (-𝑛[,]𝑛) ↔ (𝑥 ∈ ℝ ∧ -𝑛𝑥𝑥𝑛)))
5548, 50, 543imtr4d 283 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((abs‘𝑥) ≤ 𝑛𝑥 ∈ (-𝑛[,]𝑛)))
5645, 55syld 47 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((abs‘𝑥) < 𝑛𝑥 ∈ (-𝑛[,]𝑛)))
5756reximdva 3016 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (∃𝑛 ∈ ℕ (abs‘𝑥) < 𝑛 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)))
5843, 57mpd 15 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))
5939, 58syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑥𝐴) → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))
6059ex 450 . . . . . . . . . . . 12 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥𝐴 → ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛)))
61 eliun 4522 . . . . . . . . . . . 12 (𝑥 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 ∈ (-𝑛[,]𝑛))
6260, 61syl6ibr 242 . . . . . . . . . . 11 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝑥𝐴𝑥 𝑛 ∈ ℕ (-𝑛[,]𝑛)))
6362ssrdv 3607 . . . . . . . . . 10 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → 𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛))
64 df-ss 3586 . . . . . . . . . 10 (𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛) ↔ (𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴)
6563, 64sylib 208 . . . . . . . . 9 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (𝐴 𝑛 ∈ ℕ (-𝑛[,]𝑛)) = 𝐴)
6622, 36, 653eqtr3a 2679 . . . . . . . 8 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) = 𝐴)
6766fveq2d 6193 . . . . . . 7 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = (vol‘𝐴))
68 peano2re 10206 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
6925, 68syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ)
7069renegcld 10454 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ∈ ℝ)
7125lep1d 10952 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1))
7225, 69lenegd 10603 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 ≤ (𝑛 + 1) ↔ -(𝑛 + 1) ≤ -𝑛))
7371, 72mpbid 222 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → -(𝑛 + 1) ≤ -𝑛)
74 iccss 12238 . . . . . . . . . . . 12 (((-(𝑛 + 1) ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ) ∧ (-(𝑛 + 1) ≤ -𝑛𝑛 ≤ (𝑛 + 1))) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1)))
7570, 69, 73, 71, 74syl22anc 1326 . . . . . . . . . . 11 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1)))
76 sslin 3837 . . . . . . . . . . 11 ((-𝑛[,]𝑛) ⊆ (-(𝑛 + 1)[,](𝑛 + 1)) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))))
7775, 76syl 17 . . . . . . . . . 10 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐴 ∩ (-𝑛[,]𝑛)) ⊆ (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))))
7819adantl 482 . . . . . . . . . 10 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) = (𝐴 ∩ (-𝑛[,]𝑛)))
79 peano2nn 11029 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
8079adantl 482 . . . . . . . . . . 11 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
81 negeq 10270 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → -𝑚 = -(𝑛 + 1))
82 id 22 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → 𝑚 = (𝑛 + 1))
8381, 82oveq12d 6665 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (-𝑚[,]𝑚) = (-(𝑛 + 1)[,](𝑛 + 1)))
8483ineq2d 3812 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝐴 ∩ (-𝑚[,]𝑚)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))))
85 ovex 6675 . . . . . . . . . . . . 13 (-(𝑛 + 1)[,](𝑛 + 1)) ∈ V
8685inex2 4798 . . . . . . . . . . . 12 (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))) ∈ V
8784, 16, 86fvmpt 6280 . . . . . . . . . . 11 ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))))
8880, 87syl 17 . . . . . . . . . 10 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)) = (𝐴 ∩ (-(𝑛 + 1)[,](𝑛 + 1))))
8977, 78, 883sstr4d 3646 . . . . . . . . 9 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)))
9089ralrimiva 2965 . . . . . . . 8 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1)))
91 volsup 23318 . . . . . . . 8 (((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ))
9232, 90, 91syl2anc 693 . . . . . . 7 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ))
9367, 92eqtr3d 2657 . . . . . 6 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) = sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ))
9493breq1d 4661 . . . . 5 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵))
95 imassrn 5475 . . . . . . 7 (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) ⊆ ran vol
96 frn 6051 . . . . . . . . 9 (vol:dom vol⟶(0[,]+∞) → ran vol ⊆ (0[,]+∞))
975, 96ax-mp 5 . . . . . . . 8 ran vol ⊆ (0[,]+∞)
9897, 4sstri 3610 . . . . . . 7 ran vol ⊆ ℝ*
9995, 98sstri 3610 . . . . . 6 (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) ⊆ ℝ*
100 supxrleub 12153 . . . . . 6 (((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))) ⊆ ℝ*𝐵 ∈ ℝ*) → (sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛𝐵))
10199, 3, 100sylancr 695 . . . . 5 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (sup((vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛𝐵))
102 ffn 6043 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
1035, 102ax-mp 5 . . . . . . 7 vol Fn dom vol
104 frn 6051 . . . . . . . 8 ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol)
10532, 104syl 17 . . . . . . 7 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol)
106 breq1 4654 . . . . . . . 8 (𝑛 = (vol‘𝑧) → (𝑛𝐵 ↔ (vol‘𝑧) ≤ 𝐵))
107106ralima 6495 . . . . . . 7 ((vol Fn dom vol ∧ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) ⊆ dom vol) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵))
108103, 105, 107sylancr 695 . . . . . 6 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛𝐵 ↔ ∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵))
109 fveq2 6189 . . . . . . . . . 10 (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → (vol‘𝑧) = (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)))
110109breq1d 4661 . . . . . . . . 9 (𝑧 = ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛) → ((vol‘𝑧) ≤ 𝐵 ↔ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵))
111110ralrn 6360 . . . . . . . 8 ((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))) Fn ℕ → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵))
11234, 111syl 17 . . . . . . 7 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵))
11319fveq2d 6193 . . . . . . . . 9 (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
114113breq1d 4661 . . . . . . . 8 (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
115114ralbiia 2978 . . . . . . 7 (∀𝑛 ∈ ℕ (vol‘((𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))‘𝑛)) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)
116112, 115syl6bb 276 . . . . . 6 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑧 ∈ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚)))(vol‘𝑧) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
117108, 116bitrd 268 . . . . 5 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∀𝑛 ∈ (vol “ ran (𝑚 ∈ ℕ ↦ (𝐴 ∩ (-𝑚[,]𝑚))))𝑛𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
11894, 101, 1173bitrd 294 . . . 4 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ((vol‘𝐴) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
11911, 118mtbid 314 . . 3 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ¬ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)
120 rexnal 2994 . . 3 (∃𝑛 ∈ ℕ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵 ↔ ¬ ∀𝑛 ∈ ℕ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)
121119, 120sylibr 224 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵)
1223adantr 481 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ*)
1235ffvelrni 6356 . . . . . 6 ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞))
1244, 123sseldi 3599 . . . . 5 ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ ℝ*)
12530, 124syl 17 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ ℝ*)
126 xrltnle 10102 . . . 4 ((𝐵 ∈ ℝ* ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ ℝ*) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
127122, 125, 126syl2anc 693 . . 3 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
128127rexbidva 3047 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → (∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ↔ ∃𝑛 ∈ ℕ ¬ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ≤ 𝐵))
129121, 128mpbird 247 1 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wral 2911  wrex 2912  cin 3571  wss 3572   cuni 4434   ciun 4518   class class class wbr 4651  cmpt 4727  dom cdm 5112  ran crn 5113  cima 5115   Fn wfn 5881  wf 5882  cfv 5886  (class class class)co 6647  supcsup 8343  cr 9932  0cc0 9933  1c1 9934   + caddc 9936  +∞cpnf 10068  *cxr 10070   < clt 10071  cle 10072  -cneg 10264  cn 11017  [,]cicc 12175  abscabs 13968  volcvol 23226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cc 9254  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-disj 4619  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-of 6894  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-inf 8346  df-oi 8412  df-card 8762  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-q 11786  df-rp 11830  df-xadd 11944  df-ioo 12176  df-ico 12178  df-icc 12179  df-fz 12324  df-fzo 12462  df-fl 12588  df-seq 12797  df-exp 12856  df-hash 13113  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-rlim 14214  df-sum 14411  df-xmet 19733  df-met 19734  df-ovol 23227  df-vol 23228
This theorem is referenced by:  volivth  23369
  Copyright terms: Public domain W3C validator