Metamath Proof Explorer


Theorem axcontlem2

Description: Lemma for axcont . The idea here is to set up a mapping F that will allow us to transfer dedekind to two sets of points. Here, we set up F and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Hypotheses axcontlem2.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
axcontlem2.2 F = x t | x D t 0 +∞ i 1 N x i = 1 t Z i + t U i
Assertion axcontlem2 N Z 𝔼 N U 𝔼 N Z U F : D 1-1 onto 0 +∞

Proof

Step Hyp Ref Expression
1 axcontlem2.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
2 axcontlem2.2 F = x t | x D t 0 +∞ i 1 N x i = 1 t Z i + t U i
3 opeq2 p = x Z p = Z x
4 3 breq2d p = x U Btwn Z p U Btwn Z x
5 breq1 p = x p Btwn Z U x Btwn Z U
6 4 5 orbi12d p = x U Btwn Z p p Btwn Z U U Btwn Z x x Btwn Z U
7 6 1 elrab2 x D x 𝔼 N U Btwn Z x x Btwn Z U
8 simpll3 N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U 𝔼 N
9 simpll2 N Z 𝔼 N U 𝔼 N Z U x 𝔼 N Z 𝔼 N
10 simpr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N x 𝔼 N
11 brbtwn U 𝔼 N Z 𝔼 N x 𝔼 N U Btwn Z x s 0 1 i 1 N U i = 1 s Z i + s x i
12 8 9 10 11 syl3anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U Btwn Z x s 0 1 i 1 N U i = 1 s Z i + s x i
13 12 biimpa N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U Btwn Z x s 0 1 i 1 N U i = 1 s Z i + s x i
14 simp-4r N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i Z U
15 oveq2 s = 0 1 s = 1 0
16 1m0e1 1 0 = 1
17 15 16 eqtrdi s = 0 1 s = 1
18 17 oveq1d s = 0 1 s Z i = 1 Z i
19 oveq1 s = 0 s x i = 0 x i
20 18 19 oveq12d s = 0 1 s Z i + s x i = 1 Z i + 0 x i
21 20 eqeq2d s = 0 U i = 1 s Z i + s x i U i = 1 Z i + 0 x i
22 21 ralbidv s = 0 i 1 N U i = 1 s Z i + s x i i 1 N U i = 1 Z i + 0 x i
23 22 biimpac i 1 N U i = 1 s Z i + s x i s = 0 i 1 N U i = 1 Z i + 0 x i
24 eqcom Z = U U = Z
25 8 adantr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 U 𝔼 N
26 9 adantr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 Z 𝔼 N
27 eqeefv U 𝔼 N Z 𝔼 N U = Z i 1 N U i = Z i
28 25 26 27 syl2anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 U = Z i 1 N U i = Z i
29 9 ad2antrr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N Z 𝔼 N
30 fveecn Z 𝔼 N i 1 N Z i
31 29 30 sylancom N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N Z i
32 fveecn x 𝔼 N i 1 N x i
33 32 ad4ant24 N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N x i
34 mulid2 Z i 1 Z i = Z i
35 mul02 x i 0 x i = 0
36 34 35 oveqan12d Z i x i 1 Z i + 0 x i = Z i + 0
37 addid1 Z i Z i + 0 = Z i
38 37 adantr Z i x i Z i + 0 = Z i
39 36 38 eqtrd Z i x i 1 Z i + 0 x i = Z i
40 39 eqeq2d Z i x i U i = 1 Z i + 0 x i U i = Z i
41 31 33 40 syl2anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 Z i + 0 x i U i = Z i
42 41 ralbidva N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 Z i + 0 x i i 1 N U i = Z i
43 28 42 bitr4d N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 U = Z i 1 N U i = 1 Z i + 0 x i
44 24 43 syl5bb N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 Z = U i 1 N U i = 1 Z i + 0 x i
45 23 44 syl5ibr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i s = 0 Z = U
46 45 expdimp N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i s = 0 Z = U
47 46 necon3d N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i Z U s 0
48 14 47 mpd N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i s 0
49 elicc01 s 0 1 s 0 s s 1
50 49 simp1bi s 0 1 s
51 rereccl s s 0 1 s
52 50 51 sylan s 0 1 s 0 1 s
53 50 adantr s 0 1 s 0 s
54 49 simp2bi s 0 1 0 s
55 54 adantr s 0 1 s 0 0 s
56 simpr s 0 1 s 0 s 0
57 53 55 56 ne0gt0d s 0 1 s 0 0 < s
58 1re 1
59 0le1 0 1
60 divge0 1 0 1 s 0 < s 0 1 s
61 58 59 60 mpanl12 s 0 < s 0 1 s
62 53 57 61 syl2anc s 0 1 s 0 0 1 s
63 elrege0 1 s 0 +∞ 1 s 0 1 s
64 52 62 63 sylanbrc s 0 1 s 0 1 s 0 +∞
65 64 adantll N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 1 s 0 +∞
66 50 ad3antlr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N s
67 66 recnd N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N s
68 simplr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N s 0
69 32 ad5ant25 N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N x i
70 9 ad3antrrr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N Z 𝔼 N
71 70 30 sylancom N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N Z i
72 ax-1cn 1
73 reccl s s 0 1 s
74 subcl 1 1 s 1 1 s
75 72 73 74 sylancr s s 0 1 1 s
76 75 adantr s s 0 x i Z i 1 1 s
77 subcl 1 s 1 s
78 72 77 mpan s 1 s
79 78 adantr s s 0 1 s
80 73 79 mulcld s s 0 1 s 1 s
81 80 adantr s s 0 x i Z i 1 s 1 s
82 simprr s s 0 x i Z i Z i
83 76 81 82 adddird s s 0 x i Z i 1 - 1 s + 1 s 1 s Z i = 1 1 s Z i + 1 s 1 s Z i
84 simpl s s 0 s
85 subdi 1 s 1 s 1 s 1 s = 1 s 1 1 s s
86 72 85 mp3an2 1 s s 1 s 1 s = 1 s 1 1 s s
87 73 84 86 syl2anc s s 0 1 s 1 s = 1 s 1 1 s s
88 87 oveq2d s s 0 1 - 1 s + 1 s 1 s = 1 1 s + 1 s 1 - 1 s s
89 73 mulid1d s s 0 1 s 1 = 1 s
90 recid2 s s 0 1 s s = 1
91 89 90 oveq12d s s 0 1 s 1 1 s s = 1 s 1
92 91 oveq2d s s 0 1 1 s + 1 s 1 - 1 s s = 1 1 s + 1 s - 1
93 addsubass 1 1 s 1 s 1 1 1 s + 1 s - 1 = 1 1 s + 1 s - 1
94 72 93 mp3an3 1 1 s 1 s 1 1 s + 1 s - 1 = 1 1 s + 1 s - 1
95 75 73 94 syl2anc s s 0 1 1 s + 1 s - 1 = 1 1 s + 1 s - 1
96 75 73 addcld s s 0 1 - 1 s + 1 s
97 npcan 1 1 s 1 - 1 s + 1 s = 1
98 72 73 97 sylancr s s 0 1 - 1 s + 1 s = 1
99 96 98 subeq0bd s s 0 1 1 s + 1 s - 1 = 0
100 92 95 99 3eqtr2d s s 0 1 1 s + 1 s 1 - 1 s s = 0
101 88 100 eqtrd s s 0 1 - 1 s + 1 s 1 s = 0
102 101 adantr s s 0 x i Z i 1 - 1 s + 1 s 1 s = 0
103 102 oveq1d s s 0 x i Z i 1 - 1 s + 1 s 1 s Z i = 0 Z i
104 73 adantr s s 0 x i Z i 1 s
105 78 ad2antrr s s 0 x i Z i 1 s
106 104 105 82 mulassd s s 0 x i Z i 1 s 1 s Z i = 1 s 1 s Z i
107 106 oveq2d s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i = 1 1 s Z i + 1 s 1 s Z i
108 83 103 107 3eqtr3rd s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i = 0 Z i
109 mul02 Z i 0 Z i = 0
110 109 ad2antll s s 0 x i Z i 0 Z i = 0
111 108 110 eqtrd s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i = 0
112 simpll s s 0 x i Z i s
113 simprl s s 0 x i Z i x i
114 104 112 113 mulassd s s 0 x i Z i 1 s s x i = 1 s s x i
115 90 oveq1d s s 0 1 s s x i = 1 x i
116 mulid2 x i 1 x i = x i
117 116 adantr x i Z i 1 x i = x i
118 115 117 sylan9eq s s 0 x i Z i 1 s s x i = x i
119 114 118 eqtr3d s s 0 x i Z i 1 s s x i = x i
120 111 119 oveq12d s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i + 1 s s x i = 0 + x i
121 76 82 mulcld s s 0 x i Z i 1 1 s Z i
122 simpr x i Z i Z i
123 mulcl 1 s Z i 1 s Z i
124 79 122 123 syl2an s s 0 x i Z i 1 s Z i
125 104 124 mulcld s s 0 x i Z i 1 s 1 s Z i
126 mulcl s x i s x i
127 126 ad2ant2r s s 0 x i Z i s x i
128 104 127 mulcld s s 0 x i Z i 1 s s x i
129 121 125 128 addassd s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i + 1 s s x i = 1 1 s Z i + 1 s 1 s Z i + 1 s s x i
130 104 124 127 adddid s s 0 x i Z i 1 s 1 s Z i + s x i = 1 s 1 s Z i + 1 s s x i
131 130 oveq2d s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i + s x i = 1 1 s Z i + 1 s 1 s Z i + 1 s s x i
132 129 131 eqtr4d s s 0 x i Z i 1 1 s Z i + 1 s 1 s Z i + 1 s s x i = 1 1 s Z i + 1 s 1 s Z i + s x i
133 addid2 x i 0 + x i = x i
134 133 ad2antrl s s 0 x i Z i 0 + x i = x i
135 120 132 134 3eqtr3rd s s 0 x i Z i x i = 1 1 s Z i + 1 s 1 s Z i + s x i
136 67 68 69 71 135 syl22anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N x i = 1 1 s Z i + 1 s 1 s Z i + s x i
137 136 ralrimiva N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N x i = 1 1 s Z i + 1 s 1 s Z i + s x i
138 oveq2 t = 1 s 1 t = 1 1 s
139 138 oveq1d t = 1 s 1 t Z i = 1 1 s Z i
140 oveq1 t = 1 s t 1 s Z i + s x i = 1 s 1 s Z i + s x i
141 139 140 oveq12d t = 1 s 1 t Z i + t 1 s Z i + s x i = 1 1 s Z i + 1 s 1 s Z i + s x i
142 141 eqeq2d t = 1 s x i = 1 t Z i + t 1 s Z i + s x i x i = 1 1 s Z i + 1 s 1 s Z i + s x i
143 142 ralbidv t = 1 s i 1 N x i = 1 t Z i + t 1 s Z i + s x i i 1 N x i = 1 1 s Z i + 1 s 1 s Z i + s x i
144 143 rspcev 1 s 0 +∞ i 1 N x i = 1 1 s Z i + 1 s 1 s Z i + s x i t 0 +∞ i 1 N x i = 1 t Z i + t 1 s Z i + s x i
145 65 137 144 syl2anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 t 0 +∞ i 1 N x i = 1 t Z i + t 1 s Z i + s x i
146 oveq2 U i = 1 s Z i + s x i t U i = t 1 s Z i + s x i
147 146 oveq2d U i = 1 s Z i + s x i 1 t Z i + t U i = 1 t Z i + t 1 s Z i + s x i
148 147 eqeq2d U i = 1 s Z i + s x i x i = 1 t Z i + t U i x i = 1 t Z i + t 1 s Z i + s x i
149 148 ralimi i 1 N U i = 1 s Z i + s x i i 1 N x i = 1 t Z i + t U i x i = 1 t Z i + t 1 s Z i + s x i
150 ralbi i 1 N x i = 1 t Z i + t U i x i = 1 t Z i + t 1 s Z i + s x i i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 t Z i + t 1 s Z i + s x i
151 149 150 syl i 1 N U i = 1 s Z i + s x i i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 t Z i + t 1 s Z i + s x i
152 151 rexbidv i 1 N U i = 1 s Z i + s x i t 0 +∞ i 1 N x i = 1 t Z i + t U i t 0 +∞ i 1 N x i = 1 t Z i + t 1 s Z i + s x i
153 145 152 syl5ibrcom N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 s 0 i 1 N U i = 1 s Z i + s x i t 0 +∞ i 1 N x i = 1 t Z i + t U i
154 153 impancom N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i s 0 t 0 +∞ i 1 N x i = 1 t Z i + t U i
155 48 154 mpd N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i t 0 +∞ i 1 N x i = 1 t Z i + t U i
156 155 r19.29an N Z 𝔼 N U 𝔼 N Z U x 𝔼 N s 0 1 i 1 N U i = 1 s Z i + s x i t 0 +∞ i 1 N x i = 1 t Z i + t U i
157 13 156 syldan N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U Btwn Z x t 0 +∞ i 1 N x i = 1 t Z i + t U i
158 3simpa x 0 x x 1 x 0 x
159 elicc01 x 0 1 x 0 x x 1
160 elrege0 x 0 +∞ x 0 x
161 158 159 160 3imtr4i x 0 1 x 0 +∞
162 161 ssriv 0 1 0 +∞
163 brbtwn x 𝔼 N Z 𝔼 N U 𝔼 N x Btwn Z U t 0 1 i 1 N x i = 1 t Z i + t U i
164 10 9 8 163 syl3anc N Z 𝔼 N U 𝔼 N Z U x 𝔼 N x Btwn Z U t 0 1 i 1 N x i = 1 t Z i + t U i
165 164 biimpa N Z 𝔼 N U 𝔼 N Z U x 𝔼 N x Btwn Z U t 0 1 i 1 N x i = 1 t Z i + t U i
166 ssrexv 0 1 0 +∞ t 0 1 i 1 N x i = 1 t Z i + t U i t 0 +∞ i 1 N x i = 1 t Z i + t U i
167 162 165 166 mpsyl N Z 𝔼 N U 𝔼 N Z U x 𝔼 N x Btwn Z U t 0 +∞ i 1 N x i = 1 t Z i + t U i
168 157 167 jaodan N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U Btwn Z x x Btwn Z U t 0 +∞ i 1 N x i = 1 t Z i + t U i
169 168 anasss N Z 𝔼 N U 𝔼 N Z U x 𝔼 N U Btwn Z x x Btwn Z U t 0 +∞ i 1 N x i = 1 t Z i + t U i
170 7 169 sylan2b N Z 𝔼 N U 𝔼 N Z U x D t 0 +∞ i 1 N x i = 1 t Z i + t U i
171 r19.26 i 1 N x i = 1 t Z i + t U i x i = 1 s Z i + s U i i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i
172 eqtr2 x i = 1 t Z i + t U i x i = 1 s Z i + s U i 1 t Z i + t U i = 1 s Z i + s U i
173 172 ralimi i 1 N x i = 1 t Z i + t U i x i = 1 s Z i + s U i i 1 N 1 t Z i + t U i = 1 s Z i + s U i
174 171 173 sylbir i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i i 1 N 1 t Z i + t U i = 1 s Z i + s U i
175 elrege0 t 0 +∞ t 0 t
176 175 simplbi t 0 +∞ t
177 176 recnd t 0 +∞ t
178 elrege0 s 0 +∞ s 0 s
179 178 simplbi s 0 +∞ s
180 179 recnd s 0 +∞ s
181 177 180 anim12i t 0 +∞ s 0 +∞ t s
182 simplr N Z 𝔼 N U 𝔼 N Z U t s i 1 N t s
183 simpl2 N Z 𝔼 N U 𝔼 N Z U Z 𝔼 N
184 183 ad2antrr N Z 𝔼 N U 𝔼 N Z U t s i 1 N Z 𝔼 N
185 184 30 sylancom N Z 𝔼 N U 𝔼 N Z U t s i 1 N Z i
186 simpl3 N Z 𝔼 N U 𝔼 N Z U U 𝔼 N
187 186 ad2antrr N Z 𝔼 N U 𝔼 N Z U t s i 1 N U 𝔼 N
188 fveecn U 𝔼 N i 1 N U i
189 187 188 sylancom N Z 𝔼 N U 𝔼 N Z U t s i 1 N U i
190 subcl 1 t 1 t
191 72 190 mpan t 1 t
192 191 adantr t s 1 t
193 simpl Z i U i Z i
194 mulcl 1 t Z i 1 t Z i
195 192 193 194 syl2an t s Z i U i 1 t Z i
196 mulcl t U i t U i
197 196 ad2ant2rl t s Z i U i t U i
198 78 adantl t s 1 s
199 198 193 123 syl2an t s Z i U i 1 s Z i
200 mulcl s U i s U i
201 200 ad2ant2l t s Z i U i s U i
202 195 197 199 201 addsubeq4d t s Z i U i 1 t Z i + t U i = 1 s Z i + s U i 1 s Z i 1 t Z i = t U i s U i
203 nnncan1 1 s t 1 - s - 1 t = t s
204 72 203 mp3an1 s t 1 - s - 1 t = t s
205 204 ancoms t s 1 - s - 1 t = t s
206 205 oveq1d t s 1 - s - 1 t Z i = t s Z i
207 206 adantr t s Z i U i 1 - s - 1 t Z i = t s Z i
208 78 ad2antlr t s Z i U i 1 s
209 191 ad2antrr t s Z i U i 1 t
210 simprl t s Z i U i Z i
211 208 209 210 subdird t s Z i U i 1 - s - 1 t Z i = 1 s Z i 1 t Z i
212 207 211 eqtr3d t s Z i U i t s Z i = 1 s Z i 1 t Z i
213 simpll t s Z i U i t
214 simplr t s Z i U i s
215 simprr t s Z i U i U i
216 213 214 215 subdird t s Z i U i t s U i = t U i s U i
217 212 216 eqeq12d t s Z i U i t s Z i = t s U i 1 s Z i 1 t Z i = t U i s U i
218 subcl t s t s
219 218 adantr t s Z i U i t s
220 mulcan1g t s Z i U i t s Z i = t s U i t s = 0 Z i = U i
221 219 210 215 220 syl3anc t s Z i U i t s Z i = t s U i t s = 0 Z i = U i
222 202 217 221 3bitr2d t s Z i U i 1 t Z i + t U i = 1 s Z i + s U i t s = 0 Z i = U i
223 182 185 189 222 syl12anc N Z 𝔼 N U 𝔼 N Z U t s i 1 N 1 t Z i + t U i = 1 s Z i + s U i t s = 0 Z i = U i
224 223 ralbidva N Z 𝔼 N U 𝔼 N Z U t s i 1 N 1 t Z i + t U i = 1 s Z i + s U i i 1 N t s = 0 Z i = U i
225 r19.32v i 1 N t s = 0 Z i = U i t s = 0 i 1 N Z i = U i
226 simplr N Z 𝔼 N U 𝔼 N Z U t s Z U
227 226 neneqd N Z 𝔼 N U 𝔼 N Z U t s ¬ Z = U
228 simpll2 N Z 𝔼 N U 𝔼 N Z U t s Z 𝔼 N
229 simpll3 N Z 𝔼 N U 𝔼 N Z U t s U 𝔼 N
230 eqeefv Z 𝔼 N U 𝔼 N Z = U i 1 N Z i = U i
231 228 229 230 syl2anc N Z 𝔼 N U 𝔼 N Z U t s Z = U i 1 N Z i = U i
232 227 231 mtbid N Z 𝔼 N U 𝔼 N Z U t s ¬ i 1 N Z i = U i
233 orel2 ¬ i 1 N Z i = U i t s = 0 i 1 N Z i = U i t s = 0
234 232 233 syl N Z 𝔼 N U 𝔼 N Z U t s t s = 0 i 1 N Z i = U i t s = 0
235 subeq0 t s t s = 0 t = s
236 235 adantl N Z 𝔼 N U 𝔼 N Z U t s t s = 0 t = s
237 234 236 sylibd N Z 𝔼 N U 𝔼 N Z U t s t s = 0 i 1 N Z i = U i t = s
238 225 237 syl5bi N Z 𝔼 N U 𝔼 N Z U t s i 1 N t s = 0 Z i = U i t = s
239 224 238 sylbid N Z 𝔼 N U 𝔼 N Z U t s i 1 N 1 t Z i + t U i = 1 s Z i + s U i t = s
240 181 239 sylan2 N Z 𝔼 N U 𝔼 N Z U t 0 +∞ s 0 +∞ i 1 N 1 t Z i + t U i = 1 s Z i + s U i t = s
241 174 240 syl5 N Z 𝔼 N U 𝔼 N Z U t 0 +∞ s 0 +∞ i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i t = s
242 241 ralrimivva N Z 𝔼 N U 𝔼 N Z U t 0 +∞ s 0 +∞ i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i t = s
243 242 adantr N Z 𝔼 N U 𝔼 N Z U x D t 0 +∞ s 0 +∞ i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i t = s
244 oveq2 t = s 1 t = 1 s
245 244 oveq1d t = s 1 t Z i = 1 s Z i
246 oveq1 t = s t U i = s U i
247 245 246 oveq12d t = s 1 t Z i + t U i = 1 s Z i + s U i
248 247 eqeq2d t = s x i = 1 t Z i + t U i x i = 1 s Z i + s U i
249 248 ralbidv t = s i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i
250 249 reu4 ∃! t 0 +∞ i 1 N x i = 1 t Z i + t U i t 0 +∞ i 1 N x i = 1 t Z i + t U i t 0 +∞ s 0 +∞ i 1 N x i = 1 t Z i + t U i i 1 N x i = 1 s Z i + s U i t = s
251 170 243 250 sylanbrc N Z 𝔼 N U 𝔼 N Z U x D ∃! t 0 +∞ i 1 N x i = 1 t Z i + t U i
252 df-reu ∃! t 0 +∞ i 1 N x i = 1 t Z i + t U i ∃! t t 0 +∞ i 1 N x i = 1 t Z i + t U i
253 251 252 sylib N Z 𝔼 N U 𝔼 N Z U x D ∃! t t 0 +∞ i 1 N x i = 1 t Z i + t U i
254 253 ralrimiva N Z 𝔼 N U 𝔼 N Z U x D ∃! t t 0 +∞ i 1 N x i = 1 t Z i + t U i
255 2 fnopabg x D ∃! t t 0 +∞ i 1 N x i = 1 t Z i + t U i F Fn D
256 254 255 sylib N Z 𝔼 N U 𝔼 N Z U F Fn D
257 176 ad2antlr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N t
258 183 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N Z 𝔼 N
259 fveere Z 𝔼 N k 1 N Z k
260 258 259 sylancom N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N Z k
261 186 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N U 𝔼 N
262 fveere U 𝔼 N k 1 N U k
263 261 262 sylancom N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N U k
264 resubcl 1 t 1 t
265 58 264 mpan t 1 t
266 remulcl 1 t Z k 1 t Z k
267 265 266 sylan t Z k 1 t Z k
268 267 3adant3 t Z k U k 1 t Z k
269 remulcl t U k t U k
270 269 3adant2 t Z k U k t U k
271 268 270 readdcld t Z k U k 1 t Z k + t U k
272 257 260 263 271 syl3anc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N 1 t Z k + t U k
273 272 ralrimiva N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N 1 t Z k + t U k
274 simpll1 N Z 𝔼 N U 𝔼 N Z U t 0 +∞ N
275 mptelee N k 1 N 1 t Z k + t U k 𝔼 N k 1 N 1 t Z k + t U k
276 274 275 syl N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N 1 t Z k + t U k 𝔼 N k 1 N 1 t Z k + t U k
277 273 276 mpbird N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N 1 t Z k + t U k 𝔼 N
278 letric 1 t 1 t t 1
279 58 176 278 sylancr t 0 +∞ 1 t t 1
280 279 adantl N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t t 1
281 simpr t 0 +∞ 1 t 1 t
282 176 adantr t 0 +∞ 1 t t
283 0red t 0 +∞ 1 t 0
284 1red t 0 +∞ 1 t 1
285 0lt1 0 < 1
286 285 a1i t 0 +∞ 1 t 0 < 1
287 283 284 282 286 281 ltletrd t 0 +∞ 1 t 0 < t
288 divelunit 1 0 1 t 0 < t 1 t 0 1 1 t
289 58 59 288 mpanl12 t 0 < t 1 t 0 1 1 t
290 282 287 289 syl2anc t 0 +∞ 1 t 1 t 0 1 1 t
291 281 290 mpbird t 0 +∞ 1 t 1 t 0 1
292 291 adantll N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t 1 t 0 1
293 176 ad3antlr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N t
294 293 recnd N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N t
295 287 gt0ne0d t 0 +∞ 1 t t 0
296 295 adantll N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t t 0
297 296 adantr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N t 0
298 183 ad3antrrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N Z 𝔼 N
299 298 30 sylancom N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N Z i
300 186 ad3antrrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N U 𝔼 N
301 300 188 sylancom N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N U i
302 reccl t t 0 1 t
303 302 adantr t t 0 Z i U i 1 t
304 191 adantr t t 0 1 t
305 304 193 194 syl2an t t 0 Z i U i 1 t Z i
306 196 ad2ant2rl t t 0 Z i U i t U i
307 303 305 306 adddid t t 0 Z i U i 1 t 1 t Z i + t U i = 1 t 1 t Z i + 1 t t U i
308 307 oveq2d t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i + t U i = 1 1 t Z i + 1 t 1 t Z i + 1 t t U i
309 subcl 1 1 t 1 1 t
310 72 302 309 sylancr t t 0 1 1 t
311 mulcl 1 1 t Z i 1 1 t Z i
312 310 193 311 syl2an t t 0 Z i U i 1 1 t Z i
313 303 305 mulcld t t 0 Z i U i 1 t 1 t Z i
314 recid2 t t 0 1 t t = 1
315 314 oveq1d t t 0 1 t t U i = 1 U i
316 315 adantr t t 0 Z i U i 1 t t U i = 1 U i
317 simpll t t 0 Z i U i t
318 simprr t t 0 Z i U i U i
319 303 317 318 mulassd t t 0 Z i U i 1 t t U i = 1 t t U i
320 mulid2 U i 1 U i = U i
321 320 ad2antll t t 0 Z i U i 1 U i = U i
322 316 319 321 3eqtr3d t t 0 Z i U i 1 t t U i = U i
323 322 318 eqeltrd t t 0 Z i U i 1 t t U i
324 312 313 323 addassd t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i + 1 t t U i = 1 1 t Z i + 1 t 1 t Z i + 1 t t U i
325 310 adantr t t 0 Z i U i 1 1 t
326 302 304 mulcld t t 0 1 t 1 t
327 326 adantr t t 0 Z i U i 1 t 1 t
328 simprl t t 0 Z i U i Z i
329 325 327 328 adddird t t 0 Z i U i 1 - 1 t + 1 t 1 t Z i = 1 1 t Z i + 1 t 1 t Z i
330 simpl t t 0 t
331 subdi 1 t 1 t 1 t 1 t = 1 t 1 1 t t
332 72 331 mp3an2 1 t t 1 t 1 t = 1 t 1 1 t t
333 302 330 332 syl2anc t t 0 1 t 1 t = 1 t 1 1 t t
334 302 mulid1d t t 0 1 t 1 = 1 t
335 334 314 oveq12d t t 0 1 t 1 1 t t = 1 t 1
336 333 335 eqtrd t t 0 1 t 1 t = 1 t 1
337 336 oveq2d t t 0 1 - 1 t + 1 t 1 t = 1 1 t + 1 t - 1
338 npncan2 1 1 t 1 1 t + 1 t - 1 = 0
339 72 302 338 sylancr t t 0 1 1 t + 1 t - 1 = 0
340 337 339 eqtrd t t 0 1 - 1 t + 1 t 1 t = 0
341 340 adantr t t 0 Z i U i 1 - 1 t + 1 t 1 t = 0
342 341 oveq1d t t 0 Z i U i 1 - 1 t + 1 t 1 t Z i = 0 Z i
343 109 ad2antrl t t 0 Z i U i 0 Z i = 0
344 342 343 eqtrd t t 0 Z i U i 1 - 1 t + 1 t 1 t Z i = 0
345 191 ad2antrr t t 0 Z i U i 1 t
346 303 345 328 mulassd t t 0 Z i U i 1 t 1 t Z i = 1 t 1 t Z i
347 346 oveq2d t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i = 1 1 t Z i + 1 t 1 t Z i
348 329 344 347 3eqtr3rd t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i = 0
349 348 322 oveq12d t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i + 1 t t U i = 0 + U i
350 addid2 U i 0 + U i = U i
351 350 ad2antll t t 0 Z i U i 0 + U i = U i
352 349 351 eqtrd t t 0 Z i U i 1 1 t Z i + 1 t 1 t Z i + 1 t t U i = U i
353 308 324 352 3eqtr2rd t t 0 Z i U i U i = 1 1 t Z i + 1 t 1 t Z i + t U i
354 294 297 299 301 353 syl22anc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N U i = 1 1 t Z i + 1 t 1 t Z i + t U i
355 354 ralrimiva N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t i 1 N U i = 1 1 t Z i + 1 t 1 t Z i + t U i
356 oveq2 s = 1 t 1 s = 1 1 t
357 356 oveq1d s = 1 t 1 s Z i = 1 1 t Z i
358 oveq1 s = 1 t s k 1 N 1 t Z k + t U k i = 1 t k 1 N 1 t Z k + t U k i
359 357 358 oveq12d s = 1 t 1 s Z i + s k 1 N 1 t Z k + t U k i = 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i
360 359 eqeq2d s = 1 t U i = 1 s Z i + s k 1 N 1 t Z k + t U k i U i = 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i
361 360 ralbidv s = 1 t i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i i 1 N U i = 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i
362 fveq2 k = i Z k = Z i
363 362 oveq2d k = i 1 t Z k = 1 t Z i
364 fveq2 k = i U k = U i
365 364 oveq2d k = i t U k = t U i
366 363 365 oveq12d k = i 1 t Z k + t U k = 1 t Z i + t U i
367 eqid k 1 N 1 t Z k + t U k = k 1 N 1 t Z k + t U k
368 ovex 1 t Z i + t U i V
369 366 367 368 fvmpt i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
370 369 oveq2d i 1 N 1 t k 1 N 1 t Z k + t U k i = 1 t 1 t Z i + t U i
371 370 oveq2d i 1 N 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i = 1 1 t Z i + 1 t 1 t Z i + t U i
372 371 eqeq2d i 1 N U i = 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i U i = 1 1 t Z i + 1 t 1 t Z i + t U i
373 372 ralbiia i 1 N U i = 1 1 t Z i + 1 t k 1 N 1 t Z k + t U k i i 1 N U i = 1 1 t Z i + 1 t 1 t Z i + t U i
374 361 373 bitrdi s = 1 t i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i i 1 N U i = 1 1 t Z i + 1 t 1 t Z i + t U i
375 374 rspcev 1 t 0 1 i 1 N U i = 1 1 t Z i + 1 t 1 t Z i + t U i s 0 1 i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i
376 292 355 375 syl2anc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t s 0 1 i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i
377 186 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t U 𝔼 N
378 183 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t Z 𝔼 N
379 277 adantr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t k 1 N 1 t Z k + t U k 𝔼 N
380 brbtwn U 𝔼 N Z 𝔼 N k 1 N 1 t Z k + t U k 𝔼 N U Btwn Z k 1 N 1 t Z k + t U k s 0 1 i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i
381 377 378 379 380 syl3anc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t U Btwn Z k 1 N 1 t Z k + t U k s 0 1 i 1 N U i = 1 s Z i + s k 1 N 1 t Z k + t U k i
382 376 381 mpbird N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t U Btwn Z k 1 N 1 t Z k + t U k
383 382 ex N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t U Btwn Z k 1 N 1 t Z k + t U k
384 simpll t 0 t t 1 t
385 simplr t 0 t t 1 0 t
386 simpr t 0 t t 1 t 1
387 384 385 386 3jca t 0 t t 1 t 0 t t 1
388 175 anbi1i t 0 +∞ t 1 t 0 t t 1
389 elicc01 t 0 1 t 0 t t 1
390 387 388 389 3imtr4i t 0 +∞ t 1 t 0 1
391 390 adantll N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 t 0 1
392 369 rgen i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
393 oveq2 s = t 1 s = 1 t
394 393 oveq1d s = t 1 s Z i = 1 t Z i
395 oveq1 s = t s U i = t U i
396 394 395 oveq12d s = t 1 s Z i + s U i = 1 t Z i + t U i
397 396 eqeq2d s = t k 1 N 1 t Z k + t U k i = 1 s Z i + s U i k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
398 397 ralbidv s = t i 1 N k 1 N 1 t Z k + t U k i = 1 s Z i + s U i i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
399 398 rspcev t 0 1 i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i s 0 1 i 1 N k 1 N 1 t Z k + t U k i = 1 s Z i + s U i
400 391 392 399 sylancl N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 s 0 1 i 1 N k 1 N 1 t Z k + t U k i = 1 s Z i + s U i
401 277 adantr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 k 1 N 1 t Z k + t U k 𝔼 N
402 183 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 Z 𝔼 N
403 186 ad2antrr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 U 𝔼 N
404 brbtwn k 1 N 1 t Z k + t U k 𝔼 N Z 𝔼 N U 𝔼 N k 1 N 1 t Z k + t U k Btwn Z U s 0 1 i 1 N k 1 N 1 t Z k + t U k i = 1 s Z i + s U i
405 401 402 403 404 syl3anc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 k 1 N 1 t Z k + t U k Btwn Z U s 0 1 i 1 N k 1 N 1 t Z k + t U k i = 1 s Z i + s U i
406 400 405 mpbird N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 k 1 N 1 t Z k + t U k Btwn Z U
407 406 ex N Z 𝔼 N U 𝔼 N Z U t 0 +∞ t 1 k 1 N 1 t Z k + t U k Btwn Z U
408 383 407 orim12d N Z 𝔼 N U 𝔼 N Z U t 0 +∞ 1 t t 1 U Btwn Z k 1 N 1 t Z k + t U k k 1 N 1 t Z k + t U k Btwn Z U
409 280 408 mpd N Z 𝔼 N U 𝔼 N Z U t 0 +∞ U Btwn Z k 1 N 1 t Z k + t U k k 1 N 1 t Z k + t U k Btwn Z U
410 opeq2 p = k 1 N 1 t Z k + t U k Z p = Z k 1 N 1 t Z k + t U k
411 410 breq2d p = k 1 N 1 t Z k + t U k U Btwn Z p U Btwn Z k 1 N 1 t Z k + t U k
412 breq1 p = k 1 N 1 t Z k + t U k p Btwn Z U k 1 N 1 t Z k + t U k Btwn Z U
413 411 412 orbi12d p = k 1 N 1 t Z k + t U k U Btwn Z p p Btwn Z U U Btwn Z k 1 N 1 t Z k + t U k k 1 N 1 t Z k + t U k Btwn Z U
414 413 1 elrab2 k 1 N 1 t Z k + t U k D k 1 N 1 t Z k + t U k 𝔼 N U Btwn Z k 1 N 1 t Z k + t U k k 1 N 1 t Z k + t U k Btwn Z U
415 277 409 414 sylanbrc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ k 1 N 1 t Z k + t U k D
416 fveq1 x = k 1 N 1 t Z k + t U k x i = k 1 N 1 t Z k + t U k i
417 416 eqeq1d x = k 1 N 1 t Z k + t U k x i = 1 t Z i + t U i k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
418 417 ralbidv x = k 1 N 1 t Z k + t U k i 1 N x i = 1 t Z i + t U i i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i
419 418 rspcev k 1 N 1 t Z k + t U k D i 1 N k 1 N 1 t Z k + t U k i = 1 t Z i + t U i x D i 1 N x i = 1 t Z i + t U i
420 415 392 419 sylancl N Z 𝔼 N U 𝔼 N Z U t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
421 7 simplbi x D x 𝔼 N
422 1 ssrab3 D 𝔼 N
423 422 sseli y D y 𝔼 N
424 421 423 anim12i x D y D x 𝔼 N y 𝔼 N
425 r19.26 i 1 N x i = 1 t Z i + t U i y i = 1 t Z i + t U i i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i
426 eqtr3 x i = 1 t Z i + t U i y i = 1 t Z i + t U i x i = y i
427 426 ralimi i 1 N x i = 1 t Z i + t U i y i = 1 t Z i + t U i i 1 N x i = y i
428 425 427 sylbir i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i i 1 N x i = y i
429 eqeefv x 𝔼 N y 𝔼 N x = y i 1 N x i = y i
430 429 adantl N Z 𝔼 N U 𝔼 N Z U x 𝔼 N y 𝔼 N x = y i 1 N x i = y i
431 428 430 syl5ibr N Z 𝔼 N U 𝔼 N Z U x 𝔼 N y 𝔼 N i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
432 424 431 sylan2 N Z 𝔼 N U 𝔼 N Z U x D y D i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
433 432 ralrimivva N Z 𝔼 N U 𝔼 N Z U x D y D i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
434 433 adantr N Z 𝔼 N U 𝔼 N Z U t 0 +∞ x D y D i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
435 df-reu ∃! x D i 1 N x i = 1 t Z i + t U i ∃! x x D i 1 N x i = 1 t Z i + t U i
436 fveq1 x = y x i = y i
437 436 eqeq1d x = y x i = 1 t Z i + t U i y i = 1 t Z i + t U i
438 437 ralbidv x = y i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i
439 438 reu4 ∃! x D i 1 N x i = 1 t Z i + t U i x D i 1 N x i = 1 t Z i + t U i x D y D i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
440 435 439 bitr3i ∃! x x D i 1 N x i = 1 t Z i + t U i x D i 1 N x i = 1 t Z i + t U i x D y D i 1 N x i = 1 t Z i + t U i i 1 N y i = 1 t Z i + t U i x = y
441 420 434 440 sylanbrc N Z 𝔼 N U 𝔼 N Z U t 0 +∞ ∃! x x D i 1 N x i = 1 t Z i + t U i
442 441 ralrimiva N Z 𝔼 N U 𝔼 N Z U t 0 +∞ ∃! x x D i 1 N x i = 1 t Z i + t U i
443 an12 x D t 0 +∞ i 1 N x i = 1 t Z i + t U i t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
444 443 opabbii x t | x D t 0 +∞ i 1 N x i = 1 t Z i + t U i = x t | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
445 2 444 eqtri F = x t | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
446 445 cnveqi F -1 = x t | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i -1
447 cnvopab x t | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i -1 = t x | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
448 446 447 eqtri F -1 = t x | t 0 +∞ x D i 1 N x i = 1 t Z i + t U i
449 448 fnopabg t 0 +∞ ∃! x x D i 1 N x i = 1 t Z i + t U i F -1 Fn 0 +∞
450 442 449 sylib N Z 𝔼 N U 𝔼 N Z U F -1 Fn 0 +∞
451 dff1o4 F : D 1-1 onto 0 +∞ F Fn D F -1 Fn 0 +∞
452 256 450 451 sylanbrc N Z 𝔼 N U 𝔼 N Z U F : D 1-1 onto 0 +∞