mulsproplem7 - Metamath Proof Explorer

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

Theorem mulsproplem7 28149

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

**Assertion**
Ref	Expression
mulsproplem7	⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))

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

**Proof of Theorem mulsproplem7**
Step	Hyp	Ref	Expression
1		rightssno 27921	. . . 4 ⊢ ( R ‘𝐵) ⊆ No
2		mulsproplem7.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
3	1, 2	sselid 3980	. . 3 ⊢ (𝜑 → 𝑆 ∈ No )
4		mulsproplem7.6	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))
5	1, 4	sselid 3980	. . 3 ⊢ (𝜑 → 𝑈 ∈ No )
6		sltlin 27795	. . 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 27919	. . . . . . . . . 10 ⊢ ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
10		mulsproplem7.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
11	9, 10	sselid 3980	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
12		mulsproplem7.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
13	8, 11, 12	mulsproplem2 28144	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
14		mulsproplem7.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
15		rightssold 27919	. . . . . . . . . 10 ⊢ ( R ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
16	15, 2	sselid 3980	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
17	8, 14, 16	mulsproplem3 28145	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
18	13, 17	addscld 28014	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
19	8, 11, 16	mulsproplem4 28146	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
20	18, 19	subscld 28094	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
21	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
22		leftssold 27918	. . . . . . . . . 10 ⊢ ( L ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
23		mulsproplem7.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))
24	22, 23	sselid 3980	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ( O ‘( bday ‘𝐴)))
25	8, 24, 12	mulsproplem2 28144	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No )
26	25, 17	addscld 28014	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
27	8, 24, 16	mulsproplem4 28146	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑆) ∈ No )
28	26, 27	subscld 28094	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
29	28	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
30	15, 4	sselid 3980	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ ( O ‘( bday ‘𝐵)))
31	8, 14, 30	mulsproplem3 28145	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No )
32	25, 31	addscld 28014	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
33	8, 24, 30	mulsproplem4 28146	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No )
34	32, 33	subscld 28094	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
35	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
36		lltropt 27912	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
37	36	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
38	37, 23, 10	ssltsepcd 27840	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝑅)
39		ssltright 27911	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
40	12, 39	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
41		snidg 4659	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
42	12, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
43	40, 42, 2	ssltsepcd 27840	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
44		0sno 27872	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
45	44	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
46		leftssno 27920	. . . . . . . . . . . 12 ⊢ ( L ‘𝐴) ⊆ No
47	46, 23	sselid 3980	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ No )
48		rightssno 27921	. . . . . . . . . . . 12 ⊢ ( R ‘𝐴) ⊆ No
49	48, 10	sselid 3980	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ No )
50		bday0s 27874	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
51	50, 50	oveq12i 7444	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
52		0elon 6437	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
53		naddrid 8722	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
55	51, 54	eqtri 2764	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
56	55	uneq1i 4163	. . . . . . . . . . . . 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 4395	. . . . . . . . . . . . 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 2764	. . . . . . . . . . . 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 27928	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
60	24, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
61		bdayelon 27822	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑇) ∈ On
62		bdayelon 27822	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
63		bdayelon 27822	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
64		naddel1 8726	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
65	61, 62, 63, 64	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
66	60, 65	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67		oldbdayim 27928	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
68	11, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
69		oldbdayim 27928	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
70	16, 69	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
71		naddel12 8739	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
72	62, 63, 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		naddel12 8739	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
76	62, 63, 75	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
77	60, 70, 76	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
78		bdayelon 27822	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑅) ∈ On
79		naddel1 8726	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
80	78, 62, 63, 79	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
81	68, 80	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
82	77, 81	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
83		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On)
84	61, 63, 83	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On
85		bdayelon 27822	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑆) ∈ On
86		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
87	78, 85, 86	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
88	84, 87	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
89		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On)
90	61, 85, 89	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On
91		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
92	78, 63, 91	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
93	90, 92	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
94		naddcl 8716	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
95	62, 63, 94	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
96		onunel 6488	. . . . . . . . . . . . . . . 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 1462	. . . . . . . . . . . . . . 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 6488	. . . . . . . . . . . . . . . . 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 1462	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
100		onunel 6488	. . . . . . . . . . . . . . . . 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 1462	. . . . . . . . . . . . . . . 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 4181	. . . . . . . . . . . . 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 2844	. . . . . . . . . . 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, 47, 49, 12, 3, 107	mulsproplem1 28143	. . . . . . . . . 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	38, 43, 109	mp2and 699	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
111	27, 25, 19, 13	sltsubsub2bd 28115	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆))))
112	13, 19	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
113	25, 27	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ∈ No )
114	112, 113, 17	sltadd1d 28032	. . . . . . . . 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	13, 17, 19	addsubsd 28113	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
118	25, 17, 27	addsubsd 28113	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
119	116, 117, 118	3brtr4d 5174	. . . . . 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 27910	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
122	14, 121	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴})
123		snidg 4659	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
124	14, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
125	122, 23, 124	ssltsepcd 27840	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
126	55	uneq1i 4163	. . . . . . . . . . . . 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 4395	. . . . . . . . . . . . 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 2764	. . . . . . . . . . . 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 27928	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
130	30, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
131		bdayelon 27822	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑈) ∈ On
132		naddel2 8727	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑈) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
133	131, 63, 62, 132	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
134	130, 133	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	77, 134	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
136		naddel12 8739	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137	62, 63, 136	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
138	60, 130, 137	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
139		naddel2 8727	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
140	85, 63, 62, 139	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
141	70, 140	sylib 218	. . . . . . . . . . . . . . 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 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On)
144	62, 131, 143	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On
145	90, 144	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ On
146		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On)
147	61, 131, 146	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On
148		naddcl 8716	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
149	62, 85, 148	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
150	147, 149	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆))) ∈ On
151		onunel 6488	. . . . . . . . . . . . . . . 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 1462	. . . . . . . . . . . . . . 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 6488	. . . . . . . . . . . . . . . . 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	90, 144, 95, 153	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
155		onunel 6488	. . . . . . . . . . . . . . . . 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 1462	. . . . . . . . . . . . . . . 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 4181	. . . . . . . . . . . . 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 2844	. . . . . . . . . . 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, 47, 14, 3, 5, 162	mulsproplem1 28143	. . . . . . . . . 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	mpand 695	. . . . . . . 8 ⊢ (𝜑 → (𝑆 <s 𝑈 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆))))
166	165	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)))
167	33, 31, 27, 17	sltsubsub3bd 28116	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
168	17, 27	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) ∈ No )
169	31, 33	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ∈ No )
170	168, 169, 25	sltadd2d 28031	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
171	167, 170	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
172	171	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
173	166, 172	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
174	25, 17, 27	addsubsassd 28112	. . . . . . 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	25, 31, 33	addsubsassd 28112	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
177	176	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
178	173, 175, 177	3brtr4d 5174	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
179	21, 29, 35, 120, 178	slttrd 27805	. . . 4 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
180	179	ex 412	. . 3 ⊢ (𝜑 → (𝑆 <s 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
181	40, 42, 4	ssltsepcd 27840	. . . . . . 7 ⊢ (𝜑 → 𝐵 <s 𝑈)
182	55	uneq1i 4163	. . . . . . . . . . 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 ‘𝐵)))))
183		0un 4395	. . . . . . . . . . 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 ‘𝐵))))
184	182, 183	eqtri 2764	. . . . . . . . . 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 ‘𝐵))))
185		naddel12 8739	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
186	62, 63, 185	mp2an 692	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
187	68, 130, 186	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
188	66, 187	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
189	138, 81	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
190		naddcl 8716	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On)
191	78, 131, 190	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On
192	84, 191	onun2i 6505	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
193	147, 92	onun2i 6505	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
194		onunel 6488	. . . . . . . . . . . . . 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 ‘𝐵)))))
195	192, 193, 95, 194	mp3an 1462	. . . . . . . . . . . . 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 ‘𝐵))))
196		onunel 6488	. . . . . . . . . . . . . . 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	84, 191, 95, 196	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
198		onunel 6488	. . . . . . . . . . . . . . 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 ‘𝐵)))))
199	147, 92, 95, 198	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
200	197, 199	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 ‘𝐵)))))
201	195, 200	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 ‘𝐵)))))
202	188, 189, 201	sylanbrc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
203		elun1 4181	. . . . . . . . . . 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 ‘𝐸))))))
204	202, 203	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 ‘𝐸))))))
205	184, 204	eqeltrid 2844	. . . . . . . . 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 ‘𝐸))))))
206	8, 45, 45, 47, 49, 12, 5, 205	mulsproplem1 28143	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))))
207	206	simprd 495	. . . . . . 7 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵))))
208	38, 181, 207	mp2and 699	. . . . . 6 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))
209	8, 11, 30	mulsproplem4 28146	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝑈) ∈ No )
210	33, 25, 209, 13	sltsubsub2bd 28115	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈))))
211	13, 209	subscld 28094	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) ∈ No )
212	25, 33	subscld 28094	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ∈ No )
213	211, 212, 31	sltadd1d 28032	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
214	210, 213	bitrd 279	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
215	208, 214	mpbid 232	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
216	13, 31, 209	addsubsd 28113	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
217	25, 31, 33	addsubsd 28113	. . . . 5 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
218	215, 216, 217	3brtr4d 5174	. . . 4 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
219		oveq2 7440	. . . . . . 7 ⊢ (𝑆 = 𝑈 → (𝐴 ·_s 𝑆) = (𝐴 ·_s 𝑈))
220	219	oveq2d 7448	. . . . . 6 ⊢ (𝑆 = 𝑈 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)))
221		oveq2 7440	. . . . . 6 ⊢ (𝑆 = 𝑈 → (𝑅 ·_s 𝑆) = (𝑅 ·_s 𝑈))
222	220, 221	oveq12d 7450	. . . . 5 ⊢ (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
223	222	breq1d 5152	. . . 4 ⊢ (𝑆 = 𝑈 → ((((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ↔ (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
224	218, 223	syl5ibrcom 247	. . 3 ⊢ (𝜑 → (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
225	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
226	13, 31	addscld 28014	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
227	226, 209	subscld 28094	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
228	227	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
229	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
230		ssltright 27911	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
231	14, 230	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
232	231, 124, 10	ssltsepcd 27840	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
233	55	uneq1i 4163	. . . . . . . . . . . . 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 ‘𝑈)))))
234		0un 4395	. . . . . . . . . . . . 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 ‘𝑈))))
235	233, 234	eqtri 2764	. . . . . . . . . . . 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 ‘𝑈))))
236	134, 73	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
237	141, 187	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
238	144, 87	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
239	149, 191	onun2i 6505	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
240		onunel 6488	. . . . . . . . . . . . . . . 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 ‘𝐵)))))
241	238, 239, 95, 240	mp3an 1462	. . . . . . . . . . . . . . 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 ‘𝐵))))
242		onunel 6488	. . . . . . . . . . . . . . . . 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	144, 87, 95, 242	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
244		onunel 6488	. . . . . . . . . . . . . . . . 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 ‘𝐵)))))
245	149, 191, 95, 244	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
246	243, 245	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 ‘𝐵)))))
247	241, 246	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 ‘𝐵)))))
248	236, 237, 247	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
249		elun1 4181	. . . . . . . . . . . . 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 ‘𝐸))))))
250	248, 249	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 ‘𝐸))))))
251	235, 250	eqeltrid 2844	. . . . . . . . . . 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 ‘𝐸))))))
252	8, 45, 45, 14, 49, 5, 3, 251	mulsproplem1 28143	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))))
253	252	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
254	232, 253	mpand 695	. . . . . . . 8 ⊢ (𝜑 → (𝑈 <s 𝑆 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
255	254	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))
256	17, 19, 31, 209	sltsubsubbd 28114	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
257	17, 19	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
258	31, 209	subscld 28094	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ∈ No )
259	257, 258, 13	sltadd2d 28031	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
260	256, 259	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
261	260	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
262	255, 261	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
263	13, 17, 19	addsubsassd 28112	. . . . . . 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	13, 31, 209	addsubsassd 28112	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
266	265	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
267	262, 264, 266	3brtr4d 5174	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
268	218	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
269	225, 228, 229, 267, 268	slttrd 27805	. . . 4 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
270	269	ex 412	. . 3 ⊢ (𝜑 → (𝑈 <s 𝑆 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
271	180, 224, 270	3jaod 1430	. 2 ⊢ (𝜑 → ((𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
272	7, 271	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 1539 ∈ wcel 2107 ∀wral 3060 ∪ cun 3948 ∅c0 4332 {csn 4625 class class class wbr 5142 Oncon0 6383 ‘cfv 6560 (class class class)co 7432 +no cnadd 8704 No csur 27685 <s cslt 27686 bday cbday 27687 <<s csslt 27826 0_s c0s 27868 O cold 27883 L cleft 27885 R cright 27886 +_s cadds 27993 -_s csubs 28053 ·_s cmuls 28133

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-ot 4634 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-1o 8507 df-2o 8508 df-nadd 8705 df-no 27688 df-slt 27689 df-bday 27690 df-sle 27791 df-sslt 27827 df-scut 27829 df-0s 27870 df-made 27887 df-old 27888 df-left 27890 df-right 27891 df-norec 27972 df-norec2 27983 df-adds 27994 df-negs 28054 df-subs 28055

This theorem is referenced by: mulsproplem9 28151

W3C validator