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 28132

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 27892	. . 3 ⊢ (𝜑 → 𝑆 ∈ No )
3		mulsproplem7.6	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵))
4	3	rightnod 27892	. . 3 ⊢ (𝜑 → 𝑈 ∈ No )
5		ltslin 27731	. . 3 ⊢ ((𝑆 ∈ No ∧ 𝑈 ∈ No ) → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆))
6	2, 4, 5	syl2anc 590	. 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 27891	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ( O ‘( bday ‘𝐴)))
10		mulsproplem7.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No )
11	7, 9, 10	mulsproplem2 28127	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No )
12		mulsproplem7.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No )
13	1	rightoldd 27891	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ( O ‘( bday ‘𝐵)))
14	7, 12, 13	mulsproplem3 28128	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No )
15	11, 14	addscld 27990	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
16	7, 9, 13	mulsproplem4 28129	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No )
17	15, 16	subscld 28073	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
18	17	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
19		mulsproplem7.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴))
20	19	leftoldd 27889	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ( O ‘( bday ‘𝐴)))
21	7, 20, 10	mulsproplem2 28127	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No )
22	21, 14	addscld 27990	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No )
23	7, 20, 13	mulsproplem4 28129	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑆) ∈ No )
24	22, 23	subscld 28073	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
25	24	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) ∈ No )
26	3	rightoldd 27891	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ ( O ‘( bday ‘𝐵)))
27	7, 12, 26	mulsproplem3 28128	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No )
28	21, 27	addscld 27990	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
29	7, 20, 26	mulsproplem4 28129	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No )
30	28, 29	subscld 28073	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
31	30	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
32		lltr 27872	. . . . . . . . . . 11 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
33	32	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴))
34	33, 19, 8	sltssepcd 27782	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝑅)
35		sltsright 27871	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s ( R ‘𝐵))
36	10, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵))
37		snidg 4592	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
38	10, 37	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
39	36, 38, 1	sltssepcd 27782	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
40		0no 27819	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No )
42	19	leftnod 27890	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ No )
43	8	rightnod 27892	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ No )
44		bday0 27821	. . . . . . . . . . . . . . . 16 ⊢ ( bday ‘ 0_s ) = ∅
45	44, 44	oveq12i 7368	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = (∅ +no ∅)
46		0elon 6365	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8609	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2762	. . . . . . . . . . . . . 14 ⊢ (( bday ‘ 0_s ) +no ( bday ‘ 0_s )) = ∅
50	49	uneq1i 4094	. . . . . . . . . . . . 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 4324	. . . . . . . . . . . . 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 2762	. . . . . . . . . . . 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 27899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
54	20, 53	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑇) ∈ ( bday ‘𝐴))
55		bdayon 27762	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑇) ∈ On
56		bdayon 27762	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐴) ∈ On
57		bdayon 27762	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝐵) ∈ On
58		naddel1 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
59	55, 56, 57, 58	mp3an 1469	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑇) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
60	54, 59	sylib 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
61		oldbdayim 27899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
62	9, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑅) ∈ ( bday ‘𝐴))
63		oldbdayim 27899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
64	13, 63	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑆) ∈ ( bday ‘𝐵))
65		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
66	56, 57, 65	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
67	62, 64, 66	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
68	60, 67	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
69		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
70	56, 57, 69	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑆) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
71	54, 64, 70	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
72		bdayon 27762	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑅) ∈ On
73		naddel1 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
74	72, 56, 57, 73	mp3an 1469	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑅) ∈ ( bday ‘𝐴) ↔ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
75	62, 74	sylib 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
76	71, 75	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
77		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On)
78	55, 57, 77	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ On
79		bdayon 27762	. . . . . . . . . . . . . . . . . 18 ⊢ ( bday ‘𝑆) ∈ On
80		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On)
81	72, 79, 80	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ On
82	78, 81	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
83		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On)
84	55, 79, 83	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ On
85		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On)
86	72, 57, 85	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ On
87	84, 86	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
88		naddcl 8603	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
89	56, 57, 88	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
90		onunel 6417	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
94		onunel 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 634	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
99		elun1 4111	. . . . . . . . . . . . 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 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 ‘𝐸))))))
101	52, 100	eqeltrid 2843	. . . . . . . . . . 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 28126	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))))
103	102	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵))))
104	34, 39, 103	mp2and 705	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)))
105	23, 21, 16, 11	ltsubsubs2bd 28094	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆))))
106	11, 16	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) ∈ No )
107	21, 23	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ∈ No )
108	106, 107, 14	ltadds1d 28008	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
109	105, 108	bitrd 280	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
110	104, 109	mpbid 233	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
111	11, 14, 16	addsubsd 28092	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
112	21, 14, 23	addsubsd 28092	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
113	110, 111, 112	3brtr4d 5104	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)))
114	113	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)))
115		sltsleft 27870	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
116	12, 115	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴})
117		snidg 4592	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
118	12, 117	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
119	116, 19, 118	sltssepcd 27782	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
120	49	uneq1i 4094	. . . . . . . . . . . . 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 4324	. . . . . . . . . . . . 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 2762	. . . . . . . . . . . 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 27899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
124	26, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( bday ‘𝑈) ∈ ( bday ‘𝐵))
125		bdayon 27762	. . . . . . . . . . . . . . . . 17 ⊢ ( bday ‘𝑈) ∈ On
126		naddel2 8614	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑈) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
127	125, 57, 56, 126	mp3an 1469	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑈) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
128	124, 127	sylib 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
129	71, 128	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
130		naddel12 8626	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
131	56, 57, 130	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
132	54, 124, 131	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
133		naddel2 8614	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑆) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ ( bday ‘𝐴) ∈ On) → (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
134	79, 57, 56, 133	mp3an 1469	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑆) ∈ ( bday ‘𝐵) ↔ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
135	64, 134	sylib 219	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
136	132, 135	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
137		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On)
138	56, 125, 137	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ On
139	84, 138	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ On
140		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑇) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On)
141	55, 125, 140	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ On
142		naddcl 8603	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝑆) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On)
143	56, 79, 142	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ On
144	141, 143	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆))) ∈ On
145		onunel 6417	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
149		onunel 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 634	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝐴) +no ( bday ‘𝑆)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
154		elun1 4111	. . . . . . . . . . . . 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 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 ‘𝐸))))))
156	122, 155	eqeltrid 2843	. . . . . . . . . . 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 28126	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)))))
158	157	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆))))
159	119, 158	mpand 701	. . . . . . . 8 ⊢ (𝜑 → (𝑆 <s 𝑈 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆))))
160	159	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)))
161	29, 27, 23, 14	ltsubsubs3bd 28095	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
162	14, 23	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) ∈ No )
163	27, 29	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ∈ No )
164	162, 163, 21	ltadds2d 28007	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
165	161, 164	bitrd 280	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
166	165	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝐴 ·_s 𝑆)) ↔ ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈)))))
167	160, 166	mpbid 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
168	21, 14, 23	addsubsassd 28091	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))))
169	168	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑇 ·_s 𝑆))))
170	21, 27, 29	addsubsassd 28091	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
171	170	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑇 ·_s 𝑈))))
172	167, 169, 171	3brtr4d 5104	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑇 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
173	18, 25, 31, 114, 172	ltstrd 27745	. . . 4 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
174	173	ex 413	. . 3 ⊢ (𝜑 → (𝑆 <s 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
175	36, 38, 3	sltssepcd 27782	. . . . . . 7 ⊢ (𝜑 → 𝐵 <s 𝑈)
176	49	uneq1i 4094	. . . . . . . . . . 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 4324	. . . . . . . . . . 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 2762	. . . . . . . . . 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 8626	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
180	56, 57, 179	mp2an 698	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑅) ∈ ( bday ‘𝐴) ∧ ( bday ‘𝑈) ∈ ( bday ‘𝐵)) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
181	62, 124, 180	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
182	60, 181	jca 516	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
183	132, 75	jca 516	. . . . . . . . . . . 12 ⊢ (𝜑 → ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
184		naddcl 8603	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑅) ∈ On ∧ ( bday ‘𝑈) ∈ On) → (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On)
185	72, 125, 184	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ On
186	78, 185	onun2i 6433	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
187	141, 86	onun2i 6433	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵))) ∈ On
188		onunel 6417	. . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . 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 6417	. . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . 14 ⊢ (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
192		onunel 6417	. . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . 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 634	. . . . . . . . . . . . 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 276	. . . . . . . . . . . 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 589	. . . . . . . . . . 11 ⊢ (𝜑 → (((( bday ‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday ‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
197		elun1 4111	. . . . . . . . . . 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 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 ‘𝐸))))))
199	178, 198	eqeltrid 2843	. . . . . . . . 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 28126	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))))
201	200	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵))))
202	34, 175, 201	mp2and 705	. . . . . 6 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)))
203	7, 9, 26	mulsproplem4 28129	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝑈) ∈ No )
204	29, 21, 203, 11	ltsubsubs2bd 28094	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈))))
205	11, 203	subscld 28073	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) ∈ No )
206	21, 29	subscld 28073	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ∈ No )
207	205, 206, 27	ltadds1d 28008	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
208	204, 207	bitrd 280	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) -_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) -_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
209	202, 208	mpbid 233	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
210	11, 27, 203	addsubsd 28092	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = (((𝑅 ·_s 𝐵) -_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
211	21, 27, 29	addsubsd 28092	. . . . 5 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) -_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
212	209, 210, 211	3brtr4d 5104	. . . 4 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
213		oveq2 7364	. . . . . . 7 ⊢ (𝑆 = 𝑈 → (𝐴 ·_s 𝑆) = (𝐴 ·_s 𝑈))
214	213	oveq2d 7372	. . . . . 6 ⊢ (𝑆 = 𝑈 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)))
215		oveq2 7364	. . . . . 6 ⊢ (𝑆 = 𝑈 → (𝑅 ·_s 𝑆) = (𝑅 ·_s 𝑈))
216	214, 215	oveq12d 7374	. . . . 5 ⊢ (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
217	216	breq1d 5082	. . . 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 248	. . 3 ⊢ (𝜑 → (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
219	17	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) ∈ No )
220	11, 27	addscld 27990	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No )
221	220, 203	subscld 28073	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
222	221	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) ∈ No )
223	30	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)) ∈ No )
224		sltsright 27871	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
225	12, 224	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴))
226	225, 118, 8	sltssepcd 27782	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
227	49	uneq1i 4094	. . . . . . . . . . . . 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 4324	. . . . . . . . . . . . 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 2762	. . . . . . . . . . . 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 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
231	135, 181	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
232	138, 81	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ On
233	143, 185	onun2i 6433	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈))) ∈ On
234		onunel 6417	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ↔ ((( bday ‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday ‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵))))
238		onunel 6417	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 634	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((( bday ‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday ‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday ‘𝑅) +no ( bday ‘𝑈)))) ∈ (( bday ‘𝐴) +no ( bday ‘𝐵)))
243		elun1 4111	. . . . . . . . . . . . 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 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 ‘𝐸))))))
245	229, 244	eqeltrid 2843	. . . . . . . . . . 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 28126	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))))
247	246	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
248	226, 247	mpand 701	. . . . . . . 8 ⊢ (𝜑 → (𝑈 <s 𝑆 → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈))))
249	248	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)))
250	14, 16, 27, 203	ltsubsubsbd 28093	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
251	14, 16	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) ∈ No )
252	27, 203	subscld 28073	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ∈ No )
253	251, 252, 11	ltadds2d 28007	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
254	250, 253	bitrd 280	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
255	254	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝐴 ·_s 𝑆) -_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) -_s (𝑅 ·_s 𝑈)) ↔ ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈)))))
256	249, 255	mpbid 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))) <s ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
257	11, 14, 16	addsubsassd 28091	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
258	257	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) -_s (𝑅 ·_s 𝑆))))
259	11, 27, 203	addsubsassd 28091	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
260	259	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) -_s (𝑅 ·_s 𝑈))))
261	256, 258, 260	3brtr4d 5104	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)))
262	212	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
263	219, 222, 223, 261, 262	ltstrd 27745	. . . 4 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))
264	263	ex 413	. . 3 ⊢ (𝜑 → (𝑈 <s 𝑆 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
265	174, 218, 264	3jaod 1437	. 2 ⊢ (𝜑 → ((𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈))))
266	6, 265	mpd 15	1 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) -_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) -_s (𝑇 ·_s 𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ w3o 1091 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ∪ cun 3881 ∅c0 4261 {csn 4555 class class class wbr 5072 Oncon0 6310 ‘cfv 6485 (class class class)co 7356 +no cnadd 8591 No csur 27621 <s clts 27622 bday cbday 27623 <<s cslts 27767 0_s c0s 27815 O cold 27833 L cleft 27835 R cright 27836 +_s cadds 27969 -_s csubs 28030 ·_s cmuls 28116

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-ot 4564 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-1o 8395 df-2o 8396 df-nadd 8592 df-no 27624 df-lts 27625 df-bday 27626 df-les 27727 df-slts 27768 df-cuts 27770 df-0s 27817 df-made 27837 df-old 27838 df-left 27840 df-right 27841 df-norec 27948 df-norec2 27959 df-adds 27970 df-negs 28031 df-subs 28032

This theorem is referenced by: mulsproplem9 28134

W3C validator