Theorem mulsproplem8 27568

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 27365	. . . 4 ⊢ ( R ‘𝐴) ⊆ No
2		mulsproplem8.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
3	1, 2	sselid 3979	. . 3 ⊢ (𝜑 → 𝑅 ∈ No )
4		mulsproplem8.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ ( R ‘𝐴))
5	1, 4	sselid 3979	. . 3 ⊢ (𝜑 → 𝑉 ∈ No )
6		sltlin 27241	. . 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 27363	. . . . . . . . . 10 ⊢ ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
10	9, 2	sselid 3979	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
11		mulsproplem8.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
12	8, 10, 11	mulsproplem2 27562	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·s 𝐵) ∈ No )
13		mulsproplem8.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
14		rightssold 27363	. . . . . . . . . 10 ⊢ ( R ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
15		mulsproplem8.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
16	14, 15	sselid 3979	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
17	8, 13, 16	mulsproplem3 27563	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·s 𝑆) ∈ No )
18	12, 17	addscld 27453	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) ∈ No )
19	8, 10, 16	mulsproplem4 27564	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·s 𝑆) ∈ No )
20	18, 19	subscld 27524	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈ No )
21	20	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈ No )
22		leftssold 27362	. . . . . . . . . 10 ⊢ ( L ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
23		mulsproplem8.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ( L ‘𝐵))
24	22, 23	sselid 3979	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ( O ‘( bday ‘𝐵)))
25	8, 13, 24	mulsproplem3 27563	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·s 𝑊) ∈ No )
26	12, 25	addscld 27453	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No )
27	8, 10, 24	mulsproplem4 27564	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·s 𝑊) ∈ No )
28	26, 27	subscld 27524	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) ∈ No )
29	28	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) ∈ No )
30	9, 4	sselid 3979	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ( O ‘( bday ‘𝐴)))
31	8, 30, 11	mulsproplem2 27562	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·s 𝐵) ∈ No )
32	31, 25	addscld 27453	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) ∈ No )
33	8, 30, 24	mulsproplem4 27564	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·s 𝑊) ∈ No )
34	32, 33	subscld 27524	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No )
35	34	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No )
36		ssltright 27355	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
37	13, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
38		snidg 4661	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
39	13, 38	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
40	37, 39, 2	ssltsepcd 27284	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
41		lltropt 27356	. . . . . . . . . . 11 ⊢ ( L ‘𝐵) <<s ( R ‘𝐵)
42	41	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵))
43	42, 23, 15	ssltsepcd 27284	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝑆)
44		0sno 27316	. . . . . . . . . . . 12 ⊢ 0s ∈ No
45	44	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0s ∈ No )
46		leftssno 27364	. . . . . . . . . . . 12 ⊢ ( L ‘𝐵) ⊆ No
47	46, 23	sselid 3979	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ No )
48		rightssno 27365	. . . . . . . . . . . 12 ⊢ ( R ‘𝐵) ⊆ No
49	48, 15	sselid 3979	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ No )
50		bday0s 27318	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0s ) = ∅
51	50, 50	oveq12i 7417	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
52		0elon 6415	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
53		naddrid 8678	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
55	51, 54	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
56	55	uneq1i 4158	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))))) = (∅ ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊)))))
57		0un 4391	. . . . . . . . . . . . 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 2760	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))))) = (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))))
59		oldbdayim 27372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
60	24, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑊) ∈ ( bday ‘𝐵))
61		bdayelon 27267	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑊) ∈ On
62		bdayelon 27267	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
63		bdayelon 27267	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
64		naddel2 8683	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑊) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
65	61, 62, 63, 64	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑊) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
66	60, 65	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67		oldbdayim 27372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
68	10, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
69		oldbdayim 27372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
70	16, 69	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
71		naddel12 8695	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
72	63, 62, 71	mp2an 690	. . . . . . . . . . . . . . . 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 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
75		bdayelon 27267	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑆) ∈ On
76		naddel2 8683	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
77	75, 62, 63, 76	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
78	70, 77	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
79		naddel12 8695	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
80	63, 62, 79	mp2an 690	. . . . . . . . . . . . . . . 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 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
83		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On)
84	63, 61, 83	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ On
85		bdayelon 27267	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑅) ∈ On
86		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
87	85, 75, 86	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
88	84, 87	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
89		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
90	63, 75, 89	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
91		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On)
92	85, 61, 91	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ On
93	90, 92	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))) ∈ On
94		naddcl 8672	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
95	63, 62, 94	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
96		onunel 6466	. . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . 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 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
100		onunel 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 4175	. . . . . . . . . . . . 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 2837	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑊))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
108	8, 45, 45, 13, 3, 47, 49, 107	mulsproplem1 27561	. . . . . . . . . 10 ⊢ (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑊)))))
109	108	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑊 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑊))))
110	40, 43, 109	mp2and 697	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑊)))
111	17, 19, 25, 27	sltsubsubbd 27539	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑊)) ↔ ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) <s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊))))
112	17, 19	subscld 27524	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) ∈ No )
113	25, 27	subscld 27524	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊)) ∈ No )
114	112, 113, 12	sltadd2d 27469	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) <s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊)) ↔ ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊)))))
115	111, 114	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑊)) ↔ ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊)))))
116	110, 115	mpbid 231	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊))))
117	12, 17, 19	addsubsassd 27537	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))))
118	12, 25, 27	addsubsassd 27537	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑅 ·s 𝑊))))
119	116, 117, 118	3brtr4d 5179	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)))
120	119	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)))
121		ssltleft 27354	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → ( L ‘𝐵) <<s {𝐵})
122	11, 121	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵})
123		snidg 4661	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
124	11, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
125	122, 23, 124	ssltsepcd 27284	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝐵)
126	55	uneq1i 4158	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (∅ ∪ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))))
127		0un 4391	. . . . . . . . . . . . 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 2760	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))
129		oldbdayim 27372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
130	30, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑉) ∈ ( bday ‘𝐴))
131		bdayelon 27267	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑉) ∈ On
132		naddel1 8682	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
133	131, 63, 62, 132	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑉) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
134	130, 133	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	81, 134	jca 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
136		naddel1 8682	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137	85, 63, 62, 136	mp3an 1461	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
138	68, 137	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
139		naddel12 8695	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑊) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
140	63, 62, 139	mp2an 690	. . . . . . . . . . . . . . . 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 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
143		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On)
144	131, 62, 143	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ On
145	92, 144	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ On
146		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
147	85, 62, 146	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
148		naddcl 8672	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑊) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On)
149	131, 61, 148	mp2an 690	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ On
150	147, 149	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
151		onunel 6466	. . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . 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 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑅) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
155		onunel 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 4175	. . . . . . . . . . . . 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 2837	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑅) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝐵))) ∪ ((( bday ‘𝑅) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
163	8, 45, 45, 3, 5, 47, 11, 162	mulsproplem1 27561	. . . . . . . . . 10 ⊢ (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)))))
164	163	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 <s 𝑉 ∧ 𝑊 <s 𝐵) → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊))))
165	125, 164	mpan2d 692	. . . . . . . 8 ⊢ (𝜑 → (𝑅 <s 𝑉 → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊))))
166	165	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)))
167	12, 27	subscld 27524	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) ∈ No )
168	31, 33	subscld 27524	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ∈ No )
169	167, 168, 25	sltadd1d 27470	. . . . . . . 8 ⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊))))
170	169	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊))))
171	166, 170	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) +s (𝐴 ·s 𝑊)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
172	12, 25, 27	addsubsd 27538	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
173	172	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
174	31, 25, 33	addsubsd 27538	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
175	174	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑊)) +s (𝐴 ·s 𝑊)))
176	171, 173, 175	3brtr4d 5179	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑅 ·s 𝑊)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
177	21, 29, 35, 120, 176	slttrd 27251	. . . 4 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
178	177	ex 413	. . 3 ⊢ (𝜑 → (𝑅 <s 𝑉 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
179	37, 39, 4	ssltsepcd 27284	. . . . . . 7 ⊢ (𝜑 → 𝐴 <s 𝑉)
180	55	uneq1i 4158	. . . . . . . . . . 11 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (∅ ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊)))))
181		0un 4391	. . . . . . . . . . 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 2760	. . . . . . . . . 10 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) = (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))
183		naddel12 8695	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑉) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
184	63, 62, 183	mp2an 690	. . . . . . . . . . . . . 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 512	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
187	78, 141	jca 512	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
188		naddcl 8672	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On)
189	131, 75, 188	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ On
190	84, 189	onun2i 6483	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ On
191	90, 149	onun2i 6483	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))) ∈ On
192		onunel 6466	. . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . 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 6466	. . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑊)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
196		onunel 6466	. . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . 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 627	. . . . . . . . . . . . 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 274	. . . . . . . . . . . 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 4175	. . . . . . . . . . 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 2837	. . . . . . . . 9 ⊢ (𝜑 → ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday ‘𝑊)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑉) +no ( bday ‘𝑊))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
204	8, 45, 45, 13, 5, 47, 49, 203	mulsproplem1 27561	. . . . . . . 8 ⊢ (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝑊)))))
205	204	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝑊))))
206	179, 43, 205	mp2and 697	. . . . . 6 ⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝑊)))
207	8, 30, 16	mulsproplem4 27564	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·s 𝑆) ∈ No )
208	17, 207, 25, 33	sltsubsubbd 27539	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝑊)) ↔ ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))
209	17, 207	subscld 27524	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆)) ∈ No )
210	25, 33	subscld 27524	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ∈ No )
211	209, 210, 31	sltadd2d 27469	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆)) <s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))))
212	208, 211	bitrd 278	. . . . . 6 ⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑊)) <s ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝑊)) ↔ ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊)))))
213	206, 212	mpbid 231	. . . . 5 ⊢ (𝜑 → ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆))) <s ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))
214	31, 17, 207	addsubsassd 27537	. . . . 5 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑉 ·s 𝑆))))
215	31, 25, 33	addsubsassd 27537	. . . . 5 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) = ((𝑉 ·s 𝐵) +s ((𝐴 ·s 𝑊) -s (𝑉 ·s 𝑊))))
216	213, 214, 215	3brtr4d 5179	. . . 4 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
217		oveq1 7412	. . . . . . 7 ⊢ (𝑅 = 𝑉 → (𝑅 ·s 𝐵) = (𝑉 ·s 𝐵))
218	217	oveq1d 7420	. . . . . 6 ⊢ (𝑅 = 𝑉 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) = ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)))
219		oveq1 7412	. . . . . 6 ⊢ (𝑅 = 𝑉 → (𝑅 ·s 𝑆) = (𝑉 ·s 𝑆))
220	218, 219	oveq12d 7423	. . . . 5 ⊢ (𝑅 = 𝑉 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)))
221	220	breq1d 5157	. . . 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 246	. . 3 ⊢ (𝜑 → (𝑅 = 𝑉 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
223	20	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈ No )
224	31, 17	addscld 27453	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) ∈ No )
225	224, 207	subscld 27524	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) ∈ No )
226	225	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) ∈ No )
227	34	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)) ∈ No )
228		ssltright 27355	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
229	11, 228	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
230	229, 124, 15	ssltsepcd 27284	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
231	55	uneq1i 4158	. . . . . . . . . . . . 13 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))))) = (∅ ∪ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))))
232		0un 4391	. . . . . . . . . . . . 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 2760	. . . . . . . . . . . 12 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))))) = (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))))
234	134, 73	jca 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
235	185, 138	jca 512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
236	144, 87	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
237	189, 147	onun2i 6483	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
238		onunel 6466	. . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . 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 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑉) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
242		onunel 6466	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 4175	. . . . . . . . . . . . 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 2837	. . . . . . . . . . 11 ⊢ (𝜑 → ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑉) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑉) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
250	8, 45, 45, 5, 3, 11, 49, 249	mulsproplem1 27561	. . . . . . . . . 10 ⊢ (𝜑 → (( 0s ·s 0s ) ∈ No ∧ ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)))))
251	250	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵))))
252	230, 251	mpan2d 692	. . . . . . . 8 ⊢ (𝜑 → (𝑉 <s 𝑅 → ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵))))
253	252	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → ((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)))
254	207, 31, 19, 12	sltsubsub2bd 27540	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)) ↔ ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆))))
255	12, 19	subscld 27524	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) ∈ No )
256	31, 207	subscld 27524	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) ∈ No )
257	255, 256, 17	sltadd1d 27470	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) <s ((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆))))
258	254, 257	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆))))
259	258	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·s 𝑆) -s (𝑉 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆))))
260	253, 259	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆)))
261	12, 17, 19	addsubsd 27538	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)))
262	261	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)))
263	31, 17, 207	addsubsd 27538	. . . . . . 7 ⊢ (𝜑 → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆)))
264	263	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) = (((𝑉 ·s 𝐵) -s (𝑉 ·s 𝑆)) +s (𝐴 ·s 𝑆)))
265	260, 262, 264	3brtr4d 5179	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)))
266	216	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑉 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
267	223, 226, 227, 265, 266	slttrd 27251	. . . 4 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊)))
268	267	ex 413	. . 3 ⊢ (𝜑 → (𝑉 <s 𝑅 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑉 ·s 𝐵) +s (𝐴 ·s 𝑊)) -s (𝑉 ·s 𝑊))))
269	178, 222, 268	3jaod 1428	. 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 𝑊)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  ∀wral 3061   ∪ cun 3945  ∅c0 4321  {csn 4627   class class class wbr 5147  Oncon0 6361  ‘cfv 6540  (class class class)co 7405   +no cnadd 8660   No csur 27132   <s cslt 27133   bday cbday 27134   <<s csslt 27271   0_s c0s 27312   O cold 27327   L cleft 27329   R cright 27330   +_s cadds 27432   -_s csubs 27484   ·_s cmuls 27551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-1o 8462  df-2o 8463  df-nadd 8661  df-no 27135  df-slt 27136  df-bday 27137  df-sle 27237  df-sslt 27272  df-scut 27274  df-0s 27314  df-made 27331  df-old 27332  df-left 27334  df-right 27335  df-norec 27411  df-norec2 27422  df-adds 27433  df-negs 27485  df-subs 27486

This theorem is referenced by:  mulsproplem9  27569