mulsproplem8 - Metamath Proof Explorer

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

Theorem mulsproplem8 28521

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 𝑒))))))
mulsproplem8.1	⊢ (𝜑 → 𝐴 ∈ No)
mulsproplem8.2	⊢ (𝜑 → 𝐵 ∈ No)
mulsproplem8.3	⊢ (𝜑 → 𝑅 ∈ (R‘𝐴))
mulsproplem8.4	⊢ (𝜑 → 𝑆 ∈ (R‘𝐵))
mulsproplem8.5	⊢ (𝜑 → 𝑉 ∈ (R‘𝐴))
mulsproplem8.6	⊢ (𝜑 → 𝑊 ∈ (L‘𝐵))

**Assertion**
Ref	Expression
mulsproplem8	⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑅,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑆,𝑏,𝑐,𝑑,𝑒,𝑓 𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑊,𝑏,𝑐,𝑑,𝑒,𝑓 Allowed substitution hints: 𝜑(𝑒, 𝑓, 𝑎, 𝑏, 𝑐, 𝑑) 𝑆(𝑎) 𝑊(𝑎)

**Proof of Theorem mulsproplem8**
Step	Hyp	Ref	Expression
1		mulsproplem8.3	. . . 4 ⊢ (𝜑 → 𝑅 ∈ (R‘𝐴))
2	1	rightnod 28280	. . 3 ⊢ (𝜑 → 𝑅 ∈ No)
3		mulsproplem8.5	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (R‘𝐴))
4	3	rightnod 28280	. . 3 ⊢ (𝜑 → 𝑉 ∈ No)
5		ltslin 28118	. . 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	rightoldd 28279	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (O‘(bday‘𝐴)))
9		mulsproplem8.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ No)
10	7, 8, 9	mulsproplem2 28515	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ·_s 𝐵) ∈ No)
11		mulsproplem8.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ No)
12		mulsproplem8.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (R‘𝐵))
13	12	rightoldd 28279	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (O‘(bday‘𝐵)))
14	7, 11, 13	mulsproplem3 28516	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑆) ∈ No)
15	10, 14	addscld 28378	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No)
16	7, 8, 13	mulsproplem4 28517	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑆) ∈ No)
17	15, 16	subscld 28461	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
19		mulsproplem8.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ (L‘𝐵))
20	19	leftoldd 28277	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (O‘(bday‘𝐵)))
21	7, 11, 20	mulsproplem3 28516	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ·_s 𝑊) ∈ No)
22	10, 21	addscld 28378	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No)
23	7, 8, 20	mulsproplem4 28517	. . . . . . 7 ⊢ (𝜑 → (𝑅 ·_s 𝑊) ∈ No)
24	22, 23	subscld 28461	. . . . . 6 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) ∈ No)
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) ∈ No)
26	3	rightoldd 28279	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (O‘(bday‘𝐴)))
27	7, 26, 9	mulsproplem2 28515	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝐵) ∈ No)
28	27, 21	addscld 28378	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) ∈ No)
29	7, 26, 20	mulsproplem4 28517	. . . . . . 7 ⊢ (𝜑 → (𝑉 ·_s 𝑊) ∈ No)
30	28, 29	subscld 28461	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)) ∈ No)
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)) ∈ No)
32		sltsright 28259	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → {𝐴} <<s (R‘𝐴))
33	11, 32	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} <<s (R‘𝐴))
34		snidg 4620	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → 𝐴 ∈ {𝐴})
35	11, 34	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ {𝐴})
36	33, 35, 1	sltssepcd 28170	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 <s 𝑅)
37		lltr 28260	. . . . . . . . . . 11 ⊢ (L‘𝐵) <<s (R‘𝐵)
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐵) <<s (R‘𝐵))
39	38, 19, 12	sltssepcd 28170	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝑆)
40		0no 28207	. . . . . . . . . . . 12 ⊢ 0_s ∈ No
41	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0_s ∈ No)
42	19	leftnod 28278	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ No)
43	12	rightnod 28280	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ No)
44		bday0 28209	. . . . . . . . . . . . . . . 16 ⊢ (bday‘ 0_s ) = ∅
45	44, 44	oveq12i 7439	. . . . . . . . . . . . . . 15 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = (∅ +no ∅)
46		0elon 6424	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ On
47		naddrid 8704	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (∅ +no ∅) = ∅
49	45, 48	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ ((bday‘ 0_s ) +no (bday‘ 0_s )) = ∅
50	49	uneq1i 4165	. . . . . . . . . . . . 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 4348	. . . . . . . . . . . . 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 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‘𝑊))))
53		oldbdayim 28287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ (O‘(bday‘𝐵)) → (bday‘𝑊) ∈ (bday‘𝐵))
54	20, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑊) ∈ (bday‘𝐵))
55		bdayon 28150	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑊) ∈ On
56		bdayon 28150	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐵) ∈ On
57		bdayon 28150	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝐴) ∈ On
58		naddel2 8709	. . . . . . . . . . . . . . . . 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 28287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ (O‘(bday‘𝐴)) → (bday‘𝑅) ∈ (bday‘𝐴))
62	8, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑅) ∈ (bday‘𝐴))
63		oldbdayim 28287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ (O‘(bday‘𝐵)) → (bday‘𝑆) ∈ (bday‘𝐵))
64	13, 63	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑆) ∈ (bday‘𝐵))
65		naddel12 8721	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
66	57, 56, 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		bdayon 28150	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑆) ∈ On
70		naddel2 8709	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑆) ∈ On ∧ (bday‘𝐵) ∈ On ∧ (bday‘𝐴) ∈ On) → ((bday‘𝑆) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
71	69, 56, 57, 70	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑆) ∈ (bday‘𝐵) ↔ ((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
72	64, 71	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
73		naddel12 8721	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑊) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
74	57, 56, 73	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑅) ∈ (bday‘𝐴) ∧ (bday‘𝑊) ∈ (bday‘𝐵)) → ((bday‘𝑅) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
75	62, 54, 74	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑅) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
76	72, 75	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
77		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑊) ∈ On) → ((bday‘𝐴) +no (bday‘𝑊)) ∈ On)
78	57, 55, 77	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑊)) ∈ On
79		bdayon 28150	. . . . . . . . . . . . . . . . . 18 ⊢ (bday‘𝑅) ∈ On
80		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝑅) +no (bday‘𝑆)) ∈ On)
81	79, 69, 80	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑅) +no (bday‘𝑆)) ∈ On
82	78, 81	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝐴) +no (bday‘𝑊)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ On
83		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝐴) +no (bday‘𝑆)) ∈ On)
84	57, 69, 83	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐴) +no (bday‘𝑆)) ∈ On
85		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝑊) ∈ On) → ((bday‘𝑅) +no (bday‘𝑊)) ∈ On)
86	79, 55, 85	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑅) +no (bday‘𝑊)) ∈ On
87	84, 86	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝐴) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝑊))) ∈ On
88		naddcl 8697	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝐴) +no (bday‘𝐵)) ∈ On)
89	57, 56, 88	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝐴) +no (bday‘𝐵)) ∈ On
90		onunel 6476	. . . . . . . . . . . . . . . 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 6476	. . . . . . . . . . . . . . . . 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 6476	. . . . . . . . . . . . . . . . 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 4182	. . . . . . . . . . . . 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 2867	. . . . . . . . . . 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, 11, 2, 42, 43, 101	mulsproplem1 28514	. . . . . . . . . 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	36, 39, 103	mp2and 712	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑊)))
105	14, 16, 21, 23	ltsubsubsbd 28481	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) −_s (𝑅 ·_s 𝑊))))
106	14, 16	subscld 28461	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆)) ∈ No)
107	21, 23	subscld 28461	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) −_s (𝑅 ·_s 𝑊)) ∈ No)
108	106, 107, 10	ltadds2d 28395	. . . . . . . . 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	10, 14, 16	addsubsassd 28479	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑅 ·_s 𝑆))))
112	10, 21, 23	addsubsassd 28479	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) = ((𝑅 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) −_s (𝑅 ·_s 𝑊))))
113	110, 111, 112	3brtr4d 5139	. . . . . 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 28258	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → (L‘𝐵) <<s {𝐵})
116	9, 115	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (L‘𝐵) <<s {𝐵})
117		snidg 4620	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → 𝐵 ∈ {𝐵})
118	9, 117	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
119	116, 19, 118	sltssepcd 28170	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 <s 𝐵)
120	49	uneq1i 4165	. . . . . . . . . . . . 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 4348	. . . . . . . . . . . . 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 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‘𝑊))))
123		oldbdayim 28287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ (O‘(bday‘𝐴)) → (bday‘𝑉) ∈ (bday‘𝐴))
124	26, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (bday‘𝑉) ∈ (bday‘𝐴))
125		bdayon 28150	. . . . . . . . . . . . . . . . 17 ⊢ (bday‘𝑉) ∈ On
126		naddel1 8708	. . . . . . . . . . . . . . . . 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	75, 128	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑅) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑉) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
130		naddel1 8708	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑅) ∈ (bday‘𝐴) ↔ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
131	79, 57, 56, 130	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑅) ∈ (bday‘𝐴) ↔ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
132	62, 131	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
133		naddel12 8721	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑉) ∈ (bday‘𝐴) ∧ (bday‘𝑊) ∈ (bday‘𝐵)) → ((bday‘𝑉) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
134	57, 56, 133	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑉) ∈ (bday‘𝐴) ∧ (bday‘𝑊) ∈ (bday‘𝐵)) → ((bday‘𝑉) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
135	124, 54, 134	syl2anc 596	. . . . . . . . . . . . . . 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 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑉) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑉) +no (bday‘𝐵)) ∈ On)
138	125, 56, 137	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑉) +no (bday‘𝐵)) ∈ On
139	86, 138	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑅) +no (bday‘𝑊)) ∪ ((bday‘𝑉) +no (bday‘𝐵))) ∈ On
140		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑅) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝑅) +no (bday‘𝐵)) ∈ On)
141	79, 56, 140	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑅) +no (bday‘𝐵)) ∈ On
142		naddcl 8697	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑉) ∈ On ∧ (bday‘𝑊) ∈ On) → ((bday‘𝑉) +no (bday‘𝑊)) ∈ On)
143	125, 55, 142	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑉) +no (bday‘𝑊)) ∈ On
144	141, 143	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑅) +no (bday‘𝐵)) ∪ ((bday‘𝑉) +no (bday‘𝑊))) ∈ On
145		onunel 6476	. . . . . . . . . . . . . . . 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 6476	. . . . . . . . . . . . . . . . 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	86, 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 6476	. . . . . . . . . . . . . . . . 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 4182	. . . . . . . . . . . . 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 2867	. . . . . . . . . . 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, 2, 4, 42, 9, 156	mulsproplem1 28514	. . . . . . . . . 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	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑅 <s 𝑉 → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊))))
160	159	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)))
161	10, 23	subscld 28461	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) ∈ No)
162	27, 29	subscld 28461	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) ∈ No)
163	161, 162, 21	ltadds1d 28396	. . . . . . . 8 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
164	163	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) ↔ (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊))))
165	160, 164	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
166	10, 21, 23	addsubsd 28480	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
167	166	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑊)) +_s (𝐴 ·_s 𝑊)))
168	27, 21, 29	addsubsd 28480	. . . . . . 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	165, 167, 169	3brtr4d 5139	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 <s 𝑉) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑅 ·_s 𝑊)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)))
171	18, 25, 31, 114, 170	ltstrd 28132	. . . 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	33, 35, 3	sltssepcd 28170	. . . . . . 7 ⊢ (𝜑 → 𝐴 <s 𝑉)
174	49	uneq1i 4165	. . . . . . . . . . 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‘𝑊)))))
175		0un 4348	. . . . . . . . . . 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‘𝑊))))
176	174, 175	eqtri 2786	. . . . . . . . . 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‘𝑊))))
177		naddel12 8721	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → (((bday‘𝑉) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
178	57, 56, 177	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑉) ∈ (bday‘𝐴) ∧ (bday‘𝑆) ∈ (bday‘𝐵)) → ((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
179	124, 64, 178	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
180	60, 179	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (((bday‘𝐴) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
181	72, 135	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (((bday‘𝐴) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑉) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
182		naddcl 8697	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑉) ∈ On ∧ (bday‘𝑆) ∈ On) → ((bday‘𝑉) +no (bday‘𝑆)) ∈ On)
183	125, 69, 182	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝑉) +no (bday‘𝑆)) ∈ On
184	78, 183	onun2i 6492	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐴) +no (bday‘𝑊)) ∪ ((bday‘𝑉) +no (bday‘𝑆))) ∈ On
185	84, 143	onun2i 6492	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐴) +no (bday‘𝑆)) ∪ ((bday‘𝑉) +no (bday‘𝑊))) ∈ On
186		onunel 6476	. . . . . . . . . . . . . 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‘𝐵)))))
187	184, 185, 89, 186	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‘𝐵))))
188		onunel 6476	. . . . . . . . . . . . . . 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‘𝐵)))))
189	78, 183, 89, 188	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((((bday‘𝐴) +no (bday‘𝑊)) ∪ ((bday‘𝑉) +no (bday‘𝑆))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝐴) +no (bday‘𝑊)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
190		onunel 6476	. . . . . . . . . . . . . . 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	84, 143, 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	189, 191	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‘𝐵)))))
193	187, 192	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‘𝐵)))))
194	180, 181, 193	sylanbrc 595	. . . . . . . . . . 11 ⊢ (𝜑 → ((((bday‘𝐴) +no (bday‘𝑊)) ∪ ((bday‘𝑉) +no (bday‘𝑆))) ∪ (((bday‘𝐴) +no (bday‘𝑆)) ∪ ((bday‘𝑉) +no (bday‘𝑊)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
195		elun1 4182	. . . . . . . . . . 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‘𝐸))))))
196	194, 195	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‘𝐸))))))
197	176, 196	eqeltrid 2867	. . . . . . . . 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‘𝐸))))))
198	7, 41, 41, 11, 4, 42, 43, 197	mulsproplem1 28514	. . . . . . . 8 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝑊)))))
199	198	simprd 501	. . . . . . 7 ⊢ (𝜑 → ((𝐴 <s 𝑉 ∧ 𝑊 <s 𝑆) → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝑊))))
200	173, 39, 199	mp2and 712	. . . . . 6 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝑊)))
201	7, 26, 13	mulsproplem4 28517	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ·_s 𝑆) ∈ No)
202	14, 201, 21, 29	ltsubsubsbd 28481	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝑊)) ↔ ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊))))
203	14, 201	subscld 28461	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆)) ∈ No)
204	21, 29	subscld 28461	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊)) ∈ No)
205	203, 204, 27	ltadds2d 28395	. . . . . . 7 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆)) <s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊)))))
206	202, 205	bitrd 282	. . . . . 6 ⊢ (𝜑 → (((𝐴 ·_s 𝑆) −_s (𝐴 ·_s 𝑊)) <s ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝑊)) ↔ ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊)))))
207	200, 206	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆))) <s ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊))))
208	27, 14, 201	addsubsassd 28479	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑆) −_s (𝑉 ·_s 𝑆))))
209	27, 21, 29	addsubsassd 28479	. . . . 5 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)) = ((𝑉 ·_s 𝐵) +_s ((𝐴 ·_s 𝑊) −_s (𝑉 ·_s 𝑊))))
210	207, 208, 209	3brtr4d 5139	. . . 4 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)))
211		oveq1 7434	. . . . . . 7 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝐵) = (𝑉 ·_s 𝐵))
212	211	oveq1d 7442	. . . . . 6 ⊢ (𝑅 = 𝑉 → ((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) = ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)))
213		oveq1 7434	. . . . . 6 ⊢ (𝑅 = 𝑉 → (𝑅 ·_s 𝑆) = (𝑉 ·_s 𝑆))
214	212, 213	oveq12d 7445	. . . . 5 ⊢ (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)))
215	214	breq1d 5115	. . . 4 ⊢ (𝑅 = 𝑉 → ((((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)) ↔ (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊))))
216	210, 215	syl5ibrcom 250	. . 3 ⊢ (𝜑 → (𝑅 = 𝑉 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊))))
217	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) ∈ No)
218	27, 14	addscld 28378	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) ∈ No)
219	218, 201	subscld 28461	. . . . . 6 ⊢ (𝜑 → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) ∈ No)
220	219	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) ∈ No)
221	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)) ∈ No)
222		sltsright 28259	. . . . . . . . . . 11 ⊢ (𝐵 ∈ No → {𝐵} <<s (R‘𝐵))
223	9, 222	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → {𝐵} <<s (R‘𝐵))
224	223, 118, 12	sltssepcd 28170	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 <s 𝑆)
225	49	uneq1i 4165	. . . . . . . . . . . . 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‘𝐵)))))
226		0un 4348	. . . . . . . . . . . . 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‘𝐵))))
227	225, 226	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‘𝐵))))
228	128, 67	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑉) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
229	179, 132	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((bday‘𝑉) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
230	138, 81	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑉) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ On
231	183, 141	onun2i 6492	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑉) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝐵))) ∈ On
232		onunel 6476	. . . . . . . . . . . . . . . 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‘𝐵)))))
233	230, 231, 89, 232	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‘𝐵))))
234		onunel 6476	. . . . . . . . . . . . . . . . 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‘𝐵)))))
235	138, 81, 89, 234	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘𝑉) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ↔ (((bday‘𝑉) +no (bday‘𝐵)) ∈ ((bday‘𝐴) +no (bday‘𝐵)) ∧ ((bday‘𝑅) +no (bday‘𝑆)) ∈ ((bday‘𝐴) +no (bday‘𝐵))))
236		onunel 6476	. . . . . . . . . . . . . . . . 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	183, 141, 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	235, 237	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‘𝐵)))))
239	233, 238	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‘𝐵)))))
240	228, 229, 239	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((bday‘𝑉) +no (bday‘𝐵)) ∪ ((bday‘𝑅) +no (bday‘𝑆))) ∪ (((bday‘𝑉) +no (bday‘𝑆)) ∪ ((bday‘𝑅) +no (bday‘𝐵)))) ∈ ((bday‘𝐴) +no (bday‘𝐵)))
241		elun1 4182	. . . . . . . . . . . . 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‘𝐸))))))
242	240, 241	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‘𝐸))))))
243	227, 242	eqeltrid 2867	. . . . . . . . . . 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‘𝐸))))))
244	7, 41, 41, 4, 2, 9, 43, 243	mulsproplem1 28514	. . . . . . . . . 10 ⊢ (𝜑 → (( 0_s ·_s 0_s ) ∈ No ∧ ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)))))
245	244	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵))))
246	224, 245	mpan2d 707	. . . . . . . 8 ⊢ (𝜑 → (𝑉 <s 𝑅 → ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵))))
247	246	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → ((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)))
248	201, 27, 16, 10	ltsubsubs2bd 28482	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)) ↔ ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆))))
249	10, 16	subscld 28461	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) ∈ No)
250	27, 201	subscld 28461	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) ∈ No)
251	249, 250, 14	ltadds1d 28396	. . . . . . . . 9 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) <s ((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) ↔ (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
252	248, 251	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → (((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
253	252	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝑆) −_s (𝑉 ·_s 𝐵)) <s ((𝑅 ·_s 𝑆) −_s (𝑅 ·_s 𝐵)) ↔ (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆))))
254	247, 253	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) −_s (𝑉 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
255	10, 14, 16	addsubsd 28480	. . . . . . 7 ⊢ (𝜑 → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
256	255	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) = (((𝑅 ·_s 𝐵) −_s (𝑅 ·_s 𝑆)) +_s (𝐴 ·_s 𝑆)))
257	27, 14, 201	addsubsd 28480	. . . . . . 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	254, 256, 258	3brtr4d 5139	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑅 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑅 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)))
260	210	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 <s 𝑅) → (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑆)) −_s (𝑉 ·_s 𝑆)) <s (((𝑉 ·_s 𝐵) +_s (𝐴 ·_s 𝑊)) −_s (𝑉 ·_s 𝑊)))
261	217, 220, 221, 259, 260	ltstrd 28132	. . . 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, 216, 262	3jaod 1456	. 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 1569 ∈ wcel 2146 ∀wral 3079 ∪ cun 4151 ∅c0 4280 {csn 4587 class class class wbr 5105 Oncon0 6368 ‘cfv 6546 (class class class)co 7427 +no cnadd 8685 Nocsur 28009 <s clts 28010 bdaycbday 28011 <<s cslts 28155 0_s c0s 28203 Ocold 28221 Lcleft 28223 Rcright 28224 +_s cadds 28357 −_s csubs 28418 ·_s cmuls 28504

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 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758

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 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4838 df-ot 4861 df-uni 4870 df-int 4910 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-se 5608 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-1st 8008 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-1o 8487 df-2o 8488 df-nadd 8686 df-no 28012 df-lts 28013 df-bday 28014 df-les 28114 df-slts 28156 df-cuts 28158 df-0s 28205 df-made 28225 df-old 28226 df-left 28228 df-right 28229 df-norec 28336 df-norec2 28347 df-adds 28358 df-negs 28419 df-subs 28420

This theorem is used by: mulsproplem9 28522

W3C validator