Metamath Proof Explorer

Theorem mulsproplem5

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-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 𝑒 ) ) ) ) ) )
mulsproplem5.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
mulsproplem5.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
mulsproplem5.3 ⊢ ( 𝜑 → 𝑃 ∈ ( L ‘ 𝐴 ) )
mulsproplem5.4 ⊢ ( 𝜑 → 𝑄 ∈ ( L ‘ 𝐵 ) )
mulsproplem5.5 ⊢ ( 𝜑 → 𝑇 ∈ ( L ‘ 𝐴 ) )
mulsproplem5.6 ⊢ ( 𝜑 → 𝑈 ∈ ( R ‘ 𝐵 ) )
Assertion mulsproplem5 ( 𝜑 → ( ( ( 𝑃 ·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 mulsproplem5.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 mulsproplem5.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
4 mulsproplem5.3 ⊢ ( 𝜑 → 𝑃 ∈ ( L ‘ 𝐴 ) )
5 mulsproplem5.4 ⊢ ( 𝜑 → 𝑄 ∈ ( L ‘ 𝐵 ) )
6 mulsproplem5.5 ⊢ ( 𝜑 → 𝑇 ∈ ( L ‘ 𝐴 ) )
7 mulsproplem5.6 ⊢ ( 𝜑 → 𝑈 ∈ ( R ‘ 𝐵 ) )
8 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
9 8 4 sselid ⊢ ( 𝜑 → 𝑃 ∈ No )
10 8 6 sselid ⊢ ( 𝜑 → 𝑇 ∈ No )
11 sltlin ⊢ ( ( 𝑃 ∈ No ∧ 𝑇 ∈ No ) → ( 𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃 ) )
12 9 10 11 syl2anc ⊢ ( 𝜑 → ( 𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃 ) )
13 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 13 6 sselid ⊢ ( 𝜑 → 𝑇 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
24 1 23 3 mulsproplem2 ⊢ ( 𝜑 → ( 𝑇 ·s 𝐵 ) ∈ No )
25 24 18 addscld ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) ∈ No )
26 1 23 17 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 7 sselid ⊢ ( 𝜑 → 𝑈 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
31 1 2 30 mulsproplem3 ⊢ ( 𝜑 → ( 𝐴 ·s 𝑈 ) ∈ No )
32 24 31 addscld ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) ∈ No )
33 1 23 30 mulsproplem4 ⊢ ( 𝜑 → ( 𝑇 ·s 𝑈 ) ∈ No )
34 32 33 subscld ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) ∈ No )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) ∈ No )
36 ssltleft ⊢ ( 𝐵 ∈ No → ( L ‘ 𝐵 ) <<s { 𝐵 } )
37 3 36 syl ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s { 𝐵 } )
38 snidg ⊢ ( 𝐵 ∈ No → 𝐵 ∈ { 𝐵 } )
39 3 38 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
40 37 5 39 ssltsepcd ⊢ ( 𝜑 → 𝑄 <s 𝐵 )
41 0sno ⊢ 0s ∈ No
42 41 a1i ⊢ ( 𝜑 → 0s ∈ No )
43 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
44 43 5 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 naddel1 ⊢ ( ( ( bday ‘ 𝑇 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑇 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
67 65 58 59 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 bdayelon ⊢ ( bday ‘ 𝑃 ) ∈ On
71 naddel1 ⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
72 70 58 59 71 mp3an ⊢ ( ( bday ‘ 𝑃 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
73 55 72 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
74 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑇 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
75 58 59 74 mp2an ⊢ ( ( ( bday ‘ 𝑇 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
76 64 57 75 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
77 73 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 70 78 79 mp2an ⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∈ On
81 naddcl ⊢ ( ( ( bday ‘ 𝑇 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
82 65 59 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 70 59 84 mp2an ⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ On
86 naddcl ⊢ ( ( ( bday ‘ 𝑇 ) ∈ On ∧ ( bday ‘ 𝑄 ) ∈ On ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∈ On )
87 65 78 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 9 10 44 3 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 mpan2d ⊢ ( 𝜑 → ( 𝑃 <s 𝑇 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) ) )
106 105 imp ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) )
107 15 20 subscld ⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
108 24 26 subscld ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) ∈ No )
109 107 108 18 sltadd1d ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) ) )
111 106 110 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
112 15 18 20 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑄 ) ) +s ( 𝐴 ·s 𝑄 ) ) )
114 24 18 26 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑇 ·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 111 113 115 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑃 <s 𝑇 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑇 ·s 𝑄 ) ) )
117 ssltleft ⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )
118 2 117 syl ⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s { 𝐴 } )
119 snidg ⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
120 2 119 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
121 118 6 120 ssltsepcd ⊢ ( 𝜑 → 𝑇 <s 𝐴 )
122 lltropt ⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
123 122 a1i ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
124 123 5 7 ssltsepcd ⊢ ( 𝜑 → 𝑄 <s 𝑈 )
125 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
126 125 7 sselid ⊢ ( 𝜑 → 𝑈 ∈ No )
127 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 ‘ 𝑄 ) ) ) ) )
128 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 ‘ 𝑄 ) ) ) )
129 127 128 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 ‘ 𝑄 ) ) ) )
130 oldbdayim ⊢ ( 𝑈 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) )
131 30 130 syl ⊢ ( 𝜑 → ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) )
132 bdayelon ⊢ ( bday ‘ 𝑈 ) ∈ On
133 naddel2 ⊢ ( ( ( bday ‘ 𝑈 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
134 132 59 58 133 mp3an ⊢ ( ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
135 131 134 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
136 76 135 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
137 naddel12 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑇 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
138 58 59 137 mp2an ⊢ ( ( ( bday ‘ 𝑇 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑈 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
139 64 131 138 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
140 naddel2 ⊢ ( ( ( bday ‘ 𝑄 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
141 78 59 58 140 mp3an ⊢ ( ( bday ‘ 𝑄 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
142 57 141 sylib ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
143 139 142 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
144 naddcl ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑈 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ On )
145 58 132 144 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ∈ On
146 87 145 onun2i ⊢ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ) ∈ On
147 naddcl ⊢ ( ( ( bday ‘ 𝑇 ) ∈ On ∧ ( bday ‘ 𝑈 ) ∈ On ) → ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ On )
148 65 132 147 mp2an ⊢ ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ On
149 naddcl ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑄 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On )
150 58 78 149 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ On
151 148 150 onun2i ⊢ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ∈ On
152 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 ‘ 𝐵 ) ) ) ) )
153 146 151 90 152 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 ‘ 𝐵 ) ) ) )
154 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 ‘ 𝐵 ) ) ) ) )
155 87 145 90 154 mp3an ⊢ ( ( ( ( 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 148 150 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 155 157 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 ‘ 𝐵 ) ) ) ) )
159 153 158 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 ‘ 𝐵 ) ) ) ) )
160 136 143 159 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ) ∪ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
161 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 ‘ 𝐸 ) ) ) ) ) )
162 160 161 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 ‘ 𝐸 ) ) ) ) ) )
163 129 162 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 ‘ 𝐸 ) ) ) ) ) )
164 1 42 42 10 2 44 126 163 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈 ) → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ) ) )
165 164 simprd ⊢ ( 𝜑 → ( ( 𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈 ) → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ) )
166 121 124 165 mp2and ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) )
167 33 31 26 18 sltsubsub3bd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ) )
168 18 26 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) ∈ No )
169 31 33 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ∈ No )
170 168 169 24 sltadd2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ↔ ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) ) <s ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ) ) )
171 167 170 bitrd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) ) <s ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ) ) )
172 166 171 mpbid ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) ) <s ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑇 ·s 𝑈 ) ) ) )
173 24 18 26 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑇 ·s 𝑄 ) ) = ( ( 𝑇 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑇 ·s 𝑄 ) ) ) )
174 24 31 33 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑇 ·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 116 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 oveq1 ⊢ ( 𝑃 = 𝑇 → ( 𝑃 ·s 𝐵 ) = ( 𝑇 ·s 𝐵 ) )
180 179 oveq1d ⊢ ( 𝑃 = 𝑇 → ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) = ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) )
181 oveq1 ⊢ ( 𝑃 = 𝑇 → ( 𝑃 ·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 15 31 addscld ⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) ∈ No )
187 1 14 30 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 118 4 120 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 135 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 55 131 197 syl2anc ⊢ ( 𝜑 → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
199 198 142 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑄 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
200 80 145 onun2i ⊢ ( ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑄 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑈 ) ) ) ∈ On
201 naddcl ⊢ ( ( ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝑈 ) ∈ On ) → ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ∈ On )
202 70 132 201 mp2an ⊢ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ∈ On
203 202 150 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 145 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 202 150 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 9 2 44 126 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 191 124 217 mp2and ⊢ ( 𝜑 → ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) )
219 187 31 20 18 sltsubsub3bd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ) )
220 18 20 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ∈ No )
221 31 187 subscld ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ∈ No )
222 220 221 15 sltadd2d ⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ) ) )
223 219 222 bitrd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( 𝐴 ·s 𝑈 ) -s ( 𝐴 ·s 𝑄 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ) ) )
224 218 223 mpbid ⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) <s ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ) )
225 15 18 20 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑄 ) -s ( 𝑃 ·s 𝑄 ) ) ) )
226 15 31 187 addsubsassd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑃 ·s 𝑈 ) ) = ( ( 𝑃 ·s 𝐵 ) +s ( ( 𝐴 ·s 𝑈 ) -s ( 𝑃 ·s 𝑈 ) ) ) )
227 224 225 226 3brtr4d ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑃 ·s 𝑈 ) ) )
228 227 adantr ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑃 ·s 𝑈 ) ) )
229 ssltright ⊢ ( 𝐵 ∈ No → { 𝐵 } <<s ( R ‘ 𝐵 ) )
230 3 229 syl ⊢ ( 𝜑 → { 𝐵 } <<s ( R ‘ 𝐵 ) )
231 230 39 7 ssltsepcd ⊢ ( 𝜑 → 𝐵 <s 𝑈 )
232 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 ‘ 𝐵 ) ) ) ) )
233 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 ‘ 𝐵 ) ) ) )
234 232 233 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 ‘ 𝐵 ) ) ) )
235 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 ‘ 𝐵 ) ) ) ) )
236 82 202 90 235 mp3an ⊢ ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
237 68 198 236 sylanbrc ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
238 139 73 jca ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
239 82 202 onun2i ⊢ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∈ On
240 148 85 onun2i ⊢ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ) ∈ On
241 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 ‘ 𝐵 ) ) ) ) )
242 239 240 90 241 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 ‘ 𝐵 ) ) ) )
243 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 ‘ 𝐵 ) ) ) ) )
244 148 85 90 243 mp3an ⊢ ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
245 244 anbi2i ⊢ ( ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ↔ ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∧ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) ) )
246 242 245 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 ‘ 𝐵 ) ) ) ) )
247 237 238 246 sylanbrc ⊢ ( 𝜑 → ( ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝑈 ) ) ) ∪ ( ( ( bday ‘ 𝑇 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑃 ) +no ( bday ‘ 𝐵 ) ) ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
248 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 ‘ 𝐸 ) ) ) ) ) )
249 247 248 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 ‘ 𝐸 ) ) ) ) ) )
250 234 249 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 ‘ 𝐸 ) ) ) ) ) )
251 1 42 42 10 9 3 126 250 mulsproplem1 ⊢ ( 𝜑 → ( ( 0s ·s 0s ) ∈ No ∧ ( ( 𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈 ) → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ) ) )
252 251 simprd ⊢ ( 𝜑 → ( ( 𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈 ) → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ) )
253 231 252 mpan2d ⊢ ( 𝜑 → ( 𝑇 <s 𝑃 → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ) )
254 253 imp ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) )
255 33 24 187 15 sltsubsub2bd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ↔ ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) ) )
256 15 187 subscld ⊢ ( 𝜑 → ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) ∈ No )
257 24 33 subscld ⊢ ( 𝜑 → ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) ∈ No )
258 256 257 31 sltadd1d ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) <s ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) ) )
259 255 258 bitrd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) ) )
260 259 adantr ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑇 ·s 𝑈 ) -s ( 𝑇 ·s 𝐵 ) ) <s ( ( 𝑃 ·s 𝑈 ) -s ( 𝑃 ·s 𝐵 ) ) ↔ ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) ) )
261 254 260 mpbid ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑃 ·s 𝐵 ) -s ( 𝑃 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) )
262 15 31 187 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑃 ·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 24 31 33 addsubsd ⊢ ( 𝜑 → ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) = ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) )
265 264 adantr ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) = ( ( ( 𝑇 ·s 𝐵 ) -s ( 𝑇 ·s 𝑈 ) ) +s ( 𝐴 ·s 𝑈 ) ) )
266 261 263 265 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑃 ·s 𝑈 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) )
267 185 189 190 228 266 slttrd ⊢ ( ( 𝜑 ∧ 𝑇 <s 𝑃 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) )
268 267 ex ⊢ ( 𝜑 → ( 𝑇 <s 𝑃 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) ) )
269 178 184 268 3jaod ⊢ ( 𝜑 → ( ( 𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃 ) → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) ) )
270 12 269 mpd ⊢ ( 𝜑 → ( ( ( 𝑃 ·s 𝐵 ) +s ( 𝐴 ·s 𝑄 ) ) -s ( 𝑃 ·s 𝑄 ) ) <s ( ( ( 𝑇 ·s 𝐵 ) +s ( 𝐴 ·s 𝑈 ) ) -s ( 𝑇 ·s 𝑈 ) ) )