mulsproplem8 - Metamath Proof Explorer

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

Theorem mulsproplem8 28389

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 𝑒))))))
mulsproplem8.1	⊢ (𝜑 → 𝐴 ∈ No )
mulsproplem8.2	⊢ (𝜑 → 𝐵 ∈ No )
mulsproplem8.3	⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
mulsproplem8.4	⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
mulsproplem8.5	⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
mulsproplem8.6	⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))

**Assertion**
Ref	Expression
mulsproplem8	⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑅,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑆,𝑏,𝑐,𝑑,𝑒,𝑓 𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑊,𝑏,𝑐,𝑑,𝑒,𝑓 Allowed substitution hints: 𝜑(𝑒, 𝑓, 𝑎, 𝑏, 𝑐, 𝑑) 𝑆(𝑎) 𝑊(𝑎)

**Proof of Theorem mulsproplem8**
Step	Hyp	Ref	Expression
1		mulsproplem8.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
2	1	rightnod 28148	. . 3 ⊢ (𝜑 → 𝑅 ∈ No )
3		mulsproplem8.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
4	3	rightnod 28148	. . 3 ⊢ (𝜑 → 𝑉 ∈ No )
5		ltslin 27986	. . 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	1	rightoldd 28147	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
9		mulsproplem8.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
10	7, 8, 9	mulsproplem2 28383	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
11		mulsproplem8.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
12		mulsproplem8.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
13	12	rightoldd 28147	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
14	7, 11, 13	mulsproplem3 28384	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
15	10, 14	addscld 28246	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
16	7, 8, 13	mulsproplem4 28385	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
17	15, 16	subscld 28329	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
19		mulsproplem8.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))
20	19	leftoldd 28145	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ( O ‘( bday ‘𝐵)))
21	7, 11, 20	mulsproplem3 28384	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑊) ∈ No )
22	10, 21	addscld 28246	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
23	7, 8, 20	mulsproplem4 28385	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑊) ∈ No )
24	22, 23	subscld 28329	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
26	3	rightoldd 28147	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ( O ‘( bday ‘𝐴)))
27	7, 26, 9	mulsproplem2 28383	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝐵) ∈ No )
28	27, 21	addscld 28246	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
29	7, 26, 20	mulsproplem4 28385	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑊) ∈ No )
30	28, 29	subscld 28329	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
32		sltsright 28127	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
33	11, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
34		snidg 4621	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
35	11, 34	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
36	33, 35, 1	sltssepcd 28038	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
37		lltr 28128	. . . . . . . . . . 11 ⊢ ( L ‘𝐵) <<s ( R ‘𝐵)
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵))
39	38, 19, 12	sltssepcd 28038	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝑆)
40		0no 28075	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
42	19	leftnod 28146	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ No )
43	12	rightnod 28148	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ No )
44		bday0 28077	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
45	44, 44	oveq12i 7426	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
46		0elon 6413	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8673	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
50	49	uneq1i 4111	. . . . . . . . . . . . 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 ‘𝑊)))))
51		0un 4346	. . . . . . . . . . . . 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 ‘𝑊))))
52	50, 51	eqtri 2783	. . . . . . . . . . . 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 ‘𝑊))))
53		oldbdayim 28155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
54	20, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
55		bdayon 28018	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑊) ∈ On
56		bdayon 28018	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
57		bdayon 28018	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
58		naddel2 8678	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑊) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
59	55, 56, 57, 58	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
60	54, 59	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
61		oldbdayim 28155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
62	8, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
63		oldbdayim 28155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
64	13, 63	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
65		naddel12 8690	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
66	57, 56, 65	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67	62, 64, 66	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
68	60, 67	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
69		bdayon 28018	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑆) ∈ On
70		naddel2 8678	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
71	69, 56, 57, 70	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
72	64, 71	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
73		naddel12 8690	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
74	57, 56, 73	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
75	62, 54, 74	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
76	72, 75	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
77		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On)
78	57, 55, 77	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On
79		bdayon 28018	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑅) ∈ On
80		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
81	79, 69, 80	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
82	78, 81	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
83		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
84	57, 69, 83	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
85		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On)
86	79, 55, 85	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On
87	84, 86	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ On
88		naddcl 8666	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
89	57, 56, 88	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
90		onunel 6465	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
91	82, 87, 89, 90	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 ‘𝐵))))
92		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
93	78, 81, 89, 92	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
94		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
95	84, 86, 89, 94	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
96	93, 95	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 ‘𝐵)))))
97	91, 96	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 ‘𝐵)))))
98	68, 76, 97	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
99		elun1 4128	. . . . . . . . . . . . 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 ‘𝐸))))))
100	98, 99	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 ‘𝐸))))))
101	52, 100	eqeltrid 2864	. . . . . . . . . . 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 ‘𝐸))))))
102	7, 41, 41, 11, 2, 42, 43, 101	mulsproplem1 28382	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)))))
103	102	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊))))
104	36, 39, 103	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)))
105	14, 16, 21, 23	ltsubsubsbd 28349	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
106	14, 16	subscld 28329	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
107	21, 23	subscld 28329	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)) ∈ No )
108	106, 107, 10	ltadds2d 28263	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)))))
109	105, 108	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)))))
110	104, 109	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
111	10, 14, 16	addsubsassd 28347	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
112	10, 21, 23	addsubsassd 28347	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
113	110, 111, 112	3brtr4d 5137	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)))
114	113	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)))
115		sltsleft 28126	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → ( L ‘𝐵) <<s {𝐵})
116	9, 115	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵})
117		snidg 4621	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
118	9, 117	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
119	116, 19, 118	sltssepcd 28038	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝐵)
120	49	uneq1i 4111	. . . . . . . . . . . . 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 ‘𝑊)))))
121		0un 4346	. . . . . . . . . . . . 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 ‘𝑊))))
122	120, 121	eqtri 2783	. . . . . . . . . . . 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 ‘𝑊))))
123		oldbdayim 28155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
124	26, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
125		bdayon 28018	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑉) ∈ On
126		naddel1 8677	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
127	125, 57, 56, 126	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
128	124, 127	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
129	75, 128	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
130		naddel1 8677	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
131	79, 57, 56, 130	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
132	62, 131	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
133		naddel12 8690	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
134	57, 56, 133	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	124, 54, 134	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
136	132, 135	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On)
138	125, 56, 137	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On
139	86, 138	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
140		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
141	79, 56, 140	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
142		naddcl 8666	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On)
143	125, 55, 142	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On
144	141, 143	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
145		onunel 6465	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
146	139, 144, 89, 145	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 ‘𝐵))))
147		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
148	86, 138, 89, 147	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
149		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
150	141, 143, 89, 149	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
151	148, 150	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 ‘𝐵)))))
152	146, 151	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 ‘𝐵)))))
153	129, 136, 152	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
154		elun1 4128	. . . . . . . . . . . . 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 ‘𝐸))))))
155	153, 154	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 ‘𝐸))))))
156	122, 155	eqeltrid 2864	. . . . . . . . . . 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 ‘𝐸))))))
157	7, 41, 41, 2, 4, 42, 9, 156	mulsproplem1 28382	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))))
158	157	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊))))
159	119, 158	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑅 <s 𝑉 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊))))
160	159	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))
161	10, 23	subscld 28329	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) ∈ No )
162	27, 29	subscld 28329	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ∈ No )
163	161, 162, 21	ltadds1d 28264	. . . . . . . 8 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
164	163	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
165	160, 164	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
166	10, 21, 23	addsubsd 28348	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
167	166	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
168	27, 21, 29	addsubsd 28348	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
169	168	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
170	165, 167, 169	3brtr4d 5137	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
171	18, 25, 31, 114, 170	ltstrd 28000	. . . 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	33, 35, 3	sltssepcd 28038	. . . . . . 7 ⊢ (𝜑 → 𝐴 <s 𝑉)
174	49	uneq1i 4111	. . . . . . . . . . 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 ‘𝑊)))))
175		0un 4346	. . . . . . . . . . 11 ⊢ (∅ ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))
176	174, 175	eqtri 2783	. . . . . . . . . 10 ⊢ ((( 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 ‘𝑊))))
177		naddel12 8690	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
178	57, 56, 177	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
179	124, 64, 178	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
180	60, 179	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
181	72, 135	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
182		naddcl 8666	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On)
183	125, 69, 182	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On
184	78, 183	onun2i 6481	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ On
185	84, 143	onun2i 6481	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
186		onunel 6465	. . . . . . . . . . . . . 14 ⊢ ((((( 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 ‘𝐵)))))
187	184, 185, 89, 186	mp3an 1490	. . . . . . . . . . . . 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 ‘𝐵))))
188		onunel 6465	. . . . . . . . . . . . . . 15 ⊢ (((( 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 ‘𝐵)))))
189	78, 183, 89, 188	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
190		onunel 6465	. . . . . . . . . . . . . . 15 ⊢ (((( 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 ‘𝐵)))))
191	84, 143, 89, 190	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
192	189, 191	anbi12i 640	. . . . . . . . . . . . 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 ‘𝐵)))))
193	187, 192	bitri 278	. . . . . . . . . . . 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 ‘𝐵))) ∧ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
194	180, 181, 193	sylanbrc 595	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
195		elun1 4128	. . . . . . . . . . 11 ⊢ ((((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
196	194, 195	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
197	176, 196	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → ((( 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 ‘𝐸))))))
198	7, 41, 41, 11, 4, 42, 43, 197	mulsproplem1 28382	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)))))
199	198	simprd 501	. . . . . . 7 ⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊))))
200	173, 39, 199	mp2and 712	. . . . . 6 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)))
201	7, 26, 13	mulsproplem4 28385	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝑆) ∈ No )
202	14, 201, 21, 29	ltsubsubsbd 28349	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
203	14, 201	subscld 28329	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) ∈ No )
204	21, 29	subscld 28329	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ∈ No )
205	203, 204, 27	ltadds2d 28263	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
206	202, 205	bitrd 282	. . . . . 6 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
207	200, 206	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
208	27, 14, 201	addsubsassd 28347	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))))
209	27, 21, 29	addsubsassd 28347	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
210	207, 208, 209	3brtr4d 5137	. . . 4 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
211		oveq1 7421	. . . . . . 7 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝐵) = (𝑉 ·_s 𝐵))
212	211	oveq1d 7429	. . . . . 6 ⊢ (𝑅 = 𝑉 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)))
213		oveq1 7421	. . . . . 6 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝑆) = (𝑉 ·_s 𝑆))
214	212, 213	oveq12d 7432	. . . . 5 ⊢ (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)))
215	214	breq1d 5113	. . . 4 ⊢ (𝑅 = 𝑉 → ((((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
216	210, 215	syl5ibrcom 250	. . 3 ⊢ (𝜑 → (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
217	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
218	27, 14	addscld 28246	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
219	218, 201	subscld 28329	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) ∈ No )
220	219	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) ∈ No )
221	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
222		sltsright 28127	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
223	9, 222	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
224	223, 118, 12	sltssepcd 28038	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
225	49	uneq1i 4111	. . . . . . . . . . . . 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 ‘𝐵)))))
226		0un 4346	. . . . . . . . . . . . 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 ‘𝐵))))
227	225, 226	eqtri 2783	. . . . . . . . . . . 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 ‘𝐵))))
228	128, 67	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
229	179, 132	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
230	138, 81	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
231	183, 141	onun2i 6481	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
232		onunel 6465	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
233	230, 231, 89, 232	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 ‘𝐵))))
234		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
235	138, 81, 89, 234	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
236		onunel 6465	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
237	183, 141, 89, 236	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
238	235, 237	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 ‘𝐵)))))
239	233, 238	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 ‘𝐵)))))
240	228, 229, 239	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
241		elun1 4128	. . . . . . . . . . . . 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 ‘𝐸))))))
242	240, 241	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 ‘𝐸))))))
243	227, 242	eqeltrid 2864	. . . . . . . . . . 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 ‘𝐸))))))
244	7, 41, 41, 4, 2, 9, 43, 243	mulsproplem1 28382	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))))
245	244	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
246	224, 245	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑉 <s 𝑅 → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
247	246	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
248	201, 27, 16, 10	ltsubsubs2bd 28350	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆))))
249	10, 16	subscld 28329	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
250	27, 201	subscld 28329	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) ∈ No )
251	249, 250, 14	ltadds1d 28264	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
252	248, 251	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
253	252	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
254	247, 253	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
255	10, 14, 16	addsubsd 28348	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
256	255	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
257	27, 14, 201	addsubsd 28348	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
258	257	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
259	254, 256, 258	3brtr4d 5137	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)))
260	210	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
261	217, 220, 221, 259, 260	ltstrd 28000	. . . 4 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
262	261	ex 418	. . 3 ⊢ (𝜑 → (𝑉 <s 𝑅 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
263	172, 216, 262	3jaod 1456	. 2 ⊢ (𝜑 → ((𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
264	6, 263	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 2145 ∀wral 3076 ∪ cun 3897 ∅c0 4279 {csn 4584 class class class wbr 5103 Oncon0 6357 ‘cfv 6533 (class class class)co 7414 +no cnadd 8654 No csur 27877 <s clts 27878 bday cbday 27879 <<s cslts 28023 0_s c0s 28071 O cold 28089 L cleft 28091 R cright 28092 +_s cadds 28225 -_s csubs 28286 ·_s cmuls 28372

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-ot 4593 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-1o 8456 df-2o 8457 df-nadd 8655 df-no 27880 df-lts 27881 df-bday 27882 df-les 27982 df-slts 28024 df-cuts 28026 df-0s 28073 df-made 28093 df-old 28094 df-left 28096 df-right 28097 df-norec 28204 df-norec2 28215 df-adds 28226 df-negs 28287 df-subs 28288

This theorem is used by: mulsproplem9 28390

W3C validator