Theorem sleadd1

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	sleadd1	$$⊢\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	addscut	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		sslttr	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	addscut	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		sslttr	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	sltrecd	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		leftssno	$$⊢L\left(x\right)\subseteq \mathrm{No}$$
96	95	sseli	Could not format ( xL e. ( _Left ` x ) -> xL e. No ) : No typesetting found for |- ( xL e. ( _Left ` x ) -> xL e. No ) with typecode |-
97	96	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 |-
98	97	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 |-
99		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 |-
100		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 |-
101		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 |-
102		sleadd1im	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 |-
103	94 98 101 102	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 |-
104	100 103	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 |-
105		leftlt	Could not format ( xL e. ( _Left ` x ) -> xL xL
106	105	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL xL
107	106	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
108	94 98 99 104 107	slelttrd	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
109	108	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
110		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 |-
111		leftssno	$$⊢L\left(z\right)\subseteq \mathrm{No}$$
112	111	sseli	Could not format ( zL e. ( _Left ` z ) -> zL e. No ) : No typesetting found for |- ( zL e. ( _Left ` z ) -> zL e. No ) with typecode |-
113	112	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 |-
114	113	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 |-
115	110 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 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 |-
116		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 |-
117	110 116	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 |-
118		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 |-
119	118 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 ( 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 |-
120		leftlt	Could not format ( zL e. ( _Left ` z ) -> zL zL
121	120	adantr	Could not format ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL zL
122	121	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
123		sltadd2im	Could not format ( ( zL e. No /\ z e. No /\ y e. No ) -> ( zL ( y +s zL ) ( zL ( y +s zL )
124	114 116 110 123	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 )
125	122 124	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 )
126		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 |-
127	115 117 119 125 126	sltletrd	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 )
128		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 |-
129		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 |-
130	128 129	breq12d	Could not format ( zO = zL -> ( ( y +s zO ) ( y +s zL ) ( ( y +s zO ) ( y +s zL )
131	130	imbi1d	Could not format ( zO = zL -> ( ( ( y +s zO ) y ( ( y +s zL ) y ( ( ( y +s zO ) y ( ( y +s zL ) y
132		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
133		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 |-
134		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 |-
135	133 134	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 |-
136	131 132 135	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
137	127 136	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
138	137	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
139	109 138	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
140	93 139	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
141		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 |-
142		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 |-
143	142	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 |-
144	143	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 |-
145		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 |-
146		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 |-
147	146	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 |-
148	145 147	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 |-
149		ovex	Could not format ( yR +s z ) e. _V : No typesetting found for |- ( yR +s z ) e. _V with typecode |-
150		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 |-
151	149 150	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 |-
152	151	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 |-
153	148 152	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 |-
154	144 153	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 |-
155		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 |-
156	155	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 |-
157	156	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 |-
158		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 |-
159		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 |-
160	159	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 |-
161	158 160	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 |-
162		ovex	Could not format ( y +s zR ) e. _V : No typesetting found for |- ( y +s zR ) e. _V with typecode |-
163		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 |-
164	162 163	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 |-
165	164	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 |-
166	161 165	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 |-
167	157 166	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 |-
168	154 167	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 |-
169	141 168	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 |-
170		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 |-
171		rightssno	$$⊢R\left(y\right)\subseteq \mathrm{No}$$
172	171	sseli	Could not format ( yR e. ( _Right ` y ) -> yR e. No ) : No typesetting found for |- ( yR e. ( _Right ` y ) -> yR e. No ) with typecode |-
173	172	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 |-
174	173	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 |-
175		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 |-
176		rightgt	Could not format ( yR e. ( _Right ` y ) -> y y
177	176	adantr	Could not format ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> y y
178	177	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
179		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 |-
180		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 |-
181		sleadd1im	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 |-
182	174 175 180 181	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 |-
183	179 182	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 |-
184	170 174 175 178 183	sltletrd	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
185	184	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
186		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 |-
187		rightssno	$$⊢R\left(z\right)\subseteq \mathrm{No}$$
188	187	sseli	Could not format ( zR e. ( _Right ` z ) -> zR e. No ) : No typesetting found for |- ( zR e. ( _Right ` z ) -> zR e. No ) with typecode |-
189	188	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 |-
190	189	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 |-
191	186 190	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 |-
192		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 |-
193		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 |-
194	192 193	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 |-
195	192 190	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 |-
196		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 |-
197	193 190 192	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 |-
198		rightgt	Could not format ( zR e. ( _Right ` z ) -> z z
199	198	adantr	Could not format ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> z z
200	199	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
201		sltadd2im	Could not format ( ( z e. No /\ zR e. No /\ x e. No ) -> ( z ( x +s z ) ( z ( x +s z )
202	197 200 201	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 )
203	191 194 195 196 202	slelttrd	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 )
204		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 |-
205		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 |-
206	204 205	breq12d	Could not format ( zO = zR -> ( ( y +s zO ) ( y +s zR ) ( ( y +s zO ) ( y +s zR )
207	206	imbi1d	Could not format ( zO = zR -> ( ( ( y +s zO ) y ( ( y +s zR ) y ( ( ( y +s zO ) y ( ( y +s zR ) y
208		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
209		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 |-
210		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 |-
211	209 210	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 |-
212	207 208 211	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
213	203 212	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
214	213	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
215	185 214	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
216	169 215	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
217	140 216	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
218	64 217	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
219	218	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
220	4 8 12 16 20 22 25 29 33 37 219	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)$$
221		addscl	$$⊢\left(B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to B{+}_{s}C\in \mathrm{No}$$
222	221	3adant1	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to B{+}_{s}C\in \mathrm{No}$$
223		addscl	$$⊢\left(A\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{+}_{s}C\in \mathrm{No}$$
224	223	3adant2	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{+}_{s}C\in \mathrm{No}$$
225		sltnle	$$⊢\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)$$
226	222 224 225	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)$$
227		sltnle	$$⊢\left(B\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(B{<}_{s}A\leftrightarrow \neg A{\le }_{s}B\right)$$
228	227	ancoms	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(B{<}_{s}A\leftrightarrow \neg A{\le }_{s}B\right)$$
229	228	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)$$
230	220 226 229	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)$$
231	230	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)$$
232		sleadd1im	$$⊢\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)$$
233	231 232	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)$$