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