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