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 0slt1s 
 |-  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 0sno 
 |-  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 1sno 
 |-  1s e. No
80 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
81 rightssno 
 |-  ( _Right ` A ) C_ No
82 81 sseli 
 |-  ( xR e. ( _Right ` A ) -> xR e. No )
83 82 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
84 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
85 83 84 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
86 85 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
87 1 2 3 4 5 6 precsexlem8 
 |-  ( ( ph /\ j e. _om ) -> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) )
88 87 simpld 
 |-  ( ( ph /\ j e. _om ) -> ( L ` j ) C_ No )
89 88 3adant3 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( L ` j ) C_ No )
90 89 sselda 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
91 90 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
92 86 91 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s yL ) e. No )
93 80 92 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xR -s A ) x.s yL ) ) e. No )
94 83 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
95 45 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s e. No )
96 5 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
97 96 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
98 breq2 
 |-  ( xO = xR -> ( A  A
99 rightval 
 |-  ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
100 98 99 elrab2 
 |-  ( xR e. ( _Right ` A ) <-> ( xR e. ( _Old ` ( bday ` A ) ) /\ A
101 100 simprbi 
 |-  ( xR e. ( _Right ` A ) -> A
102 101 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A
103 95 84 83 97 102 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
104 103 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
105 104 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
106 breq2 
 |-  ( xO = xR -> ( 0s  0s
107 oveq1 
 |-  ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) )
108 107 eqeq1d 
 |-  ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) )
109 108 rexbidv 
 |-  ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) )
110 106 109 imbi12d 
 |-  ( xO = xR -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xR x.s y ) = 1s ) ) )
111 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 ) )
112 111 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 ) )
113 elun2 
 |-  ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
114 113 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
115 110 112 114 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 0s  E. y e. No ( xR x.s y ) = 1s ) )
116 103 115 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
117 116 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
118 78 93 94 105 117 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 ) ) )
119 oveq2 
 |-  ( b = yL -> ( A x.s b ) = ( A x.s yL ) )
120 119 breq1d 
 |-  ( b = yL -> ( ( A x.s b )  ( A x.s yL )
121 120 rspccva 
 |-  ( ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
122 74 121 sylan 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
123 122 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
124 78 91 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL ) e. No )
125 84 83 posdifsd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A  0s
126 102 125 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
127 126 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
128 124 80 86 127 sltmul2d 
 |-  ( ( ( 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 ) )
129 123 128 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yL ) )
130 86 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s ) = ( xR -s A ) )
131 129 130 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yL ) )
132 86 124 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 )
133 78 132 94 sltaddsub2d 
 |-  ( ( ( 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 ) )
134 131 133 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 ) ) )
135 78 80 92 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 ) ) ) )
136 78 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
137 78 86 91 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 ) ) )
138 136 137 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 ) ) ) )
139 135 138 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 ) ) ) )
140 94 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR ) = xR )
141 134 139 140 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 ) ) )
142 78 93 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 )
143 103 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
144 142 80 94 143 117 sltdivmul2wd 
 |-  ( ( ( 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 ) ) )
145 141 144 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 )
146 118 145 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 ) )
147 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 ) ) )
148 147 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 ) )
149 146 148 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 )
150 149 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 )
151 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
152 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
153 leftssno 
 |-  ( _Left ` A ) C_ No
154 elrabi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
155 154 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. ( _Left ` A ) )
156 153 155 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
157 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
158 156 157 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
159 158 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
160 87 simprd 
 |-  ( ( ph /\ j e. _om ) -> ( R ` j ) C_ No )
161 160 3adant3 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( R ` j ) C_ No )
162 161 sselda 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
163 162 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
164 159 163 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s yR ) e. No )
165 152 164 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xL -s A ) x.s yR ) ) e. No )
166 156 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
167 breq2 
 |-  ( x = xL -> ( 0s  0s
168 167 elrab 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  ( xL e. ( _Left ` A ) /\ 0s
169 168 simprbi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  0s
170 169 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
171 170 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
172 171 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
173 breq2 
 |-  ( xO = xL -> ( 0s  0s
174 oveq1 
 |-  ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) )
175 174 eqeq1d 
 |-  ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) )
176 175 rexbidv 
 |-  ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) )
177 173 176 imbi12d 
 |-  ( xO = xL -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xL x.s y ) = 1s ) ) )
178 111 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 ) )
179 elun1 
 |-  ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
180 155 179 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
181 177 178 180 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 0s  E. y e. No ( xL x.s y ) = 1s ) )
182 170 181 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
183 182 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
184 151 165 166 172 183 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 ) ) )
185 157 156 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
186 185 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
187 186 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s ) = ( A -s xL ) )
188 simp3r 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. c e. ( R ` j ) 1s
189 oveq2 
 |-  ( c = yR -> ( A x.s c ) = ( A x.s yR ) )
190 189 breq2d 
 |-  ( c = yR -> ( 1s  1s
191 190 rspccva 
 |-  ( ( A. c e. ( R ` j ) 1s  1s
192 188 191 sylan 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
193 192 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
194 151 163 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yR ) e. No )
195 breq1 
 |-  ( xO = xL -> ( xO  xL
196 leftval 
 |-  ( _Left ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | xO
197 195 196 elrab2 
 |-  ( xL e. ( _Left ` A ) <-> ( xL e. ( _Old ` ( bday ` A ) ) /\ xL
198 197 simprbi 
 |-  ( xL e. ( _Left ` A ) -> xL
199 155 198 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL
200 156 157 posdifsd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL  0s
201 199 200 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
202 201 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
203 152 194 186 202 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s  ( ( A -s xL ) x.s 1s )
204 193 203 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s )
205 187 204 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL )
206 156 157 negsubsdi2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
207 206 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
208 159 194 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 ) ) ) )
209 206 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 ) ) )
210 209 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 ) ) )
211 208 210 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 ) ) )
212 205 207 211 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) )
213 159 194 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 )
214 213 159 sltnegd 
 |-  ( ( ( 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 ) )
215 212 214 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s ( A x.s yR ) )
216 151 213 166 sltaddsub2d 
 |-  ( ( ( 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 ) )
217 215 216 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 ) ) )
218 151 152 164 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 ) ) ) )
219 151 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
220 151 159 163 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 ) ) )
221 219 220 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 ) ) ) )
222 218 221 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 ) ) ) )
223 166 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL x.s 1s ) = xL )
224 217 222 223 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 ) ) )
225 151 165 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 )
226 170 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
227 225 152 166 226 183 sltdivmulwd 
 |-  ( ( ( 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 ) ) )
228 224 227 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 )
229 184 228 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 ) )
230 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 ) ) )
231 230 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 ) )
232 229 231 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 )
233 232 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 )
234 150 233 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 )
235 76 234 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 )
236 73 235 sylbid 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` suc j ) -> ( A x.s r )
237 236 ralrimiv 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. r e. ( L ` suc j ) ( A x.s r )
238 1 2 3 precsexlem5 
 |-  ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
239 238 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
240 239 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
241 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
242 elun 
 |-  ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
243 vex 
 |-  s e. _V
244 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 ) ) )
245 244 2rexbidv 
 |-  ( a = s -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
246 243 245 elab 
 |-  ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
247 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 ) ) )
248 247 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 ) ) )
249 243 248 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 ) )
250 246 249 orbi12i 
 |-  ( ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xL e. { x e. ( _Left ` A ) | 0s
251 242 250 bitri 
 |-  ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xL e. { x e. ( _Left ` A ) | 0s
252 251 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
253 241 252 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
254 240 253 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
255 28 rspccv 
 |-  ( A. c e. ( R ` j ) 1s  ( s e. ( R ` j ) -> 1s
256 188 255 syl 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` j ) -> 1s
257 122 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
258 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
259 90 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
260 258 259 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL ) e. No )
261 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
262 185 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
263 201 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
264 260 261 262 263 sltmul2d 
 |-  ( ( ( 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 ) )
265 257 264 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s ( A x.s yL ) )
266 262 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s ) = ( A -s xL ) )
267 265 266 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s ( A x.s yL ) )
268 158 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
269 268 260 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 ) ) ) )
270 206 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 ) ) )
271 270 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 ) ) )
272 269 271 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 ) ) )
273 206 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
274 267 272 273 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )
275 268 260 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 )
276 268 275 sltnegd 
 |-  ( ( ( 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 ) ) )
277 274 276 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A )
278 156 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
279 278 258 275 sltsubadd2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A )  xL
280 277 279 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL
281 278 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xL ) = xL )
282 268 259 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s yL ) e. No )
283 258 261 282 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 ) ) ) )
284 258 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
285 258 268 259 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 ) ) )
286 284 285 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 ) ) ) )
287 283 286 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 ) ) ) )
288 280 281 287 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xL )
289 261 282 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xL -s A ) x.s yL ) ) e. No )
290 258 289 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 )
291 170 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
292 182 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
293 261 290 278 291 292 sltmuldivwd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( 1s x.s xL )  1s
294 288 293 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
295 171 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
296 258 289 278 295 292 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 ) ) )
297 294 296 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
298 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 ) ) )
299 298 breq2d 
 |-  ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s  1s
300 297 299 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
301 300 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( E. xL e. { x e. ( _Left ` A ) | 0s  1s
302 85 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
303 302 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s ) = ( xR -s A ) )
304 192 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
305 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
306 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
307 162 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
308 306 307 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yR ) e. No )
309 126 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
310 305 308 302 309 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s  ( ( xR -s A ) x.s 1s )
311 304 310 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s )
312 303 311 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A )
313 83 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
314 302 308 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 )
315 313 306 314 sltsubadd2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A )  xR
316 312 315 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR
317 313 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR ) = xR )
318 302 307 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s yR ) e. No )
319 306 305 318 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 ) ) ) )
320 306 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
321 306 302 307 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 ) ) )
322 320 321 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 ) ) ) )
323 319 322 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 ) ) ) )
324 316 317 323 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR )
325 305 318 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xR -s A ) x.s yR ) ) e. No )
326 306 325 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 )
327 103 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
328 116 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
329 305 326 313 327 328 sltmuldivwd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( 1s x.s xR )  1s
330 324 329 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
331 104 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
332 306 325 313 331 328 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 ) ) )
333 330 332 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
334 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 ) ) )
335 334 breq2d 
 |-  ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s  1s
336 333 335 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
337 336 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
338 301 337 jaod 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( E. xL e. { x e. ( _Left ` A ) | 0s  1s
339 256 338 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
340 254 339 sylbid 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` suc j ) -> 1s
341 340 ralrimiv 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. s e. ( R ` suc j ) 1s
342 237 341 jca 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
343 342 3exp 
 |-  ( ph -> ( j e. _om -> ( ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
344 343 com12 
 |-  ( j e. _om -> ( ph -> ( ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
345 344 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 )
346 12 18 32 38 56 345 finds 
 |-  ( I e. _om -> ( ph -> ( A. b e. ( L ` I ) ( A x.s b )
347 346 impcom 
 |-  ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b )