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