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 28277

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		mulsproplem7.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵))
2	1	rightnod 28037	. . 3 ⊢ (𝜑 → 𝑆 ∈ No )
3		mulsproplem7.6	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))
4	3	rightnod 28037	. . 3 ⊢ (𝜑 → 𝑈 ∈ No )
5		ltslin 27875	. . 3 ⊢ ((𝑆 ∈ No ∧ 𝑈 ∈ No ) → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆))
6	2, 4, 5	syl2anc 595	. 2 ⊢ (𝜑 → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆))
7		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 𝑒))))))
8		mulsproplem7.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴))
9	8	rightoldd 28036	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
10		mulsproplem7.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
11	7, 9, 10	mulsproplem2 28272	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
12		mulsproplem7.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
13	1	rightoldd 28036	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
14	7, 12, 13	mulsproplem3 28273	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
15	11, 14	addscld 28135	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
16	7, 9, 13	mulsproplem4 28274	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
17	15, 16	subscld 28218	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
18	17	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
19		mulsproplem7.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))
20	19	leftoldd 28034	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ( O ‘( bday ‘𝐴)))
21	7, 20, 10	mulsproplem2 28272	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No )
22	21, 14	addscld 28135	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
23	7, 20, 13	mulsproplem4 28274	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑆) ∈ No )
24	22, 23	subscld 28218	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
25	24	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
26	3	rightoldd 28036	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ ( O ‘( bday ‘𝐵)))
27	7, 12, 26	mulsproplem3 28273	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No )
28	21, 27	addscld 28135	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
29	7, 20, 26	mulsproplem4 28274	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No )
30	28, 29	subscld 28218	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
31	30	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
32		lltr 28017	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
33	32	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
34	33, 19, 8	sltssepcd 27927	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝑅)
35		sltsright 28016	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
36	10, 35	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
37		snidg 4628	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
38	10, 37	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
39	36, 38, 1	sltssepcd 27927	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
40		0no 27964	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
42	19	leftnod 28035	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ No )
43	8	rightnod 28037	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ No )
44		bday0 27966	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
45	44, 44	oveq12i 7420	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
46		0elon 6414	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8666	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2792	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
50	49	uneq1i 4126	. . . . . . . . . . . . 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 ‘𝐵)))))
51		0un 4359	. . . . . . . . . . . . 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 ‘𝐵))))
52	50, 51	eqtri 2792	. . . . . . . . . . . 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 ‘𝐵))))
53		oldbdayim 28044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
54	20, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
55		bdayon 27907	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑇) ∈ On
56		bdayon 27907	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
57		bdayon 27907	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
58		naddel1 8670	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
59	55, 56, 57, 58	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
60	54, 59	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
61		oldbdayim 28044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
62	9, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
63		oldbdayim 28044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
64	13, 63	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
65		naddel12 8683	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
66	56, 57, 65	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67	62, 64, 66	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
68	60, 67	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
69		naddel12 8683	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
70	56, 57, 69	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
71	54, 64, 70	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
72		bdayon 27907	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑅) ∈ On
73		naddel1 8670	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
74	72, 56, 57, 73	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
75	62, 74	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
76	71, 75	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
77		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On)
78	55, 57, 77	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On
79		bdayon 27907	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑆) ∈ On
80		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
81	72, 79, 80	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
82	78, 81	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
83		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On)
84	55, 79, 83	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On
85		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
86	72, 57, 85	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
87	84, 86	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
88		naddcl 8659	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
89	56, 57, 88	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
90		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 ‘𝐵)))))
91	82, 87, 89, 90	mp3an 1487	. . . . . . . . . . . . . . 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 ‘𝐵))))
92		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 ‘𝐵)))))
93	78, 81, 89, 92	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
94		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 ‘𝐵)))))
95	84, 86, 89, 94	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
96	93, 95	anbi12i 639	. . . . . . . . . . . . . . 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 ‘𝐵)))))
97	91, 96	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
98	68, 76, 97	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
99		elun1 4143	. . . . . . . . . . . . 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 ‘𝐸))))))
100	98, 99	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
101	52, 100	eqeltrid 2873	. . . . . . . . . . 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 ‘𝐸))))))
102	7, 41, 41, 42, 43, 10, 2, 101	mulsproplem1 28271	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))))
103	102	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
104	34, 39, 103	mp2and 711	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
105	23, 21, 16, 11	ltsubsubs2bd 28239	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆))))
106	11, 16	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
107	21, 23	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ∈ No )
108	106, 107, 14	ltadds1d 28153	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
109	105, 108	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
110	104, 109	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
111	11, 14, 16	addsubsd 28237	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
112	21, 14, 23	addsubsd 28237	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
113	110, 111, 112	3brtr4d 5144	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)))
114	113	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)))
115		sltsleft 28015	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
116	12, 115	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴})
117		snidg 4628	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
118	12, 117	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
119	116, 19, 118	sltssepcd 27927	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
120	49	uneq1i 4126	. . . . . . . . . . . . 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 ‘𝑆)))))
121		0un 4359	. . . . . . . . . . . . 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 ‘𝑆))))
122	120, 121	eqtri 2792	. . . . . . . . . . . 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 ‘𝑆))))
123		oldbdayim 28044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
124	26, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
125		bdayon 27907	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑈) ∈ On
126		naddel2 8671	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑈) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
127	125, 57, 56, 126	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
128	124, 127	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
129	71, 128	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
130		naddel12 8683	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
131	56, 57, 130	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
132	54, 124, 131	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
133		naddel2 8671	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
134	79, 57, 56, 133	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	64, 134	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
136	132, 135	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On)
138	56, 125, 137	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On
139	84, 138	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ On
140		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On)
141	55, 125, 140	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On
142		naddcl 8659	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
143	56, 79, 142	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
144	141, 143	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆))) ∈ On
145		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 ‘𝐵)))))
146	139, 144, 89, 145	mp3an 1487	. . . . . . . . . . . . . . 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 ‘𝐵))))
147		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 ‘𝐵)))))
148	84, 138, 89, 147	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
149		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 ‘𝐵)))))
150	141, 143, 89, 149	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
151	148, 150	anbi12i 639	. . . . . . . . . . . . . . 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 ‘𝐵)))))
152	146, 151	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
153	129, 136, 152	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
154		elun1 4143	. . . . . . . . . . . . 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 ‘𝐸))))))
155	153, 154	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
156	122, 155	eqeltrid 2873	. . . . . . . . . . 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 ‘𝐸))))))
157	7, 41, 41, 42, 12, 2, 4, 156	mulsproplem1 28271	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)))))
158	157	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆))))
159	119, 158	mpand 707	. . . . . . . 8 ⊢ (𝜑 → (𝑆 <s 𝑈 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆))))
160	159	imp 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)))
161	29, 27, 23, 14	ltsubsubs3bd 28240	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
162	14, 23	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) ∈ No )
163	27, 29	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ∈ No )
164	162, 163, 21	ltadds2d 28152	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
165	161, 164	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
166	165	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
167	160, 166	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
168	21, 14, 23	addsubsassd 28236	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))))
169	168	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))))
170	21, 27, 29	addsubsassd 28236	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
171	170	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
172	167, 169, 171	3brtr4d 5144	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
173	18, 25, 31, 114, 172	ltstrd 27889	. . . 4 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
174	173	ex 417	. . 3 ⊢ (𝜑 → (𝑆 <s 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
175	36, 38, 3	sltssepcd 27927	. . . . . . 7 ⊢ (𝜑 → 𝐵 <s 𝑈)
176	49	uneq1i 4126	. . . . . . . . . . 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 ‘𝐵)))))
177		0un 4359	. . . . . . . . . . 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 ‘𝐵))))
178	176, 177	eqtri 2792	. . . . . . . . . 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 ‘𝐵))))
179		naddel12 8683	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
180	56, 57, 179	mp2an 704	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
181	62, 124, 180	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
182	60, 181	jca 520	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
183	132, 75	jca 520	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
184		naddcl 8659	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On)
185	72, 125, 184	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On
186	78, 185	onun2i 6482	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
187	141, 86	onun2i 6482	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
188		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 ‘𝐵)))))
189	186, 187, 89, 188	mp3an 1487	. . . . . . . . . . . . 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 ‘𝐵))))
190		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 ‘𝐵)))))
191	78, 185, 89, 190	mp3an 1487	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
192		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 ‘𝐵)))))
193	141, 86, 89, 192	mp3an 1487	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
194	191, 193	anbi12i 639	. . . . . . . . . . . . 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 ‘𝐵)))))
195	189, 194	bitri 278	. . . . . . . . . . . 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 ‘𝐵)))))
196	182, 183, 195	sylanbrc 594	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
197		elun1 4143	. . . . . . . . . . 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 ‘𝐸))))))
198	196, 197	syl 18	. . . . . . . . . 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 ‘𝐸))))))
199	178, 198	eqeltrid 2873	. . . . . . . . 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 ‘𝐸))))))
200	7, 41, 41, 42, 43, 10, 4, 199	mulsproplem1 28271	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))))
201	200	simprd 500	. . . . . . 7 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵))))
202	34, 175, 201	mp2and 711	. . . . . 6 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))
203	7, 9, 26	mulsproplem4 28274	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝑈) ∈ No )
204	29, 21, 203, 11	ltsubsubs2bd 28239	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈))))
205	11, 203	subscld 28218	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) ∈ No )
206	21, 29	subscld 28218	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ∈ No )
207	205, 206, 27	ltadds1d 28153	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
208	204, 207	bitrd 282	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
209	202, 208	mpbid 235	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
210	11, 27, 203	addsubsd 28237	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
211	21, 27, 29	addsubsd 28237	. . . . 5 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
212	209, 210, 211	3brtr4d 5144	. . . 4 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
213		oveq2 7416	. . . . . . 7 ⊢ (𝑆 = 𝑈 → (𝐴 ·_s 𝑆) = (𝐴 ·_s 𝑈))
214	213	oveq2d 7424	. . . . . 6 ⊢ (𝑆 = 𝑈 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)))
215		oveq2 7416	. . . . . 6 ⊢ (𝑆 = 𝑈 → (𝑅 ·_s 𝑆) = (𝑅 ·_s 𝑈))
216	214, 215	oveq12d 7426	. . . . 5 ⊢ (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
217	216	breq1d 5120	. . . 4 ⊢ (𝑆 = 𝑈 → ((((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ↔ (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
218	212, 217	syl5ibrcom 250	. . 3 ⊢ (𝜑 → (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
219	17	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
220	11, 27	addscld 28135	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
221	220, 203	subscld 28218	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
222	221	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
223	30	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
224		sltsright 28016	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
225	12, 224	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
226	225, 118, 8	sltssepcd 27927	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
227	49	uneq1i 4126	. . . . . . . . . . . . 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 ‘𝑈)))))
228		0un 4359	. . . . . . . . . . . . 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 ‘𝑈))))
229	227, 228	eqtri 2792	. . . . . . . . . . . 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 ‘𝑈))))
230	128, 67	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
231	135, 181	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
232	138, 81	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
233	143, 185	onun2i 6482	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
234		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 ‘𝐵)))))
235	232, 233, 89, 234	mp3an 1487	. . . . . . . . . . . . . . 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 ‘𝐵))))
236		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 ‘𝐵)))))
237	138, 81, 89, 236	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
238		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 ‘𝐵)))))
239	143, 185, 89, 238	mp3an 1487	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
240	237, 239	anbi12i 639	. . . . . . . . . . . . . . 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 ‘𝐵)))))
241	235, 240	bitri 278	. . . . . . . . . . . . . 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 ‘𝐵)))))
242	230, 231, 241	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
243		elun1 4143	. . . . . . . . . . . . 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 ‘𝐸))))))
244	242, 243	syl 18	. . . . . . . . . . . 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 ‘𝐸))))))
245	229, 244	eqeltrid 2873	. . . . . . . . . . 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 ‘𝐸))))))
246	7, 41, 41, 12, 43, 4, 2, 245	mulsproplem1 28271	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))))
247	246	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
248	226, 247	mpand 707	. . . . . . . 8 ⊢ (𝜑 → (𝑈 <s 𝑆 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
249	248	imp 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))
250	14, 16, 27, 203	ltsubsubsbd 28238	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
251	14, 16	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
252	27, 203	subscld 28218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ∈ No )
253	251, 252, 11	ltadds2d 28152	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
254	250, 253	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
255	254	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
256	249, 255	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
257	11, 14, 16	addsubsassd 28236	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
258	257	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
259	11, 27, 203	addsubsassd 28236	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
260	259	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
261	256, 258, 260	3brtr4d 5144	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
262	212	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
263	219, 222, 223, 261, 262	ltstrd 27889	. . . 4 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
264	263	ex 417	. . 3 ⊢ (𝜑 → (𝑈 <s 𝑆 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
265	174, 218, 264	3jaod 1454	. 2 ⊢ (𝜑 → ((𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
266	6, 265	mpd 16	1 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ∀wral 3085 ∪ cun 3911 ∅c0 4294 {csn 4591 class class class wbr 5110 Oncon0 6358 ‘cfv 6534 (class class class)co 7408 +no cnadd 8647 No csur 27766 <s clts 27767 bday cbday 27768 <<s cslts 27912 0_s c0s 27960 O cold 27978 L cleft 27980 R cright 27981 +_s cadds 28114 -_s csubs 28175 ·_s cmuls 28261

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-ot 4600 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6300 df-ord 6361 df-on 6362 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-1o 8449 df-2o 8450 df-nadd 8648 df-no 27769 df-lts 27770 df-bday 27771 df-les 27871 df-slts 27913 df-cuts 27915 df-0s 27962 df-made 27982 df-old 27983 df-left 27985 df-right 27986 df-norec 28093 df-norec2 28104 df-adds 28115 df-negs 28176 df-subs 28177

This theorem is referenced by: mulsproplem9 28279

W3C validator