mulsproplem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mulsproplem5		Structured version Visualization version GIF version

Theorem mulsproplem5 28563

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-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 𝑒))))))
mulsproplem5.1	⊢ (𝜑 → 𝐴 ∈ No)
mulsproplem5.2	⊢ (𝜑 → 𝐵 ∈ No)
mulsproplem5.3	⊢ (𝜑 → 𝑃 ∈ (L‘𝐴))
mulsproplem5.4	⊢ (𝜑 → 𝑄 ∈ (L‘𝐵))
mulsproplem5.5	⊢ (𝜑 → 𝑇 ∈ (L‘𝐴))
mulsproplem5.6	⊢ (𝜑 → 𝑈 ∈ (R‘𝐵))

**Assertion**
Ref	Expression
mulsproplem5	⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑃,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑄,𝑏,𝑐,𝑑,𝑒,𝑓 𝑇,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑈,𝑏,𝑐,𝑑,𝑒,𝑓 Allowed substitution hints: 𝜑(𝑒, 𝑓, 𝑎, 𝑏, 𝑐, 𝑑) 𝑄(𝑎) 𝑈(𝑎)

**Proof of Theorem mulsproplem5**
Step	Hyp	Ref	Expression
1		mulsproplem5.3	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (L‘𝐴))
2	1	leftnod 28323	. . 3 ⊢ (𝜑 → 𝑃 ∈ No)
3		mulsproplem5.5	. . . 4 ⊢ (𝜑 → 𝑇 ∈ (L‘𝐴))
4	3	leftnod 28323	. . 3 ⊢ (𝜑 → 𝑇 ∈ No)
5		ltslin 28163	. . 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	1	leftoldd 28322	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ (O‘(bday‘𝐴)))
9		mulsproplem5.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No)
10	7, 8, 9	mulsproplem2 28560	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ·_s 𝐵) ∈ No)
11		mulsproplem5.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No)
12		mulsproplem5.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (L‘𝐵))
13	12	leftoldd 28322	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (O‘(bday‘𝐵)))
14	7, 11, 13	mulsproplem3 28561	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑄) ∈ No)
15	10, 14	addscld 28423	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) ∈ No)
16	7, 8, 13	mulsproplem4 28562	. . . . . . 7 ⊢ (𝜑 → (𝑃 ·_s 𝑄) ∈ No)
17	15, 16	subscld 28506	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) ∈ No)
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) ∈ No)
19	3	leftoldd 28322	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ (O‘(bday‘𝐴)))
20	7, 19, 9	mulsproplem2 28560	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ·_s 𝐵) ∈ No)
21	20, 14	addscld 28423	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) ∈ No)
22	7, 19, 13	mulsproplem4 28562	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑄) ∈ No)
23	21, 22	subscld 28506	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) ∈ No)
24	23	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) ∈ No)
25		mulsproplem5.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (R‘𝐵))
26	25	rightoldd 28324	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (O‘(bday‘𝐵)))
27	7, 11, 26	mulsproplem3 28561	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑈) ∈ No)
28	20, 27	addscld 28423	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No)
29	7, 19, 26	mulsproplem4 28562	. . . . . . 7 ⊢ (𝜑 → (𝑇 ·_s 𝑈) ∈ No)
30	28, 29	subscld 28506	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
32		sltsleft 28303	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → (L‘𝐵) <<s {𝐵})
33	9, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐵) <<s {𝐵})
34		snidg 4622	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
35	9, 34	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
36	33, 12, 35	sltssepcd 28215	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 <s 𝐵)
37		0no 28252	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
38	37	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No)
39	12	leftnod 28323	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ No)
40		bday0 28254	. . . . . . . . . . . . . . . 16 ⊢ (bday‘ 0_s ) = ∅
41	40, 40	oveq12i 7463	. . . . . . . . . . . . . . 15 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = (∅ +no ∅)
42		0elon 6444	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
43		naddrid 8731	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
45	41, 44	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = ∅
46	45	uneq1i 4166	. . . . . . . . . . . . 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‘𝑄)))))
47		0un 4349	. . . . . . . . . . . . 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‘𝑄))))
48	46, 47	eqtri 2786	. . . . . . . . . . . 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‘𝑄))))
49		oldbdayim 28332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (O‘(bday‘𝐴)) → (bday‘𝑃) ∈ (bday‘𝐴))
50	8, 49	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑃) ∈ (bday‘𝐴))
51		oldbdayim 28332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ (O‘(bday‘𝐵)) → (bday‘𝑄) ∈ (bday‘𝐵))
52	13, 51	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑄) ∈ (bday‘𝐵))
53		bdayon 28195	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐴) ∈ On
54		bdayon 28195	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐵) ∈ On
55		naddel12 8748	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑃) ∈ (bday‘𝐴) ∧ (bday‘𝑄) ∈ (bday‘𝐵)) → ((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
56	53, 54, 55	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) ∈ (bday‘𝐴) ∧ (bday‘𝑄) ∈ (bday‘𝐵)) → ((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
57	50, 52, 56	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
58		oldbdayim 28332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ (O‘(bday‘𝐴)) → (bday‘𝑇) ∈ (bday‘𝐴))
59	19, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑇) ∈ (bday‘𝐴))
60		bdayon 28195	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑇) ∈ On
61		naddel1 8735	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑇) ∈ (bday‘𝐴) ↔ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
62	60, 53, 54, 61	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑇) ∈ (bday‘𝐴) ↔ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
63	59, 62	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
64	57, 63	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
65		bdayon 28195	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑃) ∈ On
66		naddel1 8735	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑃) ∈ On ∧ (bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑃) ∈ (bday‘𝐴) ↔ ((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
67	65, 53, 54, 66	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑃) ∈ (bday‘𝐴) ↔ ((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
68	50, 67	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
69		naddel12 8748	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑄) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
70	53, 54, 69	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑄) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
71	59, 52, 70	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
72	68, 71	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
73		bdayon 28195	. . . . . . . . . . . . . . . . . 18 ⊢ (bday‘𝑄) ∈ On
74		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑃) ∈ On ∧ (bday‘𝑄) ∈ On) → ((bday‘𝑃) +no (bday‘𝑄)) ∈ On)
75	65, 73, 74	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑃) +no (bday‘𝑄)) ∈ On
76		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑇) +no (bday‘𝐵)) ∈ On)
77	60, 54, 76	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝐵)) ∈ On
78	75, 77	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝑇) +no (bday‘𝐵))) ∈ On
79		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑃) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑃) +no (bday‘𝐵)) ∈ On)
80	65, 54, 79	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑃) +no (bday‘𝐵)) ∈ On
81		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝑄) ∈ On) → ((bday‘𝑇) +no (bday‘𝑄)) ∈ On)
82	60, 73, 81	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝑄)) ∈ On
83	80, 82	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) +no (bday‘𝐵)) ∪ ((bday‘𝑇) +no (bday‘𝑄))) ∈ On
84		naddcl 8724	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝐴) +no (bday‘𝐵)) ∈ On)
85	53, 54, 84	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝐴) +no (bday‘𝐵)) ∈ On
86		onunel 6496	. . . . . . . . . . . . . . . 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‘𝐵)))))
87	78, 83, 85, 86	mp3an 1491	. . . . . . . . . . . . . . 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‘𝐵))))
88		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
89	75, 77, 85, 88	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝑇) +no (bday‘𝐵))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
90		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
91	80, 82, 85, 90	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑃) +no (bday‘𝐵)) ∪ ((bday‘𝑇) +no (bday‘𝑄))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
92	89, 91	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‘𝐵)))))
93	87, 92	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‘𝐵)))))
94	64, 72, 93	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝑇) +no (bday‘𝐵))) ∪ (((bday‘𝑃) +no (bday‘𝐵)) ∪ ((bday‘𝑇) +no (bday‘𝑄)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
95		elun1 4183	. . . . . . . . . . . . 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‘𝐸))))))
96	94, 95	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‘𝐸))))))
97	48, 96	eqeltrid 2868	. . . . . . . . . . 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‘𝐸))))))
98	7, 38, 38, 2, 4, 39, 9, 97	mulsproplem1 28559	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑃 <s 𝑇 ∧ 𝑄 <s 𝐵) → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)))))
99	98	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 <s 𝑇 ∧ 𝑄 <s 𝐵) → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄))))
100	36, 99	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑃 <s 𝑇 → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄))))
101	100	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)))
102	10, 16	subscld 28506	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) ∈ No)
103	20, 22	subscld 28506	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) ∈ No)
104	102, 103, 14	ltadds1d 28441	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) ↔ (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄))))
105	104	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) ↔ (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄))))
106	101, 105	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
107	10, 14, 16	addsubsd 28525	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) = (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
108	107	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) = (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
109	20, 14, 22	addsubsd 28525	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
110	109	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑄)) +_s (𝐴 ·_s 𝑄)))
111	106, 108, 110	3brtr4d 5143	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)))
112		sltsleft 28303	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → (L‘𝐴) <<s {𝐴})
113	11, 112	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐴) <<s {𝐴})
114		snidg 4622	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
115	11, 114	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
116	113, 3, 115	sltssepcd 28215	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 <s 𝐴)
117		lltr 28305	. . . . . . . . . . 11 ⊢ (L‘𝐵) <<s (R‘𝐵)
118	117	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐵) <<s (R‘𝐵))
119	118, 12, 25	sltssepcd 28215	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 <s 𝑈)
120	25	rightnod 28325	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ No)
121	45	uneq1i 4166	. . . . . . . . . . . . 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‘𝑄)))))
122		0un 4349	. . . . . . . . . . . . 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‘𝑄))))
123	121, 122	eqtri 2786	. . . . . . . . . . . 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‘𝑄))))
124		oldbdayim 28332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ (O‘(bday‘𝐵)) → (bday‘𝑈) ∈ (bday‘𝐵))
125	26, 124	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑈) ∈ (bday‘𝐵))
126		bdayon 28195	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑈) ∈ On
127		naddel2 8736	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑈) ∈ On ∧ (bday‘𝐵) ∈ On ∧ (bday‘𝐴) ∈ On) → ((bday‘𝑈) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
128	126, 54, 53, 127	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑈) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
129	125, 128	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
130	71, 129	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
131		naddel12 8748	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
132	53, 54, 131	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
133	59, 125, 132	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
134		naddel2 8736	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑄) ∈ On ∧ (bday‘𝐵) ∈ On ∧ (bday‘𝐴) ∈ On) → ((bday‘𝑄) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
135	73, 54, 53, 134	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑄) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
136	52, 135	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
137	133, 136	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
138		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝐴) +no (bday‘𝑈)) ∈ On)
139	53, 126, 138	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑈)) ∈ On
140	82, 139	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ On
141		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑇) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝑇) +no (bday‘𝑈)) ∈ On)
142	60, 126, 141	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑇) +no (bday‘𝑈)) ∈ On
143		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑄) ∈ On) → ((bday‘𝐴) +no (bday‘𝑄)) ∈ On)
144	53, 73, 143	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑄)) ∈ On
145	142, 144	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄))) ∈ On
146		onunel 6496	. . . . . . . . . . . . . . . 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‘𝐵)))))
147	140, 145, 85, 146	mp3an 1491	. . . . . . . . . . . . . . 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‘𝐵))))
148		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
149	82, 139, 85, 148	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑇) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
150		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
151	142, 144, 85, 150	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
152	149, 151	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‘𝐵)))))
153	147, 152	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‘𝐵)))))
154	130, 137, 153	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑇) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∪ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
155		elun1 4183	. . . . . . . . . . . . 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‘𝐸))))))
156	154, 155	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‘𝐸))))))
157	123, 156	eqeltrid 2868	. . . . . . . . . . 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‘𝐸))))))
158	7, 38, 38, 4, 11, 39, 120, 157	mulsproplem1 28559	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)))))
159	158	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄))))
160	116, 119, 159	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)))
161	29, 27, 22, 14	ltsubsubs3bd 28528	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)) ↔ ((𝐴 ·_s 𝑄) −_s (𝑇 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
162	14, 22	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑄) −_s (𝑇 ·_s 𝑄)) ∈ No)
163	27, 29	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈)) ∈ No)
164	162, 163, 20	ltadds2d 28440	. . . . . . . . 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	160, 165	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑇 ·_s 𝑄))) <s ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
167	20, 14, 22	addsubsassd 28524	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑇 ·_s 𝑄))))
168	20, 27, 29	addsubsassd 28524	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = ((𝑇 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑇 ·_s 𝑈))))
169	166, 167, 168	3brtr4d 5143	. . . . . 6 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
170	169	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
171	18, 24, 31, 111, 170	ltstrd 28177	. . . 4 ⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
172	171	ex 418	. . 3 ⊢ (𝜑 → (𝑃 <s 𝑇 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
173		oveq1 7458	. . . . . . 7 ⊢ (𝑃 = 𝑇 → (𝑃 ·_s 𝐵) = (𝑇 ·_s 𝐵))
174	173	oveq1d 7466	. . . . . 6 ⊢ (𝑃 = 𝑇 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) = ((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)))
175		oveq1 7458	. . . . . 6 ⊢ (𝑃 = 𝑇 → (𝑃 ·_s 𝑄) = (𝑇 ·_s 𝑄))
176	174, 175	oveq12d 7469	. . . . 5 ⊢ (𝑃 = 𝑇 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) = (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)))
177	176	breq1d 5118	. . . 4 ⊢ (𝑃 = 𝑇 → ((((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ↔ (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑇 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
178	169, 177	syl5ibrcom 250	. . 3 ⊢ (𝜑 → (𝑃 = 𝑇 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
179	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) ∈ No)
180	10, 27	addscld 28423	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) ∈ No)
181	7, 8, 26	mulsproplem4 28562	. . . . . . 7 ⊢ (𝜑 → (𝑃 ·_s 𝑈) ∈ No)
182	180, 181	subscld 28506	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) ∈ No)
183	182	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) ∈ No)
184	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) ∈ No)
185	113, 1, 115	sltssepcd 28215	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 <s 𝐴)
186	45	uneq1i 4166	. . . . . . . . . . . . 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‘𝑄)))))
187		0un 4349	. . . . . . . . . . . . 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‘𝑄))))
188	186, 187	eqtri 2786	. . . . . . . . . . . 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‘𝑄))))
189	57, 129	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
190		naddel12 8748	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑃) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
191	53, 54, 190	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) ∈ (bday‘𝐴) ∧ (bday‘𝑈) ∈ (bday‘𝐵)) → ((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
192	50, 125, 191	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
193	192, 136	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
194	75, 139	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ On
195		naddcl 8724	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑃) ∈ On ∧ (bday‘𝑈) ∈ On) → ((bday‘𝑃) +no (bday‘𝑈)) ∈ On)
196	65, 126, 195	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑃) +no (bday‘𝑈)) ∈ On
197	196, 144	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑃) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄))) ∈ On
198		onunel 6496	. . . . . . . . . . . . . . . 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‘𝐵)))))
199	194, 197, 85, 198	mp3an 1491	. . . . . . . . . . . . . . 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‘𝐵))))
200		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
201	75, 139, 85, 200	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑃) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
202		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
203	196, 144, 85, 202	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑃) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝐴) +no (bday‘𝑄)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
204	201, 203	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‘𝐵)))))
205	199, 204	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‘𝐵)))))
206	189, 193, 205	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑃) +no (bday‘𝑄)) ∪ ((bday‘𝐴) +no (bday‘𝑈))) ∪ (((bday‘𝑃) +no (bday‘𝑈)) ∪ ((bday‘𝐴) +no (bday‘𝑄)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
207		elun1 4183	. . . . . . . . . . . . 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‘𝐸))))))
208	206, 207	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‘𝐸))))))
209	188, 208	eqeltrid 2868	. . . . . . . . . . 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‘𝐸))))))
210	7, 38, 38, 2, 11, 39, 120, 209	mulsproplem1 28559	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)))))
211	210	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄))))
212	185, 119, 211	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)))
213	181, 27, 16, 14	ltsubsubs3bd 28528	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)) ↔ ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈))))
214	14, 16	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄)) ∈ No)
215	27, 181	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈)) ∈ No)
216	214, 215, 10	ltadds2d 28440	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈)) ↔ ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈)))))
217	213, 216	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝑄)) <s ((𝐴 ·_s 𝑈) −_s (𝐴 ·_s 𝑄)) ↔ ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈)))))
218	212, 217	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄))) <s ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈))))
219	10, 14, 16	addsubsassd 28524	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑄) −_s (𝑃 ·_s 𝑄))))
220	10, 27, 181	addsubsassd 28524	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) = ((𝑃 ·_s 𝐵) +_s ((𝐴 ·_s 𝑈) −_s (𝑃 ·_s 𝑈))))
221	218, 219, 220	3brtr4d 5143	. . . . . 6 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)))
222	221	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)))
223		sltsright 28304	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s (R‘𝐵))
224	9, 223	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s (R‘𝐵))
225	224, 35, 25	sltssepcd 28215	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑈)
226	45	uneq1i 4166	. . . . . . . . . . . . 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‘𝐵)))))
227		0un 4349	. . . . . . . . . . . . 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‘𝐵))))
228	226, 227	eqtri 2786	. . . . . . . . . . . 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‘𝐵))))
229		onunel 6496	. . . . . . . . . . . . . . . 16 ⊢ ((((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‘𝐵)))))
230	77, 196, 85, 229	mp3an 1491	. . . . . . . . . . . . . . 15 ⊢ ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑃) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑃) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
231	63, 192, 230	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑃) +no (bday‘𝑈))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
232	133, 68	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
233	77, 196	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑃) +no (bday‘𝑈))) ∈ On
234	142, 80	onun2i 6512	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝑃) +no (bday‘𝐵))) ∈ On
235		onunel 6496	. . . . . . . . . . . . . . . 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‘𝐵)))))
236	233, 234, 85, 235	mp3an 1491	. . . . . . . . . . . . . . 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‘𝐵))))
237		onunel 6496	. . . . . . . . . . . . . . . . 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‘𝐵)))))
238	142, 80, 85, 237	mp3an 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝑃) +no (bday‘𝐵))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑇) +no (bday‘𝑈)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑃) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
239	238	anbi2i 635	. . . . . . . . . . . . . . 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‘𝐵)))))
240	236, 239	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‘𝐵)))))
241	231, 232, 240	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑇) +no (bday‘𝐵)) ∪ ((bday‘𝑃) +no (bday‘𝑈))) ∪ (((bday‘𝑇) +no (bday‘𝑈)) ∪ ((bday‘𝑃) +no (bday‘𝐵)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
242		elun1 4183	. . . . . . . . . . . . 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‘𝐸))))))
243	241, 242	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‘𝐸))))))
244	228, 243	eqeltrid 2868	. . . . . . . . . . 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‘𝐸))))))
245	7, 38, 38, 4, 2, 9, 120, 244	mulsproplem1 28559	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵)))))
246	245	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵))))
247	225, 246	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑇 <s 𝑃 → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵))))
248	247	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → ((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵)))
249	29, 20, 181, 10	ltsubsubs2bd 28527	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵)) ↔ ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈))))
250	10, 181	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) ∈ No)
251	20, 29	subscld 28506	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) ∈ No)
252	250, 251, 27	ltadds1d 28441	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) <s ((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) ↔ (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
253	249, 252	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵)) ↔ (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
254	253	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·_s 𝑈) −_s (𝑇 ·_s 𝐵)) <s ((𝑃 ·_s 𝑈) −_s (𝑃 ·_s 𝐵)) ↔ (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈))))
255	248, 254	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
256	10, 27, 181	addsubsd 28525	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) = (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
257	256	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) = (((𝑃 ·_s 𝐵) −_s (𝑃 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
258	20, 27, 29	addsubsd 28525	. . . . . . 7 ⊢ (𝜑 → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
259	258	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)) = (((𝑇 ·_s 𝐵) −_s (𝑇 ·_s 𝑈)) +_s (𝐴 ·_s 𝑈)))
260	255, 257, 259	3brtr4d 5143	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑃 ·_s 𝑈)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
261	179, 183, 184, 222, 260	ltstrd 28177	. . . 4 ⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈)))
262	261	ex 418	. . 3 ⊢ (𝜑 → (𝑇 <s 𝑃 → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
263	172, 178, 262	3jaod 1457	. 2 ⊢ (𝜑 → ((𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃) → (((𝑃 ·_s 𝐵) +_s (𝐴 ·_s 𝑄)) −_s (𝑃 ·_s 𝑄)) <s (((𝑇 ·_s 𝐵) +_s (𝐴 ·_s 𝑈)) −_s (𝑇 ·_s 𝑈))))
264	6, 263	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 1570 ∈ wcel 2147 ∀wral 3080 ∪ cun 4152 ∅c0 4281 {csn 4588 class class class wbr 5108 Oncon0 6388 ‘cfv 6566 (class class class)co 7451 +no cnadd 8712 Nocsur 28054 <s clts 28055 bdaycbday 28056 <<s cslts 28200 0_s c0s 28248 Ocold 28266 Lcleft 28268 Rcright 28269 +_s cadds 28402 −_s csubs 28463 ·_s cmuls 28549

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-ot 4864 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-1o 8514 df-2o 8515 df-nadd 8713 df-no 28057 df-lts 28058 df-bday 28059 df-les 28159 df-slts 28201 df-cuts 28203 df-0s 28250 df-made 28270 df-old 28271 df-left 28273 df-right 28274 df-norec 28381 df-norec2 28392 df-adds 28403 df-negs 28464 df-subs 28465

This theorem is used by: mulsproplem9 28567

W3C validator