Metamath Proof Explorer


Theorem mulsuniflem

Description: Lemma for mulsunif . State the theorem with some extra distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses mulsuniflem.1 φ L s R
mulsuniflem.2 φ M s S
mulsuniflem.3 φ A = L | s R
mulsuniflem.4 φ B = M | s S
Assertion mulsuniflem φ A s B = a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w

Proof

Step Hyp Ref Expression
1 mulsuniflem.1 φ L s R
2 mulsuniflem.2 φ M s S
3 mulsuniflem.3 φ A = L | s R
4 mulsuniflem.4 φ B = M | s S
5 1 cutscld φ L | s R No
6 3 5 eqeltrd φ A No
7 2 cutscld φ M | s S No
8 4 7 eqeltrd φ B No
9 mulsval A No B No A s B = e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y
10 6 8 9 syl2anc φ A s B = e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y
11 6 8 mulcut2 φ e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y
12 1 3 cofcutr1d φ f L A p L f s p
13 2 4 cofcutr1d φ g L B q M g s q
14 13 adantr φ f L A p L f s p g L B q M g s q
15 reeanv p L q M f s p g s q p L f s p q M g s q
16 simprl φ f L A g L B f L A
17 16 leftnod φ f L A g L B f No
18 17 adantrr φ f L A g L B p L q M f No
19 8 adantr φ f L A g L B p L q M B No
20 18 19 mulscld φ f L A g L B p L q M f s B No
21 6 adantr φ f L A g L B p L q M A No
22 simprr φ f L A g L B g L B
23 22 leftnod φ f L A g L B g No
24 23 adantrr φ f L A g L B p L q M g No
25 21 24 mulscld φ f L A g L B p L q M A s g No
26 20 25 addscld φ f L A g L B p L q M f s B + s A s g No
27 18 24 mulscld φ f L A g L B p L q M f s g No
28 26 27 subscld φ f L A g L B p L q M f s B + s A s g - s f s g No
29 28 adantrrr φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g No
30 sltsss1 L s R L No
31 1 30 syl φ L No
32 31 adantr φ p L q M L No
33 simprl φ p L q M p L
34 32 33 sseldd φ p L q M p No
35 34 adantrl φ f L A g L B p L q M p No
36 35 19 mulscld φ f L A g L B p L q M p s B No
37 36 25 addscld φ f L A g L B p L q M p s B + s A s g No
38 35 24 mulscld φ f L A g L B p L q M p s g No
39 37 38 subscld φ f L A g L B p L q M p s B + s A s g - s p s g No
40 39 adantrrr φ f L A g L B p L q M f s p g s q p s B + s A s g - s p s g No
41 sltsss1 M s S M No
42 2 41 syl φ M No
43 42 adantr φ p L q M M No
44 simprr φ p L q M q M
45 43 44 sseldd φ p L q M q No
46 45 adantrl φ f L A g L B p L q M q No
47 21 46 mulscld φ f L A g L B p L q M A s q No
48 36 47 addscld φ f L A g L B p L q M p s B + s A s q No
49 35 46 mulscld φ f L A g L B p L q M p s q No
50 48 49 subscld φ f L A g L B p L q M p s B + s A s q - s p s q No
51 50 adantrrr φ f L A g L B p L q M f s p g s q p s B + s A s q - s p s q No
52 17 adantrr φ f L A g L B p L q M f s p g s q f No
53 35 adantrrr φ f L A g L B p L q M f s p g s q p No
54 23 adantrr φ f L A g L B p L q M f s p g s q g No
55 8 adantr φ f L A g L B p L q M f s p g s q B No
56 simprrl f L A g L B p L q M f s p g s q f s p
57 56 adantl φ f L A g L B p L q M f s p g s q f s p
58 8 adantr φ f L A g L B B No
59 sltsleft B No L B s B
60 8 59 syl φ L B s B
61 60 adantr φ f L A g L B L B s B
62 snidg B No B B
63 8 62 syl φ B B
64 63 adantr φ f L A g L B B B
65 61 22 64 sltssepcd φ f L A g L B g < s B
66 23 58 65 ltlesd φ f L A g L B g s B
67 66 adantrr φ f L A g L B p L q M f s p g s q g s B
68 52 53 54 55 57 67 lemulsd φ f L A g L B p L q M f s p g s q f s B - s f s g s p s B - s p s g
69 20 27 subscld φ f L A g L B p L q M f s B - s f s g No
70 36 38 subscld φ f L A g L B p L q M p s B - s p s g No
71 69 70 25 leadds1d φ f L A g L B p L q M f s B - s f s g s p s B - s p s g f s B - s f s g + s A s g s p s B - s p s g + s A s g
72 71 adantrrr φ f L A g L B p L q M f s p g s q f s B - s f s g s p s B - s p s g f s B - s f s g + s A s g s p s B - s p s g + s A s g
73 68 72 mpbid φ f L A g L B p L q M f s p g s q f s B - s f s g + s A s g s p s B - s p s g + s A s g
74 20 25 27 addsubsd φ f L A g L B p L q M f s B + s A s g - s f s g = f s B - s f s g + s A s g
75 74 adantrrr φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g = f s B - s f s g + s A s g
76 36 25 38 addsubsd φ f L A g L B p L q M p s B + s A s g - s p s g = p s B - s p s g + s A s g
77 76 adantrrr φ f L A g L B p L q M f s p g s q p s B + s A s g - s p s g = p s B - s p s g + s A s g
78 73 75 77 3brtr4d φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g s p s B + s A s g - s p s g
79 6 adantr φ f L A g L B p L q M f s p g s q A No
80 46 adantrrr φ f L A g L B p L q M f s p g s q q No
81 6 adantr φ p L q M A No
82 cutcuts L s R L | s R No L s L | s R L | s R s R
83 1 82 syl φ L | s R No L s L | s R L | s R s R
84 83 simp2d φ L s L | s R
85 84 adantr φ p L q M L s L | s R
86 ovex L | s R V
87 86 snid L | s R L | s R
88 3 87 eqeltrdi φ A L | s R
89 88 adantr φ p L q M A L | s R
90 85 33 89 sltssepcd φ p L q M p < s A
91 34 81 90 ltlesd φ p L q M p s A
92 91 adantrl φ f L A g L B p L q M p s A
93 92 adantrrr φ f L A g L B p L q M f s p g s q p s A
94 simprrr f L A g L B p L q M f s p g s q g s q
95 94 adantl φ f L A g L B p L q M f s p g s q g s q
96 53 79 54 80 93 95 lemulsd φ f L A g L B p L q M f s p g s q p s q - s p s g s A s q - s A s g
97 49 47 38 25 lesubsubs3bd φ f L A g L B p L q M p s q - s p s g s A s q - s A s g A s g - s p s g s A s q - s p s q
98 25 38 subscld φ f L A g L B p L q M A s g - s p s g No
99 47 49 subscld φ f L A g L B p L q M A s q - s p s q No
100 98 99 36 leadds2d φ f L A g L B p L q M A s g - s p s g s A s q - s p s q p s B + s A s g - s p s g s p s B + s A s q - s p s q
101 97 100 bitrd φ f L A g L B p L q M p s q - s p s g s A s q - s A s g p s B + s A s g - s p s g s p s B + s A s q - s p s q
102 101 adantrrr φ f L A g L B p L q M f s p g s q p s q - s p s g s A s q - s A s g p s B + s A s g - s p s g s p s B + s A s q - s p s q
103 96 102 mpbid φ f L A g L B p L q M f s p g s q p s B + s A s g - s p s g s p s B + s A s q - s p s q
104 36 25 38 addsubsassd φ f L A g L B p L q M p s B + s A s g - s p s g = p s B + s A s g - s p s g
105 104 adantrrr φ f L A g L B p L q M f s p g s q p s B + s A s g - s p s g = p s B + s A s g - s p s g
106 36 47 49 addsubsassd φ f L A g L B p L q M p s B + s A s q - s p s q = p s B + s A s q - s p s q
107 106 adantrrr φ f L A g L B p L q M f s p g s q p s B + s A s q - s p s q = p s B + s A s q - s p s q
108 103 105 107 3brtr4d φ f L A g L B p L q M f s p g s q p s B + s A s g - s p s g s p s B + s A s q - s p s q
109 29 40 51 78 108 lestrd φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g s p s B + s A s q - s p s q
110 109 anassrs φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g s p s B + s A s q - s p s q
111 110 expr φ f L A g L B p L q M f s p g s q f s B + s A s g - s f s g s p s B + s A s q - s p s q
112 111 reximdvva φ f L A g L B p L q M f s p g s q p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
113 112 expcom f L A g L B φ p L q M f s p g s q p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
114 113 com23 f L A g L B p L q M f s p g s q φ p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
115 114 imp f L A g L B p L q M f s p g s q φ p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
116 15 115 sylan2br f L A g L B p L f s p q M g s q φ p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
117 116 an4s f L A p L f s p g L B q M g s q φ p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
118 117 impcom φ f L A p L f s p g L B q M g s q p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
119 118 anassrs φ f L A p L f s p g L B q M g s q p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
120 119 expr φ f L A p L f s p g L B q M g s q p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
121 120 ralimdva φ f L A p L f s p g L B q M g s q g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
122 14 121 mpd φ f L A p L f s p g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
123 122 expr φ f L A p L f s p g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
124 123 ralimdva φ f L A p L f s p f L A g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
125 12 124 mpd φ f L A g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
126 eqeq1 a = z a = p s B + s A s q - s p s q z = p s B + s A s q - s p s q
127 126 2rexbidv a = z p L q M a = p s B + s A s q - s p s q p L q M z = p s B + s A s q - s p s q
128 127 rexab z a | p L q M a = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z
129 r19.41vv p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z
130 129 exbii z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z
131 rexcom4 p L z q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z
132 rexcom4 q M z z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z
133 ovex p s B + s A s q - s p s q V
134 breq2 z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z f s B + s A s g - s f s g s p s B + s A s q - s p s q
135 133 134 ceqsexv z z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z f s B + s A s g - s f s g s p s B + s A s q - s p s q
136 135 rexbii q M z z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
137 132 136 bitr3i z q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
138 137 rexbii p L z q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
139 131 138 bitr3i z p L q M z = p s B + s A s q - s p s q f s B + s A s g - s f s g s z p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
140 128 130 139 3bitr2i z a | p L q M a = p s B + s A s q - s p s q f s B + s A s g - s f s g s z p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q
141 ssun1 a | p L q M a = p s B + s A s q - s p s q a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s
142 ssrexv a | p L q M a = p s B + s A s q - s p s q a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s z a | p L q M a = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s f s B + s A s g - s f s g s z
143 141 142 ax-mp z a | p L q M a = p s B + s A s q - s p s q f s B + s A s g - s f s g s z z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s f s B + s A s g - s f s g s z
144 140 143 sylbir p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s f s B + s A s g - s f s g s z
145 144 2ralimi f L A g L B p L q M f s B + s A s g - s f s g s p s B + s A s q - s p s q f L A g L B z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s f s B + s A s g - s f s g s z
146 125 145 syl φ f L A g L B z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s f s B + s A s g - s f s g s z
147 1 3 cofcutr2d φ i R A r R r s i
148 2 4 cofcutr2d φ j R B s S s s j
149 148 adantr φ i R A r R r s i j R B s S s s j
150 reeanv r R s S r s i s s j r R r s i s S s s j
151 simprl φ i R A j R B i R A
152 151 rightnod φ i R A j R B i No
153 152 adantrr φ i R A j R B r R s S i No
154 8 adantr φ i R A j R B r R s S B No
155 153 154 mulscld φ i R A j R B r R s S i s B No
156 6 adantr φ i R A j R B r R s S A No
157 simprr φ i R A j R B j R B
158 157 rightnod φ i R A j R B j No
159 158 adantrr φ i R A j R B r R s S j No
160 156 159 mulscld φ i R A j R B r R s S A s j No
161 155 160 addscld φ i R A j R B r R s S i s B + s A s j No
162 153 159 mulscld φ i R A j R B r R s S i s j No
163 161 162 subscld φ i R A j R B r R s S i s B + s A s j - s i s j No
164 163 adantrrr φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j No
165 sltsss2 L s R R No
166 1 165 syl φ R No
167 166 adantr φ r R s S R No
168 simprl φ r R s S r R
169 167 168 sseldd φ r R s S r No
170 169 adantrl φ i R A j R B r R s S r No
171 170 154 mulscld φ i R A j R B r R s S r s B No
172 171 160 addscld φ i R A j R B r R s S r s B + s A s j No
173 170 159 mulscld φ i R A j R B r R s S r s j No
174 172 173 subscld φ i R A j R B r R s S r s B + s A s j - s r s j No
175 174 adantrrr φ i R A j R B r R s S r s i s s j r s B + s A s j - s r s j No
176 sltsss2 M s S S No
177 2 176 syl φ S No
178 177 adantr φ r R s S S No
179 simprr φ r R s S s S
180 178 179 sseldd φ r R s S s No
181 180 adantrl φ i R A j R B r R s S s No
182 156 181 mulscld φ i R A j R B r R s S A s s No
183 171 182 addscld φ i R A j R B r R s S r s B + s A s s No
184 169 180 mulscld φ r R s S r s s No
185 184 adantrl φ i R A j R B r R s S r s s No
186 183 185 subscld φ i R A j R B r R s S r s B + s A s s - s r s s No
187 186 adantrrr φ i R A j R B r R s S r s i s s j r s B + s A s s - s r s s No
188 170 adantrrr φ i R A j R B r R s S r s i s s j r No
189 152 adantrr φ i R A j R B r R s S r s i s s j i No
190 8 adantr φ i R A j R B r R s S r s i s s j B No
191 158 adantrr φ i R A j R B r R s S r s i s s j j No
192 simprrl i R A j R B r R s S r s i s s j r s i
193 192 adantl φ i R A j R B r R s S r s i s s j r s i
194 8 adantr φ i R A j R B B No
195 sltsright B No B s R B
196 8 195 syl φ B s R B
197 196 adantr φ i R A j R B B s R B
198 63 adantr φ i R A j R B B B
199 197 198 157 sltssepcd φ i R A j R B B < s j
200 194 158 199 ltlesd φ i R A j R B B s j
201 200 adantrr φ i R A j R B r R s S r s i s s j B s j
202 188 189 190 191 193 201 lemulsd φ i R A j R B r R s S r s i s s j r s j - s r s B s i s j - s i s B
203 173 171 162 155 lesubsubs2bd φ i R A j R B r R s S r s j - s r s B s i s j - s i s B i s B - s i s j s r s B - s r s j
204 155 162 subscld φ i R A j R B r R s S i s B - s i s j No
205 171 173 subscld φ i R A j R B r R s S r s B - s r s j No
206 204 205 160 leadds1d φ i R A j R B r R s S i s B - s i s j s r s B - s r s j i s B - s i s j + s A s j s r s B - s r s j + s A s j
207 203 206 bitrd φ i R A j R B r R s S r s j - s r s B s i s j - s i s B i s B - s i s j + s A s j s r s B - s r s j + s A s j
208 207 adantrrr φ i R A j R B r R s S r s i s s j r s j - s r s B s i s j - s i s B i s B - s i s j + s A s j s r s B - s r s j + s A s j
209 202 208 mpbid φ i R A j R B r R s S r s i s s j i s B - s i s j + s A s j s r s B - s r s j + s A s j
210 155 160 162 addsubsd φ i R A j R B r R s S i s B + s A s j - s i s j = i s B - s i s j + s A s j
211 210 adantrrr φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j = i s B - s i s j + s A s j
212 171 160 173 addsubsd φ i R A j R B r R s S r s B + s A s j - s r s j = r s B - s r s j + s A s j
213 212 adantrrr φ i R A j R B r R s S r s i s s j r s B + s A s j - s r s j = r s B - s r s j + s A s j
214 209 211 213 3brtr4d φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j s r s B + s A s j - s r s j
215 6 adantr φ i R A j R B r R s S r s i s s j A No
216 181 adantrrr φ i R A j R B r R s S r s i s s j s No
217 6 adantr φ r R s S A No
218 83 simp3d φ L | s R s R
219 218 adantr φ r R s S L | s R s R
220 88 adantr φ r R s S A L | s R
221 219 220 168 sltssepcd φ r R s S A < s r
222 217 169 221 ltlesd φ r R s S A s r
223 222 adantrl φ i R A j R B r R s S A s r
224 223 adantrrr φ i R A j R B r R s S r s i s s j A s r
225 simprrr i R A j R B r R s S r s i s s j s s j
226 225 adantl φ i R A j R B r R s S r s i s s j s s j
227 215 188 216 191 224 226 lemulsd φ i R A j R B r R s S r s i s s j A s j - s A s s s r s j - s r s s
228 160 173 182 185 lesubsubsbd φ i R A j R B r R s S A s j - s A s s s r s j - s r s s A s j - s r s j s A s s - s r s s
229 160 173 subscld φ i R A j R B r R s S A s j - s r s j No
230 182 185 subscld φ i R A j R B r R s S A s s - s r s s No
231 229 230 171 leadds2d φ i R A j R B r R s S A s j - s r s j s A s s - s r s s r s B + s A s j - s r s j s r s B + s A s s - s r s s
232 228 231 bitrd φ i R A j R B r R s S A s j - s A s s s r s j - s r s s r s B + s A s j - s r s j s r s B + s A s s - s r s s
233 232 adantrrr φ i R A j R B r R s S r s i s s j A s j - s A s s s r s j - s r s s r s B + s A s j - s r s j s r s B + s A s s - s r s s
234 227 233 mpbid φ i R A j R B r R s S r s i s s j r s B + s A s j - s r s j s r s B + s A s s - s r s s
235 171 160 173 addsubsassd φ i R A j R B r R s S r s B + s A s j - s r s j = r s B + s A s j - s r s j
236 235 adantrrr φ i R A j R B r R s S r s i s s j r s B + s A s j - s r s j = r s B + s A s j - s r s j
237 171 182 185 addsubsassd φ i R A j R B r R s S r s B + s A s s - s r s s = r s B + s A s s - s r s s
238 237 adantrrr φ i R A j R B r R s S r s i s s j r s B + s A s s - s r s s = r s B + s A s s - s r s s
239 234 236 238 3brtr4d φ i R A j R B r R s S r s i s s j r s B + s A s j - s r s j s r s B + s A s s - s r s s
240 164 175 187 214 239 lestrd φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j s r s B + s A s s - s r s s
241 240 anassrs φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j s r s B + s A s s - s r s s
242 241 expr φ i R A j R B r R s S r s i s s j i s B + s A s j - s i s j s r s B + s A s s - s r s s
243 242 reximdvva φ i R A j R B r R s S r s i s s j r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
244 243 expcom i R A j R B φ r R s S r s i s s j r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
245 244 com23 i R A j R B r R s S r s i s s j φ r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
246 245 imp i R A j R B r R s S r s i s s j φ r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
247 150 246 sylan2br i R A j R B r R r s i s S s s j φ r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
248 247 an4s i R A r R r s i j R B s S s s j φ r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
249 248 impcom φ i R A r R r s i j R B s S s s j r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
250 249 anassrs φ i R A r R r s i j R B s S s s j r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
251 250 expr φ i R A r R r s i j R B s S s s j r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
252 251 ralimdva φ i R A r R r s i j R B s S s s j j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
253 149 252 mpd φ i R A r R r s i j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
254 253 expr φ i R A r R r s i j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
255 254 ralimdva φ i R A r R r s i i R A j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
256 147 255 mpd φ i R A j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
257 eqeq1 b = z b = r s B + s A s s - s r s s z = r s B + s A s s - s r s s
258 257 2rexbidv b = z r R s S b = r s B + s A s s - s r s s r R s S z = r s B + s A s s - s r s s
259 258 rexab z b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
260 r19.41vv r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
261 260 exbii z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
262 rexcom4 r R z s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
263 rexcom4 s S z z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
264 ovex r s B + s A s s - s r s s V
265 breq2 z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z i s B + s A s j - s i s j s r s B + s A s s - s r s s
266 264 265 ceqsexv z z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z i s B + s A s j - s i s j s r s B + s A s s - s r s s
267 266 rexbii s S z z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
268 263 267 bitr3i z s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
269 268 rexbii r R z s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
270 262 269 bitr3i z r R s S z = r s B + s A s s - s r s s i s B + s A s j - s i s j s z r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
271 259 261 270 3bitr2i z b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s
272 ssun2 b | r R s S b = r s B + s A s s - s r s s a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s
273 ssrexv b | r R s S b = r s B + s A s s - s r s s a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s z b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
274 272 273 ax-mp z b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
275 271 274 sylbir r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
276 275 2ralimi i R A j R B r R s S i s B + s A s j - s i s j s r s B + s A s s - s r s s i R A j R B z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
277 256 276 syl φ i R A j R B z a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s i s B + s A s j - s i s j s z
278 ralunb Could not format ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
279 eqeq1 Could not format ( e = xO -> ( e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) : No typesetting found for |- ( e = xO -> ( e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) with typecode |-
280 279 2rexbidv Could not format ( e = xO -> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) : No typesetting found for |- ( e = xO -> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) with typecode |-
281 280 ralab Could not format ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
282 r19.23v Could not format ( A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
283 282 ralbii Could not format ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
284 r19.23v Could not format ( A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
285 283 284 bitri Could not format ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
286 285 albii Could not format ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
287 ralcom4 Could not format ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
288 ralcom4 Could not format ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
289 ovex f s B + s A s g - s f s g V
290 breq1 Could not format ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( xO <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( xO <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) with typecode |-
291 290 rexbidv Could not format ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) with typecode |-
292 289 291 ceqsalv Could not format ( A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
293 292 ralbii Could not format ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
294 288 293 bitr3i Could not format ( A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
295 294 ralbii Could not format ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
296 287 295 bitr3i Could not format ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
297 281 286 296 3bitr2i Could not format ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |-
298 eqeq1 Could not format ( h = xO -> ( h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) : No typesetting found for |- ( h = xO -> ( h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) with typecode |-
299 298 2rexbidv Could not format ( h = xO -> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) : No typesetting found for |- ( h = xO -> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) with typecode |-
300 299 ralab Could not format ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
301 r19.23v Could not format ( A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
302 301 ralbii Could not format ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
303 r19.23v Could not format ( A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
304 302 303 bitri Could not format ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
305 304 albii Could not format ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
306 ralcom4 Could not format ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
307 ralcom4 Could not format ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |-
308 ovex i s B + s A s j - s i s j V
309 breq1 Could not format ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( xO <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( xO <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |-
310 309 rexbidv Could not format ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |-
311 308 310 ceqsalv Could not format ( A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
312 311 ralbii Could not format ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
313 307 312 bitr3i Could not format ( A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
314 313 ralbii Could not format ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
315 306 314 bitr3i Could not format ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
316 300 305 315 3bitr2i Could not format ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |-
317 297 316 anbi12i Could not format ( ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |-
318 278 317 bitri Could not format ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |-
319 146 277 318 sylanbrc Could not format ( ph -> A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) : No typesetting found for |- ( ph -> A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) with typecode |-
320 1 3 cofcutr1d φ l L A t L l s t
321 2 4 cofcutr2d φ m R B u S u s m
322 321 adantr φ l L A t L l s t m R B u S u s m
323 reeanv t L u S l s t u s m t L l s t u S u s m
324 31 adantr φ t L u S L No
325 simprl φ t L u S t L
326 324 325 sseldd φ t L u S t No
327 326 adantrl φ l L A m R B t L u S t No
328 8 adantr φ l L A m R B t L u S B No
329 327 328 mulscld φ l L A m R B t L u S t s B No
330 6 adantr φ l L A m R B t L u S A No
331 177 adantr φ t L u S S No
332 simprr φ t L u S u S
333 331 332 sseldd φ t L u S u No
334 333 adantrl φ l L A m R B t L u S u No
335 330 334 mulscld φ l L A m R B t L u S A s u No
336 329 335 addscld φ l L A m R B t L u S t s B + s A s u No
337 327 334 mulscld φ l L A m R B t L u S t s u No
338 336 337 subscld φ l L A m R B t L u S t s B + s A s u - s t s u No
339 338 adantrrr φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u No
340 simprl φ l L A m R B l L A
341 340 leftnod φ l L A m R B l No
342 8 adantr φ l L A m R B B No
343 341 342 mulscld φ l L A m R B l s B No
344 343 adantrr φ l L A m R B t L u S l s B No
345 344 335 addscld φ l L A m R B t L u S l s B + s A s u No
346 341 adantrr φ l L A m R B t L u S l No
347 346 334 mulscld φ l L A m R B t L u S l s u No
348 345 347 subscld φ l L A m R B t L u S l s B + s A s u - s l s u No
349 348 adantrrr φ l L A m R B t L u S l s t u s m l s B + s A s u - s l s u No
350 6 adantr φ l L A m R B A No
351 simprr φ l L A m R B m R B
352 351 rightnod φ l L A m R B m No
353 350 352 mulscld φ l L A m R B A s m No
354 353 adantrr φ l L A m R B t L u S A s m No
355 344 354 addscld φ l L A m R B t L u S l s B + s A s m No
356 341 352 mulscld φ l L A m R B l s m No
357 356 adantrr φ l L A m R B t L u S l s m No
358 355 357 subscld φ l L A m R B t L u S l s B + s A s m - s l s m No
359 358 adantrrr φ l L A m R B t L u S l s t u s m l s B + s A s m - s l s m No
360 341 adantrr φ l L A m R B t L u S l s t u s m l No
361 327 adantrrr φ l L A m R B t L u S l s t u s m t No
362 8 adantr φ l L A m R B t L u S l s t u s m B No
363 334 adantrrr φ l L A m R B t L u S l s t u s m u No
364 simprrl l L A m R B t L u S l s t u s m l s t
365 364 adantl φ l L A m R B t L u S l s t u s m l s t
366 8 adantr φ t L u S B No
367 cutcuts M s S M | s S No M s M | s S M | s S s S
368 2 367 syl φ M | s S No M s M | s S M | s S s S
369 368 simp3d φ M | s S s S
370 369 adantr φ t L u S M | s S s S
371 ovex M | s S V
372 371 snid M | s S M | s S
373 4 372 eqeltrdi φ B M | s S
374 373 adantr φ t L u S B M | s S
375 370 374 332 sltssepcd φ t L u S B < s u
376 366 333 375 ltlesd φ t L u S B s u
377 376 adantrl φ l L A m R B t L u S B s u
378 377 adantrrr φ l L A m R B t L u S l s t u s m B s u
379 360 361 362 363 365 378 lemulsd φ l L A m R B t L u S l s t u s m l s u - s l s B s t s u - s t s B
380 347 344 337 329 lesubsubs2bd φ l L A m R B t L u S l s u - s l s B s t s u - s t s B t s B - s t s u s l s B - s l s u
381 329 337 subscld φ l L A m R B t L u S t s B - s t s u No
382 344 347 subscld φ l L A m R B t L u S l s B - s l s u No
383 381 382 335 leadds1d φ l L A m R B t L u S t s B - s t s u s l s B - s l s u t s B - s t s u + s A s u s l s B - s l s u + s A s u
384 380 383 bitrd φ l L A m R B t L u S l s u - s l s B s t s u - s t s B t s B - s t s u + s A s u s l s B - s l s u + s A s u
385 384 adantrrr φ l L A m R B t L u S l s t u s m l s u - s l s B s t s u - s t s B t s B - s t s u + s A s u s l s B - s l s u + s A s u
386 379 385 mpbid φ l L A m R B t L u S l s t u s m t s B - s t s u + s A s u s l s B - s l s u + s A s u
387 329 335 337 addsubsd φ l L A m R B t L u S t s B + s A s u - s t s u = t s B - s t s u + s A s u
388 387 adantrrr φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u = t s B - s t s u + s A s u
389 344 335 347 addsubsd φ l L A m R B t L u S l s B + s A s u - s l s u = l s B - s l s u + s A s u
390 389 adantrrr φ l L A m R B t L u S l s t u s m l s B + s A s u - s l s u = l s B - s l s u + s A s u
391 386 388 390 3brtr4d φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u s l s B + s A s u - s l s u
392 6 adantr φ l L A m R B t L u S l s t u s m A No
393 352 adantrr φ l L A m R B t L u S l s t u s m m No
394 sltsleft A No L A s A
395 6 394 syl φ L A s A
396 395 adantr φ l L A m R B L A s A
397 snidg A No A A
398 6 397 syl φ A A
399 398 adantr φ l L A m R B A A
400 396 340 399 sltssepcd φ l L A m R B l < s A
401 341 350 400 ltlesd φ l L A m R B l s A
402 401 adantrr φ l L A m R B t L u S l s t u s m l s A
403 simprrr l L A m R B t L u S l s t u s m u s m
404 403 adantl φ l L A m R B t L u S l s t u s m u s m
405 360 392 363 393 402 404 lemulsd φ l L A m R B t L u S l s t u s m l s m - s l s u s A s m - s A s u
406 357 354 347 335 lesubsubs3bd φ l L A m R B t L u S l s m - s l s u s A s m - s A s u A s u - s l s u s A s m - s l s m
407 335 347 subscld φ l L A m R B t L u S A s u - s l s u No
408 354 357 subscld φ l L A m R B t L u S A s m - s l s m No
409 407 408 344 leadds2d φ l L A m R B t L u S A s u - s l s u s A s m - s l s m l s B + s A s u - s l s u s l s B + s A s m - s l s m
410 406 409 bitrd φ l L A m R B t L u S l s m - s l s u s A s m - s A s u l s B + s A s u - s l s u s l s B + s A s m - s l s m
411 410 adantrrr φ l L A m R B t L u S l s t u s m l s m - s l s u s A s m - s A s u l s B + s A s u - s l s u s l s B + s A s m - s l s m
412 405 411 mpbid φ l L A m R B t L u S l s t u s m l s B + s A s u - s l s u s l s B + s A s m - s l s m
413 344 335 347 addsubsassd φ l L A m R B t L u S l s B + s A s u - s l s u = l s B + s A s u - s l s u
414 413 adantrrr φ l L A m R B t L u S l s t u s m l s B + s A s u - s l s u = l s B + s A s u - s l s u
415 344 354 357 addsubsassd φ l L A m R B t L u S l s B + s A s m - s l s m = l s B + s A s m - s l s m
416 415 adantrrr φ l L A m R B t L u S l s t u s m l s B + s A s m - s l s m = l s B + s A s m - s l s m
417 412 414 416 3brtr4d φ l L A m R B t L u S l s t u s m l s B + s A s u - s l s u s l s B + s A s m - s l s m
418 339 349 359 391 417 lestrd φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u s l s B + s A s m - s l s m
419 418 anassrs φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u s l s B + s A s m - s l s m
420 419 expr φ l L A m R B t L u S l s t u s m t s B + s A s u - s t s u s l s B + s A s m - s l s m
421 420 reximdvva φ l L A m R B t L u S l s t u s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
422 421 expcom l L A m R B φ t L u S l s t u s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
423 422 com23 l L A m R B t L u S l s t u s m φ t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
424 423 imp l L A m R B t L u S l s t u s m φ t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
425 323 424 sylan2br l L A m R B t L l s t u S u s m φ t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
426 425 an4s l L A t L l s t m R B u S u s m φ t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
427 426 impcom φ l L A t L l s t m R B u S u s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
428 427 anassrs φ l L A t L l s t m R B u S u s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
429 428 expr φ l L A t L l s t m R B u S u s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
430 429 ralimdva φ l L A t L l s t m R B u S u s m m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
431 322 430 mpd φ l L A t L l s t m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
432 431 expr φ l L A t L l s t m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
433 432 ralimdva φ l L A t L l s t l L A m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
434 320 433 mpd φ l L A m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
435 eqeq1 c = z c = t s B + s A s u - s t s u z = t s B + s A s u - s t s u
436 435 2rexbidv c = z t L u S c = t s B + s A s u - s t s u t L u S z = t s B + s A s u - s t s u
437 436 rexab z c | t L u S c = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m
438 r19.41vv t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m
439 438 exbii z t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m
440 rexcom4 t L z u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m
441 rexcom4 u S z z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m
442 ovex t s B + s A s u - s t s u V
443 breq1 z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t s B + s A s u - s t s u s l s B + s A s m - s l s m
444 442 443 ceqsexv z z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t s B + s A s u - s t s u s l s B + s A s m - s l s m
445 444 rexbii u S z z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
446 441 445 bitr3i z u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
447 446 rexbii t L z u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
448 440 447 bitr3i z t L u S z = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
449 437 439 448 3bitr2i z c | t L u S c = t s B + s A s u - s t s u z s l s B + s A s m - s l s m t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m
450 ssun1 c | t L u S c = t s B + s A s u - s t s u c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w
451 ssrexv c | t L u S c = t s B + s A s u - s t s u c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z c | t L u S c = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s l s B + s A s m - s l s m
452 450 451 ax-mp z c | t L u S c = t s B + s A s u - s t s u z s l s B + s A s m - s l s m z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s l s B + s A s m - s l s m
453 449 452 sylbir t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s l s B + s A s m - s l s m
454 453 2ralimi l L A m R B t L u S t s B + s A s u - s t s u s l s B + s A s m - s l s m l L A m R B z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s l s B + s A s m - s l s m
455 434 454 syl φ l L A m R B z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s l s B + s A s m - s l s m
456 1 3 cofcutr2d φ x R A v R v s x
457 2 4 cofcutr1d φ y L B w M y s w
458 457 adantr φ x R A v R v s x y L B w M y s w
459 reeanv v R w M v s x y s w v R v s x w M y s w
460 166 adantr φ v R w M R No
461 simprl φ v R w M v R
462 460 461 sseldd φ v R w M v No
463 8 adantr φ v R w M B No
464 462 463 mulscld φ v R w M v s B No
465 464 adantrl φ x R A y L B v R w M v s B No
466 6 adantr φ v R w M A No
467 42 adantr φ v R w M M No
468 simprr φ v R w M w M
469 467 468 sseldd φ v R w M w No
470 466 469 mulscld φ v R w M A s w No
471 470 adantrl φ x R A y L B v R w M A s w No
472 465 471 addscld φ x R A y L B v R w M v s B + s A s w No
473 462 469 mulscld φ v R w M v s w No
474 473 adantrl φ x R A y L B v R w M v s w No
475 472 474 subscld φ x R A y L B v R w M v s B + s A s w - s v s w No
476 475 adantrrr φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w No
477 6 adantr φ x R A y L B v R w M A No
478 simprr φ x R A y L B y L B
479 478 leftnod φ x R A y L B y No
480 479 adantrr φ x R A y L B v R w M y No
481 477 480 mulscld φ x R A y L B v R w M A s y No
482 465 481 addscld φ x R A y L B v R w M v s B + s A s y No
483 462 adantrl φ x R A y L B v R w M v No
484 483 480 mulscld φ x R A y L B v R w M v s y No
485 482 484 subscld φ x R A y L B v R w M v s B + s A s y - s v s y No
486 485 adantrrr φ x R A y L B v R w M v s x y s w v s B + s A s y - s v s y No
487 simprl φ x R A y L B x R A
488 487 rightnod φ x R A y L B x No
489 8 adantr φ x R A y L B B No
490 488 489 mulscld φ x R A y L B x s B No
491 490 adantrr φ x R A y L B v R w M x s B No
492 491 481 addscld φ x R A y L B v R w M x s B + s A s y No
493 488 479 mulscld φ x R A y L B x s y No
494 493 adantrr φ x R A y L B v R w M x s y No
495 492 494 subscld φ x R A y L B v R w M x s B + s A s y - s x s y No
496 495 adantrrr φ x R A y L B v R w M v s x y s w x s B + s A s y - s x s y No
497 6 adantr φ x R A y L B v R w M v s x y s w A No
498 483 adantrrr φ x R A y L B v R w M v s x y s w v No
499 479 adantrr φ x R A y L B v R w M v s x y s w y No
500 469 adantrl φ x R A y L B v R w M w No
501 500 adantrrr φ x R A y L B v R w M v s x y s w w No
502 3 sneqd φ A = L | s R
503 502 218 eqbrtrd φ A s R
504 503 adantr φ x R A y L B v R w M A s R
505 477 397 syl φ x R A y L B v R w M A A
506 simprrl φ x R A y L B v R w M v R
507 504 505 506 sltssepcd φ x R A y L B v R w M A < s v
508 477 483 507 ltlesd φ x R A y L B v R w M A s v
509 508 adantrrr φ x R A y L B v R w M v s x y s w A s v
510 simprrr x R A y L B v R w M v s x y s w y s w
511 510 adantl φ x R A y L B v R w M v s x y s w y s w
512 497 498 499 501 509 511 lemulsd φ x R A y L B v R w M v s x y s w A s w - s A s y s v s w - s v s y
513 471 474 481 484 lesubsubsbd φ x R A y L B v R w M A s w - s A s y s v s w - s v s y A s w - s v s w s A s y - s v s y
514 471 474 subscld φ x R A y L B v R w M A s w - s v s w No
515 481 484 subscld φ x R A y L B v R w M A s y - s v s y No
516 514 515 465 leadds2d φ x R A y L B v R w M A s w - s v s w s A s y - s v s y v s B + s A s w - s v s w s v s B + s A s y - s v s y
517 513 516 bitrd φ x R A y L B v R w M A s w - s A s y s v s w - s v s y v s B + s A s w - s v s w s v s B + s A s y - s v s y
518 517 adantrrr φ x R A y L B v R w M v s x y s w A s w - s A s y s v s w - s v s y v s B + s A s w - s v s w s v s B + s A s y - s v s y
519 512 518 mpbid φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w s v s B + s A s y - s v s y
520 465 471 474 addsubsassd φ x R A y L B v R w M v s B + s A s w - s v s w = v s B + s A s w - s v s w
521 520 adantrrr φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w = v s B + s A s w - s v s w
522 465 481 484 addsubsassd φ x R A y L B v R w M v s B + s A s y - s v s y = v s B + s A s y - s v s y
523 522 adantrrr φ x R A y L B v R w M v s x y s w v s B + s A s y - s v s y = v s B + s A s y - s v s y
524 519 521 523 3brtr4d φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w s v s B + s A s y - s v s y
525 488 adantrr φ x R A y L B v R w M v s x y s w x No
526 8 adantr φ x R A y L B v R w M v s x y s w B No
527 simprrl x R A y L B v R w M v s x y s w v s x
528 527 adantl φ x R A y L B v R w M v s x y s w v s x
529 489 59 syl φ x R A y L B L B s B
530 63 adantr φ x R A y L B B B
531 529 478 530 sltssepcd φ x R A y L B y < s B
532 479 489 531 ltlesd φ x R A y L B y s B
533 532 adantrr φ x R A y L B v R w M v s x y s w y s B
534 498 525 499 526 528 533 lemulsd φ x R A y L B v R w M v s x y s w v s B - s v s y s x s B - s x s y
535 465 484 subscld φ x R A y L B v R w M v s B - s v s y No
536 535 adantrrr φ x R A y L B v R w M v s x y s w v s B - s v s y No
537 491 494 subscld φ x R A y L B v R w M x s B - s x s y No
538 537 adantrrr φ x R A y L B v R w M v s x y s w x s B - s x s y No
539 481 adantrrr φ x R A y L B v R w M v s x y s w A s y No
540 536 538 539 leadds1d φ x R A y L B v R w M v s x y s w v s B - s v s y s x s B - s x s y v s B - s v s y + s A s y s x s B - s x s y + s A s y
541 534 540 mpbid φ x R A y L B v R w M v s x y s w v s B - s v s y + s A s y s x s B - s x s y + s A s y
542 465 481 484 addsubsd φ x R A y L B v R w M v s B + s A s y - s v s y = v s B - s v s y + s A s y
543 542 adantrrr φ x R A y L B v R w M v s x y s w v s B + s A s y - s v s y = v s B - s v s y + s A s y
544 6 adantr φ x R A y L B A No
545 544 479 mulscld φ x R A y L B A s y No
546 490 545 493 addsubsd φ x R A y L B x s B + s A s y - s x s y = x s B - s x s y + s A s y
547 546 adantrr φ x R A y L B v R w M v s x y s w x s B + s A s y - s x s y = x s B - s x s y + s A s y
548 541 543 547 3brtr4d φ x R A y L B v R w M v s x y s w v s B + s A s y - s v s y s x s B + s A s y - s x s y
549 476 486 496 524 548 lestrd φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w s x s B + s A s y - s x s y
550 549 anassrs φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w s x s B + s A s y - s x s y
551 550 expr φ x R A y L B v R w M v s x y s w v s B + s A s w - s v s w s x s B + s A s y - s x s y
552 551 reximdvva φ x R A y L B v R w M v s x y s w v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
553 552 expcom x R A y L B φ v R w M v s x y s w v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
554 553 com23 x R A y L B v R w M v s x y s w φ v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
555 554 imp x R A y L B v R w M v s x y s w φ v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
556 459 555 sylan2br x R A y L B v R v s x w M y s w φ v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
557 556 an4s x R A v R v s x y L B w M y s w φ v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
558 557 impcom φ x R A v R v s x y L B w M y s w v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
559 558 anassrs φ x R A v R v s x y L B w M y s w v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
560 559 expr φ x R A v R v s x y L B w M y s w v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
561 560 ralimdva φ x R A v R v s x y L B w M y s w y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
562 458 561 mpd φ x R A v R v s x y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
563 562 expr φ x R A v R v s x y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
564 563 ralimdva φ x R A v R v s x x R A y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
565 456 564 mpd φ x R A y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
566 eqeq1 d = z d = v s B + s A s w - s v s w z = v s B + s A s w - s v s w
567 566 2rexbidv d = z v R w M d = v s B + s A s w - s v s w v R w M z = v s B + s A s w - s v s w
568 567 rexab z d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
569 r19.41vv v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
570 569 exbii z v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
571 rexcom4 v R z w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
572 rexcom4 w M z z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
573 ovex v s B + s A s w - s v s w V
574 breq1 z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v s B + s A s w - s v s w s x s B + s A s y - s x s y
575 573 574 ceqsexv z z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v s B + s A s w - s v s w s x s B + s A s y - s x s y
576 575 rexbii w M z z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
577 572 576 bitr3i z w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
578 577 rexbii v R z w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
579 571 578 bitr3i z v R w M z = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
580 568 570 579 3bitr2i z d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y
581 ssun2 d | v R w M d = v s B + s A s w - s v s w c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w
582 ssrexv d | v R w M d = v s B + s A s w - s v s w c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
583 581 582 ax-mp z d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
584 580 583 sylbir v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
585 584 2ralimi x R A y L B v R w M v s B + s A s w - s v s w s x s B + s A s y - s x s y x R A y L B z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
586 565 585 syl φ x R A y L B z c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w z s x s B + s A s y - s x s y
587 ralunb Could not format ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
588 eqeq1 Could not format ( k = xO -> ( k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( k = xO -> ( k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |-
589 588 2rexbidv Could not format ( k = xO -> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( k = xO -> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |-
590 589 ralab Could not format ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
591 r19.23v Could not format ( A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
592 591 ralbii Could not format ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
593 r19.23v Could not format ( A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
594 592 593 bitri Could not format ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
595 594 albii Could not format ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
596 ralcom4 Could not format ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
597 ralcom4 Could not format ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
598 ovex l s B + s A s m - s l s m V
599 breq2 Could not format ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( z <_s xO <-> z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( z <_s xO <-> z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |-
600 599 rexbidv Could not format ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |-
601 598 600 ceqsalv Could not format ( A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
602 601 ralbii Could not format ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
603 597 602 bitr3i Could not format ( A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
604 603 ralbii Could not format ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
605 596 604 bitr3i Could not format ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
606 590 595 605 3bitr2i Could not format ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |-
607 eqeq1 Could not format ( n = xO -> ( n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( n = xO -> ( n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
608 607 2rexbidv Could not format ( n = xO -> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( n = xO -> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
609 608 ralab Could not format ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
610 r19.23v Could not format ( A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
611 610 ralbii Could not format ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
612 r19.23v Could not format ( A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
613 611 612 bitri Could not format ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
614 613 albii Could not format ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
615 ralcom4 Could not format ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
616 ralcom4 Could not format ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |-
617 ovex x s B + s A s y - s x s y V
618 breq2 Could not format ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( z <_s xO <-> z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( z <_s xO <-> z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
619 618 rexbidv Could not format ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
620 617 619 ceqsalv Could not format ( A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
621 620 ralbii Could not format ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
622 616 621 bitr3i Could not format ( A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
623 622 ralbii Could not format ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
624 615 623 bitr3i Could not format ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
625 609 614 624 3bitr2i Could not format ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |-
626 606 625 anbi12i Could not format ( ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
627 587 626 bitri Could not format ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |-
628 455 586 627 sylanbrc Could not format ( ph -> A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) : No typesetting found for |- ( ph -> A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) with typecode |-
629 1 2 3 4 sltmuls1 φ a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s s A s B
630 10 sneqd φ A s B = e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y
631 629 630 breqtrd φ a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s s e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y
632 1 2 3 4 sltmuls2 φ A s B s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w
633 630 632 eqbrtrrd φ e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w
634 11 319 628 631 633 cofcut1d φ e | f L A g L B e = f s B + s A s g - s f s g h | i R A j R B h = i s B + s A s j - s i s j | s k | l L A m R B k = l s B + s A s m - s l s m n | x R A y L B n = x s B + s A s y - s x s y = a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w
635 10 634 eqtrd φ A s B = a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w