Metamath Proof Explorer

Theorem mulsproplem7

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 ) )
mulsproplem7.1 
|- ( ph -> A e. No )
mulsproplem7.2 
|- ( ph -> B e. No )
mulsproplem7.3 
|- ( ph -> R e. ( _Right ` A ) )
mulsproplem7.4 
|- ( ph -> S e. ( _Right ` B ) )
mulsproplem7.5 
|- ( ph -> T e. ( _Left ` A ) )
mulsproplem7.6 
|- ( ph -> U e. ( _Right ` B ) )
Assertion mulsproplem7 
|- ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )

Proof

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