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 ⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
mulsproplem7.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
mulsproplem7.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
mulsproplem7.3 ⊢ ( 𝜑 → 𝑅 ∈ ( R ‘ 𝐴 ) )
mulsproplem7.4 ⊢ ( 𝜑 → 𝑆 ∈ ( R ‘ 𝐵 ) )
mulsproplem7.5 ⊢ ( 𝜑 → 𝑇 ∈ ( L ‘ 𝐴 ) )
mulsproplem7.6 ⊢ ( 𝜑 → 𝑈 ∈ ( R ‘ 𝐵 ) )
Assertion mulsproplem7 ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) )

Proof

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