Metamath Proof Explorer

Theorem mulsproplem5

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