Metamath Proof Explorer

Theorem ovoliunlem3

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t ⊢T=seq1+G
ovoliun.g ⊢G=n∈ℕ⟼vol*⁡A
ovoliun.a ⊢φ∧n∈ℕ→A⊆ℝ
ovoliun.v ⊢φ∧n∈ℕ→vol*⁡A∈ℝ
ovoliun.r ⊢φ→supran⁡Tℝ*<∈ℝ
ovoliun.b ⊢φ→B∈ℝ+
Assertion ovoliunlem3 ⊢φ→vol*⁡⋃n∈ℕA≤supran⁡Tℝ*<+B

Proof

Step Hyp Ref Expression
1 ovoliun.t ⊢T=seq1+G
2 ovoliun.g ⊢G=n∈ℕ⟼vol*⁡A
3 ovoliun.a ⊢φ∧n∈ℕ→A⊆ℝ
4 ovoliun.v ⊢φ∧n∈ℕ→vol*⁡A∈ℝ
5 ovoliun.r ⊢φ→supran⁡Tℝ*<∈ℝ
6 ovoliun.b ⊢φ→B∈ℝ+
7 nfcv ⊢Ⅎ_mA
8 nfcsb1v ⊢Ⅎ_n⦋m/n⦌A
9 csbeq1a ⊢n=m→A=⦋m/n⦌A
10 7 8 9 cbviun ⊢⋃n∈ℕA=⋃m∈ℕ⦋m/n⦌A
11 10 fveq2i ⊢vol*⁡⋃n∈ℕA=vol*⁡⋃m∈ℕ⦋m/n⦌A
12 2nn ⊢2∈ℕ
13 nnnn0 ⊢n∈ℕ→n∈ℕ0
14 nnexpcl ⊢2∈ℕ∧n∈ℕ0→2n∈ℕ
15 12 13 14 sylancr ⊢n∈ℕ→2n∈ℕ
16 15 nnrpd ⊢n∈ℕ→2n∈ℝ+
17 rpdivcl ⊢B∈ℝ+∧2n∈ℝ+→B2n∈ℝ+
18 6 16 17 syl2an ⊢φ∧n∈ℕ→B2n∈ℝ+
19 eqid ⊢seq1+abs∘−∘f=seq1+abs∘−∘f
20 19 ovolgelb ⊢A⊆ℝ∧vol*⁡A∈ℝ∧B2n∈ℝ+→∃f∈≤∩ℝ2ℕA⊆⋃ran⁡.∘f∧supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n
21 3 4 18 20 syl3anc ⊢φ∧n∈ℕ→∃f∈≤∩ℝ2ℕA⊆⋃ran⁡.∘f∧supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n
22 21 ralrimiva ⊢φ→∀n∈ℕ∃f∈≤∩ℝ2ℕA⊆⋃ran⁡.∘f∧supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n
23 ovex ⊢≤∩ℝ2ℕ∈V
24 nnenom ⊢ℕ≈ω
25 coeq2 ⊢f=g⁡n→.∘f=.∘g⁡n
26 25 rneqd ⊢f=g⁡n→ran⁡.∘f=ran⁡.∘g⁡n
27 26 unieqd ⊢f=g⁡n→⋃ran⁡.∘f=⋃ran⁡.∘g⁡n
28 27 sseq2d ⊢f=g⁡n→A⊆⋃ran⁡.∘f↔A⊆⋃ran⁡.∘g⁡n
29 coeq2 ⊢f=g⁡n→abs∘−∘f=abs∘−∘g⁡n
30 29 seqeq3d ⊢f=g⁡n→seq1+abs∘−∘f=seq1+abs∘−∘g⁡n
31 30 rneqd ⊢f=g⁡n→ran⁡seq1+abs∘−∘f=ran⁡seq1+abs∘−∘g⁡n
32 31 supeq1d ⊢f=g⁡n→supran⁡seq1+abs∘−∘fℝ*<=supran⁡seq1+abs∘−∘g⁡nℝ*<
33 32 breq1d ⊢f=g⁡n→supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n↔supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
34 28 33 anbi12d ⊢f=g⁡n→A⊆⋃ran⁡.∘f∧supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n↔A⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
35 23 24 34 axcc4 ⊢∀n∈ℕ∃f∈≤∩ℝ2ℕA⊆⋃ran⁡.∘f∧supran⁡seq1+abs∘−∘fℝ*<≤vol*⁡A+B2n→∃gg:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
36 22 35 syl ⊢φ→∃gg:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
37 xpnnen ⊢ℕ×ℕ≈ℕ
38 37 ensymi ⊢ℕ≈ℕ×ℕ
39 bren ⊢ℕ≈ℕ×ℕ↔∃jj:ℕ⟶1-1 ontoℕ×ℕ
40 38 39 mpbi ⊢∃jj:ℕ⟶1-1 ontoℕ×ℕ
41 nfcv ⊢Ⅎ_mvol*⁡A
42 nfcv ⊢Ⅎ_nvol*
43 42 8 nffv ⊢Ⅎ_nvol*⁡⦋m/n⦌A
44 9 fveq2d ⊢n=m→vol*⁡A=vol*⁡⦋m/n⦌A
45 41 43 44 cbvmpt ⊢n∈ℕ⟼vol*⁡A=m∈ℕ⟼vol*⁡⦋m/n⦌A
46 2 45 eqtri ⊢G=m∈ℕ⟼vol*⁡⦋m/n⦌A
47 3 ralrimiva ⊢φ→∀n∈ℕA⊆ℝ
48 nfv ⊢ℲmA⊆ℝ
49 nfcv ⊢Ⅎ_nℝ
50 8 49 nfss ⊢Ⅎn⦋m/n⦌A⊆ℝ
51 9 sseq1d ⊢n=m→A⊆ℝ↔⦋m/n⦌A⊆ℝ
52 48 50 51 cbvralw ⊢∀n∈ℕA⊆ℝ↔∀m∈ℕ⦋m/n⦌A⊆ℝ
53 47 52 sylib ⊢φ→∀m∈ℕ⦋m/n⦌A⊆ℝ
54 53 r19.21bi ⊢φ∧m∈ℕ→⦋m/n⦌A⊆ℝ
55 54 ad4ant14 ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n∧m∈ℕ→⦋m/n⦌A⊆ℝ
56 4 ralrimiva ⊢φ→∀n∈ℕvol*⁡A∈ℝ
57 41 nfel1 ⊢Ⅎmvol*⁡A∈ℝ
58 43 nfel1 ⊢Ⅎnvol*⁡⦋m/n⦌A∈ℝ
59 44 eleq1d ⊢n=m→vol*⁡A∈ℝ↔vol*⁡⦋m/n⦌A∈ℝ
60 57 58 59 cbvralw ⊢∀n∈ℕvol*⁡A∈ℝ↔∀m∈ℕvol*⁡⦋m/n⦌A∈ℝ
61 56 60 sylib ⊢φ→∀m∈ℕvol*⁡⦋m/n⦌A∈ℝ
62 61 r19.21bi ⊢φ∧m∈ℕ→vol*⁡⦋m/n⦌A∈ℝ
63 62 ad4ant14 ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n∧m∈ℕ→vol*⁡⦋m/n⦌A∈ℝ
64 5 ad2antrr ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→supran⁡Tℝ*<∈ℝ
65 6 ad2antrr ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→B∈ℝ+
66 eqid ⊢seq1+abs∘−∘g⁡m=seq1+abs∘−∘g⁡m
67 eqid ⊢seq1+abs∘−∘k∈ℕ⟼g⁡1st⁡j⁡k⁡2nd⁡j⁡k=seq1+abs∘−∘k∈ℕ⟼g⁡1st⁡j⁡k⁡2nd⁡j⁡k
68 eqid ⊢k∈ℕ⟼g⁡1st⁡j⁡k⁡2nd⁡j⁡k=k∈ℕ⟼g⁡1st⁡j⁡k⁡2nd⁡j⁡k
69 simplr ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→j:ℕ⟶1-1 ontoℕ×ℕ
70 simprl ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→g:ℕ⟶≤∩ℝ2ℕ
71 simprr ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
72 nfv ⊢ℲmA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n
73 nfcv ⊢Ⅎ_n⋃ran⁡.∘g⁡m
74 8 73 nfss ⊢Ⅎn⦋m/n⦌A⊆⋃ran⁡.∘g⁡m
75 nfcv ⊢Ⅎ_nsupran⁡seq1+abs∘−∘g⁡mℝ*<
76 nfcv ⊢Ⅎ_n≤
77 nfcv ⊢Ⅎ_n+
78 nfcv ⊢Ⅎ_nB2m
79 43 77 78 nfov ⊢Ⅎ_nvol*⁡⦋m/n⦌A+B2m
80 75 76 79 nfbr ⊢Ⅎnsupran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
81 74 80 nfan ⊢Ⅎn⦋m/n⦌A⊆⋃ran⁡.∘g⁡m∧supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
82 fveq2 ⊢n=m→g⁡n=g⁡m
83 82 coeq2d ⊢n=m→.∘g⁡n=.∘g⁡m
84 83 rneqd ⊢n=m→ran⁡.∘g⁡n=ran⁡.∘g⁡m
85 84 unieqd ⊢n=m→⋃ran⁡.∘g⁡n=⋃ran⁡.∘g⁡m
86 9 85 sseq12d ⊢n=m→A⊆⋃ran⁡.∘g⁡n↔⦋m/n⦌A⊆⋃ran⁡.∘g⁡m
87 82 coeq2d ⊢n=m→abs∘−∘g⁡n=abs∘−∘g⁡m
88 87 seqeq3d ⊢n=m→seq1+abs∘−∘g⁡n=seq1+abs∘−∘g⁡m
89 88 rneqd ⊢n=m→ran⁡seq1+abs∘−∘g⁡n=ran⁡seq1+abs∘−∘g⁡m
90 89 supeq1d ⊢n=m→supran⁡seq1+abs∘−∘g⁡nℝ*<=supran⁡seq1+abs∘−∘g⁡mℝ*<
91 oveq2 ⊢n=m→2n=2m
92 91 oveq2d ⊢n=m→B2n=B2m
93 44 92 oveq12d ⊢n=m→vol*⁡A+B2n=vol*⁡⦋m/n⦌A+B2m
94 90 93 breq12d ⊢n=m→supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n↔supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
95 86 94 anbi12d ⊢n=m→A⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n↔⦋m/n⦌A⊆⋃ran⁡.∘g⁡m∧supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
96 72 81 95 cbvralw ⊢∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n↔∀m∈ℕ⦋m/n⦌A⊆⋃ran⁡.∘g⁡m∧supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
97 71 96 sylib ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→∀m∈ℕ⦋m/n⦌A⊆⋃ran⁡.∘g⁡m∧supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
98 97 r19.21bi ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n∧m∈ℕ→⦋m/n⦌A⊆⋃ran⁡.∘g⁡m∧supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
99 98 simpld ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n∧m∈ℕ→⦋m/n⦌A⊆⋃ran⁡.∘g⁡m
100 98 simprd ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n∧m∈ℕ→supran⁡seq1+abs∘−∘g⁡mℝ*<≤vol*⁡⦋m/n⦌A+B2m
101 1 46 55 63 64 65 66 67 68 69 70 99 100 ovoliunlem2 ⊢φ∧j:ℕ⟶1-1 ontoℕ×ℕ∧g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
102 101 exp31 ⊢φ→j:ℕ⟶1-1 ontoℕ×ℕ→g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
103 102 exlimdv ⊢φ→∃jj:ℕ⟶1-1 ontoℕ×ℕ→g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
104 40 103 mpi ⊢φ→g:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
105 104 exlimdv ⊢φ→∃gg:ℕ⟶≤∩ℝ2ℕ∧∀n∈ℕA⊆⋃ran⁡.∘g⁡n∧supran⁡seq1+abs∘−∘g⁡nℝ*<≤vol*⁡A+B2n→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
106 36 105 mpd ⊢φ→vol*⁡⋃m∈ℕ⦋m/n⦌A≤supran⁡Tℝ*<+B
107 11 106 eqbrtrid ⊢φ→vol*⁡⋃n∈ℕA≤supran⁡Tℝ*<+B