Metamath Proof Explorer


Theorem voliunlem3

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 φ F : dom vol
voliunlem.5 φ Disj i F i
voliunlem.6 H = n vol * x F n
voliunlem3.1 S = seq 1 + G
voliunlem3.2 G = n vol F n
voliunlem3.4 φ i vol F i
Assertion voliunlem3 φ vol ran F = sup ran S * <

Proof

Step Hyp Ref Expression
1 voliunlem.3 φ F : dom vol
2 voliunlem.5 φ Disj i F i
3 voliunlem.6 H = n vol * x F n
4 voliunlem3.1 S = seq 1 + G
5 voliunlem3.2 G = n vol F n
6 voliunlem3.4 φ i vol F i
7 1 2 3 voliunlem2 φ ran F dom vol
8 mblvol ran F dom vol vol ran F = vol * ran F
9 7 8 syl φ vol ran F = vol * ran F
10 1 frnd φ ran F dom vol
11 mblss x dom vol x
12 reex V
13 12 elpw2 x 𝒫 x
14 11 13 sylibr x dom vol x 𝒫
15 14 ssriv dom vol 𝒫
16 10 15 sstrdi φ ran F 𝒫
17 sspwuni ran F 𝒫 ran F
18 16 17 sylib φ ran F
19 ovolcl ran F vol * ran F *
20 18 19 syl φ vol * ran F *
21 nnuz = 1
22 1zzd φ 1
23 2fveq3 n = k vol F n = vol F k
24 fvex vol F k V
25 23 5 24 fvmpt k G k = vol F k
26 25 adantl φ k G k = vol F k
27 2fveq3 i = k vol F i = vol F k
28 27 eleq1d i = k vol F i vol F k
29 28 rspccva i vol F i k vol F k
30 6 29 sylan φ k vol F k
31 26 30 eqeltrd φ k G k
32 21 22 31 serfre φ seq 1 + G :
33 4 feq1i S : seq 1 + G :
34 32 33 sylibr φ S :
35 34 frnd φ ran S
36 ressxr *
37 35 36 sstrdi φ ran S *
38 supxrcl ran S * sup ran S * < *
39 37 38 syl φ sup ran S * < *
40 eqid seq 1 + n vol * F n = seq 1 + n vol * F n
41 eqid n vol * F n = n vol * F n
42 1 ffvelrnda φ n F n dom vol
43 mblss F n dom vol F n
44 42 43 syl φ n F n
45 mblvol F n dom vol vol F n = vol * F n
46 42 45 syl φ n vol F n = vol * F n
47 2fveq3 i = n vol F i = vol F n
48 47 eleq1d i = n vol F i vol F n
49 48 rspccva i vol F i n vol F n
50 6 49 sylan φ n vol F n
51 46 50 eqeltrrd φ n vol * F n
52 40 41 44 51 ovoliun φ vol * n F n sup ran seq 1 + n vol * F n * <
53 1 ffnd φ F Fn
54 fniunfv F Fn n F n = ran F
55 53 54 syl φ n F n = ran F
56 55 fveq2d φ vol * n F n = vol * ran F
57 46 mpteq2dva φ n vol F n = n vol * F n
58 5 57 syl5eq φ G = n vol * F n
59 58 seqeq3d φ seq 1 + G = seq 1 + n vol * F n
60 4 59 eqtr2id φ seq 1 + n vol * F n = S
61 60 rneqd φ ran seq 1 + n vol * F n = ran S
62 61 supeq1d φ sup ran seq 1 + n vol * F n * < = sup ran S * <
63 52 56 62 3brtr3d φ vol * ran F sup ran S * <
64 ovolge0 ran F 0 vol * ran F
65 18 64 syl φ 0 vol * ran F
66 mnflt0 −∞ < 0
67 mnfxr −∞ *
68 0xr 0 *
69 xrltletr −∞ * 0 * vol * ran F * −∞ < 0 0 vol * ran F −∞ < vol * ran F
70 67 68 69 mp3an12 vol * ran F * −∞ < 0 0 vol * ran F −∞ < vol * ran F
71 66 70 mpani vol * ran F * 0 vol * ran F −∞ < vol * ran F
72 20 65 71 sylc φ −∞ < vol * ran F
73 xrrebnd vol * ran F * vol * ran F −∞ < vol * ran F vol * ran F < +∞
74 20 73 syl φ vol * ran F −∞ < vol * ran F vol * ran F < +∞
75 12 elpw2 ran F 𝒫 ran F
76 18 75 sylibr φ ran F 𝒫
77 simpl x = ran F φ x = ran F
78 77 sseq1d x = ran F φ x ran F
79 77 fveq2d x = ran F φ vol * x = vol * ran F
80 79 eleq1d x = ran F φ vol * x vol * ran F
81 simpll x = ran F φ n x = ran F
82 81 ineq1d x = ran F φ n x F n = ran F F n
83 fnfvelrn F Fn n F n ran F
84 53 83 sylan φ n F n ran F
85 elssuni F n ran F F n ran F
86 84 85 syl φ n F n ran F
87 86 adantll x = ran F φ n F n ran F
88 sseqin2 F n ran F ran F F n = F n
89 87 88 sylib x = ran F φ n ran F F n = F n
90 82 89 eqtrd x = ran F φ n x F n = F n
91 90 fveq2d x = ran F φ n vol * x F n = vol * F n
92 46 adantll x = ran F φ n vol F n = vol * F n
93 91 92 eqtr4d x = ran F φ n vol * x F n = vol F n
94 93 mpteq2dva x = ran F φ n vol * x F n = n vol F n
95 94 adantrr x = ran F φ k n vol * x F n = n vol F n
96 95 3 5 3eqtr4g x = ran F φ k H = G
97 96 seqeq3d x = ran F φ k seq 1 + H = seq 1 + G
98 97 4 eqtr4di x = ran F φ k seq 1 + H = S
99 98 fveq1d x = ran F φ k seq 1 + H k = S k
100 difeq1 x = ran F x ran F = ran F ran F
101 difid ran F ran F =
102 100 101 eqtrdi x = ran F x ran F =
103 102 fveq2d x = ran F vol * x ran F = vol *
104 ovol0 vol * = 0
105 103 104 eqtrdi x = ran F vol * x ran F = 0
106 105 adantr x = ran F φ k vol * x ran F = 0
107 99 106 oveq12d x = ran F φ k seq 1 + H k + vol * x ran F = S k + 0
108 34 ffvelrnda φ k S k
109 108 adantl x = ran F φ k S k
110 109 recnd x = ran F φ k S k
111 110 addid1d x = ran F φ k S k + 0 = S k
112 107 111 eqtrd x = ran F φ k seq 1 + H k + vol * x ran F = S k
113 fveq2 x = ran F vol * x = vol * ran F
114 113 adantr x = ran F φ k vol * x = vol * ran F
115 112 114 breq12d x = ran F φ k seq 1 + H k + vol * x ran F vol * x S k vol * ran F
116 115 expr x = ran F φ k seq 1 + H k + vol * x ran F vol * x S k vol * ran F
117 116 pm5.74d x = ran F φ k seq 1 + H k + vol * x ran F vol * x k S k vol * ran F
118 80 117 imbi12d x = ran F φ vol * x k seq 1 + H k + vol * x ran F vol * x vol * ran F k S k vol * ran F
119 78 118 imbi12d x = ran F φ x vol * x k seq 1 + H k + vol * x ran F vol * x ran F vol * ran F k S k vol * ran F
120 119 pm5.74da x = ran F φ x vol * x k seq 1 + H k + vol * x ran F vol * x φ ran F vol * ran F k S k vol * ran F
121 1 3ad2ant1 φ x vol * x F : dom vol
122 2 3ad2ant1 φ x vol * x Disj i F i
123 simp2 φ x vol * x x
124 simp3 φ x vol * x vol * x
125 121 122 3 123 124 voliunlem1 φ x vol * x k seq 1 + H k + vol * x ran F vol * x
126 125 3exp1 φ x vol * x k seq 1 + H k + vol * x ran F vol * x
127 120 126 vtoclg ran F 𝒫 φ ran F vol * ran F k S k vol * ran F
128 76 127 mpcom φ ran F vol * ran F k S k vol * ran F
129 18 128 mpd φ vol * ran F k S k vol * ran F
130 74 129 sylbird φ −∞ < vol * ran F vol * ran F < +∞ k S k vol * ran F
131 72 130 mpand φ vol * ran F < +∞ k S k vol * ran F
132 nltpnft vol * ran F * vol * ran F = +∞ ¬ vol * ran F < +∞
133 20 132 syl φ vol * ran F = +∞ ¬ vol * ran F < +∞
134 rexr S k S k *
135 pnfge S k * S k +∞
136 108 134 135 3syl φ k S k +∞
137 136 ex φ k S k +∞
138 breq2 vol * ran F = +∞ S k vol * ran F S k +∞
139 138 imbi2d vol * ran F = +∞ k S k vol * ran F k S k +∞
140 137 139 syl5ibrcom φ vol * ran F = +∞ k S k vol * ran F
141 133 140 sylbird φ ¬ vol * ran F < +∞ k S k vol * ran F
142 131 141 pm2.61d φ k S k vol * ran F
143 142 ralrimiv φ k S k vol * ran F
144 34 ffnd φ S Fn
145 breq1 z = S k z vol * ran F S k vol * ran F
146 145 ralrn S Fn z ran S z vol * ran F k S k vol * ran F
147 144 146 syl φ z ran S z vol * ran F k S k vol * ran F
148 143 147 mpbird φ z ran S z vol * ran F
149 supxrleub ran S * vol * ran F * sup ran S * < vol * ran F z ran S z vol * ran F
150 37 20 149 syl2anc φ sup ran S * < vol * ran F z ran S z vol * ran F
151 148 150 mpbird φ sup ran S * < vol * ran F
152 20 39 63 151 xrletrid φ vol * ran F = sup ran S * <
153 9 152 eqtrd φ vol ran F = sup ran S * <