Metamath Proof Explorer

Theorem mulsproplem6

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 ) )
mulsproplem6.1 
|- ( ph -> A e. No )
mulsproplem6.2 
|- ( ph -> B e. No )
mulsproplem6.3 
|- ( ph -> P e. ( _Left ` A ) )
mulsproplem6.4 
|- ( ph -> Q e. ( _Left ` B ) )
mulsproplem6.5 
|- ( ph -> V e. ( _Right ` A ) )
mulsproplem6.6 
|- ( ph -> W e. ( _Left ` B ) )
Assertion mulsproplem6 
|- ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )

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