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 28092

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		rightssno 27854	. . . 4 ⊢ ( R ‘𝐴) ⊆ No
2		mulsproplem8.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
3	1, 2	sselid 3929	. . 3 ⊢ (𝜑 → 𝑅 ∈ No )
4		mulsproplem8.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
5	1, 4	sselid 3929	. . 3 ⊢ (𝜑 → 𝑉 ∈ No )
6		sltlin 27715	. . 3 ⊢ ((𝑅 ∈ No ∧ 𝑉 ∈ No ) → (𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅))
7	3, 5, 6	syl2anc 584	. 2 ⊢ (𝜑 → (𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅))
8		mulsproplem.1	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·_s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·_s 𝑓) -_s (𝑐 ·_s 𝑒)) <s ((𝑑 ·_s 𝑓) -_s (𝑑 ·_s 𝑒))))))
9		rightssold 27852	. . . . . . . . . 10 ⊢ ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
10	9, 2	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
11		mulsproplem8.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
12	8, 10, 11	mulsproplem2 28086	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
13		mulsproplem8.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
14		rightssold 27852	. . . . . . . . . 10 ⊢ ( R ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
15		mulsproplem8.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
16	14, 15	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
17	8, 13, 16	mulsproplem3 28087	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
18	12, 17	addscld 27950	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
19	8, 10, 16	mulsproplem4 28088	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
20	18, 19	subscld 28032	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
21	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
22		leftssold 27851	. . . . . . . . . 10 ⊢ ( L ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
23		mulsproplem8.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))
24	22, 23	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ( O ‘( bday ‘𝐵)))
25	8, 13, 24	mulsproplem3 28087	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑊) ∈ No )
26	12, 25	addscld 27950	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
27	8, 10, 24	mulsproplem4 28088	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑊) ∈ No )
28	26, 27	subscld 28032	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
29	28	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) ∈ No )
30	9, 4	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ( O ‘( bday ‘𝐴)))
31	8, 30, 11	mulsproplem2 28086	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝐵) ∈ No )
32	31, 25	addscld 27950	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No )
33	8, 30, 24	mulsproplem4 28088	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑊) ∈ No )
34	32, 33	subscld 28032	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
35	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
36		ssltright 27843	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
37	13, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
38		snidg 4615	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
39	13, 38	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
40	37, 39, 2	ssltsepcd 27762	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
41		lltropt 27844	. . . . . . . . . . 11 ⊢ ( L ‘𝐵) <<s ( R ‘𝐵)
42	41	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵))
43	42, 23, 15	ssltsepcd 27762	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝑆)
44		0sno 27797	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
45	44	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
46		leftssno 27853	. . . . . . . . . . . 12 ⊢ ( L ‘𝐵) ⊆ No
47	46, 23	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ No )
48		rightssno 27854	. . . . . . . . . . . 12 ⊢ ( R ‘𝐵) ⊆ No
49	48, 15	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ No )
50		bday0s 27799	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
51	50, 50	oveq12i 7368	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
52		0elon 6370	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
53		naddrid 8609	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
55	51, 54	eqtri 2757	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
56	55	uneq1i 4114	. . . . . . . . . . . . 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 ‘𝑊)))))
57		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 ‘𝑊))))
58	56, 57	eqtri 2757	. . . . . . . . . . . 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 ‘𝑊))))
59		oldbdayim 27861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
60	24, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
61		bdayelon 27742	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑊) ∈ On
62		bdayelon 27742	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
63		bdayelon 27742	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
64		naddel2 8614	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑊) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
65	61, 62, 63, 64	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
66	60, 65	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67		oldbdayim 27861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
68	10, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
69		oldbdayim 27861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
70	16, 69	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
71		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
72	63, 62, 71	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
73	68, 70, 72	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
74	66, 73	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
75		bdayelon 27742	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑆) ∈ On
76		naddel2 8614	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
77	75, 62, 63, 76	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
78	70, 77	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
79		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
80	63, 62, 79	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
81	68, 60, 80	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
82	78, 81	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
83		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On)
84	63, 61, 83	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On
85		bdayelon 27742	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑅) ∈ On
86		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
87	85, 75, 86	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
88	84, 87	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
89		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
90	63, 75, 89	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
91		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On)
92	85, 61, 91	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On
93	90, 92	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ On
94		naddcl 8603	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
95	63, 62, 94	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
96		onunel 6422	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
97	88, 93, 95, 96	mp3an 1463	. . . . . . . . . . . . . . 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 ‘𝐵))))
98		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
99	84, 87, 95, 98	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
100		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
101	90, 92, 95, 100	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
102	99, 101	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ↔ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
103	97, 102	bitri 275	. . . . . . . . . . . . . 14 ⊢ ((((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
104	74, 82, 103	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
105		elun1 4132	. . . . . . . . . . . . 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 ‘𝐸))))))
106	104, 105	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊)))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
107	58, 106	eqeltrid 2838	. . . . . . . . . . 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 ‘𝐸))))))
108	8, 45, 45, 13, 3, 47, 49, 107	mulsproplem1 28085	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)))))
109	108	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊))))
110	40, 43, 109	mp2and 699	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)))
111	17, 19, 25, 27	sltsubsubbd 28052	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
112	17, 19	subscld 28032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
113	25, 27	subscld 28032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)) ∈ No )
114	112, 113, 12	sltadd2d 27967	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)))))
115	111, 114	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑊)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊)))))
116	110, 115	mpbid 232	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
117	12, 17, 19	addsubsassd 28050	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
118	12, 25, 27	addsubsassd 28050	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑅 ·_s 𝑊))))
119	116, 117, 118	3brtr4d 5128	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)))
120	119	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)))
121		ssltleft 27842	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → ( L ‘𝐵) <<s {𝐵})
122	11, 121	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵})
123		snidg 4615	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
124	11, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
125	122, 23, 124	ssltsepcd 27762	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝐵)
126	55	uneq1i 4114	. . . . . . . . . . . . 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 ‘𝑊)))))
127		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 ‘𝑊))))
128	126, 127	eqtri 2757	. . . . . . . . . . . 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 ‘𝑊))))
129		oldbdayim 27861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
130	30, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
131		bdayelon 27742	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑉) ∈ On
132		naddel1 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
133	131, 63, 62, 132	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
134	130, 133	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	81, 134	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
136		naddel1 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137	85, 63, 62, 136	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
138	68, 137	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
139		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
140	63, 62, 139	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
141	130, 60, 140	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
142	138, 141	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
143		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On)
144	131, 62, 143	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On
145	92, 144	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
146		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
147	85, 62, 146	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
148		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On)
149	131, 61, 148	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On
150	147, 149	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
151		onunel 6422	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
152	145, 150, 95, 151	mp3an 1463	. . . . . . . . . . . . . . 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 ‘𝐵))))
153		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
154	92, 144, 95, 153	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
155		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
156	147, 149, 95, 155	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
157	154, 156	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ↔ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
158	152, 157	bitri 275	. . . . . . . . . . . . . 14 ⊢ ((((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
159	135, 142, 158	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
160		elun1 4132	. . . . . . . . . . . . 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 ‘𝐸))))))
161	159, 160	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
162	128, 161	eqeltrid 2838	. . . . . . . . . . 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 ‘𝐸))))))
163	8, 45, 45, 3, 5, 47, 11, 162	mulsproplem1 28085	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))))
164	163	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊))))
165	125, 164	mpan2d 694	. . . . . . . 8 ⊢ (𝜑 → (𝑅 <s 𝑉 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊))))
166	165	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)))
167	12, 27	subscld 28032	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) ∈ No )
168	31, 33	subscld 28032	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ∈ No )
169	167, 168, 25	sltadd1d 27968	. . . . . . . 8 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
170	169	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
171	166, 170	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
172	12, 25, 27	addsubsd 28051	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
173	172	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
174	31, 25, 33	addsubsd 28051	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
175	174	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
176	171, 173, 175	3brtr4d 5128	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑅 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
177	21, 29, 35, 120, 176	slttrd 27725	. . . 4 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
178	177	ex 412	. . 3 ⊢ (𝜑 → (𝑅 <s 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
179	37, 39, 4	ssltsepcd 27762	. . . . . . 7 ⊢ (𝜑 → 𝐴 <s 𝑉)
180	55	uneq1i 4114	. . . . . . . . . . 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 ‘𝑊)))))
181		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 ‘𝑊))))
182	180, 181	eqtri 2757	. . . . . . . . . 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 ‘𝑊))))
183		naddel12 8626	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
184	63, 62, 183	mp2an 692	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
185	130, 70, 184	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
186	66, 185	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
187	78, 141	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
188		naddcl 8603	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On)
189	131, 75, 188	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On
190	84, 189	onun2i 6438	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ On
191	90, 149	onun2i 6438	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
192		onunel 6422	. . . . . . . . . . . . . 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 ‘𝐵)))))
193	190, 191, 95, 192	mp3an 1463	. . . . . . . . . . . . 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 ‘𝐵))))
194		onunel 6422	. . . . . . . . . . . . . . 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 ‘𝐵)))))
195	84, 189, 95, 194	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
196		onunel 6422	. . . . . . . . . . . . . . 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 ‘𝐵)))))
197	90, 149, 95, 196	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
198	195, 197	anbi12i 628	. . . . . . . . . . . . 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 ‘𝐵)))))
199	193, 198	bitri 275	. . . . . . . . . . . 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 ‘𝐵)))))
200	186, 187, 199	sylanbrc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
201		elun1 4132	. . . . . . . . . . 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 ‘𝐸))))))
202	200, 201	syl 17	. . . . . . . . . 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 ‘𝐸))))))
203	182, 202	eqeltrid 2838	. . . . . . . . 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 ‘𝐸))))))
204	8, 45, 45, 13, 5, 47, 49, 203	mulsproplem1 28085	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)))))
205	204	simprd 495	. . . . . . 7 ⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊))))
206	179, 43, 205	mp2and 699	. . . . . 6 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)))
207	8, 30, 16	mulsproplem4 28088	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝑆) ∈ No )
208	17, 207, 25, 33	sltsubsubbd 28052	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
209	17, 207	subscld 28032	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) ∈ No )
210	25, 33	subscld 28032	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ∈ No )
211	209, 210, 31	sltadd2d 27967	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
212	208, 211	bitrd 279	. . . . . 6 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊)))))
213	206, 212	mpbid 232	. . . . 5 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
214	31, 17, 207	addsubsassd 28050	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑉 ·_s 𝑆))))
215	31, 25, 33	addsubsassd 28050	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) -_s (𝑉 ·_s 𝑊))))
216	213, 214, 215	3brtr4d 5128	. . . 4 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
217		oveq1 7363	. . . . . . 7 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝐵) = (𝑉 ·_s 𝐵))
218	217	oveq1d 7371	. . . . . 6 ⊢ (𝑅 = 𝑉 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)))
219		oveq1 7363	. . . . . 6 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝑆) = (𝑉 ·_s 𝑆))
220	218, 219	oveq12d 7374	. . . . 5 ⊢ (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)))
221	220	breq1d 5106	. . . 4 ⊢ (𝑅 = 𝑉 → ((((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ↔ (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
222	216, 221	syl5ibrcom 247	. . 3 ⊢ (𝜑 → (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
223	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
224	31, 17	addscld 27950	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
225	224, 207	subscld 28032	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) ∈ No )
226	225	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) ∈ No )
227	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)) ∈ No )
228		ssltright 27843	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
229	11, 228	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
230	229, 124, 15	ssltsepcd 27762	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
231	55	uneq1i 4114	. . . . . . . . . . . . 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 ‘𝐵)))))
232		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 ‘𝐵))))
233	231, 232	eqtri 2757	. . . . . . . . . . . 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 ‘𝐵))))
234	134, 73	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
235	185, 138	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
236	144, 87	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
237	189, 147	onun2i 6438	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
238		onunel 6422	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
239	236, 237, 95, 238	mp3an 1463	. . . . . . . . . . . . . . 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 ‘𝐵))))
240		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
241	144, 87, 95, 240	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
242		onunel 6422	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
243	189, 147, 95, 242	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
244	241, 243	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ↔ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
245	239, 244	bitri 275	. . . . . . . . . . . . . 14 ⊢ ((((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))) ∧ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))))
246	234, 235, 245	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
247		elun1 4132	. . . . . . . . . . . . 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 ‘𝐸))))))
248	246, 247	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
249	233, 248	eqeltrid 2838	. . . . . . . . . . 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 ‘𝐸))))))
250	8, 45, 45, 5, 3, 11, 49, 249	mulsproplem1 28085	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))))
251	250	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
252	230, 251	mpan2d 694	. . . . . . . 8 ⊢ (𝜑 → (𝑉 <s 𝑅 → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
253	252	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → ((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
254	207, 31, 19, 12	sltsubsub2bd 28053	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆))))
255	12, 19	subscld 28032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
256	31, 207	subscld 28032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) ∈ No )
257	255, 256, 17	sltadd1d 27968	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
258	254, 257	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
259	258	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝑆) -_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
260	253, 259	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
261	12, 17, 19	addsubsd 28051	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
262	261	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
263	31, 17, 207	addsubsd 28051	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
264	263	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) -_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
265	260, 262, 264	3brtr4d 5128	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)))
266	216	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
267	223, 226, 227, 265, 266	slttrd 27725	. . . 4 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))
268	267	ex 412	. . 3 ⊢ (𝜑 → (𝑉 <s 𝑅 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
269	178, 222, 268	3jaod 1431	. 2 ⊢ (𝜑 → ((𝑅 <s 𝑉 ∨ 𝑅 = 𝑉 ∨ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊))))
270	7, 269	mpd 15	1 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) -_s (𝑉 ·_s 𝑊)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ w3o 1085 = wceq 1541 ∈ wcel 2113 ∀wral 3049 ∪ cun 3897 ∅c0 4283 {csn 4578 class class class wbr 5096 Oncon0 6315 ‘cfv 6490 (class class class)co 7356 +no cnadd 8591 No csur 27605 <s cslt 27606 bday cbday 27607 <<s csslt 27747 0_s c0s 27793 O cold 27811 L cleft 27813 R cright 27814 +_s cadds 27929 -_s csubs 27989 ·_s cmuls 28075

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-ot 4587 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-1o 8395 df-2o 8396 df-nadd 8592 df-no 27608 df-slt 27609 df-bday 27610 df-sle 27711 df-sslt 27748 df-scut 27750 df-0s 27795 df-made 27815 df-old 27816 df-left 27818 df-right 27819 df-norec 27908 df-norec2 27919 df-adds 27930 df-negs 27990 df-subs 27991

This theorem is referenced by: mulsproplem9 28093

W3C validator