Metamath Proof Explorer

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 
|- 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 } , (/) >. )
precsexlem.2 
|- L = ( 1st o. F )
precsexlem.3 
|- R = ( 2nd o. F )
precsexlem.4 
|- ( ph -> A e. No )
precsexlem.5 
|- ( ph -> 0s
precsexlem.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
Assertion precsexlem9 
|- ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b )

Proof

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