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	$⊢ φ \to A \in No$
	precsexlem.5	$⊢ φ \to 0_{s} <_{s} A$
	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	$⊢ (φ \land I \in ω) \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$

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	$⊢ φ \to A \in No$
5		precsexlem.5	$⊢ φ \to 0_{s} <_{s} A$
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 = \emptyset \to L (i) = L (\emptyset)$
8	7	raleqdv	$⊢ i = \emptyset \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s})$
9		fveq2	$⊢ i = \emptyset \to R (i) = R (\emptyset)$
10	9	raleqdv	$⊢ i = \emptyset \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))$
11	8 10	anbi12d	$⊢ i = \emptyset \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c)))$
12	11	imbi2d	$⊢ i = \emptyset \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))))$
13		fveq2	$⊢ i = j \to L (i) = L (j)$
14	13	raleqdv	$⊢ i = j \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s})$
15		fveq2	$⊢ i = j \to R (i) = R (j)$
16	15	raleqdv	$⊢ i = j \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))$
17	14 16	anbi12d	$⊢ i = j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)))$
18	17	imbi2d	$⊢ i = j \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))))$
19		fveq2	$⊢ i = suc j \to L (i) = L (suc j)$
20	19	raleqdv	$⊢ i = suc j \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s})$
21		fveq2	$⊢ i = suc j \to R (i) = R (suc j)$
22	21	raleqdv	$⊢ i = suc j \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c))$
23	20 22	anbi12d	$⊢ i = suc j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c)))$
24		oveq2	$⊢ b = r \to A \cdot_{s} b = A \cdot_{s} r$
25	24	breq1d	$⊢ b = r \to ((A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} r) <_{s} 1_{s})$
26	25	cbvralvw	$⊢ \forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s}$
27		oveq2	$⊢ c = s \to A \cdot_{s} c = A \cdot_{s} s$
28	27	breq2d	$⊢ c = s \to (1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow 1_{s} <_{s} (A \cdot_{s} s))$
29	28	cbvralvw	$⊢ \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)$
30	26 29	anbi12i	$⊢ (\forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))$
31	23 30	bitrdi	$⊢ i = suc j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)))$
32	31	imbi2d	$⊢ i = suc j \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
33		fveq2	$⊢ i = I \to L (i) = L (I)$
34	33	raleqdv	$⊢ i = I \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s})$
35		fveq2	$⊢ i = I \to R (i) = R (I)$
36	35	raleqdv	$⊢ i = I \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$
37	34 36	anbi12d	$⊢ i = I \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c)))$
38	37	imbi2d	$⊢ i = I \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))))$
39		muls01	$⊢ A \in No \to A \cdot_{s} 0_{s} = 0_{s}$
40	4 39	syl	$⊢ φ \to A \cdot_{s} 0_{s} = 0_{s}$
41		0lt1s	$⊢ 0_{s} <_{s} 1_{s}$
42	40 41	eqbrtrdi	$⊢ φ \to (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
43	1 2 3	precsexlem1	$⊢ L (\emptyset) = \{0_{s}\}$
44	43	raleqi	$⊢ \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in \{0_{s}\} (A \cdot_{s} b) <_{s} 1_{s}$
45		0no	$⊢ 0_{s} \in No$
46	45	elexi	$⊢ 0_{s} \in V$
47		oveq2	$⊢ b = 0_{s} \to A \cdot_{s} b = A \cdot_{s} 0_{s}$
48	47	breq1d	$⊢ b = 0_{s} \to ((A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s})$
49	46 48	ralsn	$⊢ \forall b \in \{0_{s}\} (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
50	44 49	bitri	$⊢ \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
51	42 50	sylibr	$⊢ φ \to \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s}$
52		ral0	$⊢ \forall c \in \emptyset 1_{s} <_{s} (A \cdot_{s} c)$
53	1 2 3	precsexlem2	$⊢ R (\emptyset) = \emptyset$
54	53	raleqi	$⊢ \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in \emptyset 1_{s} <_{s} (A \cdot_{s} c)$
55	52 54	mpbir	$⊢ \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c)$
56	51 55	jctir	$⊢ φ \to (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))$
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 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	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s}$
75	25	rspccv	$⊢ \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \to (r \in L (j) \to (A \cdot_{s} r) <_{s} 1_{s})$
76	74 75	syl	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (r \in L (j) \to (A \cdot_{s} r) <_{s} 1_{s})$
77	4	3ad2ant1	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to A \in No$
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		1no	$⊢ 1_{s} \in No$
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		rightno	Could not format ( xR e. ( _Right ` A ) -> xR e. No ) : No typesetting found for \|- ( xR e. ( _Right ` A ) -> xR e. No ) with typecode \|-
82	81	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 \|-~~~~
83	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 \|-~~~~
84	82 83	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 \|-~~~~
85	84	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 \|-~~~~
86	1 2 3 4 5 6	precsexlem8	$⊢ (φ \land j \in ω) \to (L (j) \subseteq No \land R (j) \subseteq No)$
87	86	simpld	$⊢ (φ \land j \in ω) \to L (j) \subseteq No$
88	87	3adant3	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to L (j) \subseteq No$
89	88	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 \|-~~~~
90	89	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 \|-~~~~
91	85 90	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 \|-~~~~
92	80 91	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 \|-~~~~
93	82	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 \|-~~~~
94	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 \|-~~~~
95	5	3ad2ant1	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to 0_{s} <_{s} A$
96	95	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
97		rightgt	Could not format ( xR e. ( _Right ` A ) -> A A
98	97	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A A~~
99	94 83 82 96 98	ltstrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
100	99	gt0ne0sd	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 \|-~~~~
101	100	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 \|-~~~~
102		breq2	Could not format ( xO = xR -> ( 0s ~~0s ~~( 0s 0s~~~~
103		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 \|-
104	103	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 \|-
105	104	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 \|-
106	102 105	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 \|-~~~~~~
107	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 \|-~~~~
108	107	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 \|-~~~~
109		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 \|-
110	109	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 \|-~~~~
111	106 108 110	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 \|-~~~~~~~~
112	99 111	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 \|-~~~~
113	112	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 \|-~~~~
114	78 92 93 101 113	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 \|-~~
115		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 \|-
116	115	breq1d	Could not format ( b = yL -> ( ( A x.s b ) ~~( A x.s yL ) ~~( ( A x.s b ) ~~( A x.s yL )~~~~~~
117	116	rspccva	Could not format ( ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
118	74 117	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 )~~~~
119	118	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 )~~~~
120	78 90	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 \|-~~~~
121	83 82	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A ~~0s ~~( A 0s~~~~~~
122	98 121	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
123	122	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
124	120 80 85 123	ltmuls2d	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 ) )~~~~~~~~
125	119 124	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 ) )~~~~
126	85	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 \|-~~~~
127	125 126	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 ) )~~~~
128	85 120	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 \|-~~~~
129	78 128 93	ltaddsubs2d	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 ) )~~~~~~~~
130	127 129	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 ) ) )~~~~
131	78 80 91	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 \|-~~
132	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 \|-~~~~
133	78 85 90	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 \|-~~
134	132 133	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 \|-~~
135	131 134	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 \|-~~
136	93	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 \|-~~~~
137	130 135 136	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 ) ) )~~~~
138	78 92	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 \|-~~
139	99	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
140	138 80 93 139 113	ltdivmuls2wd	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 ) ) )~~~~~~
141	137 140	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 )~~~~
142	114 141	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 ) )~~~~
143		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 \|-
144	143	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 ) )~~~~~~
145	142 144	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 )~~~~
146	145	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 )~~
147	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 \|-~~~~
148	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 \|-~~~~
149		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 \|-~~~~
150	149	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 \|-~~~~
151	150	leftnod	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 \|-~~~~
152	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 \|-~~~~
153	151 152	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 \|-~~~~
154	153	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 \|-~~~~
155	86	simprd	$⊢ (φ \land j \in ω) \to R (j) \subseteq No$
156	155	3adant3	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to R (j) \subseteq No$
157	156	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 \|-~~~~
158	157	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 \|-~~~~
159	154 158	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 \|-~~~~
160	148 159	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 \|-~~~~
161	151	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 \|-~~~~
162		breq2	Could not format ( x = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
163	162	elrab	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~( xL e. ( _Left ` A ) /\ 0s ~~( xL e. ( _Left ` A ) /\ 0s~~~~
164	163	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~0s 0s~~
165	164	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
166	165	gt0ne0sd	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 \|-~~~~
167	166	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 \|-~~~~
168		breq2	Could not format ( xO = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
169		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 \|-
170	169	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 \|-
171	170	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 \|-
172	168 171	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 \|-~~~~~~
173	107	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 \|-~~~~
174		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 \|-
175	150 174	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 \|-~~~~
176	172 173 175	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 \|-~~~~~~~~
177	165 176	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 \|-~~~~
178	177	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 \|-~~~~
179	147 160 161 167 178	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 \|-~~
180	152 151	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 \|-~~~~
181	180	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 \|-~~~~
182	181	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 \|-~~~~
183		simp3r	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)$
184		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 \|-
185	184	breq2d	Could not format ( c = yR -> ( 1s ~~1s ~~( 1s 1s~~~~
186	185	rspccva	Could not format ( ( A. c e. ( R ` j ) 1s ~~1s 1s~~
187	183 186	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
188	187	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
189	147 158	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 \|-~~~~
190		leftlt	Could not format ( xL e. ( _Left ` A ) -> xL xL
191	150 190	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
192	151 152	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL ~~0s ~~( xL 0s~~~~~~
193	191 192	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
194	193	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
195	148 189 181 194	ltmuls2d	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 )~~~~~~~~
196	188 195	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 )~~~~
197	182 196	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) ~~( A -s xL )~~~~
198	151 152	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 \|-~~~~
199	198	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 \|-~~~~
200	154 189	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 \|-~~
201	198	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 \|-~~
202	201	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 \|-~~
203	200 202	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 \|-~~
204	197 199 203	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 ) )~~~~
205	154 189	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 \|-~~~~
206	205 154	ltnegsd	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 ) )~~~~~~~~
207	204 206	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 ) )~~~~
208	147 205 161	ltaddsubs2d	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 ) )~~~~~~~~
209	207 208	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 ) ) )~~~~
210	147 148 159	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 \|-~~
211	147	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 \|-~~~~
212	147 154 158	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 \|-~~
213	211 212	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 \|-~~
214	210 213	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 \|-~~
215	161	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 \|-~~~~
216	209 214 215	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 ) ) )~~~~
217	147 160	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 \|-~~
218	165	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
219	217 148 161 218 178	ltdivmulswd	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 ) ) )~~~~~~
220	216 219	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 )~~~~
221	179 220	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 ) )~~~~
222		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 \|-
223	222	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 ) )~~~~~~
224	221 223	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 )~~~~
225	224	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 )~~~~~~~~
226	146 225	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 )~~~~~~
227	76 226	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 )~~~~~~
228	73 227	sylbid	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (r \in L (suc j) \to (A \cdot_{s} r) <_{s} 1_{s})$
229	228	ralrimiv	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s}$
230	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~~
231	230	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~~~~
232	231	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~~~~
233		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~~~~
234		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~~~~
235		vex	$⊢ s \in V$
236		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 \|-
237	236	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~~~~~~
238	235 237	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~~~~
239		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 \|-
240	239	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 \|-
241	235 240	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 \|-
242	238 241	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~~~~
243	234 242	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~~~~
244	243	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~~~~
245	233 244	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~~~~
246	232 245	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~~~~
247	28	rspccv	$⊢ \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c) \to (s \in R (j) \to 1_{s} <_{s} (A \cdot_{s} s))$
248	183 247	syl	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (s \in R (j) \to 1_{s} <_{s} (A \cdot_{s} s))$
249	118	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 )~~~~
250	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 \|-~~~~
251	89	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 \|-~~~~
252	250 251	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 \|-~~~~
253	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 \|-~~~~
254	180	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 \|-~~~~
255	193	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
256	252 253 254 255	ltmuls2d	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 ) )~~~~~~~~
257	249 256	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 ) )~~~~
258	254	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 \|-~~~~
259	257 258	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 ) )~~~~
260	153	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 \|-~~~~
261	260 252	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 \|-~~
262	198	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 \|-~~
263	262	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 \|-~~
264	261 263	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 \|-~~
265	198	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 \|-~~~~
266	259 264 265	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 ) ) )~~~~
267	260 252	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 \|-~~~~
268	260 267	ltnegsd	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 ) ) )~~~~~~~~
269	266 268	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) ~~( xL -s A )~~~~
270	151	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 \|-~~~~
271	270 250 267	ltsubadds2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) ~~xL ~~( ( xL -s A ) xL~~~~~~
272	269 271	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
273	270	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 \|-~~~~
274	260 251	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 \|-~~~~
275	250 253 274	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 \|-~~
276	250	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 \|-~~~~
277	250 260 251	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 \|-~~
278	276 277	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 \|-~~
279	275 278	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 \|-~~
280	272 273 279	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 )~~~~
281	253 274	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 \|-~~~~
282	250 281	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 \|-~~
283	165	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
284	177	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 \|-~~~~
285	253 282 270 283 284	ltmuldivswd	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~~~~~~
286	280 285	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
287	166	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 \|-~~~~
288	250 281 270 287 284	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 \|-~~
289	286 288	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
290		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 \|-
291	290	breq2d	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s ~~1s ~~( 1s 1s~~~~
292	289 291	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~~~~
293	292	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~~~~~~
294	84	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 \|-~~~~
295	294	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 \|-~~~~
296	187	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
297	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 \|-~~~~
298	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 \|-~~~~
299	157	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 \|-~~~~
300	298 299	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 \|-~~~~
301	122	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
302	297 300 294 301	ltmuls2d	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 )~~~~~~~~
303	296 302	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 )~~~~
304	295 303	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) ~~( xR -s A )~~~~
305	82	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 \|-~~~~
306	294 300	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 \|-~~~~
307	305 298 306	ltsubadds2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) ~~xR ~~( ( xR -s A ) xR~~~~~~
308	304 307	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR xR~~
309	305	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 \|-~~~~
310	294 299	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 \|-~~~~
311	298 297 310	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 \|-~~
312	298	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 \|-~~~~
313	298 294 299	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 \|-~~
314	312 313	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 \|-~~
315	311 314	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 \|-~~
316	308 309 315	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 )~~~~
317	297 310	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 \|-~~~~
318	298 317	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 \|-~~
319	99	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
320	112	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 \|-~~~~
321	297 318 305 319 320	ltmuldivswd	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~~~~~~
322	316 321	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
323	100	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 \|-~~~~
324	298 317 305 323 320	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 \|-~~
325	322 324	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
326		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 \|-
327	326	breq2d	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s ~~1s ~~( 1s 1s~~~~
328	325 327	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~~~~
329	328	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~~
330	293 329	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~~~~~~
331	248 330	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~~~~~~
332	246 331	sylbid	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (s \in R (suc j) \to 1_{s} <_{s} (A \cdot_{s} s))$
333	332	ralrimiv	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)$
334	229 333	jca	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))$
335	334	3exp	$⊢ φ \to (j \in ω \to ((\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
336	335	com12	$⊢ j \in ω \to (φ \to ((\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
337	336	a2d	$⊢ j \in ω \to ((φ \to (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (φ \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
338	12 18 32 38 56 337	finds	$⊢ I \in ω \to (φ \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c)))$
339	338	impcom	$⊢ (φ \land I \in ω) \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$

Metamath Proof Explorer

Theorem precsexlem9

Proof