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 28166

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 27938	. . . 4 ⊢ ( R ‘𝐵) ⊆ No
2		mulsproplem7.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
3	1, 2	sselid 4006	. . 3 ⊢ (𝜑 → 𝑆 ∈ No )
4		mulsproplem7.6	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))
5	1, 4	sselid 4006	. . 3 ⊢ (𝜑 → 𝑈 ∈ No )
6		sltlin 27812	. . 3 ⊢ ((𝑆 ∈ No ∧ 𝑈 ∈ No ) → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆))
7	3, 5, 6	syl2anc 583	. 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 27936	. . . . . . . . . 10 ⊢ ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
10		mulsproplem7.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
11	9, 10	sselid 4006	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
12		mulsproplem7.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
13	8, 11, 12	mulsproplem2 28161	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
14		mulsproplem7.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
15		rightssold 27936	. . . . . . . . . 10 ⊢ ( R ‘𝐵) ⊆ ( O ‘( bday ‘𝐵))
16	15, 2	sselid 4006	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
17	8, 14, 16	mulsproplem3 28162	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
18	13, 17	addscld 28031	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
19	8, 11, 16	mulsproplem4 28163	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
20	18, 19	subscld 28111	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
21	20	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
22		leftssold 27935	. . . . . . . . . 10 ⊢ ( L ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))
23		mulsproplem7.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))
24	22, 23	sselid 4006	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ( O ‘( bday ‘𝐴)))
25	8, 24, 12	mulsproplem2 28161	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No )
26	25, 17	addscld 28031	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
27	8, 24, 16	mulsproplem4 28163	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑆) ∈ No )
28	26, 27	subscld 28111	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
29	28	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
30	15, 4	sselid 4006	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ ( O ‘( bday ‘𝐵)))
31	8, 14, 30	mulsproplem3 28162	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No )
32	25, 31	addscld 28031	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
33	8, 24, 30	mulsproplem4 28163	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No )
34	32, 33	subscld 28111	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
35	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
36		lltropt 27929	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
37	36	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
38	37, 23, 10	ssltsepcd 27857	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝑅)
39		ssltright 27928	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
40	12, 39	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
41		snidg 4682	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
42	12, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
43	40, 42, 2	ssltsepcd 27857	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
44		0sno 27889	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
45	44	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
46		leftssno 27937	. . . . . . . . . . . 12 ⊢ ( L ‘𝐴) ⊆ No
47	46, 23	sselid 4006	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ No )
48		rightssno 27938	. . . . . . . . . . . 12 ⊢ ( R ‘𝐴) ⊆ No
49	48, 10	sselid 4006	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ No )
50		bday0s 27891	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
51	50, 50	oveq12i 7460	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
52		0elon 6449	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
53		naddrid 8739	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
55	51, 54	eqtri 2768	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
56	55	uneq1i 4187	. . . . . . . . . . . . 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 4419	. . . . . . . . . . . . 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 2768	. . . . . . . . . . . 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 27945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
60	24, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
61		bdayelon 27839	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑇) ∈ On
62		bdayelon 27839	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
63		bdayelon 27839	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
64		naddel1 8743	. . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67		oldbdayim 27945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
68	11, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
69		oldbdayim 27945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
70	16, 69	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
71		naddel12 8756	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
72	62, 63, 71	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
73	68, 70, 72	syl2anc 583	. . . . . . . . . . . . . . 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 8756	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
76	62, 63, 75	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
77	60, 70, 76	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
78		bdayelon 27839	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑅) ∈ On
79		naddel1 8743	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
80	78, 62, 63, 79	mp3an 1461	. . . . . . . . . . . . . . . 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 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On)
84	61, 63, 83	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On
85		bdayelon 27839	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑆) ∈ On
86		naddcl 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
87	78, 85, 86	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
88	84, 87	onun2i 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
89		naddcl 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On)
90	61, 85, 89	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On
91		naddcl 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
92	78, 63, 91	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
93	90, 92	onun2i 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
94		naddcl 8733	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
95	62, 63, 94	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
96		onunel 6500	. . . . . . . . . . . . . . . 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 6500	. . . . . . . . . . . . . . . . 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 6500	. . . . . . . . . . . . . . . . 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 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 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
105		elun1 4205	. . . . . . . . . . . . 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 2848	. . . . . . . . . . 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 28160	. . . . . . . . . 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 698	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
111	27, 25, 19, 13	sltsubsub2bd 28132	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆))))
112	13, 19	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
113	25, 27	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ∈ No )
114	112, 113, 17	sltadd1d 28049	. . . . . . . . 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 28130	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
118	25, 17, 27	addsubsd 28130	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
119	116, 117, 118	3brtr4d 5198	. . . . . 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 27927	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
122	14, 121	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴})
123		snidg 4682	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
124	14, 123	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
125	122, 23, 124	ssltsepcd 27857	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
126	55	uneq1i 4187	. . . . . . . . . . . . 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 4419	. . . . . . . . . . . . 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 2768	. . . . . . . . . . . 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 27945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
130	30, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
131		bdayelon 27839	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑈) ∈ On
132		naddel2 8744	. . . . . . . . . . . . . . . . 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 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 8756	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137	62, 63, 136	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
138	60, 130, 137	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
139		naddel2 8744	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
140	85, 63, 62, 139	mp3an 1461	. . . . . . . . . . . . . . . 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 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On)
144	62, 131, 143	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On
145	90, 144	onun2i 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ On
146		naddcl 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On)
147	61, 131, 146	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On
148		naddcl 8733	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
149	62, 85, 148	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
150	147, 149	onun2i 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆))) ∈ On
151		onunel 6500	. . . . . . . . . . . . . . . 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 6500	. . . . . . . . . . . . . . . . 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 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 6500	. . . . . . . . . . . . . . . . 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 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 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
160		elun1 4205	. . . . . . . . . . . . 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 2848	. . . . . . . . . . 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 28160	. . . . . . . . . 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 694	. . . . . . . 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 28133	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
168	17, 27	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) ∈ No )
169	31, 33	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ∈ No )
170	168, 169, 25	sltadd2d 28048	. . . . . . . . 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 28129	. . . . . . 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 28129	. . . . . . 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 5198	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
179	21, 29, 35, 120, 178	slttrd 27822	. . . 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 27857	. . . . . . 7 ⊢ (𝜑 → 𝐵 <s 𝑈)
182	55	uneq1i 4187	. . . . . . . . . . 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 4419	. . . . . . . . . . 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 2768	. . . . . . . . . 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 8756	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
186	62, 63, 185	mp2an 691	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
187	68, 130, 186	syl2anc 583	. . . . . . . . . . . . 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 8733	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On)
191	78, 131, 190	mp2an 691	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On
192	84, 191	onun2i 6517	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
193	147, 92	onun2i 6517	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
194		onunel 6500	. . . . . . . . . . . . . 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 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 ‘𝐵))))
196		onunel 6500	. . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
198		onunel 6500	. . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . 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 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 ‘𝐵)))))
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 582	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
203		elun1 4205	. . . . . . . . . . 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 2848	. . . . . . . . 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 28160	. . . . . . . 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 698	. . . . . 6 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))
209	8, 11, 30	mulsproplem4 28163	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝑈) ∈ No )
210	33, 25, 209, 13	sltsubsub2bd 28132	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈))))
211	13, 209	subscld 28111	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) ∈ No )
212	25, 33	subscld 28111	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ∈ No )
213	211, 212, 31	sltadd1d 28049	. . . . . . 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 28130	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
217	25, 31, 33	addsubsd 28130	. . . . 5 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
218	215, 216, 217	3brtr4d 5198	. . . 4 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
219		oveq2 7456	. . . . . . 7 ⊢ (𝑆 = 𝑈 → (𝐴 ·_s 𝑆) = (𝐴 ·_s 𝑈))
220	219	oveq2d 7464	. . . . . 6 ⊢ (𝑆 = 𝑈 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)))
221		oveq2 7456	. . . . . 6 ⊢ (𝑆 = 𝑈 → (𝑅 ·_s 𝑆) = (𝑅 ·_s 𝑈))
222	220, 221	oveq12d 7466	. . . . 5 ⊢ (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
223	222	breq1d 5176	. . . 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 28031	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
227	226, 209	subscld 28111	. . . . . 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 27928	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
231	14, 230	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
232	231, 124, 10	ssltsepcd 27857	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
233	55	uneq1i 4187	. . . . . . . . . . . . 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 4419	. . . . . . . . . . . . 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 2768	. . . . . . . . . . . 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 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
239	149, 191	onun2i 6517	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
240		onunel 6500	. . . . . . . . . . . . . . . 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 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 ‘𝐵))))
242		onunel 6500	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
244		onunel 6500	. . . . . . . . . . . . . . . . 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 1461	. . . . . . . . . . . . . . . 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 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 ‘𝐵)))))
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 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
249		elun1 4205	. . . . . . . . . . . . 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 2848	. . . . . . . . . . 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 28160	. . . . . . . . . 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 694	. . . . . . . 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 28131	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
257	17, 19	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
258	31, 209	subscld 28111	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ∈ No )
259	257, 258, 13	sltadd2d 28048	. . . . . . . . 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 28129	. . . . . . 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 28129	. . . . . . 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 5198	. . . . 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 27822	. . . 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 1429	. 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 1086 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∪ cun 3974 ∅c0 4352 {csn 4648 class class class wbr 5166 Oncon0 6395 ‘cfv 6573 (class class class)co 7448 +no cnadd 8721 No csur 27702 <s cslt 27703 bday cbday 27704 <<s csslt 27843 0_s c0s 27885 O cold 27900 L cleft 27902 R cright 27903 +_s cadds 28010 -_s csubs 28070 ·_s cmuls 28150

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-ot 4657 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-1o 8522 df-2o 8523 df-nadd 8722 df-no 27705 df-slt 27706 df-bday 27707 df-sle 27808 df-sslt 27844 df-scut 27846 df-0s 27887 df-made 27904 df-old 27905 df-left 27907 df-right 27908 df-norec 27989 df-norec2 28000 df-adds 28011 df-negs 28071 df-subs 28072

This theorem is referenced by: mulsproplem9 28168

W3C validator