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 4 rightnod ⊢ ( 𝜑 → 𝑅 ∈ No )
9 6 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 7 leftoldd ⊢ ( 𝜑 → 𝑊 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
21 1 2 20 mulsproplem3 ⊢ ( 𝜑 → ( 𝐴 ·s 𝑊 ) ∈ No )
22 13 21 addscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
23 1 12 20 mulsproplem4 ⊢ ( 𝜑 → ( 𝑅 ·s 𝑊 ) ∈ No )
24 22 23 subscld ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
26 6 rightoldd ⊢ ( 𝜑 → 𝑉 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
27 1 26 3 mulsproplem2 ⊢ ( 𝜑 → ( 𝑉 ·s 𝐵 ) ∈ No )
28 27 21 addscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) ∈ No )
29 1 26 20 mulsproplem4 ⊢ ( 𝜑 → ( 𝑉 ·s 𝑊 ) ∈ No )
30 28 29 subscld ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
32 sltsright ⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )
33 2 32 syl ⊢ ( 𝜑 → { 𝐴 } <<s ( R ‘ 𝐴 ) )
34 snidg ⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
35 2 34 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
36 33 35 4 sltssepcd ⊢ ( 𝜑 → 𝐴 <s 𝑅 )
37 lltr ⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
38 37 a1i ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
39 38 7 5 sltssepcd ⊢ ( 𝜑 → 𝑊 <s 𝑆 )
40 0no ⊢ 0s ∈ No
41 40 a1i ⊢ ( 𝜑 → 0s ∈ No )
42 7 leftnod ⊢ ( 𝜑 → 𝑊 ∈ No )
43 5 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 naddel2 ⊢ ( ( ( 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 57 56 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 bdayon ⊢ ( bday ‘ 𝑆 ) ∈ On
70 naddel2 ⊢ ( ( ( bday ‘ 𝑆 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
71 69 56 57 70 mp3an ⊢ ( ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
72 64 71 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
73 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
74 57 56 73 mp2an ⊢ ( ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
75 62 54 74 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
76 72 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 57 55 77 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ On
79 bdayon ⊢ ( bday ‘ 𝑅 ) ∈ On
80 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝑆 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ∈ On )
81 79 69 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 57 69 83 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ On
85 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
86 79 55 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 57 56 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 2 8 42 43 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 36 39 103 mp2and ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝑊 ) ) )
105 15 17 21 23 ltsubsubsbd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝑊 ) ) ↔ ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑅 ·s 𝑊 ) ) ) )
106 15 17 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
107 21 23 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
108 106 107 13 ltadds2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·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 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( 𝑅 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑅 ·s 𝑆 ) ) ) )
112 13 21 23 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑅 ·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 3 115 syl ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s { 𝐵 } )
117 snidg ⊢ ( 𝐵 ∈ No → 𝐵 ∈ { 𝐵 } )
118 3 117 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
119 116 7 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 naddel1 ⊢ ( ( ( 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 75 128 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
130 naddel1 ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
131 79 57 56 130 mp3an ⊢ ( ( bday ‘ 𝑅 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
132 62 131 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
133 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
134 57 56 133 mp2an ⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑊 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
135 124 54 134 syl2anc ⊢ ( 𝜑 → ( ( 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 125 56 137 mp2an ⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ On
139 86 138 onun2i ⊢ ( ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
140 naddcl ⊢ ( ( ( bday ‘ 𝑅 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
141 79 56 140 mp2an ⊢ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ On
142 naddcl ⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑊 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ On )
143 125 55 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 86 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 8 9 42 3 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 mpan2d ⊢ ( 𝜑 → ( 𝑅 <s 𝑉 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
160 159 imp ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) )
161 13 23 subscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) ∈ No )
162 27 29 subscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
163 161 162 21 ltadds1d ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) ) )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) ) )
165 160 164 mpbid ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
166 13 21 23 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑊 ) ) +s ( 𝐴 ·s 𝑊 ) ) )
168 27 21 29 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑉 ·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 165 167 169 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑅 ·s 𝑊 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
171 19 25 31 114 170 ltstrd ⊢ ( ( 𝜑 ∧ 𝑅 <s 𝑉 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
172 171 ex ⊢ ( 𝜑 → ( 𝑅 <s 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
173 33 35 6 sltssepcd ⊢ ( 𝜑 → 𝐴 <s 𝑉 )
174 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 ‘ 𝑊 ) ) ) ) )
175 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 ‘ 𝑊 ) ) ) )
176 174 175 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 ‘ 𝑊 ) ) ) )
177 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
178 57 56 177 mp2an ⊢ ( ( ( bday ‘ 𝑉 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑆 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
179 124 64 178 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
180 60 179 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
181 72 135 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
182 naddcl ⊢ ( ( ( bday ‘ 𝑉 ) ∈ On ∧ ( bday ‘ 𝑆 ) ∈ On ) → ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ On )
183 125 69 182 mp2an ⊢ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ On
184 78 183 onun2i ⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ) ∈ On
185 84 143 onun2i ⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ∈ On
186 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 ‘ 𝐵 ) ) ) ) )
187 184 185 89 186 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 ‘ 𝐵 ) ) ) )
188 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 ‘ 𝐵 ) ) ) ) )
189 78 183 89 188 mp3an ⊢ ( ( ( ( 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 84 143 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 189 191 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 ‘ 𝐵 ) ) ) ) )
193 187 192 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 ‘ 𝐵 ) ) ) ) )
194 180 181 193 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑊 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ) ∪ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑊 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
195 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 ‘ 𝐸 ) ) ) ) ) )
196 194 195 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 ‘ 𝐸 ) ) ) ) ) )
197 176 196 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 ‘ 𝐸 ) ) ) ) ) )
198 1 41 41 2 9 42 43 197 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆 ) → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
199 198 simprd ⊢ ( 𝜑 → ( ( 𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆 ) → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
200 173 39 199 mp2and ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) )
201 1 26 14 mulsproplem4 ⊢ ( 𝜑 → ( 𝑉 ·s 𝑆 ) ∈ No )
202 15 201 21 29 ltsubsubsbd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
203 15 201 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
204 21 29 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
205 203 204 27 ltadds2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
206 202 205 bitrd ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑆 ) -s ( 𝐴 ·s 𝑊 ) ) <s ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) ) )
207 200 206 mpbid ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) <s ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
208 27 15 201 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑆 ) -s ( 𝑉 ·s 𝑆 ) ) ) )
209 27 21 29 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑊 ) -s ( 𝑉 ·s 𝑊 ) ) ) )
210 207 208 209 3brtr4d ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
211 oveq1 ⊢ ( 𝑅 = 𝑉 → ( 𝑅 ·s 𝐵 ) = ( 𝑉 ·s 𝐵 ) )
212 211 oveq1d ⊢ ( 𝑅 = 𝑉 → ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) = ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) )
213 oveq1 ⊢ ( 𝑅 = 𝑉 → ( 𝑅 ·s 𝑆 ) = ( 𝑉 ·s 𝑆 ) )
214 212 213 oveq12d ⊢ ( 𝑅 = 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) )
215 214 breq1d ⊢ ( 𝑅 = 𝑉 → ( ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ↔ ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
216 210 215 syl5ibrcom ⊢ ( 𝜑 → ( 𝑅 = 𝑉 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
217 18 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
218 27 15 addscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) ∈ No )
219 218 201 subscld ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
220 219 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
221 30 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ∈ No )
222 sltsright ⊢ ( 𝐵 ∈ No → { 𝐵 } <<s ( R ‘ 𝐵 ) )
223 3 222 syl ⊢ ( 𝜑 → { 𝐵 } <<s ( R ‘ 𝐵 ) )
224 223 118 5 sltssepcd ⊢ ( 𝜑 → 𝐵 <s 𝑆 )
225 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 ‘ 𝐵 ) ) ) ) )
226 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 ‘ 𝐵 ) ) ) )
227 225 226 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 ‘ 𝐵 ) ) ) )
228 128 67 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
229 179 132 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
230 138 81 onun2i ⊢ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ) ∈ On
231 183 141 onun2i ⊢ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
232 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 ‘ 𝐵 ) ) ) ) )
233 230 231 89 232 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 ‘ 𝐵 ) ) ) )
234 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 ‘ 𝐵 ) ) ) ) )
235 138 81 89 234 mp3an ⊢ ( ( ( ( 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 183 141 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 235 237 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 ‘ 𝐵 ) ) ) ) )
239 233 238 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 ‘ 𝐵 ) ) ) ) )
240 228 229 239 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝑆 ) ) ) ∪ ( ( ( bday ‘ 𝑉 ) +no ( bday ‘ 𝑆 ) ) ∪ ( ( bday ‘ 𝑅 ) +no ( bday ‘ 𝐵 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
241 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 ‘ 𝐸 ) ) ) ) ) )
242 240 241 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 ‘ 𝐸 ) ) ) ) ) )
243 227 242 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 ‘ 𝐸 ) ) ) ) ) )
244 1 41 41 9 8 3 43 243 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) ) )
245 244 simprd ⊢ ( 𝜑 → ( ( 𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) )
246 224 245 mpan2d ⊢ ( 𝜑 → ( 𝑉 <s 𝑅 → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ) )
247 246 imp ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) )
248 201 27 17 13 ltsubsubs2bd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ) )
249 13 17 subscld ⊢ ( 𝜑 → ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) ∈ No )
250 27 201 subscld ⊢ ( 𝜑 → ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ∈ No )
251 249 250 15 ltadds1d ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
252 248 251 bitrd ⊢ ( 𝜑 → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
253 252 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝑆 ) -s ( 𝑉 ·s 𝐵 ) ) <s ( ( 𝑅 ·s 𝑆 ) -s ( 𝑅 ·s 𝐵 ) ) ↔ ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) ) )
254 247 253 mpbid ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) -s ( 𝑉 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
255 13 15 17 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
256 255 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) = ( ( ( 𝑅 ·s 𝐵 ) -s ( 𝑅 ·s 𝑆 ) ) +s ( 𝐴 ·s 𝑆 ) ) )
257 27 15 201 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑉 ·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 254 256 258 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) )
260 210 adantr ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑉 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
261 217 220 221 259 260 ltstrd ⊢ ( ( 𝜑 ∧ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )
262 261 ex ⊢ ( 𝜑 → ( 𝑉 <s 𝑅 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
263 172 216 262 3jaod ⊢ ( 𝜑 → ( ( 𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅 ) → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) ) )
264 11 263 mpd ⊢ ( 𝜑 → ( ( ( 𝑅 ·s 𝐵 ) +s ( 𝐴 ·s 𝑆 ) ) -s ( 𝑅 ·s 𝑆 ) ) <s ( ( ( 𝑉 ·s 𝐵 ) +s ( 𝐴 ·s 𝑊 ) ) -s ( 𝑉 ·s 𝑊 ) ) )