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