Metamath Proof Explorer

Theorem mulsproplem8

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 
|- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
mulsproplem8.1 
|- ( ph -> A e. No )
mulsproplem8.2 
|- ( ph -> B e. No )
mulsproplem8.3 
|- ( ph -> R e. ( _Right ` A ) )
mulsproplem8.4 
|- ( ph -> S e. ( _Right ` B ) )
mulsproplem8.5 
|- ( ph -> V e. ( _Right ` A ) )
mulsproplem8.6 
|- ( ph -> W e. ( _Left ` B ) )
Assertion mulsproplem8 
|- ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )

Proof

Step Hyp Ref Expression
1 mulsproplem.1 
 |-  ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
2 mulsproplem8.1 
 |-  ( ph -> A e. No )
3 mulsproplem8.2 
 |-  ( ph -> B e. No )
4 mulsproplem8.3 
 |-  ( ph -> R e. ( _Right ` A ) )
5 mulsproplem8.4 
 |-  ( ph -> S e. ( _Right ` B ) )
6 mulsproplem8.5 
 |-  ( ph -> V e. ( _Right ` A ) )
7 mulsproplem8.6 
 |-  ( ph -> W e. ( _Left ` B ) )
8 rightssno 
 |-  ( _Right ` A ) C_ No
9 8 4 sselid 
 |-  ( ph -> R e. No )
10 8 6 sselid 
 |-  ( ph -> V e. No )
11 sltlin 
 |-  ( ( R e. No /\ V e. No ) -> ( R
12 9 10 11 syl2anc 
 |-  ( ph -> ( R
13 rightssold 
 |-  ( _Right ` A ) C_ ( _Old ` ( bday ` A ) )
14 13 4 sselid 
 |-  ( ph -> R e. ( _Old ` ( bday ` A ) ) )
15 1 14 3 mulsproplem2 
 |-  ( ph -> ( R x.s B ) e. No )
16 rightssold 
 |-  ( _Right ` B ) C_ ( _Old ` ( bday ` B ) )
17 16 5 sselid 
 |-  ( ph -> S e. ( _Old ` ( bday ` B ) ) )
18 1 2 17 mulsproplem3 
 |-  ( ph -> ( A x.s S ) e. No )
19 15 18 addscld 
 |-  ( ph -> ( ( R x.s B ) +s ( A x.s S ) ) e. No )
20 1 14 17 mulsproplem4 
 |-  ( ph -> ( R x.s S ) e. No )
21 19 20 subscld 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) e. No )
22 21 adantr 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) e. No )
23 leftssold 
 |-  ( _Left ` B ) C_ ( _Old ` ( bday ` B ) )
24 23 7 sselid 
 |-  ( ph -> W e. ( _Old ` ( bday ` B ) ) )
25 1 2 24 mulsproplem3 
 |-  ( ph -> ( A x.s W ) e. No )
26 15 25 addscld 
 |-  ( ph -> ( ( R x.s B ) +s ( A x.s W ) ) e. No )
27 1 14 24 mulsproplem4 
 |-  ( ph -> ( R x.s W ) e. No )
28 26 27 subscld 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) ) e. No )
29 28 adantr 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) ) e. No )
30 13 6 sselid 
 |-  ( ph -> V e. ( _Old ` ( bday ` A ) ) )
31 1 30 3 mulsproplem2 
 |-  ( ph -> ( V x.s B ) e. No )
32 31 25 addscld 
 |-  ( ph -> ( ( V x.s B ) +s ( A x.s W ) ) e. No )
33 1 30 24 mulsproplem4 
 |-  ( ph -> ( V x.s W ) e. No )
34 32 33 subscld 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) e. No )
35 34 adantr 
 |-  ( ( ph /\ R  ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) e. No )
36 ssltright 
 |-  ( A e. No -> { A } <
37 2 36 syl 
 |-  ( ph -> { A } <
38 snidg 
 |-  ( A e. No -> A e. { A } )
39 2 38 syl 
 |-  ( ph -> A e. { A } )
40 37 39 4 ssltsepcd 
 |-  ( ph -> A
41 lltropt 
 |-  ( _Left ` B ) <
42 41 a1i 
 |-  ( ph -> ( _Left ` B ) <
43 42 7 5 ssltsepcd 
 |-  ( ph -> W
44 0sno 
 |-  0s e. No
45 44 a1i 
 |-  ( ph -> 0s e. No )
46 leftssno 
 |-  ( _Left ` B ) C_ No
47 46 7 sselid 
 |-  ( ph -> W e. No )
48 rightssno 
 |-  ( _Right ` B ) C_ No
49 48 5 sselid 
 |-  ( ph -> S e. No )
50 bday0s 
 |-  ( bday ` 0s ) = (/)
51 50 50 oveq12i 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
52 0elon 
 |-  (/) e. On
53 naddrid 
 |-  ( (/) e. On -> ( (/) +no (/) ) = (/) )
54 52 53 ax-mp 
 |-  ( (/) +no (/) ) = (/)
55 51 54 eqtri 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
56 55 uneq1i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) )
57 0un 
 |-  ( (/) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) )
58 56 57 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) )
59 oldbdayim 
 |-  ( W e. ( _Old ` ( bday ` B ) ) -> ( bday ` W ) e. ( bday ` B ) )
60 24 59 syl 
 |-  ( ph -> ( bday ` W ) e. ( bday ` B ) )
61 bdayelon 
 |-  ( bday ` W ) e. On
62 bdayelon 
 |-  ( bday ` B ) e. On
63 bdayelon 
 |-  ( bday ` A ) e. On
64 naddel2 
 |-  ( ( ( bday ` W ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` W ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
65 61 62 63 64 mp3an 
 |-  ( ( bday ` W ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
66 60 65 sylib 
 |-  ( ph -> ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
67 oldbdayim 
 |-  ( R e. ( _Old ` ( bday ` A ) ) -> ( bday ` R ) e. ( bday ` A ) )
68 14 67 syl 
 |-  ( ph -> ( bday ` R ) e. ( bday ` A ) )
69 oldbdayim 
 |-  ( S e. ( _Old ` ( bday ` B ) ) -> ( bday ` S ) e. ( bday ` B ) )
70 17 69 syl 
 |-  ( ph -> ( bday ` S ) e. ( bday ` B ) )
71 naddel12 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` R ) e. ( bday ` A ) /\ ( bday ` S ) e. ( bday ` B ) ) -> ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
72 63 62 71 mp2an 
 |-  ( ( ( bday ` R ) e. ( bday ` A ) /\ ( bday ` S ) e. ( bday ` B ) ) -> ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
73 68 70 72 syl2anc 
 |-  ( ph -> ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
74 66 73 jca 
 |-  ( ph -> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
75 bdayelon 
 |-  ( bday ` S ) e. On
76 naddel2 
 |-  ( ( ( bday ` S ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` S ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
77 75 62 63 76 mp3an 
 |-  ( ( bday ` S ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
78 70 77 sylib 
 |-  ( ph -> ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
79 naddel12 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` R ) e. ( bday ` A ) /\ ( bday ` W ) e. ( bday ` B ) ) -> ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
80 63 62 79 mp2an 
 |-  ( ( ( bday ` R ) e. ( bday ` A ) /\ ( bday ` W ) e. ( bday ` B ) ) -> ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
81 68 60 80 syl2anc 
 |-  ( ph -> ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
82 78 81 jca 
 |-  ( ph -> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
83 naddcl 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` W ) e. On ) -> ( ( bday ` A ) +no ( bday ` W ) ) e. On )
84 63 61 83 mp2an 
 |-  ( ( bday ` A ) +no ( bday ` W ) ) e. On
85 bdayelon 
 |-  ( bday ` R ) e. On
86 naddcl 
 |-  ( ( ( bday ` R ) e. On /\ ( bday ` S ) e. On ) -> ( ( bday ` R ) +no ( bday ` S ) ) e. On )
87 85 75 86 mp2an 
 |-  ( ( bday ` R ) +no ( bday ` S ) ) e. On
88 84 87 onun2i 
 |-  ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. On
89 naddcl 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` S ) e. On ) -> ( ( bday ` A ) +no ( bday ` S ) ) e. On )
90 63 75 89 mp2an 
 |-  ( ( bday ` A ) +no ( bday ` S ) ) e. On
91 naddcl 
 |-  ( ( ( bday ` R ) e. On /\ ( bday ` W ) e. On ) -> ( ( bday ` R ) +no ( bday ` W ) ) e. On )
92 85 61 91 mp2an 
 |-  ( ( bday ` R ) +no ( bday ` W ) ) e. On
93 90 92 onun2i 
 |-  ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. On
94 naddcl 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On )
95 63 62 94 mp2an 
 |-  ( ( bday ` A ) +no ( bday ` B ) ) e. On
96 onunel 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. On /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
97 88 93 95 96 mp3an 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
98 onunel 
 |-  ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. On /\ ( ( bday ` R ) +no ( bday ` S ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
99 84 87 95 98 mp3an 
 |-  ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
100 onunel 
 |-  ( ( ( ( bday ` A ) +no ( bday ` S ) ) e. On /\ ( ( bday ` R ) +no ( bday ` W ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
101 90 92 95 100 mp3an 
 |-  ( ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
102 99 101 anbi12i 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
103 97 102 bitri 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
104 74 82 103 sylanbrc 
 |-  ( ph -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
105 elun1 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
106 104 105 syl 
 |-  ( ph -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
107 58 106 eqeltrid 
 |-  ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` W ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
108 1 45 45 2 9 47 49 107 mulsproplem1 
 |-  ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( A  ( ( A x.s S ) -s ( A x.s W ) )
109 108 simprd 
 |-  ( ph -> ( ( A  ( ( A x.s S ) -s ( A x.s W ) )
110 40 43 109 mp2and 
 |-  ( ph -> ( ( A x.s S ) -s ( A x.s W ) )
111 18 20 25 27 sltsubsubbd 
 |-  ( ph -> ( ( ( A x.s S ) -s ( A x.s W ) )  ( ( A x.s S ) -s ( R x.s S ) )
112 18 20 subscld 
 |-  ( ph -> ( ( A x.s S ) -s ( R x.s S ) ) e. No )
113 25 27 subscld 
 |-  ( ph -> ( ( A x.s W ) -s ( R x.s W ) ) e. No )
114 112 113 15 sltadd2d 
 |-  ( ph -> ( ( ( A x.s S ) -s ( R x.s S ) )  ( ( R x.s B ) +s ( ( A x.s S ) -s ( R x.s S ) ) )
115 111 114 bitrd 
 |-  ( ph -> ( ( ( A x.s S ) -s ( A x.s W ) )  ( ( R x.s B ) +s ( ( A x.s S ) -s ( R x.s S ) ) )
116 110 115 mpbid 
 |-  ( ph -> ( ( R x.s B ) +s ( ( A x.s S ) -s ( R x.s S ) ) )
117 15 18 20 addsubsassd 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) = ( ( R x.s B ) +s ( ( A x.s S ) -s ( R x.s S ) ) ) )
118 15 25 27 addsubsassd 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) ) = ( ( R x.s B ) +s ( ( A x.s W ) -s ( R x.s W ) ) ) )
119 116 117 118 3brtr4d 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
120 119 adantr 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
121 ssltleft 
 |-  ( B e. No -> ( _Left ` B ) <
122 3 121 syl 
 |-  ( ph -> ( _Left ` B ) <
123 snidg 
 |-  ( B e. No -> B e. { B } )
124 3 123 syl 
 |-  ( ph -> B e. { B } )
125 122 7 124 ssltsepcd 
 |-  ( ph -> W
126 55 uneq1i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) )
127 0un 
 |-  ( (/) u. ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) )
128 126 127 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) )
129 oldbdayim 
 |-  ( V e. ( _Old ` ( bday ` A ) ) -> ( bday ` V ) e. ( bday ` A ) )
130 30 129 syl 
 |-  ( ph -> ( bday ` V ) e. ( bday ` A ) )
131 bdayelon 
 |-  ( bday ` V ) e. On
132 naddel1 
 |-  ( ( ( bday ` V ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` V ) e. ( bday ` A ) <-> ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
133 131 63 62 132 mp3an 
 |-  ( ( bday ` V ) e. ( bday ` A ) <-> ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
134 130 133 sylib 
 |-  ( ph -> ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
135 81 134 jca 
 |-  ( ph -> ( ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
136 naddel1 
 |-  ( ( ( bday ` R ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` R ) e. ( bday ` A ) <-> ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
137 85 63 62 136 mp3an 
 |-  ( ( bday ` R ) e. ( bday ` A ) <-> ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
138 68 137 sylib 
 |-  ( ph -> ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
139 naddel12 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` V ) e. ( bday ` A ) /\ ( bday ` W ) e. ( bday ` B ) ) -> ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
140 63 62 139 mp2an 
 |-  ( ( ( bday ` V ) e. ( bday ` A ) /\ ( bday ` W ) e. ( bday ` B ) ) -> ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
141 130 60 140 syl2anc 
 |-  ( ph -> ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
142 138 141 jca 
 |-  ( ph -> ( ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
143 naddcl 
 |-  ( ( ( bday ` V ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` V ) +no ( bday ` B ) ) e. On )
144 131 62 143 mp2an 
 |-  ( ( bday ` V ) +no ( bday ` B ) ) e. On
145 92 144 onun2i 
 |-  ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. On
146 naddcl 
 |-  ( ( ( bday ` R ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` R ) +no ( bday ` B ) ) e. On )
147 85 62 146 mp2an 
 |-  ( ( bday ` R ) +no ( bday ` B ) ) e. On
148 naddcl 
 |-  ( ( ( bday ` V ) e. On /\ ( bday ` W ) e. On ) -> ( ( bday ` V ) +no ( bday ` W ) ) e. On )
149 131 61 148 mp2an 
 |-  ( ( bday ` V ) +no ( bday ` W ) ) e. On
150 147 149 onun2i 
 |-  ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. On
151 onunel 
 |-  ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. On /\ ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
152 145 150 95 151 mp3an 
 |-  ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
153 onunel 
 |-  ( ( ( ( bday ` R ) +no ( bday ` W ) ) e. On /\ ( ( bday ` V ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
154 92 144 95 153 mp3an 
 |-  ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
155 onunel 
 |-  ( ( ( ( bday ` R ) +no ( bday ` B ) ) e. On /\ ( ( bday ` V ) +no ( bday ` W ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
156 147 149 95 155 mp3an 
 |-  ( ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
157 154 156 anbi12i 
 |-  ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
158 152 157 bitri 
 |-  ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` R ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
159 135 142 158 sylanbrc 
 |-  ( ph -> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
160 elun1 
 |-  ( ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
161 159 160 syl 
 |-  ( ph -> ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
162 128 161 eqeltrid 
 |-  ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` R ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` B ) ) ) u. ( ( ( bday ` R ) +no ( bday ` B ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
163 1 45 45 9 10 47 3 162 mulsproplem1 
 |-  ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( R  ( ( R x.s B ) -s ( R x.s W ) )
164 163 simprd 
 |-  ( ph -> ( ( R  ( ( R x.s B ) -s ( R x.s W ) )
165 125 164 mpan2d 
 |-  ( ph -> ( R  ( ( R x.s B ) -s ( R x.s W ) )
166 165 imp 
 |-  ( ( ph /\ R  ( ( R x.s B ) -s ( R x.s W ) )
167 15 27 subscld 
 |-  ( ph -> ( ( R x.s B ) -s ( R x.s W ) ) e. No )
168 31 33 subscld 
 |-  ( ph -> ( ( V x.s B ) -s ( V x.s W ) ) e. No )
169 167 168 25 sltadd1d 
 |-  ( ph -> ( ( ( R x.s B ) -s ( R x.s W ) )  ( ( ( R x.s B ) -s ( R x.s W ) ) +s ( A x.s W ) )
170 169 adantr 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) -s ( R x.s W ) )  ( ( ( R x.s B ) -s ( R x.s W ) ) +s ( A x.s W ) )
171 166 170 mpbid 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) -s ( R x.s W ) ) +s ( A x.s W ) )
172 15 25 27 addsubsd 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) ) = ( ( ( R x.s B ) -s ( R x.s W ) ) +s ( A x.s W ) ) )
173 172 adantr 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) ) = ( ( ( R x.s B ) -s ( R x.s W ) ) +s ( A x.s W ) ) )
174 31 25 33 addsubsd 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) = ( ( ( V x.s B ) -s ( V x.s W ) ) +s ( A x.s W ) ) )
175 174 adantr 
 |-  ( ( ph /\ R  ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) = ( ( ( V x.s B ) -s ( V x.s W ) ) +s ( A x.s W ) ) )
176 171 173 175 3brtr4d 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s W ) ) -s ( R x.s W ) )
177 22 29 35 120 176 slttrd 
 |-  ( ( ph /\ R  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
178 177 ex 
 |-  ( ph -> ( R  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
179 37 39 6 ssltsepcd 
 |-  ( ph -> A
180 55 uneq1i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) )
181 0un 
 |-  ( (/) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) )
182 180 181 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) = ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) )
183 naddel12 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` V ) e. ( bday ` A ) /\ ( bday ` S ) e. ( bday ` B ) ) -> ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
184 63 62 183 mp2an 
 |-  ( ( ( bday ` V ) e. ( bday ` A ) /\ ( bday ` S ) e. ( bday ` B ) ) -> ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
185 130 70 184 syl2anc 
 |-  ( ph -> ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
186 66 185 jca 
 |-  ( ph -> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
187 78 141 jca 
 |-  ( ph -> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
188 naddcl 
 |-  ( ( ( bday ` V ) e. On /\ ( bday ` S ) e. On ) -> ( ( bday ` V ) +no ( bday ` S ) ) e. On )
189 131 75 188 mp2an 
 |-  ( ( bday ` V ) +no ( bday ` S ) ) e. On
190 84 189 onun2i 
 |-  ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. On
191 90 149 onun2i 
 |-  ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. On
192 onunel 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. On /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
193 190 191 95 192 mp3an 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
194 onunel 
 |-  ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. On /\ ( ( bday ` V ) +no ( bday ` S ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
195 84 189 95 194 mp3an 
 |-  ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
196 onunel 
 |-  ( ( ( ( bday ` A ) +no ( bday ` S ) ) e. On /\ ( ( bday ` V ) +no ( bday ` W ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
197 90 149 95 196 mp3an 
 |-  ( ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
198 195 197 anbi12i 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
199 193 198 bitri 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` A ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` A ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` V ) +no ( bday ` W ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
200 186 187 199 sylanbrc 
 |-  ( ph -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
201 elun1 
 |-  ( ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
202 200 201 syl 
 |-  ( ph -> ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
203 182 202 eqeltrid 
 |-  ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` A ) +no ( bday ` W ) ) u. ( ( bday ` V ) +no ( bday ` S ) ) ) u. ( ( ( bday ` A ) +no ( bday ` S ) ) u. ( ( bday ` V ) +no ( bday ` W ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
204 1 45 45 2 10 47 49 203 mulsproplem1 
 |-  ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( A  ( ( A x.s S ) -s ( A x.s W ) )
205 204 simprd 
 |-  ( ph -> ( ( A  ( ( A x.s S ) -s ( A x.s W ) )
206 179 43 205 mp2and 
 |-  ( ph -> ( ( A x.s S ) -s ( A x.s W ) )
207 1 30 17 mulsproplem4 
 |-  ( ph -> ( V x.s S ) e. No )
208 18 207 25 33 sltsubsubbd 
 |-  ( ph -> ( ( ( A x.s S ) -s ( A x.s W ) )  ( ( A x.s S ) -s ( V x.s S ) )
209 18 207 subscld 
 |-  ( ph -> ( ( A x.s S ) -s ( V x.s S ) ) e. No )
210 25 33 subscld 
 |-  ( ph -> ( ( A x.s W ) -s ( V x.s W ) ) e. No )
211 209 210 31 sltadd2d 
 |-  ( ph -> ( ( ( A x.s S ) -s ( V x.s S ) )  ( ( V x.s B ) +s ( ( A x.s S ) -s ( V x.s S ) ) )
212 208 211 bitrd 
 |-  ( ph -> ( ( ( A x.s S ) -s ( A x.s W ) )  ( ( V x.s B ) +s ( ( A x.s S ) -s ( V x.s S ) ) )
213 206 212 mpbid 
 |-  ( ph -> ( ( V x.s B ) +s ( ( A x.s S ) -s ( V x.s S ) ) )
214 31 18 207 addsubsassd 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) = ( ( V x.s B ) +s ( ( A x.s S ) -s ( V x.s S ) ) ) )
215 31 25 33 addsubsassd 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) = ( ( V x.s B ) +s ( ( A x.s W ) -s ( V x.s W ) ) ) )
216 213 214 215 3brtr4d 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) )
217 oveq1 
 |-  ( R = V -> ( R x.s B ) = ( V x.s B ) )
218 217 oveq1d 
 |-  ( R = V -> ( ( R x.s B ) +s ( A x.s S ) ) = ( ( V x.s B ) +s ( A x.s S ) ) )
219 oveq1 
 |-  ( R = V -> ( R x.s S ) = ( V x.s S ) )
220 218 219 oveq12d 
 |-  ( R = V -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) = ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) )
221 220 breq1d 
 |-  ( R = V -> ( ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )  ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) )
222 216 221 syl5ibrcom 
 |-  ( ph -> ( R = V -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
223 21 adantr 
 |-  ( ( ph /\ V  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) e. No )
224 31 18 addscld 
 |-  ( ph -> ( ( V x.s B ) +s ( A x.s S ) ) e. No )
225 224 207 subscld 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) e. No )
226 225 adantr 
 |-  ( ( ph /\ V  ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) e. No )
227 34 adantr 
 |-  ( ( ph /\ V  ( ( ( V x.s B ) +s ( A x.s W ) ) -s ( V x.s W ) ) e. No )
228 ssltright 
 |-  ( B e. No -> { B } <
229 3 228 syl 
 |-  ( ph -> { B } <
230 229 124 5 ssltsepcd 
 |-  ( ph -> B
231 55 uneq1i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) )
232 0un 
 |-  ( (/) u. ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) )
233 231 232 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) )
234 134 73 jca 
 |-  ( ph -> ( ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
235 185 138 jca 
 |-  ( ph -> ( ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
236 144 87 onun2i 
 |-  ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. On
237 189 147 onun2i 
 |-  ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. On
238 onunel 
 |-  ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. On /\ ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
239 236 237 95 238 mp3an 
 |-  ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
240 onunel 
 |-  ( ( ( ( bday ` V ) +no ( bday ` B ) ) e. On /\ ( ( bday ` R ) +no ( bday ` S ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
241 144 87 95 240 mp3an 
 |-  ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
242 onunel 
 |-  ( ( ( ( bday ` V ) +no ( bday ` S ) ) e. On /\ ( ( bday ` R ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
243 189 147 95 242 mp3an 
 |-  ( ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
244 241 243 anbi12i 
 |-  ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
245 239 244 bitri 
 |-  ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` V ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` V ) +no ( bday ` S ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` R ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) )
246 234 235 245 sylanbrc 
 |-  ( ph -> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
247 elun1 
 |-  ( ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
248 246 247 syl 
 |-  ( ph -> ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
249 233 248 eqeltrid 
 |-  ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` V ) +no ( bday ` B ) ) u. ( ( bday ` R ) +no ( bday ` S ) ) ) u. ( ( ( bday ` V ) +no ( bday ` S ) ) u. ( ( bday ` R ) +no ( bday ` B ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
250 1 45 45 10 9 3 49 249 mulsproplem1 
 |-  ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( V  ( ( V x.s S ) -s ( V x.s B ) )
251 250 simprd 
 |-  ( ph -> ( ( V  ( ( V x.s S ) -s ( V x.s B ) )
252 230 251 mpan2d 
 |-  ( ph -> ( V  ( ( V x.s S ) -s ( V x.s B ) )
253 252 imp 
 |-  ( ( ph /\ V  ( ( V x.s S ) -s ( V x.s B ) )
254 207 31 20 15 sltsubsub2bd 
 |-  ( ph -> ( ( ( V x.s S ) -s ( V x.s B ) )  ( ( R x.s B ) -s ( R x.s S ) )
255 15 20 subscld 
 |-  ( ph -> ( ( R x.s B ) -s ( R x.s S ) ) e. No )
256 31 207 subscld 
 |-  ( ph -> ( ( V x.s B ) -s ( V x.s S ) ) e. No )
257 255 256 18 sltadd1d 
 |-  ( ph -> ( ( ( R x.s B ) -s ( R x.s S ) )  ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) )
258 254 257 bitrd 
 |-  ( ph -> ( ( ( V x.s S ) -s ( V x.s B ) )  ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) )
259 258 adantr 
 |-  ( ( ph /\ V  ( ( ( V x.s S ) -s ( V x.s B ) )  ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) )
260 253 259 mpbid 
 |-  ( ( ph /\ V  ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) )
261 15 18 20 addsubsd 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) = ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) ) )
262 261 adantr 
 |-  ( ( ph /\ V  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) ) = ( ( ( R x.s B ) -s ( R x.s S ) ) +s ( A x.s S ) ) )
263 31 18 207 addsubsd 
 |-  ( ph -> ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) = ( ( ( V x.s B ) -s ( V x.s S ) ) +s ( A x.s S ) ) )
264 263 adantr 
 |-  ( ( ph /\ V  ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) ) = ( ( ( V x.s B ) -s ( V x.s S ) ) +s ( A x.s S ) ) )
265 260 262 264 3brtr4d 
 |-  ( ( ph /\ V  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
266 216 adantr 
 |-  ( ( ph /\ V  ( ( ( V x.s B ) +s ( A x.s S ) ) -s ( V x.s S ) )
267 223 226 227 265 266 slttrd 
 |-  ( ( ph /\ V  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
268 267 ex 
 |-  ( ph -> ( V  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
269 178 222 268 3jaod 
 |-  ( ph -> ( ( R  ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )
270 12 269 mpd 
 |-  ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )