Theorem leadds1

Description: Addition to both sides of surreal less-than or equal. Theorem 5 of Conway p. 18. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	leadds1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A{\le }_{s}B\leftrightarrow \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x +s z ) = ( xO +s z ) ) : No typesetting found for |- ( x = xO -> ( x +s z ) = ( xO +s z ) ) with typecode |-
2	1	breq2d	Could not format ( x = xO -> ( ( y +s z ) ( y +s z ) ( ( y +s z ) ( y +s z )
3		breq2	Could not format ( x = xO -> ( y y ( y y
4	2 3	imbi12d	Could not format ( x = xO -> ( ( ( y +s z ) y ( ( y +s z ) y ( ( ( y +s z ) y ( ( y +s z ) y
5		oveq1	Could not format ( y = yO -> ( y +s z ) = ( yO +s z ) ) : No typesetting found for |- ( y = yO -> ( y +s z ) = ( yO +s z ) ) with typecode |-
6	5	breq1d	Could not format ( y = yO -> ( ( y +s z ) ( yO +s z ) ( ( y +s z ) ( yO +s z )
7		breq1	Could not format ( y = yO -> ( y yO ( y yO
8	6 7	imbi12d	Could not format ( y = yO -> ( ( ( y +s z ) y ( ( yO +s z ) yO ( ( ( y +s z ) y ( ( yO +s z ) yO
9		oveq2	Could not format ( z = zO -> ( yO +s z ) = ( yO +s zO ) ) : No typesetting found for |- ( z = zO -> ( yO +s z ) = ( yO +s zO ) ) with typecode |-
10		oveq2	Could not format ( z = zO -> ( xO +s z ) = ( xO +s zO ) ) : No typesetting found for |- ( z = zO -> ( xO +s z ) = ( xO +s zO ) ) with typecode |-
11	9 10	breq12d	Could not format ( z = zO -> ( ( yO +s z ) ( yO +s zO ) ( ( yO +s z ) ( yO +s zO )
12	11	imbi1d	Could not format ( z = zO -> ( ( ( yO +s z ) yO ( ( yO +s zO ) yO ( ( ( yO +s z ) yO ( ( yO +s zO ) yO
13		oveq1	Could not format ( x = xO -> ( x +s zO ) = ( xO +s zO ) ) : No typesetting found for |- ( x = xO -> ( x +s zO ) = ( xO +s zO ) ) with typecode |-
14	13	breq2d	Could not format ( x = xO -> ( ( yO +s zO ) ( yO +s zO ) ( ( yO +s zO ) ( yO +s zO )
15		breq2	Could not format ( x = xO -> ( yO yO ( yO yO
16	14 15	imbi12d	Could not format ( x = xO -> ( ( ( yO +s zO ) yO ( ( yO +s zO ) yO ( ( ( yO +s zO ) yO ( ( yO +s zO ) yO
17		oveq1	Could not format ( y = yO -> ( y +s zO ) = ( yO +s zO ) ) : No typesetting found for |- ( y = yO -> ( y +s zO ) = ( yO +s zO ) ) with typecode |-
18	17	breq1d	Could not format ( y = yO -> ( ( y +s zO ) ( yO +s zO ) ( ( y +s zO ) ( yO +s zO )
19		breq1	Could not format ( y = yO -> ( y yO ( y yO
20	18 19	imbi12d	Could not format ( y = yO -> ( ( ( y +s zO ) y ( ( yO +s zO ) yO ( ( ( y +s zO ) y ( ( yO +s zO ) yO
21	17	breq1d	Could not format ( y = yO -> ( ( y +s zO ) ( yO +s zO ) ( ( y +s zO ) ( yO +s zO )
22	21 7	imbi12d	Could not format ( y = yO -> ( ( ( y +s zO ) y ( ( yO +s zO ) yO ( ( ( y +s zO ) y ( ( yO +s zO ) yO
23		oveq2	Could not format ( z = zO -> ( x +s z ) = ( x +s zO ) ) : No typesetting found for |- ( z = zO -> ( x +s z ) = ( x +s zO ) ) with typecode |-
24	9 23	breq12d	Could not format ( z = zO -> ( ( yO +s z ) ( yO +s zO ) ( ( yO +s z ) ( yO +s zO )
25	24	imbi1d	Could not format ( z = zO -> ( ( ( yO +s z ) yO ( ( yO +s zO ) yO ( ( ( yO +s z ) yO ( ( yO +s zO ) yO
26		oveq1	$$⊢x=A\to x{+}_{s}z=A{+}_{s}z$$
27	26	breq2d	$$⊢x=A\to \left(\left(y{+}_{s}z\right){<}_s\left(x{+}_{s}z\right)\leftrightarrow \left(y{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\right)$$
28		breq2	$$⊢x=A\to \left(y{<}_{s}x\leftrightarrow y{<}_{s}A\right)$$
29	27 28	imbi12d	$$⊢x=A\to \left(\left(\left(y{+}_{s}z\right){<}_s\left(x{+}_{s}z\right)\to y{<}_{s}x\right)\leftrightarrow \left(\left(y{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\to y{<}_{s}A\right)\right)$$
30		oveq1	$$⊢y=B\to y{+}_{s}z=B{+}_{s}z$$
31	30	breq1d	$$⊢y=B\to \left(\left(y{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\leftrightarrow \left(B{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\right)$$
32		breq1	$$⊢y=B\to \left(y{<}_{s}A\leftrightarrow B{<}_{s}A\right)$$
33	31 32	imbi12d	$$⊢y=B\to \left(\left(\left(y{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\to y{<}_{s}A\right)\leftrightarrow \left(\left(B{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\to B{<}_{s}A\right)\right)$$
34		oveq2	$$⊢z=C\to B{+}_{s}z=B{+}_{s}C$$
35		oveq2	$$⊢z=C\to A{+}_{s}z=A{+}_{s}C$$
36	34 35	breq12d	$$⊢z=C\to \left(\left(B{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\leftrightarrow \left(B{+}_{s}C\right){<}_s\left(A{+}_{s}C\right)\right)$$
37	36	imbi1d	$$⊢z=C\to \left(\left(\left(B{+}_{s}z\right){<}_s\left(A{+}_{s}z\right)\to B{<}_{s}A\right)\leftrightarrow \left(\left(B{+}_{s}C\right){<}_s\left(A{+}_{s}C\right)\to B{<}_{s}A\right)\right)$$
38		simp2	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\wedge z\in \mathrm{No}\right)\to y\in \mathrm{No}$$
39		simp3	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\wedge z\in \mathrm{No}\right)\to z\in \mathrm{No}$$
40	38 39	addcuts	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( y +s z ) e. No /\ ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( ( y +s z ) e. No /\ ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
41		simp2	Could not format ( ( ( y +s z ) e. No /\ ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
42	40 41	syl	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
43	40	simp3d	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> { ( y +s z ) } < { ( y +s z ) } <
44		ovex	$$⊢y{+}_{s}z\in \mathrm{V}$$
45	44	snnz	$$⊢\left\{y{+}_{s}z\right\}\ne \varnothing$$
46		sltstr	Could not format ( ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
47	45 46	mp3an3	Could not format ( ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
48	42 43 47	syl2anc	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
49		simp1	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\wedge z\in \mathrm{No}\right)\to x\in \mathrm{No}$$
50	49 39	addcuts	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( x +s z ) e. No /\ ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( ( x +s z ) e. No /\ ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
51		simp2	Could not format ( ( ( x +s z ) e. No /\ ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
52	50 51	syl	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
53	50	simp3d	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> { ( x +s z ) } < { ( x +s z ) } <
54		ovex	$$⊢x{+}_{s}z\in \mathrm{V}$$
55	54	snnz	$$⊢\left\{x{+}_{s}z\right\}\ne \varnothing$$
56		sltstr	Could not format ( ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
57	55 56	mp3an3	Could not format ( ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
58	52 53 57	syl2anc	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
59		addsval2	Could not format ( ( y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) ) : No typesetting found for |- ( ( y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) ) with typecode |-
60	59	3adant1	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) ) with typecode |-
61		addsval2	Could not format ( ( x e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) ) with typecode |-
62	61	3adant2	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) ) with typecode |-
63	48 58 60 62	ltsrecd	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( y +s z ) ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( y +s z ) ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) ) with typecode |-
64	63	adantr	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) ) with typecode |-
65		rexun	Could not format ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) ) with typecode |-
66		eqeq1	Could not format ( a = p -> ( a = ( xL +s z ) <-> p = ( xL +s z ) ) ) : No typesetting found for |- ( a = p -> ( a = ( xL +s z ) <-> p = ( xL +s z ) ) ) with typecode |-
67	66	rexbidv	Could not format ( a = p -> ( E. xL e. ( _Left ` x ) a = ( xL +s z ) <-> E. xL e. ( _Left ` x ) p = ( xL +s z ) ) ) : No typesetting found for |- ( a = p -> ( E. xL e. ( _Left ` x ) a = ( xL +s z ) <-> E. xL e. ( _Left ` x ) p = ( xL +s z ) ) ) with typecode |-
68	67	rexab	Could not format ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) with typecode |-
69		rexcom4	Could not format ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) with typecode |-
70		r19.41v	Could not format ( E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) with typecode |-
71	70	exbii	Could not format ( E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) with typecode |-
72	69 71	bitri	Could not format ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) ) with typecode |-
73		ovex	Could not format ( xL +s z ) e. _V : No typesetting found for |- ( xL +s z ) e. _V with typecode |-
74		breq2	Could not format ( p = ( xL +s z ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( xL +s z ) ) ) : No typesetting found for |- ( p = ( xL +s z ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( xL +s z ) ) ) with typecode |-
75	73 74	ceqsexv	Could not format ( E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( xL +s z ) ) : No typesetting found for |- ( E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( xL +s z ) ) with typecode |-
76	75	rexbii	Could not format ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) : No typesetting found for |- ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) with typecode |-
77	72 76	bitr3i	Could not format ( E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) : No typesetting found for |- ( E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) with typecode |-
78	68 77	bitri	Could not format ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) : No typesetting found for |- ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) ) with typecode |-
79		eqeq1	Could not format ( b = p -> ( b = ( x +s zL ) <-> p = ( x +s zL ) ) ) : No typesetting found for |- ( b = p -> ( b = ( x +s zL ) <-> p = ( x +s zL ) ) ) with typecode |-
80	79	rexbidv	Could not format ( b = p -> ( E. zL e. ( _Left ` z ) b = ( x +s zL ) <-> E. zL e. ( _Left ` z ) p = ( x +s zL ) ) ) : No typesetting found for |- ( b = p -> ( E. zL e. ( _Left ` z ) b = ( x +s zL ) <-> E. zL e. ( _Left ` z ) p = ( x +s zL ) ) ) with typecode |-
81	80	rexab	Could not format ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) with typecode |-
82		rexcom4	Could not format ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) with typecode |-
83		r19.41v	Could not format ( E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) with typecode |-
84	83	exbii	Could not format ( E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) with typecode |-
85	82 84	bitri	Could not format ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) : No typesetting found for |- ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) ) with typecode |-
86		ovex	Could not format ( x +s zL ) e. _V : No typesetting found for |- ( x +s zL ) e. _V with typecode |-
87		breq2	Could not format ( p = ( x +s zL ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( x +s zL ) ) ) : No typesetting found for |- ( p = ( x +s zL ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( x +s zL ) ) ) with typecode |-
88	86 87	ceqsexv	Could not format ( E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( x +s zL ) ) : No typesetting found for |- ( E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( x +s zL ) ) with typecode |-
89	88	rexbii	Could not format ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) : No typesetting found for |- ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) with typecode |-
90	85 89	bitr3i	Could not format ( E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) : No typesetting found for |- ( E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) with typecode |-
91	81 90	bitri	Could not format ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) : No typesetting found for |- ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) with typecode |-
92	78 91	orbi12i	Could not format ( ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) ) : No typesetting found for |- ( ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) ) with typecode |-
93	65 92	bitri	Could not format ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) ) : No typesetting found for |- ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) ) with typecode |-
94		simpll2	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) with typecode |-
95		leftno	Could not format ( xL e. ( _Left ` x ) -> xL e. No ) : No typesetting found for |- ( xL e. ( _Left ` x ) -> xL e. No ) with typecode |-
96	95	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL e. No ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL e. No ) with typecode |-
97	96	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y xL e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y xL e. No ) with typecode |-
98		simpll1	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) with typecode |-
99		simprr	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) <_s ( xL +s z ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) <_s ( xL +s z ) ) with typecode |-
100		simpll3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) with typecode |-
101		leadds1im	Could not format ( ( y e. No /\ xL e. No /\ z e. No ) -> ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) ) : No typesetting found for |- ( ( y e. No /\ xL e. No /\ z e. No ) -> ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) ) with typecode |-
102	94 97 100 101	syl3anc	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) ) with typecode |-
103	99 102	mpd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y <_s xL ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y <_s xL ) with typecode |-
104		leftlt	Could not format ( xL e. ( _Left ` x ) -> xL xL
105	104	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL xL
106	105	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y xL yO yO y y yO yO y xL
107	94 97 98 103 106	leltstrd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y yO yO y y yO yO y y
108	107	rexlimdvaa	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) -> y yO yO y y yO yO y ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) -> y
109		simpll2	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) with typecode |-
110		leftno	Could not format ( zL e. ( _Left ` z ) -> zL e. No ) : No typesetting found for |- ( zL e. ( _Left ` z ) -> zL e. No ) with typecode |-
111	110	adantr	Could not format ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL e. No ) : No typesetting found for |- ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL e. No ) with typecode |-
112	111	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. No ) with typecode |-
113	109 112	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zL ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zL ) e. No ) with typecode |-
114		simpll3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) with typecode |-
115	109 114	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) e. No ) with typecode |-
116		simpll1	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) with typecode |-
117	116 112	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s zL ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s zL ) e. No ) with typecode |-
118		leftlt	Could not format ( zL e. ( _Left ` z ) -> zL zL
119	118	adantr	Could not format ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL zL
120	119	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL yO yO y y yO yO y zL
121		ltadds2im	Could not format ( ( zL e. No /\ z e. No /\ y e. No ) -> ( zL ( y +s zL ) ( zL ( y +s zL )
122	112 114 109 121	syl3anc	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( zL ( y +s zL ) yO yO y y yO yO y ( zL ( y +s zL )
123	120 122	mpd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zL ) yO yO y y yO yO y ( y +s zL )
124		simprr	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) <_s ( x +s zL ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s z ) <_s ( x +s zL ) ) with typecode |-
125	113 115 117 123 124	ltlestrd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zL ) yO yO y y yO yO y ( y +s zL )
126		oveq2	Could not format ( zO = zL -> ( y +s zO ) = ( y +s zL ) ) : No typesetting found for |- ( zO = zL -> ( y +s zO ) = ( y +s zL ) ) with typecode |-
127		oveq2	Could not format ( zO = zL -> ( x +s zO ) = ( x +s zL ) ) : No typesetting found for |- ( zO = zL -> ( x +s zO ) = ( x +s zL ) ) with typecode |-
128	126 127	breq12d	Could not format ( zO = zL -> ( ( y +s zO ) ( y +s zL ) ( ( y +s zO ) ( y +s zL )
129	128	imbi1d	Could not format ( zO = zL -> ( ( ( y +s zO ) y ( ( y +s zL ) y ( ( ( y +s zO ) y ( ( y +s zL ) y
130		simplr3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO ) y yO yO y y yO yO y A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO ) y
131		simprl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. ( _Left ` z ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. ( _Left ` z ) ) with typecode |-
132		elun1	Could not format ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
133	131 132	syl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
134	129 130 133	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s zL ) y yO yO y y yO yO y ( ( y +s zL ) y
135	125 134	mpd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y yO yO y y yO yO y y
136	135	rexlimdvaa	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) -> y yO yO y y yO yO y ( E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) -> y
137	108 136	jaod	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) -> y yO yO y y yO yO y ( ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) -> y
138	93 137	biimtrid	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p -> y yO yO y y yO yO y ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p -> y
139		rexun	Could not format ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) ) with typecode |-
140		eqeq1	Could not format ( c = q -> ( c = ( yR +s z ) <-> q = ( yR +s z ) ) ) : No typesetting found for |- ( c = q -> ( c = ( yR +s z ) <-> q = ( yR +s z ) ) ) with typecode |-
141	140	rexbidv	Could not format ( c = q -> ( E. yR e. ( _Right ` y ) c = ( yR +s z ) <-> E. yR e. ( _Right ` y ) q = ( yR +s z ) ) ) : No typesetting found for |- ( c = q -> ( E. yR e. ( _Right ` y ) c = ( yR +s z ) <-> E. yR e. ( _Right ` y ) q = ( yR +s z ) ) ) with typecode |-
142	141	rexab	Could not format ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) with typecode |-
143		rexcom4	Could not format ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) with typecode |-
144		r19.41v	Could not format ( E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) with typecode |-
145	144	exbii	Could not format ( E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) with typecode |-
146	143 145	bitri	Could not format ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) ) with typecode |-
147		ovex	Could not format ( yR +s z ) e. _V : No typesetting found for |- ( yR +s z ) e. _V with typecode |-
148		breq1	Could not format ( q = ( yR +s z ) -> ( q <_s ( x +s z ) <-> ( yR +s z ) <_s ( x +s z ) ) ) : No typesetting found for |- ( q = ( yR +s z ) -> ( q <_s ( x +s z ) <-> ( yR +s z ) <_s ( x +s z ) ) ) with typecode |-
149	147 148	ceqsexv	Could not format ( E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( yR +s z ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( yR +s z ) <_s ( x +s z ) ) with typecode |-
150	149	rexbii	Could not format ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) : No typesetting found for |- ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) with typecode |-
151	146 150	bitr3i	Could not format ( E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) with typecode |-
152	142 151	bitri	Could not format ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) ) with typecode |-
153		eqeq1	Could not format ( d = q -> ( d = ( y +s zR ) <-> q = ( y +s zR ) ) ) : No typesetting found for |- ( d = q -> ( d = ( y +s zR ) <-> q = ( y +s zR ) ) ) with typecode |-
154	153	rexbidv	Could not format ( d = q -> ( E. zR e. ( _Right ` z ) d = ( y +s zR ) <-> E. zR e. ( _Right ` z ) q = ( y +s zR ) ) ) : No typesetting found for |- ( d = q -> ( E. zR e. ( _Right ` z ) d = ( y +s zR ) <-> E. zR e. ( _Right ` z ) q = ( y +s zR ) ) ) with typecode |-
155	154	rexab	Could not format ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) with typecode |-
156		rexcom4	Could not format ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) with typecode |-
157		r19.41v	Could not format ( E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) with typecode |-
158	157	exbii	Could not format ( E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) with typecode |-
159	156 158	bitri	Could not format ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) ) with typecode |-
160		ovex	Could not format ( y +s zR ) e. _V : No typesetting found for |- ( y +s zR ) e. _V with typecode |-
161		breq1	Could not format ( q = ( y +s zR ) -> ( q <_s ( x +s z ) <-> ( y +s zR ) <_s ( x +s z ) ) ) : No typesetting found for |- ( q = ( y +s zR ) -> ( q <_s ( x +s z ) <-> ( y +s zR ) <_s ( x +s z ) ) ) with typecode |-
162	160 161	ceqsexv	Could not format ( E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( y +s zR ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( y +s zR ) <_s ( x +s z ) ) with typecode |-
163	162	rexbii	Could not format ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) : No typesetting found for |- ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) with typecode |-
164	159 163	bitr3i	Could not format ( E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) with typecode |-
165	155 164	bitri	Could not format ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) : No typesetting found for |- ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) with typecode |-
166	152 165	orbi12i	Could not format ( ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) ) : No typesetting found for |- ( ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) ) with typecode |-
167	139 166	bitri	Could not format ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) ) : No typesetting found for |- ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) ) with typecode |-
168		simpll2	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) with typecode |-
169		rightno	Could not format ( yR e. ( _Right ` y ) -> yR e. No ) : No typesetting found for |- ( yR e. ( _Right ` y ) -> yR e. No ) with typecode |-
170	169	adantr	Could not format ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> yR e. No ) : No typesetting found for |- ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> yR e. No ) with typecode |-
171	170	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y yR e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y yR e. No ) with typecode |-
172		simpll1	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) with typecode |-
173		rightgt	Could not format ( yR e. ( _Right ` y ) -> y y
174	173	adantr	Could not format ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> y y
175	174	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y yO yO y y yO yO y y
176		simprr	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( yR +s z ) <_s ( x +s z ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( yR +s z ) <_s ( x +s z ) ) with typecode |-
177		simpll3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) with typecode |-
178		leadds1im	Could not format ( ( yR e. No /\ x e. No /\ z e. No ) -> ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) ) : No typesetting found for |- ( ( yR e. No /\ x e. No /\ z e. No ) -> ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) ) with typecode |-
179	171 172 177 178	syl3anc	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) ) with typecode |-
180	176 179	mpd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y yR <_s x ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y yR <_s x ) with typecode |-
181	168 171 172 175 180	ltlestrd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y yO yO y y yO yO y y
182	181	rexlimdvaa	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) -> y yO yO y y yO yO y ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) -> y
183		simpll2	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y e. No ) with typecode |-
184		rightno	Could not format ( zR e. ( _Right ` z ) -> zR e. No ) : No typesetting found for |- ( zR e. ( _Right ` z ) -> zR e. No ) with typecode |-
185	184	adantr	Could not format ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> zR e. No ) : No typesetting found for |- ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> zR e. No ) with typecode |-
186	185	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. No ) with typecode |-
187	183 186	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zR ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zR ) e. No ) with typecode |-
188		simpll1	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y x e. No ) with typecode |-
189		simpll3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z e. No ) with typecode |-
190	188 189	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s z ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s z ) e. No ) with typecode |-
191	188 186	addscld	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s zR ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s zR ) e. No ) with typecode |-
192		simprr	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zR ) <_s ( x +s z ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zR ) <_s ( x +s z ) ) with typecode |-
193	189 186 188	3jca	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( z e. No /\ zR e. No /\ x e. No ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( z e. No /\ zR e. No /\ x e. No ) ) with typecode |-
194		rightgt	Could not format ( zR e. ( _Right ` z ) -> z z
195	194	adantr	Could not format ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> z z
196	195	adantl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y z yO yO y y yO yO y z
197		ltadds2im	Could not format ( ( z e. No /\ zR e. No /\ x e. No ) -> ( z ( x +s z ) ( z ( x +s z )
198	193 196 197	sylc	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( x +s z ) yO yO y y yO yO y ( x +s z )
199	187 190 191 192 198	leltstrd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( y +s zR ) yO yO y y yO yO y ( y +s zR )
200		oveq2	Could not format ( zO = zR -> ( y +s zO ) = ( y +s zR ) ) : No typesetting found for |- ( zO = zR -> ( y +s zO ) = ( y +s zR ) ) with typecode |-
201		oveq2	Could not format ( zO = zR -> ( x +s zO ) = ( x +s zR ) ) : No typesetting found for |- ( zO = zR -> ( x +s zO ) = ( x +s zR ) ) with typecode |-
202	200 201	breq12d	Could not format ( zO = zR -> ( ( y +s zO ) ( y +s zR ) ( ( y +s zO ) ( y +s zR )
203	202	imbi1d	Could not format ( zO = zR -> ( ( ( y +s zO ) y ( ( y +s zR ) y ( ( ( y +s zO ) y ( ( y +s zR ) y
204		simplr3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO ) y yO yO y y yO yO y A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO ) y
205		simprl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. ( _Right ` z ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. ( _Right ` z ) ) with typecode |-
206		elun2	Could not format ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
207	205 206	syl	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
208	203 204 207	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s zR ) y yO yO y y yO yO y ( ( y +s zR ) y
209	199 208	mpd	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y y yO yO y y yO yO y y
210	209	rexlimdvaa	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) -> y yO yO y y yO yO y ( E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) -> y
211	182 210	jaod	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) -> y yO yO y y yO yO y ( ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) -> y
212	167 211	biimtrid	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) -> y yO yO y y yO yO y ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) -> y
213	138 212	jaod	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) -> y yO yO y y yO yO y ( ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) -> y
214	64 213	sylbid	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) y yO yO y y yO yO y ( ( y +s z ) y
215	214	ex	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) y ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO ) yO yO y y yO yO y ( ( y +s z ) y
216	4 8 12 16 20 22 25 29 33 37 215	no3inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\left(B{+}_{s}C\right){<}_s\left(A{+}_{s}C\right)\to B{<}_{s}A\right)$$
217		addscl	$$⊢\left(B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to B{+}_{s}C\in \mathrm{No}$$
218	217	3adant1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to B{+}_{s}C\in \mathrm{No}$$
219		addscl	$$⊢\left(A\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{+}_{s}C\in \mathrm{No}$$
220	219	3adant2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{+}_{s}C\in \mathrm{No}$$
221		ltnles	$$⊢\left(B{+}_{s}C\in \mathrm{No}\wedge A{+}_{s}C\in \mathrm{No}\right)\to \left(\left(B{+}_{s}C\right){<}_s\left(A{+}_{s}C\right)\leftrightarrow \neg \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\right)$$
222	218 220 221	syl2anc	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\left(B{+}_{s}C\right){<}_s\left(A{+}_{s}C\right)\leftrightarrow \neg \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\right)$$
223		ltnles	$$⊢\left(B\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(B{<}_{s}A\leftrightarrow \neg A{\le }_{s}B\right)$$
224	223	ancoms	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(B{<}_{s}A\leftrightarrow \neg A{\le }_{s}B\right)$$
225	224	3adant3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(B{<}_{s}A\leftrightarrow \neg A{\le }_{s}B\right)$$
226	216 222 225	3imtr3d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\neg \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\to \neg A{\le }_{s}B\right)$$
227	226	con4d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A{\le }_{s}B\to \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\right)$$
228		leadds1im	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\to A{\le }_{s}B\right)$$
229	227 228	impbid	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A{\le }_{s}B\leftrightarrow \left(A{+}_{s}C\right){\le }_s\left(B{+}_{s}C\right)\right)$$