Metamath Proof Explorer

Theorem mulsproplem8

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 𝑒 ) ) ) ) ) )
mulsproplem8.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
mulsproplem8.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
mulsproplem8.3 ⊢ ( 𝜑 → 𝑅 ∈ ( R ‘ 𝐴 ) )
mulsproplem8.4 ⊢ ( 𝜑 → 𝑆 ∈ ( R ‘ 𝐵 ) )
mulsproplem8.5 ⊢ ( 𝜑 → 𝑉 ∈ ( R ‘ 𝐴 ) )
mulsproplem8.6 ⊢ ( 𝜑 → 𝑊 ∈ ( L ‘ 𝐵 ) )
Assertion mulsproplem8 ( 𝜑 → ( ( ( 𝑅 ·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 mulsproplem8.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 mulsproplem8.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
4 mulsproplem8.3 ⊢ ( 𝜑 → 𝑅 ∈ ( R ‘ 𝐴 ) )
5 mulsproplem8.4 ⊢ ( 𝜑 → 𝑆 ∈ ( R ‘ 𝐵 ) )
6 mulsproplem8.5 ⊢ ( 𝜑 → 𝑉 ∈ ( R ‘ 𝐴 ) )
7 mulsproplem8.6 ⊢ ( 𝜑 → 𝑊 ∈ ( L ‘ 𝐵 ) )
8 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
9 8 4 sselid ⊢ ( 𝜑 → 𝑅 ∈ No )
10 8 6 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 7 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
25 1 2 24 mulsproplem3 ⊢ ( 𝜑 → ( 𝐴 ·s 𝑊 ) ∈ No )
26 15 25 addscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
27 1 14 24 mulsproplem4 ⊢ ( 𝜑 → ( 𝑅 ·s 𝑊 ) ∈ No )
28 26 27 subscld ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
30 13 6 sselid ⊢ ( 𝜑 → 𝑉 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
31 1 30 3 mulsproplem2 ⊢ ( 𝜑 → ( 𝑉 ·s 𝐵 ) ∈ No )
32 31 25 addscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
33 1 30 24 mulsproplem4 ⊢ ( 𝜑 → ( 𝑉 ·s 𝑊 ) ∈ No )
34 32 33 subscld ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
36 ssltright ⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )
37 2 36 syl ⊢ ( 𝜑 → { 𝐴 } <<s ( R ‘ 𝐴 ) )
38 snidg ⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
39 2 38 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
40 37 39 4 ssltsepcd ⊢ ( 𝜑 → 𝐴 <s 𝑅 )
41 lltropt ⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
42 41 a1i ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
43 42 7 5 ssltsepcd ⊢ ( 𝜑 → 𝑊 <s 𝑆 )
44 0sno ⊢ 0s ∈ No
45 44 a1i ⊢ ( 𝜑 → 0s ∈ No )
46 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
47 46 7 sselid ⊢ ( 𝜑 → 𝑊 ∈ No )
48 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
49 48 5 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 naddel2 ⊢ ( ( ( 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 63 62 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 bdayelon ⊢ ( bday ‘ 𝑆 ) ∈ On
76 naddel2 ⊢ ( ( ( bday ‘ 𝑆 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
77 75 62 63 76 mp3an ⊢ ( ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
78 70 77 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
79 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
80 63 62 79 mp2an ⊢ ( ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
81 68 60 80 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
82 78 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 63 61 83 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On
85 bdayelon ⊢ ( bday ‘ 𝑅 ) ∈ On
86 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝑆 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ∈ On )
87 85 75 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 63 75 89 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ On
91 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
92 85 61 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 63 62 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 2 9 47 49 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 40 43 109 mp2and ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝑊 ) ) )
111 18 20 25 27 sltsubsubbd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝑊 ) ) ↔ ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑅 ·s 𝑊 ) ) ) )
112 18 20 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
113 25 27 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
114 112 113 15 sltadd2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·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 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( 𝑅 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) ) )
118 15 25 27 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑅 ·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 3 121 syl ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s { 𝐵 } )
123 snidg ⊢ ( 𝐵 ∈ No → 𝐵 ∈ { 𝐵 } )
124 3 123 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
125 122 7 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 naddel1 ⊢ ( ( ( 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 81 134 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
136 naddel1 ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
137 85 63 62 136 mp3an ⊢ ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
138 68 137 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
139 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
140 63 62 139 mp2an ⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
141 130 60 140 syl2anc ⊢ ( 𝜑 → ( ( 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 131 62 143 mp2an ⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On
145 92 144 onun2i ⊢ ( ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
146 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
147 85 62 146 mp2an ⊢ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ On
148 naddcl ⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
149 131 61 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 92 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 9 10 47 3 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 mpan2d ⊢ ( 𝜑 → ( 𝑅 <s 𝑉 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
166 165 imp ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) )
167 15 27 subscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
168 31 33 subscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
169 167 168 25 sltadd1d ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) ) )
171 166 170 mpbid ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
172 15 25 27 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
174 31 25 33 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑉 ·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 171 173 175 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
177 22 29 35 120 176 slttrd ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
178 177 ex ⊢ ( 𝜑 → ( 𝑅 <s 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
179 37 39 6 ssltsepcd ⊢ ( 𝜑 → 𝐴 <s 𝑉 )
180 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 ‘ 𝑊 ) ) ) ) )
181 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 ‘ 𝑊 ) ) ) )
182 180 181 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 ‘ 𝑊 ) ) ) )
183 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
184 63 62 183 mp2an ⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
185 130 70 184 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
186 66 185 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
187 78 141 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
188 naddcl ⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑆 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ On )
189 131 75 188 mp2an ⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ On
190 84 189 onun2i ⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ) ∈ On
191 90 149 onun2i ⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On
192 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 ‘ 𝐵 ) ) ) ) )
193 190 191 95 192 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 ‘ 𝐵 ) ) ) )
194 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 ‘ 𝐵 ) ) ) ) )
195 84 189 95 194 mp3an ⊢ ( ( ( ( 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 90 149 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 195 197 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 ‘ 𝐵 ) ) ) ) )
199 193 198 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 ‘ 𝐵 ) ) ) ) )
200 186 187 199 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
201 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 ‘ 𝐸 ) ) ) ) ) )
202 200 201 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 ‘ 𝐸 ) ) ) ) ) )
203 182 202 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 ‘ 𝐸 ) ) ) ) ) )
204 1 45 45 2 10 47 49 203 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆 ) → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
205 204 simprd ⊢ ( 𝜑 → ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆 ) → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
206 179 43 205 mp2and ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) )
207 1 30 17 mulsproplem4 ⊢ ( 𝜑 → ( 𝑉 ·s 𝑆 ) ∈ No )
208 18 207 25 33 sltsubsubbd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
209 18 207 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
210 25 33 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
211 209 210 31 sltadd2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
212 208 211 bitrd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
213 206 212 mpbid ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
214 31 18 207 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) )
215 31 25 33 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
216 213 214 215 3brtr4d ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
217 oveq1 ⊢ ( 𝑅 = 𝑉 → ( 𝑅 ·s 𝐵 ) = ( 𝑉 ·s 𝐵 ) )
218 217 oveq1d ⊢ ( 𝑅 = 𝑉 → ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) )
219 oveq1 ⊢ ( 𝑅 = 𝑉 → ( 𝑅 ·s 𝑆 ) = ( 𝑉 ·s 𝑆 ) )
220 218 219 oveq12d ⊢ ( 𝑅 = 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) )
221 220 breq1d ⊢ ( 𝑅 = 𝑉 → ( ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
222 216 221 syl5ibrcom ⊢ ( 𝜑 → ( 𝑅 = 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
223 21 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
224 31 18 addscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) ∈ No )
225 224 207 subscld ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
226 225 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
227 34 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
228 ssltright ⊢ ( 𝐵 ∈ No → { 𝐵 } <<s ( R ‘ 𝐵 ) )
229 3 228 syl ⊢ ( 𝜑 → { 𝐵 } <<s ( R ‘ 𝐵 ) )
230 229 124 5 ssltsepcd ⊢ ( 𝜑 → 𝐵 <s 𝑆 )
231 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 ‘ 𝐵 ) ) ) ) )
232 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 ‘ 𝐵 ) ) ) )
233 231 232 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 ‘ 𝐵 ) ) ) )
234 134 73 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
235 185 138 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
236 144 87 onun2i ⊢ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ) ∈ On
237 189 147 onun2i ⊢ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
238 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 ‘ 𝐵 ) ) ) ) )
239 236 237 95 238 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 ‘ 𝐵 ) ) ) )
240 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 ‘ 𝐵 ) ) ) ) )
241 144 87 95 240 mp3an ⊢ ( ( ( ( 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 189 147 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 241 243 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 ‘ 𝐵 ) ) ) ) )
245 239 244 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 ‘ 𝐵 ) ) ) ) )
246 234 235 245 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ) ∪ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
247 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 ‘ 𝐸 ) ) ) ) ) )
248 246 247 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 ‘ 𝐸 ) ) ) ) ) )
249 233 248 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 ‘ 𝐸 ) ) ) ) ) )
250 1 45 45 10 9 3 49 249 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) ) )
251 250 simprd ⊢ ( 𝜑 → ( ( 𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) )
252 230 251 mpan2d ⊢ ( 𝜑 → ( 𝑉 <s 𝑅 → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) )
253 252 imp ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) )
254 207 31 20 15 sltsubsub2bd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ) )
255 15 20 subscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
256 31 207 subscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
257 255 256 18 sltadd1d ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
258 254 257 bitrd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
259 258 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
260 253 259 mpbid ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
261 15 18 20 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
262 261 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
263 31 18 207 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑉 ·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 260 262 264 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) )
266 216 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
267 223 226 227 265 266 slttrd ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
268 267 ex ⊢ ( 𝜑 → ( 𝑉 <s 𝑅 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
269 178 222 268 3jaod ⊢ ( 𝜑 → ( ( 𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
270 12 269 mpd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )