MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsproplem5 Structured version   Visualization version   GIF version

Theorem mulsproplem5 27936
Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-Mar-2025.)
Hypotheses
Ref Expression
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
Ref Expression
mulsproplem5 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑃,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑄,𝑏,𝑐,𝑑,𝑒,𝑓   𝑇,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑈,𝑏,𝑐,𝑑,𝑒,𝑓
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑄(𝑎)   𝑈(𝑎)

Proof of Theorem mulsproplem5
StepHypRef Expression
1 leftssno 27723 . . . 4 ( L ‘𝐴) ⊆ No
2 mulsproplem5.3 . . . 4 (𝜑𝑃 ∈ ( L ‘𝐴))
31, 2sselid 3972 . . 3 (𝜑𝑃 No )
4 mulsproplem5.5 . . . 4 (𝜑𝑇 ∈ ( L ‘𝐴))
51, 4sselid 3972 . . 3 (𝜑𝑇 No )
6 sltlin 27598 . . 3 ((𝑃 No 𝑇 No ) → (𝑃 <s 𝑇𝑃 = 𝑇𝑇 <s 𝑃))
73, 5, 6syl2anc 583 . 2 (𝜑 → (𝑃 <s 𝑇𝑃 = 𝑇𝑇 <s 𝑃))
8 mulsproplem.1 . . . . . . . . 9 (𝜑 → ∀𝑎 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 𝑒))))))
9 leftssold 27721 . . . . . . . . . 10 ( L ‘𝐴) ⊆ ( O ‘( bday 𝐴))
109, 2sselid 3972 . . . . . . . . 9 (𝜑𝑃 ∈ ( O ‘( bday 𝐴)))
11 mulsproplem5.2 . . . . . . . . 9 (𝜑𝐵 No )
128, 10, 11mulsproplem2 27933 . . . . . . . 8 (𝜑 → (𝑃 ·s 𝐵) ∈ No )
13 mulsproplem5.1 . . . . . . . . 9 (𝜑𝐴 No )
14 leftssold 27721 . . . . . . . . . 10 ( L ‘𝐵) ⊆ ( O ‘( bday 𝐵))
15 mulsproplem5.4 . . . . . . . . . 10 (𝜑𝑄 ∈ ( L ‘𝐵))
1614, 15sselid 3972 . . . . . . . . 9 (𝜑𝑄 ∈ ( O ‘( bday 𝐵)))
178, 13, 16mulsproplem3 27934 . . . . . . . 8 (𝜑 → (𝐴 ·s 𝑄) ∈ No )
1812, 17addscld 27813 . . . . . . 7 (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No )
198, 10, 16mulsproplem4 27935 . . . . . . 7 (𝜑 → (𝑃 ·s 𝑄) ∈ No )
2018, 19subscld 27889 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
2120adantr 480 . . . . 5 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
229, 4sselid 3972 . . . . . . . . 9 (𝜑𝑇 ∈ ( O ‘( bday 𝐴)))
238, 22, 11mulsproplem2 27933 . . . . . . . 8 (𝜑 → (𝑇 ·s 𝐵) ∈ No )
2423, 17addscld 27813 . . . . . . 7 (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No )
258, 22, 16mulsproplem4 27935 . . . . . . 7 (𝜑 → (𝑇 ·s 𝑄) ∈ No )
2624, 25subscld 27889 . . . . . 6 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) ∈ No )
2726adantr 480 . . . . 5 ((𝜑𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) ∈ No )
28 rightssold 27722 . . . . . . . . . 10 ( R ‘𝐵) ⊆ ( O ‘( bday 𝐵))
29 mulsproplem5.6 . . . . . . . . . 10 (𝜑𝑈 ∈ ( R ‘𝐵))
3028, 29sselid 3972 . . . . . . . . 9 (𝜑𝑈 ∈ ( O ‘( bday 𝐵)))
318, 13, 30mulsproplem3 27934 . . . . . . . 8 (𝜑 → (𝐴 ·s 𝑈) ∈ No )
3223, 31addscld 27813 . . . . . . 7 (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈ No )
338, 22, 30mulsproplem4 27935 . . . . . . 7 (𝜑 → (𝑇 ·s 𝑈) ∈ No )
3432, 33subscld 27889 . . . . . 6 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No )
3534adantr 480 . . . . 5 ((𝜑𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No )
36 ssltleft 27713 . . . . . . . . . . 11 (𝐵 No → ( L ‘𝐵) <<s {𝐵})
3711, 36syl 17 . . . . . . . . . 10 (𝜑 → ( L ‘𝐵) <<s {𝐵})
38 snidg 4654 . . . . . . . . . . 11 (𝐵 No 𝐵 ∈ {𝐵})
3911, 38syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ {𝐵})
4037, 15, 39ssltsepcd 27643 . . . . . . . . 9 (𝜑𝑄 <s 𝐵)
41 0sno 27675 . . . . . . . . . . . 12 0s No
4241a1i 11 . . . . . . . . . . 11 (𝜑 → 0s No )
43 leftssno 27723 . . . . . . . . . . . 12 ( L ‘𝐵) ⊆ No
4443, 15sselid 3972 . . . . . . . . . . 11 (𝜑𝑄 No )
45 bday0s 27677 . . . . . . . . . . . . . . . 16 ( bday ‘ 0s ) = ∅
4645, 45oveq12i 7413 . . . . . . . . . . . . . . 15 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
47 0elon 6408 . . . . . . . . . . . . . . . 16 ∅ ∈ On
48 naddrid 8678 . . . . . . . . . . . . . . . 16 (∅ ∈ On → (∅ +no ∅) = ∅)
4947, 48ax-mp 5 . . . . . . . . . . . . . . 15 (∅ +no ∅) = ∅
5046, 49eqtri 2752 . . . . . . . . . . . . . 14 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
5150uneq1i 4151 . . . . . . . . . . . . 13 ((( 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 4384 . . . . . . . . . . . . 13 (∅ ∪ (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄))))) = (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄))))
5351, 52eqtri 2752 . . . . . . . . . . . 12 ((( 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 27731 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑃) ∈ ( bday 𝐴))
5510, 54syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑃) ∈ ( bday 𝐴))
56 oldbdayim 27731 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ ( O ‘( bday 𝐵)) → ( bday 𝑄) ∈ ( bday 𝐵))
5716, 56syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑄) ∈ ( bday 𝐵))
58 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday 𝐴) ∈ On
59 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday 𝐵) ∈ On
60 naddel12 8695 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
6158, 59, 60mp2an 689 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6255, 57, 61syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
63 oldbdayim 27731 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑇) ∈ ( bday 𝐴))
6422, 63syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑇) ∈ ( bday 𝐴))
65 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday 𝑇) ∈ On
66 naddel1 8682 . . . . . . . . . . . . . . . . 17 ((( bday 𝑇) ∈ On ∧ ( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑇) ∈ ( bday 𝐴) ↔ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
6765, 58, 59, 66mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday 𝑇) ∈ ( bday 𝐴) ↔ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6864, 67sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6962, 68jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
70 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday 𝑃) ∈ On
71 naddel1 8682 . . . . . . . . . . . . . . . . 17 ((( bday 𝑃) ∈ On ∧ ( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑃) ∈ ( bday 𝐴) ↔ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
7270, 58, 59, 71mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday 𝑃) ∈ ( bday 𝐴) ↔ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7355, 72sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
74 naddel12 8695 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑇) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
7558, 59, 74mp2an 689 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7664, 57, 75syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7773, 76jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
78 bdayelon 27625 . . . . . . . . . . . . . . . . . 18 ( bday 𝑄) ∈ On
79 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝑃) +no ( bday 𝑄)) ∈ On)
8070, 78, 79mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝑄)) ∈ On
81 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑇) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑇) +no ( bday 𝐵)) ∈ On)
8265, 59, 81mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑇) +no ( bday 𝐵)) ∈ On
8380, 82onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∈ On
84 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑃) +no ( bday 𝐵)) ∈ On)
8570, 59, 84mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝐵)) ∈ On
86 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑇) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝑇) +no ( bday 𝑄)) ∈ On)
8765, 78, 86mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑇) +no ( bday 𝑄)) ∈ On
8885, 87onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄))) ∈ On
89 naddcl 8672 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝐴) +no ( bday 𝐵)) ∈ On)
9058, 59, 89mp2an 689 . . . . . . . . . . . . . . . 16 (( bday 𝐴) +no ( bday 𝐵)) ∈ On
91 onunel 6459 . . . . . . . . . . . . . . . 16 ((((( 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 𝐵)))))
9283, 88, 90, 91mp3an 1457 . . . . . . . . . . . . . . 15 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( 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 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
9480, 82, 90, 93mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
95 onunel 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
9685, 87, 90, 95mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
9794, 96anbi12i 626 . . . . . . . . . . . . . . 15 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵))) ↔ (((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
9892, 97bitri 275 . . . . . . . . . . . . . 14 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ (((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
9969, 77, 98sylanbrc 582 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
100 elun1 4168 . . . . . . . . . . . . 13 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
10199, 100syl 17 . . . . . . . . . . . 12 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑇) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑇) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
10253, 101eqeltrid 2829 . . . . . . . . . . 11 (𝜑 → ((( 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 𝐸))))))
1038, 42, 42, 3, 5, 44, 11, 102mulsproplem1 27932 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑃 <s 𝑇𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)))))
104103simprd 495 . . . . . . . . 9 (𝜑 → ((𝑃 <s 𝑇𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄))))
10540, 104mpan2d 691 . . . . . . . 8 (𝜑 → (𝑃 <s 𝑇 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄))))
106105imp 406 . . . . . . 7 ((𝜑𝑃 <s 𝑇) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)))
10712, 19subscld 27889 . . . . . . . . 9 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) ∈ No )
10823, 25subscld 27889 . . . . . . . . 9 (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ∈ No )
109107, 108, 17sltadd1d 27831 . . . . . . . 8 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄))))
110109adantr 480 . . . . . . 7 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄))))
111106, 110mpbid 231 . . . . . 6 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
11212, 17, 19addsubsd 27906 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
113112adantr 480 . . . . . 6 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
11423, 17, 25addsubsd 27906 . . . . . . 7 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
115114adantr 480 . . . . . 6 ((𝜑𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
116111, 113, 1153brtr4d 5170 . . . . 5 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)))
117 ssltleft 27713 . . . . . . . . . . 11 (𝐴 No → ( L ‘𝐴) <<s {𝐴})
11813, 117syl 17 . . . . . . . . . 10 (𝜑 → ( L ‘𝐴) <<s {𝐴})
119 snidg 4654 . . . . . . . . . . 11 (𝐴 No 𝐴 ∈ {𝐴})
12013, 119syl 17 . . . . . . . . . 10 (𝜑𝐴 ∈ {𝐴})
121118, 4, 120ssltsepcd 27643 . . . . . . . . 9 (𝜑𝑇 <s 𝐴)
122 lltropt 27715 . . . . . . . . . . 11 ( L ‘𝐵) <<s ( R ‘𝐵)
123122a1i 11 . . . . . . . . . 10 (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵))
124123, 15, 29ssltsepcd 27643 . . . . . . . . 9 (𝜑𝑄 <s 𝑈)
125 rightssno 27724 . . . . . . . . . . . 12 ( R ‘𝐵) ⊆ No
126125, 29sselid 3972 . . . . . . . . . . 11 (𝜑𝑈 No )
12750uneq1i 4151 . . . . . . . . . . . . 13 ((( 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 4384 . . . . . . . . . . . . 13 (∅ ∪ (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))))) = (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))))
129127, 128eqtri 2752 . . . . . . . . . . . 12 ((( 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 27731 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ ( O ‘( bday 𝐵)) → ( bday 𝑈) ∈ ( bday 𝐵))
13130, 130syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑈) ∈ ( bday 𝐵))
132 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday 𝑈) ∈ On
133 naddel2 8683 . . . . . . . . . . . . . . . . 17 ((( bday 𝑈) ∈ On ∧ ( bday 𝐵) ∈ On ∧ ( bday 𝐴) ∈ On) → (( bday 𝑈) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
134132, 59, 58, 133mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday 𝑈) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
135131, 134sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
13676, 135jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
137 naddel12 8695 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑇) ∈ ( bday 𝐴) ∧ ( bday 𝑈) ∈ ( bday 𝐵)) → (( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
13858, 59, 137mp2an 689 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) ∈ ( bday 𝐴) ∧ ( bday 𝑈) ∈ ( bday 𝐵)) → (( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
13964, 131, 138syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
140 naddel2 8683 . . . . . . . . . . . . . . . . 17 ((( bday 𝑄) ∈ On ∧ ( bday 𝐵) ∈ On ∧ ( bday 𝐴) ∈ On) → (( bday 𝑄) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
14178, 59, 58, 140mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday 𝑄) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
14257, 141sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
143139, 142jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
144 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝐴) ∈ On ∧ ( bday 𝑈) ∈ On) → (( bday 𝐴) +no ( bday 𝑈)) ∈ On)
14558, 132, 144mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝐴) +no ( bday 𝑈)) ∈ On
14687, 145onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ On
147 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑇) ∈ On ∧ ( bday 𝑈) ∈ On) → (( bday 𝑇) +no ( bday 𝑈)) ∈ On)
14865, 132, 147mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑇) +no ( bday 𝑈)) ∈ On
149 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝐴) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝐴) +no ( bday 𝑄)) ∈ On)
15058, 78, 149mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝐴) +no ( bday 𝑄)) ∈ On
151148, 150onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ On
152 onunel 6459 . . . . . . . . . . . . . . . 16 ((((( 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 𝐵)))))
153146, 151, 90, 152mp3an 1457 . . . . . . . . . . . . . . 15 ((((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( 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 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
15587, 145, 90, 154mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
156 onunel 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
157148, 150, 90, 156mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
158155, 157anbi12i 626 . . . . . . . . . . . . . . 15 ((((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵))) ↔ (((( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
159153, 158bitri 275 . . . . . . . . . . . . . 14 ((((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ (((( bday 𝑇) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
160136, 143, 159sylanbrc 582 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
161 elun1 4168 . . . . . . . . . . . . 13 ((((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) → (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
162160, 161syl 17 . . . . . . . . . . . 12 (𝜑 → (((( bday 𝑇) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
163129, 162eqeltrid 2829 . . . . . . . . . . 11 (𝜑 → ((( 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 𝐸))))))
1648, 42, 42, 5, 13, 44, 126, 163mulsproplem1 27932 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑇 <s 𝐴𝑄 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))))
165164simprd 495 . . . . . . . . 9 (𝜑 → ((𝑇 <s 𝐴𝑄 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))))
166121, 124, 165mp2and 696 . . . . . . . 8 (𝜑 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))
16733, 31, 25, 17sltsubsub3bd 27909 . . . . . . . . 9 (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))
16817, 25subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) ∈ No )
16931, 33subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ∈ No )
170168, 169, 23sltadd2d 27830 . . . . . . . . 9 (𝜑 → (((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))))
171167, 170bitrd 279 . . . . . . . 8 (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))))
172166, 171mpbid 231 . . . . . . 7 (𝜑 → ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))
17323, 17, 25addsubsassd 27905 . . . . . . 7 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))))
17423, 31, 33addsubsassd 27905 . . . . . . 7 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))
175172, 173, 1743brtr4d 5170 . . . . . 6 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
176175adantr 480 . . . . 5 ((𝜑𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
17721, 27, 35, 116, 176slttrd 27608 . . . 4 ((𝜑𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
178177ex 412 . . 3 (𝜑 → (𝑃 <s 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))))
179 oveq1 7408 . . . . . . 7 (𝑃 = 𝑇 → (𝑃 ·s 𝐵) = (𝑇 ·s 𝐵))
180179oveq1d 7416 . . . . . 6 (𝑃 = 𝑇 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) = ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)))
181 oveq1 7408 . . . . . 6 (𝑃 = 𝑇 → (𝑃 ·s 𝑄) = (𝑇 ·s 𝑄))
182180, 181oveq12d 7419 . . . . 5 (𝑃 = 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)))
183182breq1d 5148 . . . 4 (𝑃 = 𝑇 → ((((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ↔ (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))))
184175, 183syl5ibrcom 246 . . 3 (𝜑 → (𝑃 = 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))))
18520adantr 480 . . . . 5 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
18612, 31addscld 27813 . . . . . . 7 (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈ No )
1878, 10, 30mulsproplem4 27935 . . . . . . 7 (𝜑 → (𝑃 ·s 𝑈) ∈ No )
188186, 187subscld 27889 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) ∈ No )
189188adantr 480 . . . . 5 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) ∈ No )
19034adantr 480 . . . . 5 ((𝜑𝑇 <s 𝑃) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No )
191118, 2, 120ssltsepcd 27643 . . . . . . . . 9 (𝜑𝑃 <s 𝐴)
19250uneq1i 4151 . . . . . . . . . . . . 13 ((( 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 4384 . . . . . . . . . . . . 13 (∅ ∪ (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))))) = (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))))
194192, 193eqtri 2752 . . . . . . . . . . . 12 ((( 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 𝑄))))
19562, 135jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
196 naddel12 8695 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑈) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
19758, 59, 196mp2an 689 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑈) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
19855, 131, 197syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
199198, 142jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
20080, 145onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ On
201 naddcl 8672 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝑈) ∈ On) → (( bday 𝑃) +no ( bday 𝑈)) ∈ On)
20270, 132, 201mp2an 689 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝑈)) ∈ On
203202, 150onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ On
204 onunel 6459 . . . . . . . . . . . . . . . 16 ((((( 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 𝐵)))))
205200, 203, 90, 204mp3an 1457 . . . . . . . . . . . . . . 15 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( 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 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
20780, 145, 90, 206mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
208 onunel 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
209202, 150, 90, 208mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
210207, 209anbi12i 626 . . . . . . . . . . . . . . 15 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵))) ↔ (((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
211205, 210bitri 275 . . . . . . . . . . . . . 14 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ (((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))) ∧ ((( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
212195, 199, 211sylanbrc 582 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
213 elun1 4168 . . . . . . . . . . . . 13 ((((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
214212, 213syl 17 . . . . . . . . . . . 12 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑈))) ∪ ((( bday 𝑃) +no ( bday 𝑈)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
215194, 214eqeltrid 2829 . . . . . . . . . . 11 (𝜑 → ((( 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 𝐸))))))
2168, 42, 42, 3, 13, 44, 126, 215mulsproplem1 27932 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑃 <s 𝐴𝑄 <s 𝑈) → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))))
217216simprd 495 . . . . . . . . 9 (𝜑 → ((𝑃 <s 𝐴𝑄 <s 𝑈) → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))))
218191, 124, 217mp2and 696 . . . . . . . 8 (𝜑 → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))
219187, 31, 19, 17sltsubsub3bd 27909 . . . . . . . . 9 (𝜑 → (((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈))))
22017, 19subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) ∈ No )
22131, 187subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)) ∈ No )
222220, 221, 12sltadd2d 27830 . . . . . . . . 9 (𝜑 → (((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)))))
223219, 222bitrd 279 . . . . . . . 8 (𝜑 → (((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)))))
224218, 223mpbid 231 . . . . . . 7 (𝜑 → ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈))))
22512, 17, 19addsubsassd 27905 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))))
22612, 31, 187addsubsassd 27905 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈))))
227224, 225, 2263brtr4d 5170 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)))
228227adantr 480 . . . . 5 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)))
229 ssltright 27714 . . . . . . . . . . 11 (𝐵 No → {𝐵} <<s ( R ‘𝐵))
23011, 229syl 17 . . . . . . . . . 10 (𝜑 → {𝐵} <<s ( R ‘𝐵))
231230, 39, 29ssltsepcd 27643 . . . . . . . . 9 (𝜑𝐵 <s 𝑈)
23250uneq1i 4151 . . . . . . . . . . . . 13 ((( 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 4384 . . . . . . . . . . . . 13 (∅ ∪ (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵))))) = (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵))))
234232, 233eqtri 2752 . . . . . . . . . . . 12 ((( 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 6459 . . . . . . . . . . . . . . . 16 (((( 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 𝐵)))))
23682, 202, 90, 235mp3an 1457 . . . . . . . . . . . . . . 15 (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑇) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑃) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
23768, 198, 236sylanbrc 582 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
238139, 73jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
23982, 202onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ On
240148, 85onun2i 6476 . . . . . . . . . . . . . . . 16 ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵))) ∈ On
241 onunel 6459 . . . . . . . . . . . . . . . 16 ((((( 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 𝐵)))))
242239, 240, 90, 241mp3an 1457 . . . . . . . . . . . . . . 15 ((((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( 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 6459 . . . . . . . . . . . . . . . . 17 (((( 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 𝐵)))))
244148, 85, 90, 243mp3an 1457 . . . . . . . . . . . . . . . 16 (((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
245244anbi2i 622 . . . . . . . . . . . . . . 15 ((((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵))) ↔ (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
246242, 245bitri 275 . . . . . . . . . . . . . 14 ((((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ ((( bday 𝑇) +no ( bday 𝑈)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))))
247237, 238, 246sylanbrc 582 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
248 elun1 4168 . . . . . . . . . . . . 13 ((((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵)))) ∈ (( bday 𝐴) +no ( bday 𝐵)) → (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
249247, 248syl 17 . . . . . . . . . . . 12 (𝜑 → (((( bday 𝑇) +no ( bday 𝐵)) ∪ (( bday 𝑃) +no ( bday 𝑈))) ∪ ((( bday 𝑇) +no ( bday 𝑈)) ∪ (( bday 𝑃) +no ( bday 𝐵)))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
250234, 249eqeltrid 2829 . . . . . . . . . . 11 (𝜑 → ((( 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 𝐸))))))
2518, 42, 42, 5, 3, 11, 126, 250mulsproplem1 27932 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑇 <s 𝑃𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)))))
252251simprd 495 . . . . . . . . 9 (𝜑 → ((𝑇 <s 𝑃𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵))))
253231, 252mpan2d 691 . . . . . . . 8 (𝜑 → (𝑇 <s 𝑃 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵))))
254253imp 406 . . . . . . 7 ((𝜑𝑇 <s 𝑃) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)))
25533, 23, 187, 12sltsubsub2bd 27908 . . . . . . . . 9 (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈))))
25612, 187subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) ∈ No )
25723, 33subscld 27889 . . . . . . . . . 10 (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ∈ No )
258256, 257, 31sltadd1d 27831 . . . . . . . . 9 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))))
259255, 258bitrd 279 . . . . . . . 8 (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))))
260259adantr 480 . . . . . . 7 ((𝜑𝑇 <s 𝑃) → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))))
261254, 260mpbid 231 . . . . . 6 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))
26212, 31, 187addsubsd 27906 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)))
263262adantr 480 . . . . . 6 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)))
26423, 31, 33addsubsd 27906 . . . . . . 7 (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))
265264adantr 480 . . . . . 6 ((𝜑𝑇 <s 𝑃) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))
266261, 263, 2653brtr4d 5170 . . . . 5 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
267185, 189, 190, 228, 266slttrd 27608 . . . 4 ((𝜑𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
268267ex 412 . . 3 (𝜑 → (𝑇 <s 𝑃 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))))
269178, 184, 2683jaod 1425 . 2 (𝜑 → ((𝑃 <s 𝑇𝑃 = 𝑇𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))))
2707, 269mpd 15 1 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3o 1083   = wceq 1533  wcel 2098  wral 3053  cun 3938  c0 4314  {csn 4620   class class class wbr 5138  Oncon0 6354  cfv 6533  (class class class)co 7401   +no cnadd 8660   No csur 27489   <s cslt 27490   bday cbday 27491   <<s csslt 27629   0s c0s 27671   O cold 27686   L cleft 27688   R cright 27689   +s cadds 27792   -s csubs 27849   ·s cmuls 27922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27492  df-slt 27493  df-bday 27494  df-sle 27594  df-sslt 27630  df-scut 27632  df-0s 27673  df-made 27690  df-old 27691  df-left 27693  df-right 27694  df-norec 27771  df-norec2 27782  df-adds 27793  df-negs 27850  df-subs 27851
This theorem is referenced by:  mulsproplem9  27940
  Copyright terms: Public domain W3C validator