Metamath Proof Explorer


Theorem ovolscalem1

Description: Lemma for ovolsca . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses ovolsca.1 φ A
ovolsca.2 φ C +
ovolsca.3 φ B = x | C x A
ovolsca.4 φ vol * A
ovolsca.5 S = seq 1 + abs F
ovolsca.6 G = n 1 st F n C 2 nd F n C
ovolsca.7 φ F : 2
ovolsca.8 φ A ran . F
ovolsca.9 φ R +
ovolsca.10 φ sup ran S * < vol * A + C R
Assertion ovolscalem1 φ vol * B vol * A C + R

Proof

Step Hyp Ref Expression
1 ovolsca.1 φ A
2 ovolsca.2 φ C +
3 ovolsca.3 φ B = x | C x A
4 ovolsca.4 φ vol * A
5 ovolsca.5 S = seq 1 + abs F
6 ovolsca.6 G = n 1 st F n C 2 nd F n C
7 ovolsca.7 φ F : 2
8 ovolsca.8 φ A ran . F
9 ovolsca.9 φ R +
10 ovolsca.10 φ sup ran S * < vol * A + C R
11 ssrab2 x | C x A
12 3 11 eqsstrdi φ B
13 ovolcl B vol * B *
14 12 13 syl φ vol * B *
15 ovolfcl F : 2 n 1 st F n 2 nd F n 1 st F n 2 nd F n
16 7 15 sylan φ n 1 st F n 2 nd F n 1 st F n 2 nd F n
17 16 simp3d φ n 1 st F n 2 nd F n
18 16 simp1d φ n 1 st F n
19 16 simp2d φ n 2 nd F n
20 2 rpregt0d φ C 0 < C
21 20 adantr φ n C 0 < C
22 lediv1 1 st F n 2 nd F n C 0 < C 1 st F n 2 nd F n 1 st F n C 2 nd F n C
23 18 19 21 22 syl3anc φ n 1 st F n 2 nd F n 1 st F n C 2 nd F n C
24 17 23 mpbid φ n 1 st F n C 2 nd F n C
25 df-br 1 st F n C 2 nd F n C 1 st F n C 2 nd F n C
26 24 25 sylib φ n 1 st F n C 2 nd F n C
27 2 adantr φ n C +
28 18 27 rerpdivcld φ n 1 st F n C
29 19 27 rerpdivcld φ n 2 nd F n C
30 28 29 opelxpd φ n 1 st F n C 2 nd F n C 2
31 26 30 elind φ n 1 st F n C 2 nd F n C 2
32 31 6 fmptd φ G : 2
33 eqid abs G = abs G
34 eqid seq 1 + abs G = seq 1 + abs G
35 33 34 ovolsf G : 2 seq 1 + abs G : 0 +∞
36 32 35 syl φ seq 1 + abs G : 0 +∞
37 36 frnd φ ran seq 1 + abs G 0 +∞
38 icossxr 0 +∞ *
39 37 38 sstrdi φ ran seq 1 + abs G *
40 supxrcl ran seq 1 + abs G * sup ran seq 1 + abs G * < *
41 39 40 syl φ sup ran seq 1 + abs G * < *
42 4 2 rerpdivcld φ vol * A C
43 9 rpred φ R
44 42 43 readdcld φ vol * A C + R
45 44 rexrd φ vol * A C + R *
46 3 eleq2d φ y B y x | C x A
47 oveq2 x = y C x = C y
48 47 eleq1d x = y C x A C y A
49 48 elrab y x | C x A y C y A
50 46 49 bitrdi φ y B y C y A
51 breq2 x = C y 1 st F n < x 1 st F n < C y
52 breq1 x = C y x < 2 nd F n C y < 2 nd F n
53 51 52 anbi12d x = C y 1 st F n < x x < 2 nd F n 1 st F n < C y C y < 2 nd F n
54 53 rexbidv x = C y n 1 st F n < x x < 2 nd F n n 1 st F n < C y C y < 2 nd F n
55 ovolfioo A F : 2 A ran . F x A n 1 st F n < x x < 2 nd F n
56 1 7 55 syl2anc φ A ran . F x A n 1 st F n < x x < 2 nd F n
57 8 56 mpbid φ x A n 1 st F n < x x < 2 nd F n
58 57 adantr φ y C y A x A n 1 st F n < x x < 2 nd F n
59 simprr φ y C y A C y A
60 54 58 59 rspcdva φ y C y A n 1 st F n < C y C y < 2 nd F n
61 opex 1 st F n C 2 nd F n C V
62 6 fvmpt2 n 1 st F n C 2 nd F n C V G n = 1 st F n C 2 nd F n C
63 61 62 mpan2 n G n = 1 st F n C 2 nd F n C
64 63 fveq2d n 1 st G n = 1 st 1 st F n C 2 nd F n C
65 ovex 1 st F n C V
66 ovex 2 nd F n C V
67 65 66 op1st 1 st 1 st F n C 2 nd F n C = 1 st F n C
68 64 67 eqtrdi n 1 st G n = 1 st F n C
69 68 adantl φ y C y A n 1 st G n = 1 st F n C
70 69 breq1d φ y C y A n 1 st G n < y 1 st F n C < y
71 18 adantlr φ y C y A n 1 st F n
72 simplrl φ y C y A n y
73 21 adantlr φ y C y A n C 0 < C
74 ltdivmul 1 st F n y C 0 < C 1 st F n C < y 1 st F n < C y
75 71 72 73 74 syl3anc φ y C y A n 1 st F n C < y 1 st F n < C y
76 70 75 bitr2d φ y C y A n 1 st F n < C y 1 st G n < y
77 19 adantlr φ y C y A n 2 nd F n
78 ltmuldiv2 y 2 nd F n C 0 < C C y < 2 nd F n y < 2 nd F n C
79 72 77 73 78 syl3anc φ y C y A n C y < 2 nd F n y < 2 nd F n C
80 63 fveq2d n 2 nd G n = 2 nd 1 st F n C 2 nd F n C
81 65 66 op2nd 2 nd 1 st F n C 2 nd F n C = 2 nd F n C
82 80 81 eqtrdi n 2 nd G n = 2 nd F n C
83 82 adantl φ y C y A n 2 nd G n = 2 nd F n C
84 83 breq2d φ y C y A n y < 2 nd G n y < 2 nd F n C
85 79 84 bitr4d φ y C y A n C y < 2 nd F n y < 2 nd G n
86 76 85 anbi12d φ y C y A n 1 st F n < C y C y < 2 nd F n 1 st G n < y y < 2 nd G n
87 86 rexbidva φ y C y A n 1 st F n < C y C y < 2 nd F n n 1 st G n < y y < 2 nd G n
88 60 87 mpbid φ y C y A n 1 st G n < y y < 2 nd G n
89 88 ex φ y C y A n 1 st G n < y y < 2 nd G n
90 50 89 sylbid φ y B n 1 st G n < y y < 2 nd G n
91 90 ralrimiv φ y B n 1 st G n < y y < 2 nd G n
92 ovolfioo B G : 2 B ran . G y B n 1 st G n < y y < 2 nd G n
93 12 32 92 syl2anc φ B ran . G y B n 1 st G n < y y < 2 nd G n
94 91 93 mpbird φ B ran . G
95 34 ovollb G : 2 B ran . G vol * B sup ran seq 1 + abs G * <
96 32 94 95 syl2anc φ vol * B sup ran seq 1 + abs G * <
97 fzfid φ k 1 k Fin
98 2 rpcnd φ C
99 98 adantr φ k C
100 simpl φ k φ
101 elfznn n 1 k n
102 19 18 resubcld φ n 2 nd F n 1 st F n
103 100 101 102 syl2an φ k n 1 k 2 nd F n 1 st F n
104 103 recnd φ k n 1 k 2 nd F n 1 st F n
105 2 rpne0d φ C 0
106 105 adantr φ k C 0
107 97 99 104 106 fsumdivc φ k n = 1 k 2 nd F n 1 st F n C = n = 1 k 2 nd F n 1 st F n C
108 82 68 oveq12d n 2 nd G n 1 st G n = 2 nd F n C 1 st F n C
109 108 adantl φ n 2 nd G n 1 st G n = 2 nd F n C 1 st F n C
110 33 ovolfsval G : 2 n abs G n = 2 nd G n 1 st G n
111 32 110 sylan φ n abs G n = 2 nd G n 1 st G n
112 19 recnd φ n 2 nd F n
113 18 recnd φ n 1 st F n
114 2 rpcnne0d φ C C 0
115 114 adantr φ n C C 0
116 divsubdir 2 nd F n 1 st F n C C 0 2 nd F n 1 st F n C = 2 nd F n C 1 st F n C
117 112 113 115 116 syl3anc φ n 2 nd F n 1 st F n C = 2 nd F n C 1 st F n C
118 109 111 117 3eqtr4d φ n abs G n = 2 nd F n 1 st F n C
119 100 101 118 syl2an φ k n 1 k abs G n = 2 nd F n 1 st F n C
120 simpr φ k k
121 nnuz = 1
122 120 121 eleqtrdi φ k k 1
123 102 27 rerpdivcld φ n 2 nd F n 1 st F n C
124 123 recnd φ n 2 nd F n 1 st F n C
125 100 101 124 syl2an φ k n 1 k 2 nd F n 1 st F n C
126 119 122 125 fsumser φ k n = 1 k 2 nd F n 1 st F n C = seq 1 + abs G k
127 107 126 eqtrd φ k n = 1 k 2 nd F n 1 st F n C = seq 1 + abs G k
128 eqid abs F = abs F
129 128 5 ovolsf F : 2 S : 0 +∞
130 7 129 syl φ S : 0 +∞
131 130 frnd φ ran S 0 +∞
132 131 38 sstrdi φ ran S *
133 2 9 rpmulcld φ C R +
134 133 rpred φ C R
135 4 134 readdcld φ vol * A + C R
136 135 rexrd φ vol * A + C R *
137 supxrleub ran S * vol * A + C R * sup ran S * < vol * A + C R x ran S x vol * A + C R
138 132 136 137 syl2anc φ sup ran S * < vol * A + C R x ran S x vol * A + C R
139 10 138 mpbid φ x ran S x vol * A + C R
140 130 ffnd φ S Fn
141 breq1 x = S k x vol * A + C R S k vol * A + C R
142 141 ralrn S Fn x ran S x vol * A + C R k S k vol * A + C R
143 140 142 syl φ x ran S x vol * A + C R k S k vol * A + C R
144 139 143 mpbid φ k S k vol * A + C R
145 144 r19.21bi φ k S k vol * A + C R
146 7 adantr φ k F : 2
147 128 ovolfsval F : 2 n abs F n = 2 nd F n 1 st F n
148 146 101 147 syl2an φ k n 1 k abs F n = 2 nd F n 1 st F n
149 148 122 104 fsumser φ k n = 1 k 2 nd F n 1 st F n = seq 1 + abs F k
150 5 fveq1i S k = seq 1 + abs F k
151 149 150 eqtr4di φ k n = 1 k 2 nd F n 1 st F n = S k
152 42 recnd φ vol * A C
153 9 rpcnd φ R
154 98 152 153 adddid φ C vol * A C + R = C vol * A C + C R
155 4 recnd φ vol * A
156 155 98 105 divcan2d φ C vol * A C = vol * A
157 156 oveq1d φ C vol * A C + C R = vol * A + C R
158 154 157 eqtrd φ C vol * A C + R = vol * A + C R
159 158 adantr φ k C vol * A C + R = vol * A + C R
160 145 151 159 3brtr4d φ k n = 1 k 2 nd F n 1 st F n C vol * A C + R
161 97 103 fsumrecl φ k n = 1 k 2 nd F n 1 st F n
162 44 adantr φ k vol * A C + R
163 20 adantr φ k C 0 < C
164 ledivmul n = 1 k 2 nd F n 1 st F n vol * A C + R C 0 < C n = 1 k 2 nd F n 1 st F n C vol * A C + R n = 1 k 2 nd F n 1 st F n C vol * A C + R
165 161 162 163 164 syl3anc φ k n = 1 k 2 nd F n 1 st F n C vol * A C + R n = 1 k 2 nd F n 1 st F n C vol * A C + R
166 160 165 mpbird φ k n = 1 k 2 nd F n 1 st F n C vol * A C + R
167 127 166 eqbrtrrd φ k seq 1 + abs G k vol * A C + R
168 167 ralrimiva φ k seq 1 + abs G k vol * A C + R
169 36 ffnd φ seq 1 + abs G Fn
170 breq1 y = seq 1 + abs G k y vol * A C + R seq 1 + abs G k vol * A C + R
171 170 ralrn seq 1 + abs G Fn y ran seq 1 + abs G y vol * A C + R k seq 1 + abs G k vol * A C + R
172 169 171 syl φ y ran seq 1 + abs G y vol * A C + R k seq 1 + abs G k vol * A C + R
173 168 172 mpbird φ y ran seq 1 + abs G y vol * A C + R
174 supxrleub ran seq 1 + abs G * vol * A C + R * sup ran seq 1 + abs G * < vol * A C + R y ran seq 1 + abs G y vol * A C + R
175 39 45 174 syl2anc φ sup ran seq 1 + abs G * < vol * A C + R y ran seq 1 + abs G y vol * A C + R
176 173 175 mpbird φ sup ran seq 1 + abs G * < vol * A C + R
177 14 41 45 96 176 xrletrd φ vol * B vol * A C + R