Metamath Proof Explorer


Theorem ovoliunlem2

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

Ref Expression
Hypotheses ovoliun.t T = seq 1 + G
ovoliun.g G = n vol * A
ovoliun.a φ n A
ovoliun.v φ n vol * A
ovoliun.r φ sup ran T * <
ovoliun.b φ B +
ovoliun.s S = seq 1 + abs F n
ovoliun.u U = seq 1 + abs H
ovoliun.h H = k F 1 st J k 2 nd J k
ovoliun.j φ J : 1-1 onto ×
ovoliun.f φ F : 2
ovoliun.x1 φ n A ran . F n
ovoliun.x2 φ n sup ran S * < vol * A + B 2 n
Assertion ovoliunlem2 φ vol * n A sup ran T * < + B

Proof

Step Hyp Ref Expression
1 ovoliun.t T = seq 1 + G
2 ovoliun.g G = n vol * A
3 ovoliun.a φ n A
4 ovoliun.v φ n vol * A
5 ovoliun.r φ sup ran T * <
6 ovoliun.b φ B +
7 ovoliun.s S = seq 1 + abs F n
8 ovoliun.u U = seq 1 + abs H
9 ovoliun.h H = k F 1 st J k 2 nd J k
10 ovoliun.j φ J : 1-1 onto ×
11 ovoliun.f φ F : 2
12 ovoliun.x1 φ n A ran . F n
13 ovoliun.x2 φ n sup ran S * < vol * A + B 2 n
14 3 ralrimiva φ n A
15 iunss n A n A
16 14 15 sylibr φ n A
17 ovolcl n A vol * n A *
18 16 17 syl φ vol * n A *
19 11 adantr φ k F : 2
20 f1of J : 1-1 onto × J : ×
21 10 20 syl φ J : ×
22 21 ffvelrnda φ k J k ×
23 xp1st J k × 1 st J k
24 22 23 syl φ k 1 st J k
25 19 24 ffvelrnd φ k F 1 st J k 2
26 elovolmlem F 1 st J k 2 F 1 st J k : 2
27 25 26 sylib φ k F 1 st J k : 2
28 xp2nd J k × 2 nd J k
29 22 28 syl φ k 2 nd J k
30 27 29 ffvelrnd φ k F 1 st J k 2 nd J k 2
31 30 9 fmptd φ H : 2
32 eqid abs H = abs H
33 32 8 ovolsf H : 2 U : 0 +∞
34 frn U : 0 +∞ ran U 0 +∞
35 31 33 34 3syl φ ran U 0 +∞
36 icossxr 0 +∞ *
37 35 36 sstrdi φ ran U *
38 supxrcl ran U * sup ran U * < *
39 37 38 syl φ sup ran U * < *
40 6 rpred φ B
41 5 40 readdcld φ sup ran T * < + B
42 41 rexrd φ sup ran T * < + B *
43 eliun z n A n z A
44 12 3adant3 φ n z A A ran . F n
45 3 3adant3 φ n z A A
46 11 ffvelrnda φ n F n 2
47 elovolmlem F n 2 F n : 2
48 46 47 sylib φ n F n : 2
49 48 3adant3 φ n z A F n : 2
50 ovolfioo A F n : 2 A ran . F n z A j 1 st F n j < z z < 2 nd F n j
51 45 49 50 syl2anc φ n z A A ran . F n z A j 1 st F n j < z z < 2 nd F n j
52 44 51 mpbid φ n z A z A j 1 st F n j < z z < 2 nd F n j
53 simp3 φ n z A z A
54 rsp z A j 1 st F n j < z z < 2 nd F n j z A j 1 st F n j < z z < 2 nd F n j
55 52 53 54 sylc φ n z A j 1 st F n j < z z < 2 nd F n j
56 simpl1 φ n z A j φ
57 f1ocnv J : 1-1 onto × J -1 : × 1-1 onto
58 f1of J -1 : × 1-1 onto J -1 : ×
59 56 10 57 58 4syl φ n z A j J -1 : ×
60 simpl2 φ n z A j n
61 simpr φ n z A j j
62 59 60 61 fovrnd φ n z A j n J -1 j
63 2fveq3 k = n J -1 j 1 st J k = 1 st J n J -1 j
64 63 fveq2d k = n J -1 j F 1 st J k = F 1 st J n J -1 j
65 2fveq3 k = n J -1 j 2 nd J k = 2 nd J n J -1 j
66 64 65 fveq12d k = n J -1 j F 1 st J k 2 nd J k = F 1 st J n J -1 j 2 nd J n J -1 j
67 fvex F 1 st J n J -1 j 2 nd J n J -1 j V
68 66 9 67 fvmpt n J -1 j H n J -1 j = F 1 st J n J -1 j 2 nd J n J -1 j
69 62 68 syl φ n z A j H n J -1 j = F 1 st J n J -1 j 2 nd J n J -1 j
70 df-ov n J -1 j = J -1 n j
71 70 fveq2i J n J -1 j = J J -1 n j
72 56 10 syl φ n z A j J : 1-1 onto ×
73 60 61 opelxpd φ n z A j n j ×
74 f1ocnvfv2 J : 1-1 onto × n j × J J -1 n j = n j
75 72 73 74 syl2anc φ n z A j J J -1 n j = n j
76 71 75 syl5eq φ n z A j J n J -1 j = n j
77 76 fveq2d φ n z A j 1 st J n J -1 j = 1 st n j
78 vex n V
79 vex j V
80 78 79 op1st 1 st n j = n
81 77 80 syl6eq φ n z A j 1 st J n J -1 j = n
82 81 fveq2d φ n z A j F 1 st J n J -1 j = F n
83 76 fveq2d φ n z A j 2 nd J n J -1 j = 2 nd n j
84 78 79 op2nd 2 nd n j = j
85 83 84 syl6eq φ n z A j 2 nd J n J -1 j = j
86 82 85 fveq12d φ n z A j F 1 st J n J -1 j 2 nd J n J -1 j = F n j
87 69 86 eqtrd φ n z A j H n J -1 j = F n j
88 87 fveq2d φ n z A j 1 st H n J -1 j = 1 st F n j
89 88 breq1d φ n z A j 1 st H n J -1 j < z 1 st F n j < z
90 87 fveq2d φ n z A j 2 nd H n J -1 j = 2 nd F n j
91 90 breq2d φ n z A j z < 2 nd H n J -1 j z < 2 nd F n j
92 89 91 anbi12d φ n z A j 1 st H n J -1 j < z z < 2 nd H n J -1 j 1 st F n j < z z < 2 nd F n j
93 92 biimprd φ n z A j 1 st F n j < z z < 2 nd F n j 1 st H n J -1 j < z z < 2 nd H n J -1 j
94 2fveq3 m = n J -1 j 1 st H m = 1 st H n J -1 j
95 94 breq1d m = n J -1 j 1 st H m < z 1 st H n J -1 j < z
96 2fveq3 m = n J -1 j 2 nd H m = 2 nd H n J -1 j
97 96 breq2d m = n J -1 j z < 2 nd H m z < 2 nd H n J -1 j
98 95 97 anbi12d m = n J -1 j 1 st H m < z z < 2 nd H m 1 st H n J -1 j < z z < 2 nd H n J -1 j
99 98 rspcev n J -1 j 1 st H n J -1 j < z z < 2 nd H n J -1 j m 1 st H m < z z < 2 nd H m
100 62 93 99 syl6an φ n z A j 1 st F n j < z z < 2 nd F n j m 1 st H m < z z < 2 nd H m
101 100 rexlimdva φ n z A j 1 st F n j < z z < 2 nd F n j m 1 st H m < z z < 2 nd H m
102 55 101 mpd φ n z A m 1 st H m < z z < 2 nd H m
103 102 rexlimdv3a φ n z A m 1 st H m < z z < 2 nd H m
104 43 103 syl5bi φ z n A m 1 st H m < z z < 2 nd H m
105 104 ralrimiv φ z n A m 1 st H m < z z < 2 nd H m
106 ovolfioo n A H : 2 n A ran . H z n A m 1 st H m < z z < 2 nd H m
107 16 31 106 syl2anc φ n A ran . H z n A m 1 st H m < z z < 2 nd H m
108 105 107 mpbird φ n A ran . H
109 8 ovollb H : 2 n A ran . H vol * n A sup ran U * <
110 31 108 109 syl2anc φ vol * n A sup ran U * <
111 fzfi 1 j Fin
112 elfznn w 1 j w
113 ffvelrn J : × w J w ×
114 xp1st J w × 1 st J w
115 nnre 1 st J w 1 st J w
116 113 114 115 3syl J : × w 1 st J w
117 21 112 116 syl2an φ w 1 j 1 st J w
118 117 ralrimiva φ w 1 j 1 st J w
119 118 adantr φ j w 1 j 1 st J w
120 fimaxre3 1 j Fin w 1 j 1 st J w x w 1 j 1 st J w x
121 111 119 120 sylancr φ j x w 1 j 1 st J w x
122 fllep1 x x x + 1
123 122 ad2antlr φ x w 1 j x x + 1
124 117 adantlr φ x w 1 j 1 st J w
125 simplr φ x w 1 j x
126 flcl x x
127 126 peano2zd x x + 1
128 127 zred x x + 1
129 128 ad2antlr φ x w 1 j x + 1
130 letr 1 st J w x x + 1 1 st J w x x x + 1 1 st J w x + 1
131 124 125 129 130 syl3anc φ x w 1 j 1 st J w x x x + 1 1 st J w x + 1
132 123 131 mpan2d φ x w 1 j 1 st J w x 1 st J w x + 1
133 132 ralimdva φ x w 1 j 1 st J w x w 1 j 1 st J w x + 1
134 133 adantlr φ j x w 1 j 1 st J w x w 1 j 1 st J w x + 1
135 simpll φ j x w 1 j 1 st J w x + 1 φ
136 135 3 sylan φ j x w 1 j 1 st J w x + 1 n A
137 135 4 sylan φ j x w 1 j 1 st J w x + 1 n vol * A
138 135 5 syl φ j x w 1 j 1 st J w x + 1 sup ran T * <
139 135 6 syl φ j x w 1 j 1 st J w x + 1 B +
140 135 10 syl φ j x w 1 j 1 st J w x + 1 J : 1-1 onto ×
141 135 11 syl φ j x w 1 j 1 st J w x + 1 F : 2
142 135 12 sylan φ j x w 1 j 1 st J w x + 1 n A ran . F n
143 135 13 sylan φ j x w 1 j 1 st J w x + 1 n sup ran S * < vol * A + B 2 n
144 simplr φ j x w 1 j 1 st J w x + 1 j
145 127 ad2antrl φ j x w 1 j 1 st J w x + 1 x + 1
146 simprr φ j x w 1 j 1 st J w x + 1 w 1 j 1 st J w x + 1
147 1 2 136 137 138 139 7 8 9 140 141 142 143 144 145 146 ovoliunlem1 φ j x w 1 j 1 st J w x + 1 U j sup ran T * < + B
148 147 expr φ j x w 1 j 1 st J w x + 1 U j sup ran T * < + B
149 134 148 syld φ j x w 1 j 1 st J w x U j sup ran T * < + B
150 149 rexlimdva φ j x w 1 j 1 st J w x U j sup ran T * < + B
151 121 150 mpd φ j U j sup ran T * < + B
152 151 ralrimiva φ j U j sup ran T * < + B
153 ffn U : 0 +∞ U Fn
154 breq1 z = U j z sup ran T * < + B U j sup ran T * < + B
155 154 ralrn U Fn z ran U z sup ran T * < + B j U j sup ran T * < + B
156 31 33 153 155 4syl φ z ran U z sup ran T * < + B j U j sup ran T * < + B
157 152 156 mpbird φ z ran U z sup ran T * < + B
158 supxrleub ran U * sup ran T * < + B * sup ran U * < sup ran T * < + B z ran U z sup ran T * < + B
159 37 42 158 syl2anc φ sup ran U * < sup ran T * < + B z ran U z sup ran T * < + B
160 157 159 mpbird φ sup ran U * < sup ran T * < + B
161 18 39 42 110 160 xrletrd φ vol * n A sup ran T * < + B