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