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 28509

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 28268	. . 3 ⊢ (𝜑 → 𝑅 ∈ No )
3		mulsproplem8.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
4	3	rightnod 28268	. . 3 ⊢ (𝜑 → 𝑉 ∈ No )
5		ltslin 28106	. . 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 28267	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
9		mulsproplem8.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
10	7, 8, 9	mulsproplem2 28503	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
11		mulsproplem8.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
12		mulsproplem8.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
13	12	rightoldd 28267	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
14	7, 11, 13	mulsproplem3 28504	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
15	10, 14	addscld 28366	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
16	7, 8, 13	mulsproplem4 28505	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
17	15, 16	subscld 28449	. . . . . 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 28265	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ( O ‘( bday ‘𝐵)))
21	7, 11, 20	mulsproplem3 28504	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑊) ∈ No )
22	10, 21	addscld 28366	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
23	7, 8, 20	mulsproplem4 28505	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑊) ∈ No )
24	22, 23	subscld 28449	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
26	3	rightoldd 28267	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ( O ‘( bday ‘𝐴)))
27	7, 26, 9	mulsproplem2 28503	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝐵) ∈ No )
28	27, 21	addscld 28366	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
29	7, 26, 20	mulsproplem4 28505	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑊) ∈ No )
30	28, 29	subscld 28449	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
32		sltsright 28247	. . . . . . . . . . 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 28158	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
37		lltr 28248	. . . . . . . . . . 11 ⊢ ( L ‘𝐵) <<s ( R ‘𝐵)
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵))
39	38, 19, 12	sltssepcd 28158	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝑆)
40		0no 28195	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
42	19	leftnod 28266	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ No )
43	12	rightnod 28268	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ No )
44		bday0 28197	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
45	44, 44	oveq12i 7432	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
46		0elon 6418	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8693	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2784	. . . . . . . . . . . . . 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 2784	. . . . . . . . . . . 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 28275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
54	20, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
55		bdayon 28138	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑊) ∈ On
56		bdayon 28138	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
57		bdayon 28138	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
58		naddel2 8698	. . . . . . . . . . . . . . . . 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 28275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
62	8, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
63		oldbdayim 28275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
64	13, 63	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
65		naddel12 8710	. . . . . . . . . . . . . . . . 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 28138	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑆) ∈ On
70		naddel2 8698	. . . . . . . . . . . . . . . . 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 8710	. . . . . . . . . . . . . . . . 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 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On)
78	57, 55, 77	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On
79		bdayon 28138	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑅) ∈ On
80		naddcl 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
81	79, 69, 80	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
82	78, 81	onun2i 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
83		naddcl 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
84	57, 69, 83	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
85		naddcl 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On)
86	79, 55, 85	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On
87	84, 86	onun2i 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ On
88		naddcl 8686	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
89	57, 56, 88	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
90		onunel 6470	. . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . 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 28502	. . . . . . . . . 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 28469	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
106	14, 16	subscld 28449	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
107	21, 23	subscld 28449	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)) ∈ No )
108	106, 107, 10	ltadds2d 28383	. . . . . . . . 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 28467	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
112	10, 21, 23	addsubsassd 28467	. . . . . . 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 28246	. . . . . . . . . . 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 28158	. . . . . . . . 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 2784	. . . . . . . . . . . 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 28275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
124	26, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
125		bdayon 28138	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑉) ∈ On
126		naddel1 8697	. . . . . . . . . . . . . . . . 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 8697	. . . . . . . . . . . . . . . . 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 8710	. . . . . . . . . . . . . . . . 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 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On)
138	125, 56, 137	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On
139	86, 138	onun2i 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
140		naddcl 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
141	79, 56, 140	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
142		naddcl 8686	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On)
143	125, 55, 142	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On
144	141, 143	onun2i 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
145		onunel 6470	. . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . 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 28502	. . . . . . . . . 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 28449	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) ∈ No )
162	27, 29	subscld 28449	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ∈ No )
163	161, 162, 21	ltadds1d 28384	. . . . . . . 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 28468	. . . . . . 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 28468	. . . . . . 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 28120	. . . 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 28158	. . . . . . 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 2784	. . . . . . . . . 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 8710	. . . . . . . . . . . . . . 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 8686	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On)
183	125, 69, 182	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On
184	78, 183	onun2i 6486	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ On
185	84, 143	onun2i 6486	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
186		onunel 6470	. . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . 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 2865	. . . . . . . . 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 28502	. . . . . . . 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 28505	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝑆) ∈ No )
202	14, 201, 21, 29	ltsubsubsbd 28469	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
203	14, 201	subscld 28449	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) ∈ No )
204	21, 29	subscld 28449	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ∈ No )
205	203, 204, 27	ltadds2d 28383	. . . . . . 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 28467	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))))
209	27, 21, 29	addsubsassd 28467	. . . . 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 7427	. . . . . . 7 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝐵) = (𝑉 ·_s 𝐵))
212	211	oveq1d 7435	. . . . . 6 ⊢ (𝑅 = 𝑉 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)))
213		oveq1 7427	. . . . . 6 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝑆) = (𝑉 ·_s 𝑆))
214	212, 213	oveq12d 7438	. . . . 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 28366	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
219	218, 201	subscld 28449	. . . . . 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 28247	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
223	9, 222	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
224	223, 118, 12	sltssepcd 28158	. . . . . . . . 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 2784	. . . . . . . . . . . 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 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
231	183, 141	onun2i 6486	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
232		onunel 6470	. . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 6470	. . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . 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 28502	. . . . . . . . . 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 28470	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆))))
249	10, 16	subscld 28449	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
250	27, 201	subscld 28449	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) ∈ No )
251	249, 250, 14	ltadds1d 28384	. . . . . . . . 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 28468	. . . . . . 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 28468	. . . . . . 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 28120	. . . 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 3077 ∪ cun 3897 ∅c0 4279 {csn 4584 class class class wbr 5103 Oncon0 6362 ‘cfv 6538 (class class class)co 7420 +no cnadd 8674 No csur 27997 <s clts 27998 bday cbday 27999 <<s cslts 28143 0_s c0s 28191 O cold 28209 L cleft 28211 R cright 28212 +_s cadds 28345 -_s csubs 28406 ·_s cmuls 28492

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 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 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 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-1o 8476 df-2o 8477 df-nadd 8675 df-no 28000 df-lts 28001 df-bday 28002 df-les 28102 df-slts 28144 df-cuts 28146 df-0s 28193 df-made 28213 df-old 28214 df-left 28216 df-right 28217 df-norec 28324 df-norec2 28335 df-adds 28346 df-negs 28407 df-subs 28408

This theorem is used by: mulsproplem9 28510

W3C validator