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

Theorem mulsproplem6 28162
Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-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 𝑒))))))
mulsproplem6.1 (𝜑𝐴 No )
mulsproplem6.2 (𝜑𝐵 No )
mulsproplem6.3 (𝜑𝑃 ∈ ( L ‘𝐴))
mulsproplem6.4 (𝜑𝑄 ∈ ( L ‘𝐵))
mulsproplem6.5 (𝜑𝑉 ∈ ( R ‘𝐴))
mulsproplem6.6 (𝜑𝑊 ∈ ( L ‘𝐵))
Assertion
Ref Expression
mulsproplem6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑃,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑄,𝑏,𝑐,𝑑,𝑒,𝑓   𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑊,𝑏,𝑐,𝑑,𝑒,𝑓
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑄(𝑎)   𝑊(𝑎)

Proof of Theorem mulsproplem6
StepHypRef Expression
1 leftssno 27934 . . . 4 ( L ‘𝐵) ⊆ No
2 mulsproplem6.4 . . . 4 (𝜑𝑄 ∈ ( L ‘𝐵))
31, 2sselid 3993 . . 3 (𝜑𝑄 No )
4 mulsproplem6.6 . . . 4 (𝜑𝑊 ∈ ( L ‘𝐵))
51, 4sselid 3993 . . 3 (𝜑𝑊 No )
6 sltlin 27809 . . 3 ((𝑄 No 𝑊 No ) → (𝑄 <s 𝑊𝑄 = 𝑊𝑊 <s 𝑄))
73, 5, 6syl2anc 584 . 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 27932 . . . . . . . . . 10 ( L ‘𝐴) ⊆ ( O ‘( bday 𝐴))
10 mulsproplem6.3 . . . . . . . . . 10 (𝜑𝑃 ∈ ( L ‘𝐴))
119, 10sselid 3993 . . . . . . . . 9 (𝜑𝑃 ∈ ( O ‘( bday 𝐴)))
12 mulsproplem6.2 . . . . . . . . 9 (𝜑𝐵 No )
138, 11, 12mulsproplem2 28158 . . . . . . . 8 (𝜑 → (𝑃 ·s 𝐵) ∈ No )
14 mulsproplem6.1 . . . . . . . . 9 (𝜑𝐴 No )
15 leftssold 27932 . . . . . . . . . 10 ( L ‘𝐵) ⊆ ( O ‘( bday 𝐵))
1615, 2sselid 3993 . . . . . . . . 9 (𝜑𝑄 ∈ ( O ‘( bday 𝐵)))
178, 14, 16mulsproplem3 28159 . . . . . . . 8 (𝜑 → (𝐴 ·s 𝑄) ∈ No )
1813, 17addscld 28028 . . . . . . 7 (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No )
198, 11, 16mulsproplem4 28160 . . . . . . 7 (𝜑 → (𝑃 ·s 𝑄) ∈ No )
2018, 19subscld 28108 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
2120adantr 480 . . . . 5 ((𝜑𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
2215, 4sselid 3993 . . . . . . . . 9 (𝜑𝑊 ∈ ( O ‘( bday 𝐵)))
238, 14, 22mulsproplem3 28159 . . . . . . . 8 (𝜑 → (𝐴 ·s 𝑊) ∈ No )
2413, 23addscld 28028 . . . . . . 7 (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No )
258, 11, 22mulsproplem4 28160 . . . . . . 7 (𝜑 → (𝑃 ·s 𝑊) ∈ No )
2624, 25subscld 28108 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) ∈ No )
2726adantr 480 . . . . 5 ((𝜑𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) ∈ No )
28 rightssold 27933 . . . . . . . . . 10 ( R ‘𝐴) ⊆ ( O ‘( bday 𝐴))
29 mulsproplem6.5 . . . . . . . . . 10 (𝜑𝑉 ∈ ( R ‘𝐴))
3028, 29sselid 3993 . . . . . . . . 9 (𝜑𝑉 ∈ ( O ‘( bday 𝐴)))
318, 30, 12mulsproplem2 28158 . . . . . . . 8 (𝜑 → (𝑉 ·s 𝐵) ∈ No )
3231, 23addscld 28028 . . . . . . 7 (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No )
338, 30, 22mulsproplem4 28160 . . . . . . 7 (𝜑 → (𝑉 ·s 𝑊) ∈ No )
3432, 33subscld 28108 . . . . . 6 (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No )
3534adantr 480 . . . . 5 ((𝜑𝑄 <s 𝑊) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No )
36 ssltleft 27924 . . . . . . . . . . 11 (𝐴 No → ( L ‘𝐴) <<s {𝐴})
3714, 36syl 17 . . . . . . . . . 10 (𝜑 → ( L ‘𝐴) <<s {𝐴})
38 snidg 4665 . . . . . . . . . . 11 (𝐴 No 𝐴 ∈ {𝐴})
3914, 38syl 17 . . . . . . . . . 10 (𝜑𝐴 ∈ {𝐴})
4037, 10, 39ssltsepcd 27854 . . . . . . . . 9 (𝜑𝑃 <s 𝐴)
41 0sno 27886 . . . . . . . . . . . 12 0s No
4241a1i 11 . . . . . . . . . . 11 (𝜑 → 0s No )
43 leftssno 27934 . . . . . . . . . . . 12 ( L ‘𝐴) ⊆ No
4443, 10sselid 3993 . . . . . . . . . . 11 (𝜑𝑃 No )
45 bday0s 27888 . . . . . . . . . . . . . . . 16 ( bday ‘ 0s ) = ∅
4645, 45oveq12i 7443 . . . . . . . . . . . . . . 15 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
47 0elon 6440 . . . . . . . . . . . . . . . 16 ∅ ∈ On
48 naddrid 8720 . . . . . . . . . . . . . . . 16 (∅ ∈ On → (∅ +no ∅) = ∅)
4947, 48ax-mp 5 . . . . . . . . . . . . . . 15 (∅ +no ∅) = ∅
5046, 49eqtri 2763 . . . . . . . . . . . . . 14 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
5150uneq1i 4174 . . . . . . . . . . . . 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 4402 . . . . . . . . . . . . 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 2763 . . . . . . . . . . . 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 27942 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑃) ∈ ( bday 𝐴))
5511, 54syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑃) ∈ ( bday 𝐴))
56 oldbdayim 27942 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ ( O ‘( bday 𝐵)) → ( bday 𝑄) ∈ ( bday 𝐵))
5716, 56syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑄) ∈ ( bday 𝐵))
58 bdayelon 27836 . . . . . . . . . . . . . . . . 17 ( bday 𝐴) ∈ On
59 bdayelon 27836 . . . . . . . . . . . . . . . . 17 ( bday 𝐵) ∈ On
60 naddel12 8737 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
6158, 59, 60mp2an 692 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6255, 57, 61syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
63 oldbdayim 27942 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ ( O ‘( bday 𝐵)) → ( bday 𝑊) ∈ ( bday 𝐵))
6422, 63syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑊) ∈ ( bday 𝐵))
65 bdayelon 27836 . . . . . . . . . . . . . . . . 17 ( bday 𝑊) ∈ On
66 naddel2 8725 . . . . . . . . . . . . . . . . 17 ((( bday 𝑊) ∈ On ∧ ( bday 𝐵) ∈ On ∧ ( bday 𝐴) ∈ On) → (( bday 𝑊) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
6765, 59, 58, 66mp3an 1460 . . . . . . . . . . . . . . . 16 (( bday 𝑊) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6864, 67sylib 218 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
6962, 68jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
70 naddel12 8737 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑊) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
7158, 59, 70mp2an 692 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) ∈ ( bday 𝐴) ∧ ( bday 𝑊) ∈ ( bday 𝐵)) → (( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7255, 64, 71syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
73 bdayelon 27836 . . . . . . . . . . . . . . . . 17 ( bday 𝑄) ∈ On
74 naddel2 8725 . . . . . . . . . . . . . . . . 17 ((( bday 𝑄) ∈ On ∧ ( bday 𝐵) ∈ On ∧ ( bday 𝐴) ∈ On) → (( bday 𝑄) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
7573, 59, 58, 74mp3an 1460 . . . . . . . . . . . . . . . 16 (( bday 𝑄) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7657, 75sylib 218 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
7772, 76jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
78 bdayelon 27836 . . . . . . . . . . . . . . . . . 18 ( bday 𝑃) ∈ On
79 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝑃) +no ( bday 𝑄)) ∈ On)
8078, 73, 79mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝑄)) ∈ On
81 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝐴) ∈ On ∧ ( bday 𝑊) ∈ On) → (( bday 𝐴) +no ( bday 𝑊)) ∈ On)
8258, 65, 81mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝐴) +no ( bday 𝑊)) ∈ On
8380, 82onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑊))) ∈ On
84 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝑊) ∈ On) → (( bday 𝑃) +no ( bday 𝑊)) ∈ On)
8578, 65, 84mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝑊)) ∈ On
86 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝐴) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝐴) +no ( bday 𝑄)) ∈ On)
8758, 73, 86mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝐴) +no ( bday 𝑄)) ∈ On
8885, 87onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ On
89 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝐴) +no ( bday 𝐵)) ∈ On)
9058, 59, 89mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝐴) +no ( bday 𝐵)) ∈ On
91 onunel 6491 . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . 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 6491 . . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑊))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
95 onunel 6491 . . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝐴) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
9794, 96anbi12i 628 . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝐴) +no ( bday 𝑊))) ∪ ((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝐴) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
100 elun1 4192 . . . . . . . . . . . . 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 2843 . . . . . . . . . . 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, 44, 14, 3, 5, 102mulsproplem1 28157 . . . . . . . . . 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, 104mpand 695 . . . . . . . 8 (𝜑 → (𝑄 <s 𝑊 → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄))))
106105imp 406 . . . . . . 7 ((𝜑𝑄 <s 𝑊) → ((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)))
10725, 23, 19, 17sltsubsub3bd 28130 . . . . . . . . 9 (𝜑 → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))
10817, 19subscld 28108 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) ∈ No )
10923, 25subscld 28108 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)) ∈ No )
110108, 109, 13sltadd2d 28045 . . . . . . . . 9 (𝜑 → (((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))))
111107, 110bitrd 279 . . . . . . . 8 (𝜑 → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))))
112111adantr 480 . . . . . . 7 ((𝜑𝑄 <s 𝑊) → (((𝑃 ·s 𝑊) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊)))))
113106, 112mpbid 232 . . . . . 6 ((𝜑𝑄 <s 𝑊) → ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))
11413, 17, 19addsubsassd 28126 . . . . . . 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 𝑄))))
11613, 23, 25addsubsassd 28126 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))
117116adantr 480 . . . . . 6 ((𝜑𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑃 ·s 𝑊))))
118113, 115, 1173brtr4d 5180 . . . . 5 ((𝜑𝑄 <s 𝑊) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)))
119 lltropt 27926 . . . . . . . . . . 11 ( L ‘𝐴) <<s ( R ‘𝐴)
120119a1i 11 . . . . . . . . . 10 (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
121120, 10, 29ssltsepcd 27854 . . . . . . . . 9 (𝜑𝑃 <s 𝑉)
122 ssltleft 27924 . . . . . . . . . . 11 (𝐵 No → ( L ‘𝐵) <<s {𝐵})
12312, 122syl 17 . . . . . . . . . 10 (𝜑 → ( L ‘𝐵) <<s {𝐵})
124 snidg 4665 . . . . . . . . . . 11 (𝐵 No 𝐵 ∈ {𝐵})
12512, 124syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ {𝐵})
126123, 4, 125ssltsepcd 27854 . . . . . . . . 9 (𝜑𝑊 <s 𝐵)
127 rightssno 27935 . . . . . . . . . . . 12 ( R ‘𝐴) ⊆ No
128127, 29sselid 3993 . . . . . . . . . . 11 (𝜑𝑉 No )
12950uneq1i 4174 . . . . . . . . . . . . 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 𝑊)))))
130 0un 4402 . . . . . . . . . . . . 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 𝑊))))
131129, 130eqtri 2763 . . . . . . . . . . . 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 𝑊))))
132 oldbdayim 27942 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ ( O ‘( bday 𝐴)) → ( bday 𝑉) ∈ ( bday 𝐴))
13330, 132syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ( bday 𝑉) ∈ ( bday 𝐴))
134 bdayelon 27836 . . . . . . . . . . . . . . . . 17 ( bday 𝑉) ∈ On
135 naddel1 8724 . . . . . . . . . . . . . . . . 17 ((( bday 𝑉) ∈ On ∧ ( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑉) ∈ ( bday 𝐴) ↔ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
136134, 58, 59, 135mp3an 1460 . . . . . . . . . . . . . . . 16 (( bday 𝑉) ∈ ( bday 𝐴) ↔ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
137133, 136sylib 218 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
13872, 137jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
139 naddel1 8724 . . . . . . . . . . . . . . . . 17 ((( bday 𝑃) ∈ On ∧ ( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑃) ∈ ( bday 𝐴) ↔ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
14078, 58, 59, 139mp3an 1460 . . . . . . . . . . . . . . . 16 (( bday 𝑃) ∈ ( bday 𝐴) ↔ (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
14155, 140sylib 218 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
142 naddel12 8737 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑉) ∈ ( bday 𝐴) ∧ ( bday 𝑊) ∈ ( bday 𝐵)) → (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
14358, 59, 142mp2an 692 . . . . . . . . . . . . . . . 16 ((( bday 𝑉) ∈ ( bday 𝐴) ∧ ( bday 𝑊) ∈ ( bday 𝐵)) → (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
144133, 64, 143syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
145141, 144jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
146 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑉) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑉) +no ( bday 𝐵)) ∈ On)
147134, 59, 146mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑉) +no ( bday 𝐵)) ∈ On
14885, 147onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∈ On
149 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑃) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝑃) +no ( bday 𝐵)) ∈ On)
15078, 59, 149mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑃) +no ( bday 𝐵)) ∈ On
151 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑉) ∈ On ∧ ( bday 𝑊) ∈ On) → (( bday 𝑉) +no ( bday 𝑊)) ∈ On)
152134, 65, 151mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑉) +no ( bday 𝑊)) ∈ On
153150, 152onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑊))) ∈ On
154 onunel 6491 . . . . . . . . . . . . . . . 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 𝐵)))))
155148, 153, 90, 154mp3an 1460 . . . . . . . . . . . . . . 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 𝐵))))
156 onunel 6491 . . . . . . . . . . . . . . . . 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 𝐵)))))
15785, 147, 90, 156mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
158 onunel 6491 . . . . . . . . . . . . . . . . 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 𝐵)))))
159150, 152, 90, 158mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑊))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
160157, 159anbi12i 628 . . . . . . . . . . . . . . 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 𝐵)))))
161155, 160bitri 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 𝐵)))))
162138, 145, 161sylanbrc 583 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑃) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑊)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
163 elun1 4192 . . . . . . . . . . . . 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 𝐸))))))
164162, 163syl 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 𝐸))))))
165131, 164eqeltrid 2843 . . . . . . . . . . 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 𝐸))))))
1668, 42, 42, 44, 128, 5, 12, 165mulsproplem1 28157 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑃 <s 𝑉𝑊 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)))))
167166simprd 495 . . . . . . . . 9 (𝜑 → ((𝑃 <s 𝑉𝑊 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊))))
168121, 126, 167mp2and 699 . . . . . . . 8 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)))
16913, 25subscld 28108 . . . . . . . . 9 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) ∈ No )
17031, 33subscld 28108 . . . . . . . . 9 (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ∈ No )
171169, 170, 23sltadd1d 28046 . . . . . . . 8 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊))))
172168, 171mpbid 232 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
17313, 23, 25addsubsd 28127 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
17431, 23, 33addsubsd 28127 . . . . . . 7 (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
175172, 173, 1743brtr4d 5180 . . . . . 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, 118, 176slttrd 27819 . . . 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 oveq2 7439 . . . . . . 7 (𝑄 = 𝑊 → (𝐴 ·s 𝑄) = (𝐴 ·s 𝑊))
180179oveq2d 7447 . . . . . 6 (𝑄 = 𝑊 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)))
181 oveq2 7439 . . . . . 6 (𝑄 = 𝑊 → (𝑃 ·s 𝑄) = (𝑃 ·s 𝑊))
182180, 181oveq12d 7449 . . . . 5 (𝑄 = 𝑊 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑃 ·s 𝑊)))
183182breq1d 5158 . . . 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 247 . . 3 (𝜑 → (𝑄 = 𝑊 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
18520adantr 480 . . . . 5 ((𝜑𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No )
18631, 17addscld 28028 . . . . . . 7 (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No )
1878, 30, 16mulsproplem4 28160 . . . . . . 7 (𝜑 → (𝑉 ·s 𝑄) ∈ No )
188186, 187subscld 28108 . . . . . 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 )
191123, 2, 125ssltsepcd 27854 . . . . . . . . 9 (𝜑𝑄 <s 𝐵)
19250uneq1i 4174 . . . . . . . . . . . . 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 4402 . . . . . . . . . . . . 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 2763 . . . . . . . . . . . 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, 137jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
196 naddel12 8737 . . . . . . . . . . . . . . . . 17 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → ((( bday 𝑉) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
19758, 59, 196mp2an 692 . . . . . . . . . . . . . . . 16 ((( bday 𝑉) ∈ ( bday 𝐴) ∧ ( bday 𝑄) ∈ ( bday 𝐵)) → (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
198133, 57, 197syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
199141, 198jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
20080, 147onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∈ On
201 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑉) ∈ On ∧ ( bday 𝑄) ∈ On) → (( bday 𝑉) +no ( bday 𝑄)) ∈ On)
202134, 73, 201mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑉) +no ( bday 𝑄)) ∈ On
203150, 202onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑄))) ∈ On
204 onunel 6491 . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . 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 6491 . . . . . . . . . . . . . . . . 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, 147, 90, 206mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
208 onunel 6491 . . . . . . . . . . . . . . . . 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 𝐵)))))
209150, 202, 90, 208mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝑃) +no ( bday 𝐵)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
210207, 209anbi12i 628 . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝑃) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝐵))) ∪ ((( bday 𝑃) +no ( bday 𝐵)) ∪ (( bday 𝑉) +no ( bday 𝑄)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
213 elun1 4192 . . . . . . . . . . . . 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 2843 . . . . . . . . . . 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, 44, 128, 3, 12, 215mulsproplem1 28157 . . . . . . . . . 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 𝑄))))
218121, 191, 217mp2and 699 . . . . . . . 8 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)))
21913, 19subscld 28108 . . . . . . . . 9 (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) ∈ No )
22031, 187subscld 28108 . . . . . . . . 9 (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) ∈ No )
221219, 220, 17sltadd1d 28046 . . . . . . . 8 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄))))
222218, 221mpbid 232 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
22313, 17, 19addsubsd 28127 . . . . . . 7 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
22431, 17, 187addsubsd 28127 . . . . . . 7 (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑄)) +s (𝐴 ·s 𝑄)))
225222, 223, 2243brtr4d 5180 . . . . . 6 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)))
226225adantr 480 . . . . 5 ((𝜑𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)))
227 ssltright 27925 . . . . . . . . . . 11 (𝐴 No → {𝐴} <<s ( R ‘𝐴))
22814, 227syl 17 . . . . . . . . . 10 (𝜑 → {𝐴} <<s ( R ‘𝐴))
229228, 39, 29ssltsepcd 27854 . . . . . . . . 9 (𝜑𝐴 <s 𝑉)
23050uneq1i 4174 . . . . . . . . . . . . 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 𝑊)))))
231 0un 4402 . . . . . . . . . . . . 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 𝑊))))
232230, 231eqtri 2763 . . . . . . . . . . . 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 𝑊))))
23368, 198jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
23476, 144jca 511 . . . . . . . . . . . . . 14 (𝜑 → ((( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
23582, 202onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝐴) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝑄))) ∈ On
23687, 152onun2i 6508 . . . . . . . . . . . . . . . 16 ((( bday 𝐴) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝑊))) ∈ On
237 onunel 6491 . . . . . . . . . . . . . . . 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 𝐵)))))
238235, 236, 90, 237mp3an 1460 . . . . . . . . . . . . . . 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 𝐵))))
239 onunel 6491 . . . . . . . . . . . . . . . . 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 𝐵)))))
24082, 202, 90, 239mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝐴) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝑄))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝐴) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
241 onunel 6491 . . . . . . . . . . . . . . . . 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 𝐵)))))
24287, 152, 90, 241mp3an 1460 . . . . . . . . . . . . . . . 16 (((( bday 𝐴) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝑊))) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ((( bday 𝐴) +no ( bday 𝑄)) ∈ (( bday 𝐴) +no ( bday 𝐵)) ∧ (( bday 𝑉) +no ( bday 𝑊)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
243240, 242anbi12i 628 . . . . . . . . . . . . . . 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 𝐵)))))
244238, 243bitri 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 𝐵)))))
245233, 234, 244sylanbrc 583 . . . . . . . . . . . . 13 (𝜑 → (((( bday 𝐴) +no ( bday 𝑊)) ∪ (( bday 𝑉) +no ( bday 𝑄))) ∪ ((( bday 𝐴) +no ( bday 𝑄)) ∪ (( bday 𝑉) +no ( bday 𝑊)))) ∈ (( bday 𝐴) +no ( bday 𝐵)))
246 elun1 4192 . . . . . . . . . . . . 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 𝐸))))))
247245, 246syl 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 𝐸))))))
248232, 247eqeltrid 2843 . . . . . . . . . . 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 𝐸))))))
2498, 42, 42, 14, 128, 5, 3, 248mulsproplem1 28157 . . . . . . . . . 10 (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝐴 <s 𝑉𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)))))
250249simprd 495 . . . . . . . . 9 (𝜑 → ((𝐴 <s 𝑉𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊))))
251229, 250mpand 695 . . . . . . . 8 (𝜑 → (𝑊 <s 𝑄 → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊))))
252251imp 406 . . . . . . 7 ((𝜑𝑊 <s 𝑄) → ((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)))
25317, 187, 23, 33sltsubsubbd 28128 . . . . . . . . 9 (𝜑 → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))
25417, 187subscld 28108 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) ∈ No )
25523, 33subscld 28108 . . . . . . . . . 10 (𝜑 → ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ∈ No )
256254, 255, 31sltadd2d 28045 . . . . . . . . 9 (𝜑 → (((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))))
257253, 256bitrd 279 . . . . . . . 8 (𝜑 → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))))
258257adantr 480 . . . . . . 7 ((𝜑𝑊 <s 𝑄) → (((𝐴 ·s 𝑄) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑄) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))))
259252, 258mpbid 232 . . . . . 6 ((𝜑𝑊 <s 𝑄) → ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))
26031, 17, 187addsubsassd 28126 . . . . . . 7 (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))))
261260adantr 480 . . . . . 6 ((𝜑𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑉 ·s 𝑄))))
26231, 23, 33addsubsassd 28126 . . . . . . 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 𝑊))))
264259, 261, 2633brtr4d 5180 . . . . 5 ((𝜑𝑊 <s 𝑄) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑉 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
265185, 189, 190, 226, 264slttrd 27819 . . . 4 ((𝜑𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
266265ex 412 . . 3 (𝜑 → (𝑊 <s 𝑄 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
267178, 184, 2663jaod 1428 . 2 (𝜑 → ((𝑄 <s 𝑊𝑄 = 𝑊𝑊 <s 𝑄) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
2687, 267mpd 15 1 (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3o 1085   = wceq 1537  wcel 2106  wral 3059  cun 3961  c0 4339  {csn 4631   class class class wbr 5148  Oncon0 6386  cfv 6563  (class class class)co 7431   +no cnadd 8702   No csur 27699   <s cslt 27700   bday cbday 27701   <<s csslt 27840   0s c0s 27882   O cold 27897   L cleft 27899   R cright 27900   +s cadds 28007   -s csubs 28067   ·s cmuls 28147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-1o 8505  df-2o 8506  df-nadd 8703  df-no 27702  df-slt 27703  df-bday 27704  df-sle 27805  df-sslt 27841  df-scut 27843  df-0s 27884  df-made 27901  df-old 27902  df-left 27904  df-right 27905  df-norec 27986  df-norec2 27997  df-adds 28008  df-negs 28068  df-subs 28069
This theorem is referenced by:  mulsproplem9  28165
  Copyright terms: Public domain W3C validator