Theorem precsexlem9

Description: Lemma for surreal reciprocal. Show that the product of A and a left element is less than one and the product of A and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025)

	Ref	Expression
Hypotheses	precsexlem.1	No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
	precsexlem.2	$$⊢L=1^{st}\circ F$$
	precsexlem.3	$$⊢R=2^{nd}\circ F$$
	precsexlem.4	$$⊢\phi \to A\in \mathrm{No}$$
	precsexlem.5	No typesetting found for |- ( ph -> 0s
	precsexlem.6	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
Assertion	precsexlem9	Could not format assertion : No typesetting found for |- ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b )

Proof

Step	Hyp	Ref	Expression
1		precsexlem.1	Could not format F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
2		precsexlem.2	$$⊢L=1^{st}\circ F$$
3		precsexlem.3	$$⊢R=2^{nd}\circ F$$
4		precsexlem.4	$$⊢\phi \to A\in \mathrm{No}$$
5		precsexlem.5	Could not format ( ph -> 0s 0s
6		precsexlem.6	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
7		fveq2	$$⊢i=\varnothing \to L\left(i\right)=L\left(\varnothing \right)$$
8	7	raleqdv	Could not format ( i = (/) -> ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` (/) ) ( A x.s b ) ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` (/) ) ( A x.s b )
9		fveq2	$$⊢i=\varnothing \to R\left(i\right)=R\left(\varnothing \right)$$
10	9	raleqdv	Could not format ( i = (/) -> ( A. c e. ( R ` i ) 1s A. c e. ( R ` (/) ) 1s ( A. c e. ( R ` i ) 1s A. c e. ( R ` (/) ) 1s
11	8 10	anbi12d	Could not format ( i = (/) -> ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` (/) ) ( A x.s b ) ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` (/) ) ( A x.s b )
12	11	imbi2d	Could not format ( i = (/) -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` (/) ) ( A x.s b ) ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` (/) ) ( A x.s b )
13		fveq2	$$⊢i=j\to L\left(i\right)=L\left(j\right)$$
14	13	raleqdv	Could not format ( i = j -> ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` j ) ( A x.s b ) ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` j ) ( A x.s b )
15		fveq2	$$⊢i=j\to R\left(i\right)=R\left(j\right)$$
16	15	raleqdv	Could not format ( i = j -> ( A. c e. ( R ` i ) 1s A. c e. ( R ` j ) 1s ( A. c e. ( R ` i ) 1s A. c e. ( R ` j ) 1s
17	14 16	anbi12d	Could not format ( i = j -> ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` j ) ( A x.s b ) ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` j ) ( A x.s b )
18	17	imbi2d	Could not format ( i = j -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` j ) ( A x.s b ) ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` j ) ( A x.s b )
19		fveq2	$$⊢i=\mathrm{suc}j\to L\left(i\right)=L\left(\mathrm{suc}j\right)$$
20	19	raleqdv	Could not format ( i = suc j -> ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` suc j ) ( A x.s b ) ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` suc j ) ( A x.s b )
21		fveq2	$$⊢i=\mathrm{suc}j\to R\left(i\right)=R\left(\mathrm{suc}j\right)$$
22	21	raleqdv	Could not format ( i = suc j -> ( A. c e. ( R ` i ) 1s A. c e. ( R ` suc j ) 1s ( A. c e. ( R ` i ) 1s A. c e. ( R ` suc j ) 1s
23	20 22	anbi12d	Could not format ( i = suc j -> ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` suc j ) ( A x.s b ) ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` suc j ) ( A x.s b )
24		oveq2	Could not format ( b = r -> ( A x.s b ) = ( A x.s r ) ) : No typesetting found for |- ( b = r -> ( A x.s b ) = ( A x.s r ) ) with typecode |-
25	24	breq1d	Could not format ( b = r -> ( ( A x.s b ) ( A x.s r ) ( ( A x.s b ) ( A x.s r )
26	25	cbvralvw	Could not format ( A. b e. ( L ` suc j ) ( A x.s b ) A. r e. ( L ` suc j ) ( A x.s r ) A. r e. ( L ` suc j ) ( A x.s r )
27		oveq2	Could not format ( c = s -> ( A x.s c ) = ( A x.s s ) ) : No typesetting found for |- ( c = s -> ( A x.s c ) = ( A x.s s ) ) with typecode |-
28	27	breq2d	Could not format ( c = s -> ( 1s 1s ( 1s 1s
29	28	cbvralvw	Could not format ( A. c e. ( R ` suc j ) 1s A. s e. ( R ` suc j ) 1s A. s e. ( R ` suc j ) 1s
30	26 29	anbi12i	Could not format ( ( A. b e. ( L ` suc j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r ) ( A. r e. ( L ` suc j ) ( A x.s r )
31	23 30	bitrdi	Could not format ( i = suc j -> ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r ) ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r )
32	31	imbi2d	Could not format ( i = suc j -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r ) ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r )
33		fveq2	$$⊢i=I\to L\left(i\right)=L\left(I\right)$$
34	33	raleqdv	Could not format ( i = I -> ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` I ) ( A x.s b ) ( A. b e. ( L ` i ) ( A x.s b ) A. b e. ( L ` I ) ( A x.s b )
35		fveq2	$$⊢i=I\to R\left(i\right)=R\left(I\right)$$
36	35	raleqdv	Could not format ( i = I -> ( A. c e. ( R ` i ) 1s A. c e. ( R ` I ) 1s ( A. c e. ( R ` i ) 1s A. c e. ( R ` I ) 1s
37	34 36	anbi12d	Could not format ( i = I -> ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` I ) ( A x.s b ) ( ( A. b e. ( L ` i ) ( A x.s b ) ( A. b e. ( L ` I ) ( A x.s b )
38	37	imbi2d	Could not format ( i = I -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` I ) ( A x.s b ) ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b ) ( ph -> ( A. b e. ( L ` I ) ( A x.s b )
39		muls01	Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-
40	4 39	syl	Could not format ( ph -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( A x.s 0s ) = 0s ) with typecode |-
41		0slt1s	Could not format 0s
42	40 41	eqbrtrdi	Could not format ( ph -> ( A x.s 0s ) ( A x.s 0s )
43	1 2 3	precsexlem1	Could not format ( L ` (/) ) = { 0s } : No typesetting found for |- ( L ` (/) ) = { 0s } with typecode |-
44	43	raleqi	Could not format ( A. b e. ( L ` (/) ) ( A x.s b ) A. b e. { 0s } ( A x.s b ) A. b e. { 0s } ( A x.s b )
45		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
46	45	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
47		oveq2	Could not format ( b = 0s -> ( A x.s b ) = ( A x.s 0s ) ) : No typesetting found for |- ( b = 0s -> ( A x.s b ) = ( A x.s 0s ) ) with typecode |-
48	47	breq1d	Could not format ( b = 0s -> ( ( A x.s b ) ( A x.s 0s ) ( ( A x.s b ) ( A x.s 0s )
49	46 48	ralsn	Could not format ( A. b e. { 0s } ( A x.s b ) ( A x.s 0s ) ( A x.s 0s )
50	44 49	bitri	Could not format ( A. b e. ( L ` (/) ) ( A x.s b ) ( A x.s 0s ) ( A x.s 0s )
51	42 50	sylibr	Could not format ( ph -> A. b e. ( L ` (/) ) ( A x.s b ) A. b e. ( L ` (/) ) ( A x.s b )
52		ral0	Could not format A. c e. (/) 1s
53	1 2 3	precsexlem2	$$⊢R\left(\varnothing \right)=\varnothing$$
54	53	raleqi	Could not format ( A. c e. ( R ` (/) ) 1s A. c e. (/) 1s A. c e. (/) 1s
55	52 54	mpbir	Could not format A. c e. ( R ` (/) ) 1s
56	51 55	jctir	Could not format ( ph -> ( A. b e. ( L ` (/) ) ( A x.s b ) ( A. b e. ( L ` (/) ) ( A x.s b )
57	1 2 3	precsexlem4	Could not format ( j e. _om -> ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
58	57	3ad2ant2	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
59	58	eleq2d	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` suc j ) <-> r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` suc j ) <-> r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
60		elun	Could not format ( r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
61		elun	Could not format ( r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
62		vex	$$⊢r\in \mathrm{V}$$
63		eqeq1	Could not format ( a = r -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = r -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
64	63	2rexbidv	Could not format ( a = r -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = r -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
65	62 64	elab	Could not format ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for |- ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode |-
66		eqeq1	Could not format ( a = r -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( a = r -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
67	66	2rexbidv	Could not format ( a = r -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
68	62 67	elab	Could not format ( r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
69	65 68	orbi12i	Could not format ( ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
70	61 69	bitri	Could not format ( r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
71	70	orbi2i	Could not format ( ( r e. ( L ` j ) \/ r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
72	60 71	bitri	Could not format ( r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
73	59 72	bitrdi	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` suc j ) <-> ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( r e. ( L ` suc j ) <-> ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
74		simp3l	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. b e. ( L ` j ) ( A x.s b ) A. b e. ( L ` j ) ( A x.s b )
75	25	rspccv	Could not format ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` j ) -> ( A x.s r ) ( r e. ( L ` j ) -> ( A x.s r )
76	74 75	syl	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` j ) -> ( A x.s r ) ( r e. ( L ` j ) -> ( A x.s r )
77	4	3ad2ant1	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
78	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
79		1sno	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
80	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) with typecode |-
81		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
82	81	sseli	Could not format ( xR e. ( _Right ` A ) -> xR e. No ) : No typesetting found for |- ( xR e. ( _Right ` A ) -> xR e. No ) with typecode |-
83	82	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) with typecode |-
84	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
85	83 84	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) with typecode |-
86	85	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) with typecode |-
87	1 2 3 4 5 6	precsexlem8	$$⊢\left(\phi \wedge j\in \mathrm{\omega }\right)\to \left(L\left(j\right)\subseteq \mathrm{No}\wedge R\left(j\right)\subseteq \mathrm{No}\right)$$
88	87	simpld	$$⊢\left(\phi \wedge j\in \mathrm{\omega }\right)\to L\left(j\right)\subseteq \mathrm{No}$$
89	88	3adant3	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( L ` j ) C_ No ) : No typesetting found for |- ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( L ` j ) C_ No ) with typecode |-
90	89	sselda	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) with typecode |-
91	90	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) with typecode |-
92	86 91	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s yL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s yL ) e. No ) with typecode |-
93	80 92	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xR -s A ) x.s yL ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xR -s A ) x.s yL ) ) e. No ) with typecode |-
94	83	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) with typecode |-
95	45	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s e. No ) with typecode |-
96	5	3ad2ant1	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
97	96	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
98		breq2	Could not format ( xO = xR -> ( A A ( A A
99		rightval	Could not format ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
100	98 99	elrab2	Could not format ( xR e. ( _Right ` A ) <-> ( xR e. ( _Old ` ( bday ` A ) ) /\ A ( xR e. ( _Old ` ( bday ` A ) ) /\ A
101	100	simprbi	Could not format ( xR e. ( _Right ` A ) -> A A
102	101	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A A
103	95 84 83 97 102	slttrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
104	103	sgt0ne0d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) with typecode |-
105	104	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) with typecode |-
106		breq2	Could not format ( xO = xR -> ( 0s 0s ( 0s 0s
107		oveq1	Could not format ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) ) : No typesetting found for |- ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) ) with typecode |-
108	107	eqeq1d	Could not format ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) ) : No typesetting found for |- ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) ) with typecode |-
109	108	rexbidv	Could not format ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) ) : No typesetting found for |- ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) ) with typecode |-
110	106 109	imbi12d	Could not format ( xO = xR -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( xR x.s y ) = 1s ) ) ) : No typesetting found for |- ( xO = xR -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( xR x.s y ) = 1s ) ) ) with typecode |-
111	6	3ad2ant1	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
112	111	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
113		elun2	Could not format ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
114	113	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
115	110 112 114	rspcdva	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 0s E. y e. No ( xR x.s y ) = 1s ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 0s E. y e. No ( xR x.s y ) = 1s ) ) with typecode |-
116	103 115	mpd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) with typecode |-
117	116	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) with typecode |-
118	78 93 94 105 117	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
119		oveq2	Could not format ( b = yL -> ( A x.s b ) = ( A x.s yL ) ) : No typesetting found for |- ( b = yL -> ( A x.s b ) = ( A x.s yL ) ) with typecode |-
120	119	breq1d	Could not format ( b = yL -> ( ( A x.s b ) ( A x.s yL ) ( ( A x.s b ) ( A x.s yL )
121	120	rspccva	Could not format ( ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) ( A x.s yL )
122	74 121	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) ( A x.s yL )
123	122	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) ( A x.s yL )
124	78 91	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) e. No ) with typecode |-
125	84 83	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A 0s ( A 0s
126	102 125	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
127	126	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
128	124 80 86 127	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s yL ) ( ( xR -s A ) x.s ( A x.s yL ) ) ( ( A x.s yL ) ( ( xR -s A ) x.s ( A x.s yL ) )
129	123 128	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yL ) ) ( ( xR -s A ) x.s ( A x.s yL ) )
130	86	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) with typecode |-
131	129 130	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yL ) ) ( ( xR -s A ) x.s ( A x.s yL ) )
132	86 124	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yL ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yL ) ) e. No ) with typecode |-
133	78 132 94	sltaddsub2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ( ( xR -s A ) x.s ( A x.s yL ) ) ( ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ( ( xR -s A ) x.s ( A x.s yL ) )
134	131 133	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) )
135	78 80 92	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) ) with typecode |-
136	78	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) with typecode |-
137	78 86 91	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yL ) ) = ( ( xR -s A ) x.s ( A x.s yL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yL ) ) = ( ( xR -s A ) x.s ( A x.s yL ) ) ) with typecode |-
138	136 137	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) with typecode |-
139	135 138	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) with typecode |-
140	94	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xR ) = xR ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xR ) = xR ) with typecode |-
141	134 139 140	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )
142	78 93	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) e. No ) with typecode |-
143	103	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
144	142 80 94 143 117	sltdivmul2wd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) ( ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )
145	141 144	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR )
146	118 145	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
147		oveq2	Could not format ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
148	147	breq1d	Could not format ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( ( A x.s r ) ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ( ( A x.s r ) ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
149	146 148	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )
150	149	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )
151	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
152	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) with typecode |-
153		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
154		elrabi	Could not format ( xL e. { x e. ( _Left ` A ) | 0s xL e. ( _Left ` A ) ) : No typesetting found for |- ( xL e. { x e. ( _Left ` A ) | 0s xL e. ( _Left ` A ) ) with typecode |-
155	154	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. ( _Left ` A ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. ( _Left ` A ) ) with typecode |-
156	153 155	sselid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) with typecode |-
157	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
158	156 157	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) with typecode |-
159	158	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) with typecode |-
160	87	simprd	$$⊢\left(\phi \wedge j\in \mathrm{\omega }\right)\to R\left(j\right)\subseteq \mathrm{No}$$
161	160	3adant3	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( R ` j ) C_ No ) : No typesetting found for |- ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( R ` j ) C_ No ) with typecode |-
162	161	sselda	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) with typecode |-
163	162	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) with typecode |-
164	159 163	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s yR ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s yR ) e. No ) with typecode |-
165	152 164	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xL -s A ) x.s yR ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xL -s A ) x.s yR ) ) e. No ) with typecode |-
166	156	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) with typecode |-
167		breq2	Could not format ( x = xL -> ( 0s 0s ( 0s 0s
168	167	elrab	Could not format ( xL e. { x e. ( _Left ` A ) | 0s ( xL e. ( _Left ` A ) /\ 0s ( xL e. ( _Left ` A ) /\ 0s
169	168	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) | 0s 0s 0s
170	169	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
171	170	sgt0ne0d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) with typecode |-
172	171	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) with typecode |-
173		breq2	Could not format ( xO = xL -> ( 0s 0s ( 0s 0s
174		oveq1	Could not format ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) ) : No typesetting found for |- ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) ) with typecode |-
175	174	eqeq1d	Could not format ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) ) : No typesetting found for |- ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) ) with typecode |-
176	175	rexbidv	Could not format ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) ) : No typesetting found for |- ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) ) with typecode |-
177	173 176	imbi12d	Could not format ( xO = xL -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( xL x.s y ) = 1s ) ) ) : No typesetting found for |- ( xO = xL -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( xL x.s y ) = 1s ) ) ) with typecode |-
178	111	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
179		elun1	Could not format ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
180	155 179	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
181	177 178 180	rspcdva	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 0s E. y e. No ( xL x.s y ) = 1s ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 0s E. y e. No ( xL x.s y ) = 1s ) ) with typecode |-
182	170 181	mpd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) with typecode |-
183	182	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) with typecode |-
184	151 165 166 172 183	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
185	157 156	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) with typecode |-
186	185	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) with typecode |-
187	186	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) with typecode |-
188		simp3r	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. c e. ( R ` j ) 1s A. c e. ( R ` j ) 1s
189		oveq2	Could not format ( c = yR -> ( A x.s c ) = ( A x.s yR ) ) : No typesetting found for |- ( c = yR -> ( A x.s c ) = ( A x.s yR ) ) with typecode |-
190	189	breq2d	Could not format ( c = yR -> ( 1s 1s ( 1s 1s
191	190	rspccva	Could not format ( ( A. c e. ( R ` j ) 1s 1s 1s
192	188 191	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
193	192	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
194	151 163	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yR ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yR ) e. No ) with typecode |-
195		breq1	Could not format ( xO = xL -> ( xO xL ( xO xL
196		leftval	Could not format ( _Left ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | xO
197	195 196	elrab2	Could not format ( xL e. ( _Left ` A ) <-> ( xL e. ( _Old ` ( bday ` A ) ) /\ xL ( xL e. ( _Old ` ( bday ` A ) ) /\ xL
198	197	simprbi	Could not format ( xL e. ( _Left ` A ) -> xL xL
199	155 198	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL xL
200	156 157	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL 0s ( xL 0s
201	199 200	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
202	201	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
203	152 194 186 202	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s ( ( A -s xL ) x.s 1s ) ( 1s ( ( A -s xL ) x.s 1s )
204	193 203	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s 1s ) ( ( A -s xL ) x.s 1s )
205	187 204	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) ( A -s xL )
206	156 157	negsubsdi2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode |-
207	206	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode |-
208	159 194	mulnegs1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode |-
209	206	oveq1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode |-
210	209	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode |-
211	208 210	eqtr3d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode |-
212	205 207 211	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) ( -us ` ( xL -s A ) )
213	159 194	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s ( A x.s yR ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s ( A x.s yR ) ) e. No ) with typecode |-
214	213 159	sltnegd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( ( xL -s A ) x.s ( A x.s yR ) ) ( -us ` ( xL -s A ) ) ( ( ( xL -s A ) x.s ( A x.s yR ) ) ( -us ` ( xL -s A ) )
215	212 214	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s ( A x.s yR ) ) ( ( xL -s A ) x.s ( A x.s yR ) )
216	151 213 166	sltaddsub2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ( ( xL -s A ) x.s ( A x.s yR ) ) ( ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ( ( xL -s A ) x.s ( A x.s yR ) )
217	215 216	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) )
218	151 152 164	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) ) with typecode |-
219	151	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) with typecode |-
220	151 159 163	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yR ) ) = ( ( xL -s A ) x.s ( A x.s yR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yR ) ) = ( ( xL -s A ) x.s ( A x.s yR ) ) ) with typecode |-
221	219 220	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode |-
222	218 221	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode |-
223	166	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL x.s 1s ) = xL ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL x.s 1s ) = xL ) with typecode |-
224	217 222 223	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )
225	151 165	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) e. No ) with typecode |-
226	170	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
227	225 152 166 226 183	sltdivmulwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) ( ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )
228	224 227	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL )
229	184 228	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )
230		oveq2	Could not format ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
231	230	breq1d	Could not format ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( ( A x.s r ) ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ( ( A x.s r ) ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )
232	229 231	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r )
233	232	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r ) ( E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r )
234	150 233	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r ) ( ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r )
235	76 234	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r ) ( ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s ( A x.s r )
236	73 235	sylbid	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` suc j ) -> ( A x.s r ) ( r e. ( L ` suc j ) -> ( A x.s r )
237	236	ralrimiv	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. r e. ( L ` suc j ) ( A x.s r ) A. r e. ( L ` suc j ) ( A x.s r )
238	1 2 3	precsexlem5	Could not format ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
239	238	3ad2ant2	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
240	239	eleq2d	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s e. ( R ` suc j ) <-> s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` suc j ) <-> s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
241		elun	Could not format ( s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
242		elun	Could not format ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
243		vex	$$⊢s\in \mathrm{V}$$
244		eqeq1	Could not format ( a = s -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for |- ( a = s -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode |-
245	244	2rexbidv	Could not format ( a = s -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
246	243 245	elab	Could not format ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
247		eqeq1	Could not format ( a = s -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = s -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
248	247	2rexbidv	Could not format ( a = s -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = s -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
249	243 248	elab	Could not format ( s e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for |- ( s e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode |-
250	246 249	orbi12i	Could not format ( ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s
251	242 250	bitri	Could not format ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s
252	251	orbi2i	Could not format ( ( s e. ( R ` j ) \/ s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
253	241 252	bitri	Could not format ( s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
254	240 253	bitrdi	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s e. ( R ` suc j ) <-> ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s ( s e. ( R ` suc j ) <-> ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
255	28	rspccv	Could not format ( A. c e. ( R ` j ) 1s ( s e. ( R ` j ) -> 1s ( s e. ( R ` j ) -> 1s
256	188 255	syl	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s e. ( R ` j ) -> 1s ( s e. ( R ` j ) -> 1s
257	122	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) ( A x.s yL )
258	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
259	90	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yL e. No ) with typecode |-
260	258 259	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yL ) e. No ) with typecode |-
261	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) with typecode |-
262	185	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A -s xL ) e. No ) with typecode |-
263	201	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
264	260 261 262 263	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s yL ) ( ( A -s xL ) x.s ( A x.s yL ) ) ( ( A x.s yL ) ( ( A -s xL ) x.s ( A x.s yL ) )
265	257 264	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s ( A x.s yL ) ) ( ( A -s xL ) x.s ( A x.s yL ) )
266	262	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) with typecode |-
267	265 266	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A -s xL ) x.s ( A x.s yL ) ) ( ( A -s xL ) x.s ( A x.s yL ) )
268	158	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) e. No ) with typecode |-
269	268 260	mulnegs1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode |-
270	206	oveq1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode |-
271	270	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode |-
272	269 271	eqtr3d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode |-
273	206	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode |-
274	267 272 273	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )
275	268 260	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s ( A x.s yL ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s ( A x.s yL ) ) e. No ) with typecode |-
276	268 275	sltnegd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ( ( xL -s A ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )
277	274 276	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xL -s A ) ( xL -s A )
278	156	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL e. No ) with typecode |-
279	278 258 275	sltsubadd2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) xL ( ( xL -s A ) xL
280	277 279	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL xL
281	278	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xL ) = xL ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xL ) = xL ) with typecode |-
282	268 259	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s yL ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xL -s A ) x.s yL ) e. No ) with typecode |-
283	258 261 282	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) ) with typecode |-
284	258	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) with typecode |-
285	258 268 259	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yL ) ) = ( ( xL -s A ) x.s ( A x.s yL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yL ) ) = ( ( xL -s A ) x.s ( A x.s yL ) ) ) with typecode |-
286	284 285	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode |-
287	283 286	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode |-
288	280 281 287	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xL ) ( 1s x.s xL )
289	261 282	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xL -s A ) x.s yL ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xL -s A ) x.s yL ) ) e. No ) with typecode |-
290	258 289	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) e. No ) with typecode |-
291	170	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
292	182	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xL x.s y ) = 1s ) with typecode |-
293	261 290 278 291 292	sltmuldivwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( 1s x.s xL ) 1s ( ( 1s x.s xL ) 1s
294	288 293	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
295	171	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xL =/= 0s ) with typecode |-
296	258 289 278 295 292	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode |-
297	294 296	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
298		oveq2	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for |- ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode |-
299	298	breq2d	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s 1s ( 1s 1s
300	297 299	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> 1s ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> 1s
301	300	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xL e. { x e. ( _Left ` A ) | 0s 1s ( E. xL e. { x e. ( _Left ` A ) | 0s 1s
302	85	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) e. No ) with typecode |-
303	302	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) with typecode |-
304	192	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
305	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s e. No ) with typecode |-
306	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A e. No ) with typecode |-
307	162	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) yR e. No ) with typecode |-
308	306 307	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yR ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s yR ) e. No ) with typecode |-
309	126	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
310	305 308 302 309	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s ( ( xR -s A ) x.s 1s ) ( 1s ( ( xR -s A ) x.s 1s )
311	304 310	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s 1s ) ( ( xR -s A ) x.s 1s )
312	303 311	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( xR -s A ) ( xR -s A )
313	83	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR e. No ) with typecode |-
314	302 308	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yR ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s ( A x.s yR ) ) e. No ) with typecode |-
315	313 306 314	sltsubadd2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) xR ( ( xR -s A ) xR
316	312 315	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR xR
317	313	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xR ) = xR ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xR ) = xR ) with typecode |-
318	302 307	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s yR ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( xR -s A ) x.s yR ) e. No ) with typecode |-
319	306 305 318	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) ) with typecode |-
320	306	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s 1s ) = A ) with typecode |-
321	306 302 307	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yR ) ) = ( ( xR -s A ) x.s ( A x.s yR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yR ) ) = ( ( xR -s A ) x.s ( A x.s yR ) ) ) with typecode |-
322	320 321	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) with typecode |-
323	319 322	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) with typecode |-
324	316 317 323	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s x.s xR ) ( 1s x.s xR )
325	305 318	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xR -s A ) x.s yR ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( 1s +s ( ( xR -s A ) x.s yR ) ) e. No ) with typecode |-
326	306 325	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) e. No ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) e. No ) with typecode |-
327	103	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 0s 0s
328	116	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) E. y e. No ( xR x.s y ) = 1s ) with typecode |-
329	305 326 313 327 328	sltmuldivwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( 1s x.s xR ) 1s ( ( 1s x.s xR ) 1s
330	324 329	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
331	104	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) xR =/= 0s ) with typecode |-
332	306 325 313 331 328	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
333	330 332	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) 1s 1s
334		oveq2	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
335	334	breq2d	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s 1s ( 1s 1s
336	333 335	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s
337	336	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s
338	301 337	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( E. xL e. { x e. ( _Left ` A ) | 0s 1s ( ( E. xL e. { x e. ( _Left ` A ) | 0s 1s
339	256 338	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s 1s ( ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s 1s
340	254 339	sylbid	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( s e. ( R ` suc j ) -> 1s ( s e. ( R ` suc j ) -> 1s
341	340	ralrimiv	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. s e. ( R ` suc j ) 1s A. s e. ( R ` suc j ) 1s
342	237 341	jca	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r ) ( A. r e. ( L ` suc j ) ( A x.s r )
343	342	3exp	Could not format ( ph -> ( j e. _om -> ( ( A. b e. ( L ` j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r ) ( j e. _om -> ( ( A. b e. ( L ` j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r )
344	343	com12	Could not format ( j e. _om -> ( ph -> ( ( A. b e. ( L ` j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r ) ( ph -> ( ( A. b e. ( L ` j ) ( A x.s b ) ( A. r e. ( L ` suc j ) ( A x.s r )
345	344	a2d	Could not format ( j e. _om -> ( ( ph -> ( A. b e. ( L ` j ) ( A x.s b ) ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r ) ( ( ph -> ( A. b e. ( L ` j ) ( A x.s b ) ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r )
346	12 18 32 38 56 345	finds	Could not format ( I e. _om -> ( ph -> ( A. b e. ( L ` I ) ( A x.s b ) ( ph -> ( A. b e. ( L ` I ) ( A x.s b )
347	346	impcom	Could not format ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b ) ( A. b e. ( L ` I ) ( A x.s b )