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

Theorem ovoliunlem3 24099
 Description: Lemma for ovoliun 24100. (Contributed by Mario Carneiro, 12-Jun-2014.)
Hypotheses
Ref Expression
ovoliun.t 𝑇 = seq1( + , 𝐺)
ovoliun.g 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
ovoliun.a ((𝜑𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)
ovoliun.v ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
ovoliun.r (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
ovoliun.b (𝜑𝐵 ∈ ℝ+)
Assertion
Ref Expression
ovoliunlem3 (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Distinct variable groups:   𝐵,𝑛   𝜑,𝑛   𝑛,𝐺   𝑇,𝑛
Allowed substitution hint:   𝐴(𝑛)

Proof of Theorem ovoliunlem3
Dummy variables 𝑓 𝑔 𝑗 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2977 . . . 4 𝑚𝐴
2 nfcsb1v 3907 . . . 4 𝑛𝑚 / 𝑛𝐴
3 csbeq1a 3897 . . . 4 (𝑛 = 𝑚𝐴 = 𝑚 / 𝑛𝐴)
41, 2, 3cbviun 4954 . . 3 𝑛 ∈ ℕ 𝐴 = 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴
54fveq2i 6668 . 2 (vol*‘ 𝑛 ∈ ℕ 𝐴) = (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴)
6 ovoliun.a . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)
7 ovoliun.v . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
8 ovoliun.b . . . . . . 7 (𝜑𝐵 ∈ ℝ+)
9 2nn 11704 . . . . . . . . 9 2 ∈ ℕ
10 nnnn0 11898 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
11 nnexpcl 13436 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
129, 10, 11sylancr 589 . . . . . . . 8 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
1312nnrpd 12423 . . . . . . 7 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
14 rpdivcl 12408 . . . . . . 7 ((𝐵 ∈ ℝ+ ∧ (2↑𝑛) ∈ ℝ+) → (𝐵 / (2↑𝑛)) ∈ ℝ+)
158, 13, 14syl2an 597 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ+)
16 eqid 2821 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − ) ∘ 𝑓))
1716ovolgelb 24075 . . . . . 6 ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ ∧ (𝐵 / (2↑𝑛)) ∈ ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))
186, 7, 15, 17syl3anc 1367 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))
1918ralrimiva 3182 . . . 4 (𝜑 → ∀𝑛 ∈ ℕ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))
20 ovex 7183 . . . . 5 (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∈ V
21 nnenom 13342 . . . . 5 ℕ ≈ ω
22 coeq2 5724 . . . . . . . . 9 (𝑓 = (𝑔𝑛) → ((,) ∘ 𝑓) = ((,) ∘ (𝑔𝑛)))
2322rneqd 5803 . . . . . . . 8 (𝑓 = (𝑔𝑛) → ran ((,) ∘ 𝑓) = ran ((,) ∘ (𝑔𝑛)))
2423unieqd 4842 . . . . . . 7 (𝑓 = (𝑔𝑛) → ran ((,) ∘ 𝑓) = ran ((,) ∘ (𝑔𝑛)))
2524sseq2d 3999 . . . . . 6 (𝑓 = (𝑔𝑛) → (𝐴 ran ((,) ∘ 𝑓) ↔ 𝐴 ran ((,) ∘ (𝑔𝑛))))
26 coeq2 5724 . . . . . . . . . 10 (𝑓 = (𝑔𝑛) → ((abs ∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ (𝑔𝑛)))
2726seqeq3d 13371 . . . . . . . . 9 (𝑓 = (𝑔𝑛) → seq1( + , ((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))))
2827rneqd 5803 . . . . . . . 8 (𝑓 = (𝑔𝑛) → ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) = ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))))
2928supeq1d 8904 . . . . . . 7 (𝑓 = (𝑔𝑛) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ))
3029breq1d 5069 . . . . . 6 (𝑓 = (𝑔𝑛) → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))
3125, 30anbi12d 632 . . . . 5 (𝑓 = (𝑔𝑛) → ((𝐴 ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))))
3220, 21, 31axcc4 9855 . . . 4 (∀𝑛 ∈ ℕ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))))
3319, 32syl 17 . . 3 (𝜑 → ∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))))
34 xpnnen 15558 . . . . . . 7 (ℕ × ℕ) ≈ ℕ
3534ensymi 8553 . . . . . 6 ℕ ≈ (ℕ × ℕ)
36 bren 8512 . . . . . 6 (ℕ ≈ (ℕ × ℕ) ↔ ∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ))
3735, 36mpbi 232 . . . . 5 𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ)
38 ovoliun.t . . . . . . . 8 𝑇 = seq1( + , 𝐺)
39 ovoliun.g . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
40 nfcv 2977 . . . . . . . . . 10 𝑚(vol*‘𝐴)
41 nfcv 2977 . . . . . . . . . . 11 𝑛vol*
4241, 2nffv 6675 . . . . . . . . . 10 𝑛(vol*‘𝑚 / 𝑛𝐴)
433fveq2d 6669 . . . . . . . . . 10 (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘𝑚 / 𝑛𝐴))
4440, 42, 43cbvmpt 5160 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) = (𝑚 ∈ ℕ ↦ (vol*‘𝑚 / 𝑛𝐴))
4539, 44eqtri 2844 . . . . . . . 8 𝐺 = (𝑚 ∈ ℕ ↦ (vol*‘𝑚 / 𝑛𝐴))
466ralrimiva 3182 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ)
47 nfv 1911 . . . . . . . . . . . 12 𝑚 𝐴 ⊆ ℝ
48 nfcv 2977 . . . . . . . . . . . . 13 𝑛
492, 48nfss 3960 . . . . . . . . . . . 12 𝑛𝑚 / 𝑛𝐴 ⊆ ℝ
503sseq1d 3998 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ 𝑚 / 𝑛𝐴 ⊆ ℝ))
5147, 49, 50cbvralw 3442 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑚 ∈ ℕ 𝑚 / 𝑛𝐴 ⊆ ℝ)
5246, 51sylib 220 . . . . . . . . . 10 (𝜑 → ∀𝑚 ∈ ℕ 𝑚 / 𝑛𝐴 ⊆ ℝ)
5352r19.21bi 3208 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → 𝑚 / 𝑛𝐴 ⊆ ℝ)
5453ad4ant14 750 . . . . . . . 8 ((((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → 𝑚 / 𝑛𝐴 ⊆ ℝ)
557ralrimiva 3182 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ)
5640nfel1 2994 . . . . . . . . . . . 12 𝑚(vol*‘𝐴) ∈ ℝ
5742nfel1 2994 . . . . . . . . . . . 12 𝑛(vol*‘𝑚 / 𝑛𝐴) ∈ ℝ
5843eleq1d 2897 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ))
5956, 57, 58cbvralw 3442 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ ↔ ∀𝑚 ∈ ℕ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
6055, 59sylib 220 . . . . . . . . . 10 (𝜑 → ∀𝑚 ∈ ℕ (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
6160r19.21bi 3208 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
6261ad4ant14 750 . . . . . . . 8 ((((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → (vol*‘𝑚 / 𝑛𝐴) ∈ ℝ)
63 ovoliun.r . . . . . . . . 9 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
6463ad2antrr 724 . . . . . . . 8 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
658ad2antrr 724 . . . . . . . 8 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝐵 ∈ ℝ+)
66 eqid 2821 . . . . . . . 8 seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))) = seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚)))
67 eqid 2821 . . . . . . . 8 seq1( + , ((abs ∘ − ) ∘ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗𝑘)))‘(2nd ‘(𝑗𝑘)))))) = seq1( + , ((abs ∘ − ) ∘ (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗𝑘)))‘(2nd ‘(𝑗𝑘))))))
68 eqid 2821 . . . . . . . 8 (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗𝑘)))‘(2nd ‘(𝑗𝑘)))) = (𝑘 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑗𝑘)))‘(2nd ‘(𝑗𝑘))))
69 simplr 767 . . . . . . . 8 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑗:ℕ–1-1-onto→(ℕ × ℕ))
70 simprl 769 . . . . . . . 8 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → 𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
71 simprr 771 . . . . . . . . . . 11 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))
72 nfv 1911 . . . . . . . . . . . 12 𝑚(𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
73 nfcv 2977 . . . . . . . . . . . . . 14 𝑛 ran ((,) ∘ (𝑔𝑚))
742, 73nfss 3960 . . . . . . . . . . . . 13 𝑛𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚))
75 nfcv 2977 . . . . . . . . . . . . . 14 𝑛sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < )
76 nfcv 2977 . . . . . . . . . . . . . 14 𝑛
77 nfcv 2977 . . . . . . . . . . . . . . 15 𝑛 +
78 nfcv 2977 . . . . . . . . . . . . . . 15 𝑛(𝐵 / (2↑𝑚))
7942, 77, 78nfov 7180 . . . . . . . . . . . . . 14 𝑛((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))
8075, 76, 79nfbr 5106 . . . . . . . . . . . . 13 𝑛sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))
8174, 80nfan 1896 . . . . . . . . . . . 12 𝑛(𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚))))
82 fveq2 6665 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (𝑔𝑛) = (𝑔𝑚))
8382coeq2d 5728 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((,) ∘ (𝑔𝑛)) = ((,) ∘ (𝑔𝑚)))
8483rneqd 5803 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ran ((,) ∘ (𝑔𝑛)) = ran ((,) ∘ (𝑔𝑚)))
8584unieqd 4842 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 ran ((,) ∘ (𝑔𝑛)) = ran ((,) ∘ (𝑔𝑚)))
863, 85sseq12d 4000 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (𝐴 ran ((,) ∘ (𝑔𝑛)) ↔ 𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚))))
8782coeq2d 5728 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((abs ∘ − ) ∘ (𝑔𝑛)) = ((abs ∘ − ) ∘ (𝑔𝑚)))
8887seqeq3d 13371 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))) = seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))))
8988rneqd 5803 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))) = ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))))
9089supeq1d 8904 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) = sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ))
91 oveq2 7158 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
9291oveq2d 7166 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐵 / (2↑𝑛)) = (𝐵 / (2↑𝑚)))
9343, 92oveq12d 7168 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚))))
9490, 93breq12d 5072 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ↔ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))))
9586, 94anbi12d 632 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ (𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚))))))
9672, 81, 95cbvralw 3442 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ↔ ∀𝑚 ∈ ℕ (𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))))
9771, 96sylib 220 . . . . . . . . . 10 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → ∀𝑚 ∈ ℕ (𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))))
9897r19.21bi 3208 . . . . . . . . 9 ((((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → (𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚)))))
9998simpld 497 . . . . . . . 8 ((((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → 𝑚 / 𝑛𝐴 ran ((,) ∘ (𝑔𝑚)))
10098simprd 498 . . . . . . . 8 ((((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) ∧ 𝑚 ∈ ℕ) → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑚))), ℝ*, < ) ≤ ((vol*‘𝑚 / 𝑛𝐴) + (𝐵 / (2↑𝑚))))
10138, 45, 54, 62, 64, 65, 66, 67, 68, 69, 70, 99, 100ovoliunlem2 24098 . . . . . . 7 (((𝜑𝑗:ℕ–1-1-onto→(ℕ × ℕ)) ∧ (𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))))) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
102101exp31 422 . . . . . 6 (𝜑 → (𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))))
103102exlimdv 1930 . . . . 5 (𝜑 → (∃𝑗 𝑗:ℕ–1-1-onto→(ℕ × ℕ) → ((𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))))
10437, 103mpi 20 . . . 4 (𝜑 → ((𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))
105104exlimdv 1930 . . 3 (𝜑 → (∃𝑔(𝑔:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ ∀𝑛 ∈ ℕ (𝐴 ran ((,) ∘ (𝑔𝑛)) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑔𝑛))), ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)))
10633, 105mpd 15 . 2 (𝜑 → (vol*‘ 𝑚 ∈ ℕ 𝑚 / 𝑛𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
1075, 106eqbrtrid 5094 1 (𝜑 → (vol*‘ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139  ⦋csb 3883   ∩ cin 3935   ⊆ wss 3936  ∪ cuni 4832  ∪ ciun 4912   class class class wbr 5059   ↦ cmpt 5139   × cxp 5548  ran crn 5551   ∘ ccom 5554  ⟶wf 6346  –1-1-onto→wf1o 6349  ‘cfv 6350  (class class class)co 7150  1st c1st 7681  2nd c2nd 7682   ↑m cmap 8400   ≈ cen 8500  supcsup 8898  ℝcr 10530  1c1 10532   + caddc 10534  ℝ*cxr 10668   < clt 10669   ≤ cle 10670   − cmin 10864   / cdiv 11291  ℕcn 11632  2c2 11686  ℕ0cn0 11891  ℝ+crp 12383  (,)cioo 12732  seqcseq 13363  ↑cexp 13423  abscabs 14587  vol*covol 24057 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-inf2 9098  ax-cc 9851  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-map 8402  df-pm 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12384  df-ioo 12736  df-ico 12738  df-fz 12887  df-fzo 13028  df-fl 13156  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-rlim 14840  df-sum 15037  df-ovol 24059 This theorem is referenced by:  ovoliun  24100
 Copyright terms: Public domain W3C validator