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