mulsproplem6 - Metamath Proof Explorer

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

Theorem mulsproplem6 28365

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**
Step	Hyp	Ref	Expression
1		mulsproplem6.4	. . . 4 ⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵))
2	1	leftnod 28124	. . 3 ⊢ (𝜑 → 𝑄 ∈ No )
3		mulsproplem6.6	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))
4	3	leftnod 28124	. . 3 ⊢ (𝜑 → 𝑊 ∈ No )
5		ltslin 27964	. . 3 ⊢ ((𝑄 ∈ No ∧ 𝑊 ∈ No ) → (𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄))
6	2, 4, 5	syl2anc 596	. 2 ⊢ (𝜑 → (𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄))
7		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 𝑒))))))
8		mulsproplem6.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴))
9	8	leftoldd 28123	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ( O ‘( bday ‘𝐴)))
10		mulsproplem6.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
11	7, 9, 10	mulsproplem2 28361	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ·_s 𝐵) ∈ No )
12		mulsproplem6.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
13	1	leftoldd 28123	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ( O ‘( bday ‘𝐵)))
14	7, 12, 13	mulsproplem3 28362	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑄) ∈ No )
15	11, 14	addscld 28224	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) ∈ No )
16	7, 9, 13	mulsproplem4 28363	. . . . . . 7 ⊢ (𝜑 → (𝑃 ·_s 𝑄) ∈ No )
17	15, 16	subscld 28307	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) ∈ No )
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) ∈ No )
19	3	leftoldd 28123	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ( O ‘( bday ‘𝐵)))
20	7, 12, 19	mulsproplem3 28362	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑊) ∈ No )
21	11, 20	addscld 28224	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
22	7, 9, 19	mulsproplem4 28363	. . . . . . 7 ⊢ (𝜑 → (𝑃 ·_s 𝑊) ∈ No )
23	21, 22	subscld 28307	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) ∈ No )
24	23	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) ∈ No )
25		mulsproplem6.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
26	25	rightoldd 28125	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ( O ‘( bday ‘𝐴)))
27	7, 26, 10	mulsproplem2 28361	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝐵) ∈ No )
28	27, 20	addscld 28224	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
29	7, 26, 19	mulsproplem4 28363	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑊) ∈ No )
30	28, 29	subscld 28307	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
32		sltsleft 28104	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
33	12, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴})
34		snidg 4628	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
35	12, 34	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
36	33, 8, 35	sltssepcd 28016	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 <s 𝐴)
37		0no 28053	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
38	37	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
39	8	leftnod 28124	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ No )
40		bday0 28055	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
41	40, 40	oveq12i 7431	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
42		0elon 6420	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
43		naddrid 8676	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
45	41, 44	eqtri 2788	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
46	45	uneq1i 4118	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))))) = (∅ ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄)))))
47		0un 4353	. . . . . . . . . . . . 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 ‘𝑄))))
48	46, 47	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))))) = (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))))
49		oldbdayim 28133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑃) ∈ ( bday ‘𝐴))
50	9, 49	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑃) ∈ ( bday ‘𝐴))
51		oldbdayim 28133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑄) ∈ ( bday ‘𝐵))
52	13, 51	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑄) ∈ ( bday ‘𝐵))
53		bdayon 27996	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
54		bdayon 27996	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
55		naddel12 8693	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑃) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑄) ∈ ( bday ‘𝐵)) → (( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
56	53, 54, 55	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑄) ∈ ( bday ‘𝐵)) → (( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
57	50, 52, 56	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
58		oldbdayim 28133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
59	19, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
60		bdayon 27996	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑊) ∈ On
61		naddel2 8681	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑊) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
62	60, 54, 53, 61	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
63	59, 62	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
64	57, 63	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
65		naddel12 8693	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑃) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
66	53, 54, 65	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67	50, 59, 66	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
68		bdayon 27996	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑄) ∈ On
69		naddel2 8681	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑄) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑄) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
70	68, 54, 53, 69	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑄) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
71	52, 70	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
72	67, 71	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
73		bdayon 27996	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑃) ∈ On
74		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑃) ∈ On ∧ ( bday ‘𝑄) ∈ On) → (( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ On)
75	73, 68, 74	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ On
76		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On)
77	53, 60, 76	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On
78	75, 77	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∈ On
79		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑃) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ On)
80	73, 60, 79	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ On
81		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑄) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ On)
82	53, 68, 81	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ On
83	80, 82	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))) ∈ On
84		naddcl 8669	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
85	53, 54, 84	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
86		onunel 6472	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
87	78, 83, 85, 86	mp3an 1490	. . . . . . . . . . . . . . 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 ‘𝐵))))
88		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
89	75, 77, 85, 88	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
90		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
91	80, 82, 85, 90	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
92	89, 91	anbi12i 640	. . . . . . . . . . . . . . 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 ‘𝐵)))))
93	87, 92	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
94	64, 72, 93	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
95		elun1 4135	. . . . . . . . . . . . 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 ‘𝐸))))))
96	94, 95	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
97	48, 96	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑊))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑄))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
98	7, 38, 38, 39, 12, 2, 4, 97	mulsproplem1 28360	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊) → ((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄)))))
99	98	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑊) → ((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄))))
100	36, 99	mpand 708	. . . . . . . 8 ⊢ (𝜑 → (𝑄 <s 𝑊 → ((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄))))
101	100	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → ((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄)))
102	22, 20, 16, 14	ltsubsubs3bd 28329	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄)) ↔ ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊))))
103	14, 16	subscld 28307	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄)) ∈ No )
104	20, 22	subscld 28307	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊)) ∈ No )
105	103, 104, 11	ltadds2d 28241	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊)) ↔ ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊)))))
106	102, 105	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄)) ↔ ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊)))))
107	106	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝑊) -_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝐴 ·_s 𝑄)) ↔ ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊)))))
108	101, 107	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊))))
109	11, 14, 16	addsubsassd 28325	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))))
110	109	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑃 ·_s 𝑄))))
111	11, 20, 22	addsubsassd 28325	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊))))
112	111	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑃 ·_s 𝑊))))
113	108, 110, 112	3brtr4d 5145	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)))
114		lltr 28106	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
115	114	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
116	115, 8, 25	sltssepcd 28016	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 <s 𝑉)
117		sltsleft 28104	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → ( L ‘𝐵) <<s {𝐵})
118	10, 117	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵})
119		snidg 4628	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
120	10, 119	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
121	118, 3, 120	sltssepcd 28016	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝐵)
122	25	rightnod 28126	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ No )
123	45	uneq1i 4118	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (∅ ∪ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))))
124		0un 4353	. . . . . . . . . . . . 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 ‘𝑊))))
125	123, 124	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))
126		oldbdayim 28133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
127	26, 126	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
128		bdayon 27996	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑉) ∈ On
129		naddel1 8680	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
130	128, 53, 54, 129	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
131	127, 130	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
132	67, 131	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
133		naddel1 8680	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑃) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑃) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
134	73, 53, 54, 133	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑃) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	50, 134	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
136		naddel12 8693	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137	53, 54, 136	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
138	127, 59, 137	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
139	135, 138	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
140		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On)
141	128, 54, 140	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On
142	80, 141	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
143		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑃) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ On)
144	73, 54, 143	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ On
145		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On)
146	128, 60, 145	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On
147	144, 146	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
148		onunel 6472	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
149	142, 147, 85, 148	mp3an 1490	. . . . . . . . . . . . . . 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 ‘𝐵))))
150		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
151	80, 141, 85, 150	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
152		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
153	144, 146, 85, 152	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
154	151, 153	anbi12i 640	. . . . . . . . . . . . . . 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 ‘𝐵)))))
155	149, 154	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
156	132, 139, 155	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
157		elun1 4135	. . . . . . . . . . . . 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 ‘𝐸))))))
158	156, 157	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
159	125, 158	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
160	7, 38, 38, 39, 122, 4, 10, 159	mulsproplem1 28360	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))))
161	160	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊))))
162	116, 121, 161	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))
163	11, 22	subscld 28307	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) ∈ No )
164	27, 29	subscld 28307	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ∈ No )
165	163, 164, 20	ltadds1d 28242	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
166	162, 165	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
167	11, 20, 22	addsubsd 28326	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) = (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
168	27, 20, 29	addsubsd 28326	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
169	166, 167, 168	3brtr4d 5145	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
170	169	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
171	18, 24, 31, 113, 170	ltstrd 27978	. . . 4 ⊢ ((𝜑 ∧ 𝑄 <s 𝑊) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
172	171	ex 418	. . 3 ⊢ (𝜑 → (𝑄 <s 𝑊 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
173		oveq2 7427	. . . . . . 7 ⊢ (𝑄 = 𝑊 → (𝐴 ·_s 𝑄) = (𝐴 ·_s 𝑊))
174	173	oveq2d 7435	. . . . . 6 ⊢ (𝑄 = 𝑊 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) = ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)))
175		oveq2 7427	. . . . . 6 ⊢ (𝑄 = 𝑊 → (𝑃 ·_s 𝑄) = (𝑃 ·_s 𝑊))
176	174, 175	oveq12d 7437	. . . . 5 ⊢ (𝑄 = 𝑊 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) = (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)))
177	176	breq1d 5121	. . . 4 ⊢ (𝑄 = 𝑊 → ((((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑃 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
178	169, 177	syl5ibrcom 250	. . 3 ⊢ (𝜑 → (𝑄 = 𝑊 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
179	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) ∈ No )
180	27, 14	addscld 28224	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) ∈ No )
181	7, 26, 13	mulsproplem4 28363	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑄) ∈ No )
182	180, 181	subscld 28307	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) ∈ No )
183	182	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) ∈ No )
184	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
185	118, 1, 120	sltssepcd 28016	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 <s 𝐵)
186	45	uneq1i 4118	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))))) = (∅ ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄)))))
187		0un 4353	. . . . . . . . . . . . 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 ‘𝑄))))
188	186, 187	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))))) = (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))))
189	57, 131	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
190		naddel12 8693	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑄) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
191	53, 54, 190	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑄) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
192	127, 52, 191	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
193	135, 192	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
194	75, 141	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
195		naddcl 8669	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑄) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ On)
196	128, 68, 195	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ On
197	144, 196	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∈ On
198		onunel 6472	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
199	194, 197, 85, 198	mp3an 1490	. . . . . . . . . . . . . . 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 ‘𝐵))))
200		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
201	75, 141, 85, 200	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
202		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
203	144, 196, 85, 202	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
204	201, 203	anbi12i 640	. . . . . . . . . . . . . . 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 ‘𝐵)))))
205	199, 204	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
206	189, 193, 205	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
207		elun1 4135	. . . . . . . . . . . . 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 ‘𝐸))))))
208	206, 207	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
209	188, 208	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
210	7, 38, 38, 39, 122, 2, 10, 209	mulsproplem1 28360	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵) → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)))))
211	210	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 <s 𝑉 ∧ 𝑄 <s 𝐵) → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄))))
212	116, 185, 211	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)))
213	11, 16	subscld 28307	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) ∈ No )
214	27, 181	subscld 28307	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)) ∈ No )
215	213, 214, 14	ltadds1d 28242	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)) ↔ (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄))))
216	212, 215	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
217	11, 14, 16	addsubsd 28326	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) = (((𝑃 ·_s 𝐵) -_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
218	27, 14, 181	addsubsd 28326	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
219	216, 217, 218	3brtr4d 5145	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)))
220	219	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)))
221		sltsright 28105	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
222	12, 221	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
223	222, 35, 25	sltssepcd 28016	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑉)
224	45	uneq1i 4118	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (∅ ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))))
225		0un 4353	. . . . . . . . . . . . 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 ‘𝑊))))
226	224, 225	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))
227	63, 192	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
228	71, 138	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
229	77, 196	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∈ On
230	82, 146	onun2i 6488	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
231		onunel 6472	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
232	229, 230, 85, 231	mp3an 1490	. . . . . . . . . . . . . . 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 ‘𝐵))))
233		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
234	77, 196, 85, 233	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
235		onunel 6472	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
236	82, 146, 85, 235	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
237	234, 236	anbi12i 640	. . . . . . . . . . . . . . 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 ‘𝐵)))))
238	232, 237	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
239	227, 228, 238	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑄))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑄)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
240		elun1 4135	. . . . . . . . . . . . 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 ‘𝐸))))))
241	239, 240	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
242	226, 241	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0_s ) +no ( bday ‘ 0_s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( 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	7, 38, 38, 12, 122, 4, 2, 242	mulsproplem1 28360	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄) → ((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊)))))
244	243	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑄) → ((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊))))
245	223, 244	mpand 708	. . . . . . . 8 ⊢ (𝜑 → (𝑊 <s 𝑄 → ((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊))))
246	245	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → ((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊)))
247	14, 181, 20, 29	ltsubsubsbd 28327	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
248	14, 181	subscld 28307	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄)) ∈ No )
249	20, 29	subscld 28307	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ∈ No )
250	248, 249, 27	ltadds2d 28241	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
251	247, 250	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
252	251	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝐴 ·_s 𝑄) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑄) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
253	246, 252	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
254	27, 14, 181	addsubsassd 28325	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))))
255	254	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) -_s (𝑉 ·_s 𝑄))))
256	27, 20, 29	addsubsassd 28325	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
257	256	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
258	253, 255, 257	3brtr4d 5145	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑉 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
259	179, 183, 184, 220, 258	ltstrd 27978	. . . 4 ⊢ ((𝜑 ∧ 𝑊 <s 𝑄) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
260	259	ex 418	. . 3 ⊢ (𝜑 → (𝑊 <s 𝑄 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
261	172, 178, 260	3jaod 1456	. 2 ⊢ (𝜑 → ((𝑄 <s 𝑊 ∨ 𝑄 = 𝑊 ∨ 𝑊 <s 𝑄) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
262	6, 261	mpd 16	1 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) -_s (𝑃 ·_s 𝑄)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 = wceq 1570 ∈ wcel 2146 ∀wral 3081 ∪ cun 3904 ∅c0 4286 {csn 4591 class class class wbr 5111 Oncon0 6364 ‘cfv 6540 (class class class)co 7419 +no cnadd 8657 No csur 27855 <s clts 27856 bday cbday 27857 <<s cslts 28001 0_s c0s 28049 O cold 28067 L cleft 28069 R cright 28070 +_s cadds 28203 -_s csubs 28264 ·_s cmuls 28350

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-ot 4600 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-1o 8459 df-2o 8460 df-nadd 8658 df-no 27858 df-lts 27859 df-bday 27860 df-les 27960 df-slts 28002 df-cuts 28004 df-0s 28051 df-made 28071 df-old 28072 df-left 28074 df-right 28075 df-norec 28182 df-norec2 28193 df-adds 28204 df-negs 28265 df-subs 28266

This theorem is used by: mulsproplem9 28368

W3C validator