Metamath Proof Explorer


Theorem axcontlem4

Description: Lemma for axcont . Given the separation assumption, A is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem4.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
Assertion axcontlem4 N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U A D

Proof

Step Hyp Ref Expression
1 axcontlem4.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
2 simplr1 N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U A 𝔼 N
3 n0 B b b B
4 idd b B A 𝔼 N A 𝔼 N
5 ssel B 𝔼 N b B b 𝔼 N
6 5 com12 b B B 𝔼 N b 𝔼 N
7 opeq2 y = b Z y = Z b
8 7 breq2d y = b x Btwn Z y x Btwn Z b
9 8 rspcv b B y B x Btwn Z y x Btwn Z b
10 9 ralimdv b B x A y B x Btwn Z y x A x Btwn Z b
11 4 6 10 3anim123d b B A 𝔼 N B 𝔼 N x A y B x Btwn Z y A 𝔼 N b 𝔼 N x A x Btwn Z b
12 11 anim2d b B N A 𝔼 N B 𝔼 N x A y B x Btwn Z y N A 𝔼 N b 𝔼 N x A x Btwn Z b
13 simplr1 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U A 𝔼 N
14 13 adantr N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A A 𝔼 N
15 simplr2 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U A
16 14 15 sseldd N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U 𝔼 N
17 simpr3 N A 𝔼 N b 𝔼 N x A x Btwn Z b x A x Btwn Z b
18 simp2 Z 𝔼 N U A Z U U A
19 breq1 x = U x Btwn Z b U Btwn Z b
20 19 rspccva x A x Btwn Z b U A U Btwn Z b
21 17 18 20 syl2an N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U U Btwn Z b
22 21 adantr N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U Btwn Z b
23 16 22 jca N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U 𝔼 N U Btwn Z b
24 13 sselda N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A p 𝔼 N
25 17 adantr N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U x A x Btwn Z b
26 breq1 x = p x Btwn Z b p Btwn Z b
27 26 rspccva x A x Btwn Z b p A p Btwn Z b
28 25 27 sylan N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A p Btwn Z b
29 23 24 28 jca32 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U 𝔼 N U Btwn Z b p 𝔼 N p Btwn Z b
30 an4 U 𝔼 N U Btwn Z b p 𝔼 N p Btwn Z b U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b
31 29 30 sylib N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b
32 simp2 A 𝔼 N b 𝔼 N x A x Btwn Z b b 𝔼 N
33 simpl2r N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 Z U
34 33 adantr N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i Z U
35 simpl U i = 1 t Z i + t b i p i = 1 s Z i + s b i U i = 1 t Z i + t b i
36 35 ralimi i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N U i = 1 t Z i + t b i
37 eqcom U i = 1 t Z i + t b i 1 t Z i + t b i = U i
38 oveq2 t = 0 1 t = 1 0
39 1m0e1 1 0 = 1
40 38 39 eqtrdi t = 0 1 t = 1
41 40 oveq1d t = 0 1 t Z i = 1 Z i
42 oveq1 t = 0 t b i = 0 b i
43 41 42 oveq12d t = 0 1 t Z i + t b i = 1 Z i + 0 b i
44 43 eqeq1d t = 0 1 t Z i + t b i = U i 1 Z i + 0 b i = U i
45 37 44 syl5bb t = 0 U i = 1 t Z i + t b i 1 Z i + 0 b i = U i
46 45 ralbidv t = 0 i 1 N U i = 1 t Z i + t b i i 1 N 1 Z i + 0 b i = U i
47 46 biimpac i 1 N U i = 1 t Z i + t b i t = 0 i 1 N 1 Z i + 0 b i = U i
48 simpl2l N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 Z 𝔼 N
49 simpl3l N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 U 𝔼 N
50 eqeefv Z 𝔼 N U 𝔼 N Z = U i 1 N Z i = U i
51 48 49 50 syl2anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 Z = U i 1 N Z i = U i
52 fveecn Z 𝔼 N i 1 N Z i
53 48 52 sylan N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N Z i
54 simp1r N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N b 𝔼 N
55 54 ad2antrr N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N b 𝔼 N
56 fveecn b 𝔼 N i 1 N b i
57 55 56 sylancom N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N b i
58 mulid2 Z i 1 Z i = Z i
59 mul02 b i 0 b i = 0
60 58 59 oveqan12d Z i b i 1 Z i + 0 b i = Z i + 0
61 addid1 Z i Z i + 0 = Z i
62 61 adantr Z i b i Z i + 0 = Z i
63 60 62 eqtrd Z i b i 1 Z i + 0 b i = Z i
64 53 57 63 syl2anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N 1 Z i + 0 b i = Z i
65 64 eqeq1d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N 1 Z i + 0 b i = U i Z i = U i
66 65 ralbidva N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N 1 Z i + 0 b i = U i i 1 N Z i = U i
67 51 66 bitr4d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 Z = U i 1 N 1 Z i + 0 b i = U i
68 47 67 syl5ibr N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i t = 0 Z = U
69 68 expdimp N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i t = 0 Z = U
70 36 69 sylan2 N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t = 0 Z = U
71 70 necon3d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i Z U t 0
72 34 71 mpd N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0
73 simp1l N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N N
74 simp2l N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N Z 𝔼 N
75 73 74 54 3jca N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N N Z 𝔼 N b 𝔼 N
76 simp2l N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t 0 1
77 elicc01 t 0 1 t 0 t t 1
78 77 simp1bi t 0 1 t
79 76 78 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t
80 simp2r N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s 0 1
81 elicc01 s 0 1 s 0 s s 1
82 81 simp1bi s 0 1 s
83 80 82 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s
84 79 83 letrid N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s s t
85 simpr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s t s
86 79 adantr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s t
87 77 simp2bi t 0 1 0 t
88 76 87 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 0 t
89 88 adantr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s 0 t
90 83 adantr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s s
91 0red N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s 0
92 simp3 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t 0
93 79 88 92 ne0gt0d N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 0 < t
94 93 adantr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s 0 < t
95 91 86 90 94 85 ltletrd N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s 0 < s
96 divelunit t 0 t s 0 < s t s 0 1 t s
97 86 89 90 95 96 syl22anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s t s 0 1 t s
98 85 97 mpbird N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s t s 0 1
99 simp12 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 Z 𝔼 N
100 99 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N Z 𝔼 N
101 100 52 sylancom N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N Z i
102 simp13 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 b 𝔼 N
103 102 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N b 𝔼 N
104 103 56 sylancom N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N b i
105 78 recnd t 0 1 t
106 76 105 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t
107 106 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N t
108 82 recnd s 0 1 s
109 80 108 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s
110 109 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N s
111 0red N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 0
112 79 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N t
113 83 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N s
114 88 ad2antrr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 0 t
115 simpll3 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N t 0
116 112 114 115 ne0gt0d N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 0 < t
117 simplr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N t s
118 111 112 113 116 117 ltletrd N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 0 < s
119 118 gt0ne0d N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N s 0
120 divcl t s s 0 t s
121 120 adantl Z i b i t s s 0 t s
122 ax-1cn 1
123 simpr2 Z i b i t s s 0 s
124 subcl 1 s 1 s
125 122 123 124 sylancr Z i b i t s s 0 1 s
126 simpll Z i b i t s s 0 Z i
127 125 126 mulcld Z i b i t s s 0 1 s Z i
128 simplr Z i b i t s s 0 b i
129 123 128 mulcld Z i b i t s s 0 s b i
130 121 127 129 adddid Z i b i t s s 0 t s 1 s Z i + s b i = t s 1 s Z i + t s s b i
131 130 oveq2d Z i b i t s s 0 1 t s Z i + t s 1 s Z i + s b i = 1 t s Z i + t s 1 s Z i + t s s b i
132 subcl 1 t s 1 t s
133 122 121 132 sylancr Z i b i t s s 0 1 t s
134 133 126 mulcld Z i b i t s s 0 1 t s Z i
135 121 127 mulcld Z i b i t s s 0 t s 1 s Z i
136 121 129 mulcld Z i b i t s s 0 t s s b i
137 134 135 136 addassd Z i b i t s s 0 1 t s Z i + t s 1 s Z i + t s s b i = 1 t s Z i + t s 1 s Z i + t s s b i
138 121 125 mulcld Z i b i t s s 0 t s 1 s
139 133 138 126 adddird Z i b i t s s 0 1 - t s + t s 1 s Z i = 1 t s Z i + t s 1 s Z i
140 simp2 t s s 0 s
141 subdi t s 1 s t s 1 s = t s 1 t s s
142 122 141 mp3an2 t s s t s 1 s = t s 1 t s s
143 120 140 142 syl2anc t s s 0 t s 1 s = t s 1 t s s
144 120 mulid1d t s s 0 t s 1 = t s
145 divcan1 t s s 0 t s s = t
146 144 145 oveq12d t s s 0 t s 1 t s s = t s t
147 143 146 eqtrd t s s 0 t s 1 s = t s t
148 147 oveq2d t s s 0 1 - t s + t s 1 s = 1 t s + t s - t
149 simp1 t s s 0 t
150 npncan 1 t s t 1 t s + t s - t = 1 t
151 122 120 149 150 mp3an2i t s s 0 1 t s + t s - t = 1 t
152 148 151 eqtrd t s s 0 1 - t s + t s 1 s = 1 t
153 152 adantl Z i b i t s s 0 1 - t s + t s 1 s = 1 t
154 153 oveq1d Z i b i t s s 0 1 - t s + t s 1 s Z i = 1 t Z i
155 121 125 126 mulassd Z i b i t s s 0 t s 1 s Z i = t s 1 s Z i
156 155 oveq2d Z i b i t s s 0 1 t s Z i + t s 1 s Z i = 1 t s Z i + t s 1 s Z i
157 139 154 156 3eqtr3rd Z i b i t s s 0 1 t s Z i + t s 1 s Z i = 1 t Z i
158 121 123 128 mulassd Z i b i t s s 0 t s s b i = t s s b i
159 145 adantl Z i b i t s s 0 t s s = t
160 159 oveq1d Z i b i t s s 0 t s s b i = t b i
161 158 160 eqtr3d Z i b i t s s 0 t s s b i = t b i
162 157 161 oveq12d Z i b i t s s 0 1 t s Z i + t s 1 s Z i + t s s b i = 1 t Z i + t b i
163 131 137 162 3eqtr2rd Z i b i t s s 0 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i
164 101 104 107 110 119 163 syl23anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i
165 164 ralrimiva N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s i 1 N 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i
166 oveq2 r = t s 1 r = 1 t s
167 166 oveq1d r = t s 1 r Z i = 1 t s Z i
168 oveq1 r = t s r 1 s Z i + s b i = t s 1 s Z i + s b i
169 167 168 oveq12d r = t s 1 r Z i + r 1 s Z i + s b i = 1 t s Z i + t s 1 s Z i + s b i
170 169 eqeq2d r = t s 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i
171 170 ralbidv r = t s i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i
172 171 rspcev t s 0 1 i 1 N 1 t Z i + t b i = 1 t s Z i + t s 1 s Z i + s b i r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
173 98 165 172 syl2anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
174 173 ex N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
175 81 simp2bi s 0 1 0 s
176 80 175 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 0 s
177 divelunit s 0 s t 0 < t s t 0 1 s t
178 83 176 79 93 177 syl22anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t 0 1 s t
179 178 biimpar N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t s t 0 1
180 simp112 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N Z 𝔼 N
181 simp3 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N i 1 N
182 180 181 52 syl2anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N Z i
183 simp113 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N b 𝔼 N
184 183 181 56 syl2anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N b i
185 simp12r N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N s 0 1
186 185 108 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N s
187 simp12l N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N t 0 1
188 187 105 syl N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N t
189 simp13 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N t 0
190 divcl s t t 0 s t
191 190 adantl Z i b i s t t 0 s t
192 simpr2 Z i b i s t t 0 t
193 subcl 1 t 1 t
194 122 192 193 sylancr Z i b i s t t 0 1 t
195 simpll Z i b i s t t 0 Z i
196 194 195 mulcld Z i b i s t t 0 1 t Z i
197 simplr Z i b i s t t 0 b i
198 192 197 mulcld Z i b i s t t 0 t b i
199 191 196 198 adddid Z i b i s t t 0 s t 1 t Z i + t b i = s t 1 t Z i + s t t b i
200 199 oveq2d Z i b i s t t 0 1 s t Z i + s t 1 t Z i + t b i = 1 s t Z i + s t 1 t Z i + s t t b i
201 subcl 1 s t 1 s t
202 122 191 201 sylancr Z i b i s t t 0 1 s t
203 202 195 mulcld Z i b i s t t 0 1 s t Z i
204 191 196 mulcld Z i b i s t t 0 s t 1 t Z i
205 191 198 mulcld Z i b i s t t 0 s t t b i
206 203 204 205 addassd Z i b i s t t 0 1 s t Z i + s t 1 t Z i + s t t b i = 1 s t Z i + s t 1 t Z i + s t t b i
207 simp2 s t t 0 t
208 subdi s t 1 t s t 1 t = s t 1 s t t
209 122 208 mp3an2 s t t s t 1 t = s t 1 s t t
210 190 207 209 syl2anc s t t 0 s t 1 t = s t 1 s t t
211 190 mulid1d s t t 0 s t 1 = s t
212 divcan1 s t t 0 s t t = s
213 211 212 oveq12d s t t 0 s t 1 s t t = s t s
214 210 213 eqtrd s t t 0 s t 1 t = s t s
215 214 oveq2d s t t 0 1 - s t + s t 1 t = 1 s t + s t - s
216 simp1 s t t 0 s
217 npncan 1 s t s 1 s t + s t - s = 1 s
218 122 190 216 217 mp3an2i s t t 0 1 s t + s t - s = 1 s
219 215 218 eqtr2d s t t 0 1 s = 1 - s t + s t 1 t
220 219 oveq1d s t t 0 1 s Z i = 1 - s t + s t 1 t Z i
221 220 adantl Z i b i s t t 0 1 s Z i = 1 - s t + s t 1 t Z i
222 191 194 mulcld Z i b i s t t 0 s t 1 t
223 202 222 195 adddird Z i b i s t t 0 1 - s t + s t 1 t Z i = 1 s t Z i + s t 1 t Z i
224 191 194 195 mulassd Z i b i s t t 0 s t 1 t Z i = s t 1 t Z i
225 224 oveq2d Z i b i s t t 0 1 s t Z i + s t 1 t Z i = 1 s t Z i + s t 1 t Z i
226 221 223 225 3eqtrrd Z i b i s t t 0 1 s t Z i + s t 1 t Z i = 1 s Z i
227 191 192 197 mulassd Z i b i s t t 0 s t t b i = s t t b i
228 212 oveq1d s t t 0 s t t b i = s b i
229 228 adantl Z i b i s t t 0 s t t b i = s b i
230 227 229 eqtr3d Z i b i s t t 0 s t t b i = s b i
231 226 230 oveq12d Z i b i s t t 0 1 s t Z i + s t 1 t Z i + s t t b i = 1 s Z i + s b i
232 200 206 231 3eqtr2rd Z i b i s t t 0 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
233 182 184 186 188 189 232 syl23anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
234 233 3expa N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
235 234 ralrimiva N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t i 1 N 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
236 oveq2 r = s t 1 r = 1 s t
237 236 oveq1d r = s t 1 r Z i = 1 s t Z i
238 oveq1 r = s t r 1 t Z i + t b i = s t 1 t Z i + t b i
239 237 238 oveq12d r = s t 1 r Z i + r 1 t Z i + t b i = 1 s t Z i + s t 1 t Z i + t b i
240 239 eqeq2d r = s t 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
241 240 ralbidv r = s t i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i i 1 N 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i
242 241 rspcev s t 0 1 i 1 N 1 s Z i + s b i = 1 s t Z i + s t 1 t Z i + t b i r 0 1 i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
243 179 235 242 syl2anc N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t r 0 1 i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
244 243 ex N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 s t r 0 1 i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
245 174 244 orim12d N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s s t r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i r 0 1 i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
246 r19.43 r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i r 0 1 i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
247 245 246 syl6ibr N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 t s s t r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
248 84 247 mpd N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
249 id U i = 1 t Z i + t b i U i = 1 t Z i + t b i
250 oveq2 p i = 1 s Z i + s b i r p i = r 1 s Z i + s b i
251 250 oveq2d p i = 1 s Z i + s b i 1 r Z i + r p i = 1 r Z i + r 1 s Z i + s b i
252 249 251 eqeqan12d U i = 1 t Z i + t b i p i = 1 s Z i + s b i U i = 1 r Z i + r p i 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
253 252 ralimi i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N U i = 1 r Z i + r p i 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
254 ralbi i 1 N U i = 1 r Z i + r p i 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N U i = 1 r Z i + r p i i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
255 253 254 syl i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N U i = 1 r Z i + r p i i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i
256 id p i = 1 s Z i + s b i p i = 1 s Z i + s b i
257 oveq2 U i = 1 t Z i + t b i r U i = r 1 t Z i + t b i
258 257 oveq2d U i = 1 t Z i + t b i 1 r Z i + r U i = 1 r Z i + r 1 t Z i + t b i
259 256 258 eqeqan12rd U i = 1 t Z i + t b i p i = 1 s Z i + s b i p i = 1 r Z i + r U i 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
260 259 ralimi i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N p i = 1 r Z i + r U i 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
261 ralbi i 1 N p i = 1 r Z i + r U i 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i i 1 N p i = 1 r Z i + r U i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
262 260 261 syl i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N p i = 1 r Z i + r U i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
263 255 262 orbi12d i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
264 263 rexbidv i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i r 0 1 i 1 N 1 t Z i + t b i = 1 r Z i + r 1 s Z i + s b i i 1 N 1 s Z i + s b i = 1 r Z i + r 1 t Z i + t b i
265 248 264 syl5ibrcom N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
266 265 3expia N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 t 0 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
267 266 com23 N Z 𝔼 N b 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0 r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
268 75 267 sylan N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0 r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
269 268 imp N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0 r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
270 72 269 mpd N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
271 270 ex N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
272 271 rexlimdvva N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
273 simp3l N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U 𝔼 N
274 brbtwn U 𝔼 N Z 𝔼 N b 𝔼 N U Btwn Z b t 0 1 i 1 N U i = 1 t Z i + t b i
275 273 74 54 274 syl3anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b t 0 1 i 1 N U i = 1 t Z i + t b i
276 simp3r N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N p 𝔼 N
277 brbtwn p 𝔼 N Z 𝔼 N b 𝔼 N p Btwn Z b s 0 1 i 1 N p i = 1 s Z i + s b i
278 276 74 54 277 syl3anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N p Btwn Z b s 0 1 i 1 N p i = 1 s Z i + s b i
279 275 278 anbi12d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b t 0 1 i 1 N U i = 1 t Z i + t b i s 0 1 i 1 N p i = 1 s Z i + s b i
280 r19.26 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i i 1 N U i = 1 t Z i + t b i i 1 N p i = 1 s Z i + s b i
281 280 2rexbii t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i i 1 N p i = 1 s Z i + s b i
282 reeanv t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i i 1 N p i = 1 s Z i + s b i t 0 1 i 1 N U i = 1 t Z i + t b i s 0 1 i 1 N p i = 1 s Z i + s b i
283 281 282 bitri t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i t 0 1 i 1 N U i = 1 t Z i + t b i s 0 1 i 1 N p i = 1 s Z i + s b i
284 279 283 bitr4di N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b t 0 1 s 0 1 i 1 N U i = 1 t Z i + t b i p i = 1 s Z i + s b i
285 brbtwn U 𝔼 N Z 𝔼 N p 𝔼 N U Btwn Z p r 0 1 i 1 N U i = 1 r Z i + r p i
286 273 74 276 285 syl3anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z p r 0 1 i 1 N U i = 1 r Z i + r p i
287 brbtwn p 𝔼 N Z 𝔼 N U 𝔼 N p Btwn Z U r 0 1 i 1 N p i = 1 r Z i + r U i
288 276 74 273 287 syl3anc N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N p Btwn Z U r 0 1 i 1 N p i = 1 r Z i + r U i
289 286 288 orbi12d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z p p Btwn Z U r 0 1 i 1 N U i = 1 r Z i + r p i r 0 1 i 1 N p i = 1 r Z i + r U i
290 r19.43 r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i r 0 1 i 1 N U i = 1 r Z i + r p i r 0 1 i 1 N p i = 1 r Z i + r U i
291 289 290 bitr4di N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z p p Btwn Z U r 0 1 i 1 N U i = 1 r Z i + r p i i 1 N p i = 1 r Z i + r U i
292 272 284 291 3imtr4d N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
293 292 3expia N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
294 293 impd N b 𝔼 N Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
295 32 294 sylanl2 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
296 295 3adantr2 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
297 296 adantr N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U 𝔼 N p 𝔼 N U Btwn Z b p Btwn Z b U Btwn Z p p Btwn Z U
298 31 297 mpd N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
299 298 ralrimiva N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
300 299 3exp2 N A 𝔼 N b 𝔼 N x A x Btwn Z b Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
301 12 300 syl6 b B N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
302 301 exlimiv b b B N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
303 3 302 sylbi B N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A Z U p A U Btwn Z p p Btwn Z U
304 303 com4l N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U p A U Btwn Z p p Btwn Z U
305 304 3impd N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U p A U Btwn Z p p Btwn Z U
306 305 imp32 N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U p A U Btwn Z p p Btwn Z U
307 1 sseq2i A D A p 𝔼 N | U Btwn Z p p Btwn Z U
308 ssrab A p 𝔼 N | U Btwn Z p p Btwn Z U A 𝔼 N p A U Btwn Z p p Btwn Z U
309 307 308 bitri A D A 𝔼 N p A U Btwn Z p p Btwn Z U
310 2 306 309 sylanbrc N A 𝔼 N B 𝔼 N x A y B x Btwn Z y Z 𝔼 N U A B Z U A D