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 28517

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 28277	. . 3 ⊢ (𝜑 → 𝑆 ∈ No)
3		mulsproplem7.6	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (R‘𝐵))
4	3	rightnod 28277	. . 3 ⊢ (𝜑 → 𝑈 ∈ No)
5		ltslin 28115	. . 3 ⊢ ((𝑆 ∈ No ∧ 𝑈 ∈ No) → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆))
6	2, 4, 5	syl2anc 596	. 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 28276	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (O‘(bday‘𝐴)))
10		mulsproplem7.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No)
11	7, 9, 10	mulsproplem2 28512	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No)
12		mulsproplem7.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No)
13	1	rightoldd 28276	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (O‘(bday‘𝐵)))
14	7, 12, 13	mulsproplem3 28513	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No)
15	11, 14	addscld 28375	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No)
16	7, 9, 13	mulsproplem4 28514	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No)
17	15, 16	subscld 28458	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
19		mulsproplem7.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ (L‘𝐴))
20	19	leftoldd 28274	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ (O‘(bday‘𝐴)))
21	7, 20, 10	mulsproplem2 28512	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No)
22	21, 14	addscld 28375	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No)
23	7, 20, 13	mulsproplem4 28514	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑆) ∈ No)
24	22, 23	subscld 28458	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) ∈ No)
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) ∈ No)
26	3	rightoldd 28276	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (O‘(bday‘𝐵)))
27	7, 12, 26	mulsproplem3 28513	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No)
28	21, 27	addscld 28375	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No)
29	7, 20, 26	mulsproplem4 28514	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No)
30	28, 29	subscld 28458	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
32		lltr 28257	. . . . . . . . . . 11 ⊢ (L‘𝐴) <<s (R‘𝐴)
33	32	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐴) <<s (R‘𝐴))
34	33, 19, 8	sltssepcd 28167	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝑅)
35		sltsright 28256	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s (R‘𝐵))
36	10, 35	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s (R‘𝐵))
37		snidg 4617	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
38	10, 37	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
39	36, 38, 1	sltssepcd 28167	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
40		0no 28204	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No)
42	19	leftnod 28275	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ No)
43	8	rightnod 28277	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ No)
44		bday0 28206	. . . . . . . . . . . . . . . 16 ⊢ (bday‘ 0_s ) = ∅
45	44, 44	oveq12i 7436	. . . . . . . . . . . . . . 15 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = (∅ +no ∅)
46		0elon 6421	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8700	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = ∅
50	49	uneq1i 4162	. . . . . . . . . . . . 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 4345	. . . . . . . . . . . . 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 2783	. . . . . . . . . . . 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 28284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ (O‘(bday‘𝐴)) → (bday‘𝑇) ∈ (bday‘𝐴))
54	20, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑇) ∈ (bday‘𝐴))
55		bdayon 28147	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑇) ∈ On
56		bdayon 28147	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐴) ∈ On
57		bdayon 28147	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐵) ∈ On
58		naddel1 8704	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑇) ∈ (bday‘𝐴) ↔ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
59	55, 56, 57, 58	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑇) ∈ (bday‘𝐴) ↔ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
60	54, 59	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
61		oldbdayim 28284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ (O‘(bday‘𝐴)) → (bday‘𝑅) ∈ (bday‘𝐴))
62	9, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑅) ∈ (bday‘𝐴))
63		oldbdayim 28284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (O‘(bday‘𝐵)) → (bday‘𝑆) ∈ (bday‘𝐵))
64	13, 63	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑆) ∈ (bday‘𝐵))
65		naddel12 8717	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
66	56, 57, 65	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
67	62, 64, 66	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
68	60, 67	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
69		naddel12 8717	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
70	56, 57, 69	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
71	54, 64, 70	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
72		bdayon 28147	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑅) ∈ On
73		naddel1 8704	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑅) ∈ (bday‘𝐴) ↔ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
74	72, 56, 57, 73	mp3an 1490	. . . . . . . . . . . . . . . 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 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
77		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑇) +no (bday‘𝐵)) ∈ On)
78	55, 57, 77	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝐵)) ∈ On
79		bdayon 28147	. . . . . . . . . . . . . . . . . 18 ⊢ (bday‘𝑆) ∈ On
80		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝑅) +no (bday‘𝑆)) ∈ On)
81	72, 79, 80	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑅) +no (bday‘𝑆)) ∈ On
82	78, 81	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ On
83		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝑇) +no (bday‘𝑆)) ∈ On)
84	55, 79, 83	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝑆)) ∈ On
85		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑅) +no (bday‘𝐵)) ∈ On)
86	72, 57, 85	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑅) +no (bday‘𝐵)) ∈ On
87	84, 86	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝐵))) ∈ On
88		naddcl 8693	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝐴) +no (bday‘𝐵)) ∈ On)
89	56, 57, 88	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝐴) +no (bday‘𝐵)) ∈ On
90		onunel 6473	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
94		onunel 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 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 640	. . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∪ (((bday‘𝑇) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝐵)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
99		elun1 4179	. . . . . . . . . . . . 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 2864	. . . . . . . . . . 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 28511	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)))))
103	102	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·_s 𝑆) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵))))
104	34, 39, 103	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑆) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)))
105	23, 21, 16, 11	ltsubsubs2bd 28479	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑆) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑆))))
106	11, 16	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) ∈ No)
107	21, 23	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑆)) ∈ No)
108	106, 107, 14	ltadds1d 28393	. . . . . . . . 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 28477	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
112	21, 14, 23	addsubsd 28477	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
113	110, 111, 112	3brtr4d 5136	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)))
114	113	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)))
115		sltsleft 28255	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → (L‘𝐴) <<s {𝐴})
116	12, 115	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐴) <<s {𝐴})
117		snidg 4617	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
118	12, 117	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
119	116, 19, 118	sltssepcd 28167	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
120	49	uneq1i 4162	. . . . . . . . . . . . 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 4345	. . . . . . . . . . . . 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 2783	. . . . . . . . . . . 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 28284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (O‘(bday‘𝐵)) → (bday‘𝑈) ∈ (bday‘𝐵))
124	26, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑈) ∈ (bday‘𝐵))
125		bdayon 28147	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑈) ∈ On
126		naddel2 8705	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑈) ∈ On ∧ (bday‘𝐵) ∈ On ∧ (bday‘𝐴) ∈ On) → ((bday‘𝑈) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
127	125, 57, 56, 126	mp3an 1490	. . . . . . . . . . . . . . . 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 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
130		naddel12 8717	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
131	56, 57, 130	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
132	54, 124, 131	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
133		naddel2 8705	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑆) ∈ On ∧ (bday‘𝐵) ∈ On ∧ (bday‘𝐴) ∈ On) → ((bday‘𝑆) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
134	79, 57, 56, 133	mp3an 1490	. . . . . . . . . . . . . . . 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 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
137		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝐴) +no (bday‘𝑈)) ∈ On)
138	56, 125, 137	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑈)) ∈ On
139	84, 138	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑆)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ On
140		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ On)
141	55, 125, 140	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝑈)) ∈ On
142		naddcl 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝐴) +no (bday‘𝑆)) ∈ On)
143	56, 79, 142	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑆)) ∈ On
144	141, 143	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑆))) ∈ On
145		onunel 6473	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑇) +no (bday‘𝑆)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
149		onunel 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 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 640	. . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑇) +no (bday‘𝑆)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∪ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑆)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
154		elun1 4179	. . . . . . . . . . . . 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 2864	. . . . . . . . . . 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 28511	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑆)))))
158	157	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑆))))
159	119, 158	mpand 708	. . . . . . . 8 ⊢ (𝜑 → (𝑆 <s 𝑈 → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑆))))
160	159	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑆)))
161	29, 27, 23, 14	ltsubsubs3bd 28480	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑆)) ↔ ((𝐴 ·_s 𝑆) −_s (𝑇 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
162	14, 23	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝑇 ·_s 𝑆)) ∈ No)
163	27, 29	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈)) ∈ No)
164	162, 163, 21	ltadds2d 28392	. . . . . . . . 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 486	. . . . . . 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 28476	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑇 ·_s 𝑆))))
169	168	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑇 ·_s 𝑆))))
170	21, 27, 29	addsubsassd 28476	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
171	170	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
172	167, 169, 171	3brtr4d 5136	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑇 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
173	18, 25, 31, 114, 172	ltstrd 28129	. . . 4 ⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
174	173	ex 418	. . 3 ⊢ (𝜑 → (𝑆 <s 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
175	36, 38, 3	sltssepcd 28167	. . . . . . 7 ⊢ (𝜑 → 𝐵 <s 𝑈)
176	49	uneq1i 4162	. . . . . . . . . . 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 4345	. . . . . . . . . . 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 2783	. . . . . . . . . 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 8717	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
180	56, 57, 179	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
181	62, 124, 180	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
182	60, 181	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
183	132, 75	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
184		naddcl 8693	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝑅) +no (bday‘𝑈)) ∈ On)
185	72, 125, 184	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝑅) +no (bday‘𝑈)) ∈ On
186	78, 185	onun2i 6489	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑈))) ∈ On
187	141, 86	onun2i 6489	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝑅) +no (bday‘𝐵))) ∈ On
188		onunel 6473	. . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . 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 6473	. . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . 14 ⊢ ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
192		onunel 6473	. . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . 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 640	. . . . . . . . . . . . 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 595	. . . . . . . . . . 11 ⊢ (𝜑 → ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑈))) ∪ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝑅) +no (bday‘𝐵)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
197		elun1 4179	. . . . . . . . . . 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 2864	. . . . . . . . 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 28511	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) −_s (𝑅 ·_s 𝐵)))))
201	200	simprd 501	. . . . . . 7 ⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) −_s (𝑅 ·_s 𝐵))))
202	34, 175, 201	mp2and 712	. . . . . 6 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) −_s (𝑅 ·_s 𝐵)))
203	7, 9, 26	mulsproplem4 28514	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝑈) ∈ No)
204	29, 21, 203, 11	ltsubsubs2bd 28479	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑅 ·_s 𝑈) −_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈))))
205	11, 203	subscld 28458	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑈)) ∈ No)
206	21, 29	subscld 28458	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) ∈ No)
207	205, 206, 27	ltadds1d 28393	. . . . . . 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 28477	. . . . 5 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
211	21, 27, 29	addsubsd 28477	. . . . 5 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
212	209, 210, 211	3brtr4d 5136	. . . 4 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
213		oveq2 7432	. . . . . . 7 ⊢ (𝑆 = 𝑈 → (𝐴 ·_s 𝑆) = (𝐴 ·_s 𝑈))
214	213	oveq2d 7440	. . . . . 6 ⊢ (𝑆 = 𝑈 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)))
215		oveq2 7432	. . . . . 6 ⊢ (𝑆 = 𝑈 → (𝑅 ·_s 𝑆) = (𝑅 ·_s 𝑈))
216	214, 215	oveq12d 7442	. . . . 5 ⊢ (𝑆 = 𝑈 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)))
217	216	breq1d 5112	. . . 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 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
220	11, 27	addscld 28375	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No)
221	220, 203	subscld 28458	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) ∈ No)
222	221	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) ∈ No)
223	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
224		sltsright 28256	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s (R‘𝐴))
225	12, 224	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s (R‘𝐴))
226	225, 118, 8	sltssepcd 28167	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
227	49	uneq1i 4162	. . . . . . . . . . . . 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 4345	. . . . . . . . . . . . 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 2783	. . . . . . . . . . . 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 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
231	135, 181	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
232	138, 81	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝐴) +no (bday‘𝑈)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ On
233	143, 185	onun2i 6489	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝐴) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝑈))) ∈ On
234		onunel 6473	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝐴) +no (bday‘𝑈)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
238		onunel 6473	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 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 640	. . . . . . . . . . . . . . 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 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝐴) +no (bday‘𝑈)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∪ (((bday‘𝐴) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝑈)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
243		elun1 4179	. . . . . . . . . . . . 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 2864	. . . . . . . . . . 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 28511	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑈)))))
247	246	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑈))))
248	226, 247	mpand 708	. . . . . . . 8 ⊢ (𝜑 → (𝑈 <s 𝑆 → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑈))))
249	248	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑈)))
250	14, 16, 27, 203	ltsubsubsbd 28478	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑈)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑈)) ↔ ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑈) −_s (𝑅 ·_s 𝑈))))
251	14, 16	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆)) ∈ No)
252	27, 203	subscld 28458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) −_s (𝑅 ·_s 𝑈)) ∈ No)
253	251, 252, 11	ltadds2d 28392	. . . . . . . . 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 486	. . . . . . 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 28476	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆))))
258	257	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆))))
259	11, 27, 203	addsubsassd 28476	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑅 ·_s 𝑈))))
260	259	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑅 ·_s 𝑈))))
261	256, 258, 260	3brtr4d 5136	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)))
262	212	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑅 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
263	219, 222, 223, 261, 262	ltstrd 28129	. . . 4 ⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
264	263	ex 418	. . 3 ⊢ (𝜑 → (𝑈 <s 𝑆 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
265	174, 218, 264	3jaod 1456	. 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∪ cun 4148 ∅c0 4277 {csn 4584 class class class wbr 5102 Oncon0 6365 ‘cfv 6543 (class class class)co 7424 +no cnadd 8681 Nocsur 28006 <s clts 28007 bdaycbday 28008 <<s cslts 28152 0_s c0s 28200 Ocold 28218 Lcleft 28220 Rcright 28221 +_s cadds 28354 −_s csubs 28415 ·_s cmuls 28501

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-ot 4858 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-1st 8005 df-2nd 8006 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-1o 8483 df-2o 8484 df-nadd 8682 df-no 28009 df-lts 28010 df-bday 28011 df-les 28111 df-slts 28153 df-cuts 28155 df-0s 28202 df-made 28222 df-old 28223 df-left 28225 df-right 28226 df-norec 28333 df-norec2 28344 df-adds 28355 df-negs 28416 df-subs 28417

This theorem is used by: mulsproplem9 28519

W3C validator