Theorem mulsproplem7 27567

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

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

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

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

This theorem is referenced by:  mulsproplem9  27569