Metamath Proof Explorer

Theorem mulsproplem6

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