Theorem mulsproplem13 28514

Description: Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 28513. (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 𝑒))))))
mulsproplem.2	⊢ (𝜑 → 𝐶 ∈ No)
mulsproplem.3	⊢ (𝜑 → 𝐷 ∈ No)
mulsproplem.4	⊢ (𝜑 → 𝐸 ∈ No)
mulsproplem.5	⊢ (𝜑 → 𝐹 ∈ No)
mulsproplem.6	⊢ (𝜑 → 𝐶 <s 𝐷)
mulsproplem.7	⊢ (𝜑 → 𝐸 <s 𝐹)
mulsproplem13.1	⊢ (𝜑 → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))

Assertion

Ref	Expression
mulsproplem13	⊢ (𝜑 → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓

Allowed substitution hints:   𝜑(𝑒, 𝑓, 𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem mulsproplem13

Dummy variables 𝑔 ℎ 𝑖 𝑗 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mulsproplem.1	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 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 𝑒))))))
2	1	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → ∀𝑎 ∈ 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 𝑒))))))
3		mulsproplem.2	. . . 4 ⊢ (𝜑 → 𝐶 ∈ No)
4	3	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐶 ∈ No)
5		mulsproplem.3	. . . 4 ⊢ (𝜑 → 𝐷 ∈ No)
6	5	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐷 ∈ No)
7		mulsproplem.4	. . . 4 ⊢ (𝜑 → 𝐸 ∈ No)
8	7	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐸 ∈ No)
9		mulsproplem.5	. . . 4 ⊢ (𝜑 → 𝐹 ∈ No)
10	9	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐹 ∈ No)
11		mulsproplem.6	. . . 4 ⊢ (𝜑 → 𝐶 <s 𝐷)
12	11	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐶 <s 𝐷)
13		mulsproplem.7	. . . 4 ⊢ (𝜑 → 𝐸 <s 𝐹)
14	13	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → 𝐸 <s 𝐹)
15		simpr 490	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)))
16		mulsproplem13.1	. . . 4 ⊢ (𝜑 → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
17	16	adantr 486	. . 3 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
18	2, 4, 6, 8, 10, 12, 14, 15, 17	mulsproplem12 28513	. 2 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
19	3	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → 𝐶 ∈ No)
20	5	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → 𝐷 ∈ No)
21		simpr 490	. . . 4 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → (bday‘𝐶) = (bday‘𝐷))
22	11	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → 𝐶 <s 𝐷)
23		nodense 28049	. . . 4 ⊢ (((𝐶 ∈ No ∧ 𝐷 ∈ No) ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ 𝐶 <s 𝐷)) → ∃𝑥 ∈ No ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))
24	19, 20, 21, 22, 23	syl22anc 852	. . 3 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → ∃𝑥 ∈ No ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))
25		unidm 4104	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s )))) = (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s )))
26		unidm 4104	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) = ((bday‘ 0s ) +no (bday‘ 0s ))
27		bday0 28197	. . . . . . . . . . . . . . . . . 18 ⊢ (bday‘ 0s ) = ∅
28	27, 27	oveq12i 7432	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘ 0s ) +no (bday‘ 0s )) = (∅ +no ∅)
29		0elon 6418	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ On
30		naddrid 8693	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ +no ∅) = ∅
32	28, 31	eqtri 2784	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘ 0s ) +no (bday‘ 0s )) = ∅
33	25, 26, 32	3eqtri 2788	. . . . . . . . . . . . . . 15 ⊢ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s )))) = ∅
34	33	uneq2i 4112	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = (((bday‘𝐶) +no (bday‘𝐹)) ∪ ∅)
35		un0 4344	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ∅) = ((bday‘𝐶) +no (bday‘𝐹))
36	34, 35	eqtri 2784	. . . . . . . . . . . . 13 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = ((bday‘𝐶) +no (bday‘𝐹))
37		ssun1 4124	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))
38		ssun2 4125	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
39	37, 38	sstri 3940	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
40		ssun2 4125	. . . . . . . . . . . . . 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‘𝐸)))))
41	39, 40	sstri 3940	. . . . . . . . . . . . 13 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
42	36, 41	eqsstri 3977	. . . . . . . . . . . 12 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
43	42	sseli 3927	. . . . . . . . . . 11 ⊢ ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → (((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
44	43	imim1i 64	. . . . . . . . . 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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))) → ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
45	44	6ralimi 3137	. . . . . . . . 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 𝑒))))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
46	1, 45	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
47	46, 3, 9	mulsproplem11 28512	. . . . . . 7 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No)
48	33	uneq2i 4112	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = (((bday‘𝐶) +no (bday‘𝐸)) ∪ ∅)
49		un0 4344	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ∅) = ((bday‘𝐶) +no (bday‘𝐸))
50	48, 49	eqtri 2784	. . . . . . . . . . . . 13 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = ((bday‘𝐶) +no (bday‘𝐸))
51		ssun1 4124	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹)))
52		ssun1 4124	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
53	51, 52	sstri 3940	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
54	53, 40	sstri 3940	. . . . . . . . . . . . 13 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
55	50, 54	eqsstri 3977	. . . . . . . . . . . 12 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
56	55	sseli 3927	. . . . . . . . . . 11 ⊢ ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → (((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
57	56	imim1i 64	. . . . . . . . . 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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))) → ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
58	57	6ralimi 3137	. . . . . . . . 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 𝑒))))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
59	1, 58	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
60	59, 3, 7	mulsproplem11 28512	. . . . . . 7 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No)
61	47, 60	subscld 28449	. . . . . 6 ⊢ (𝜑 → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) ∈ No)
62	61	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) ∈ No)
63	46	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
64		simprr1 1240	. . . . . . . . 9 ⊢ (((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → (bday‘𝑥) ∈ (bday‘𝐶))
65	64	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (bday‘𝑥) ∈ (bday‘𝐶))
66		bdayon 28138	. . . . . . . . 9 ⊢ (bday‘𝐶) ∈ On
67		simprrl 793	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 ∈ No)
68		oldbday 28287	. . . . . . . . 9 ⊢ (((bday‘𝐶) ∈ On ∧ 𝑥 ∈ No) → (𝑥 ∈ (O‘(bday‘𝐶)) ↔ (bday‘𝑥) ∈ (bday‘𝐶)))
69	66, 67, 68	sylancr 599	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ∈ (O‘(bday‘𝐶)) ↔ (bday‘𝑥) ∈ (bday‘𝐶)))
70	65, 69	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 ∈ (O‘(bday‘𝐶)))
71	9	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐹 ∈ No)
72	63, 70, 71	mulsproplem2 28503	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ·s 𝐹) ∈ No)
73	59	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
74	7	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐸 ∈ No)
75	73, 70, 74	mulsproplem2 28503	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (𝑥 ·s 𝐸) ∈ No)
76	72, 75	subscld 28449	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) −s (𝑥 ·s 𝐸)) ∈ No)
77	33	uneq2i 4112	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = (((bday‘𝐷) +no (bday‘𝐹)) ∪ ∅)
78		un0 4344	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ∅) = ((bday‘𝐷) +no (bday‘𝐹))
79	77, 78	eqtri 2784	. . . . . . . . . . . . 13 ⊢ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = ((bday‘𝐷) +no (bday‘𝐹))
80		ssun2 4125	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹)))
81	80, 52	sstri 3940	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
82	81, 40	sstri 3940	. . . . . . . . . . . . 13 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
83	79, 82	eqsstri 3977	. . . . . . . . . . . 12 ⊢ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
84	83	sseli 3927	. . . . . . . . . . 11 ⊢ ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → (((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
85	84	imim1i 64	. . . . . . . . . 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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))) → ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
86	85	6ralimi 3137	. . . . . . . . 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 𝑒))))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
87	1, 86	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
88	87, 5, 9	mulsproplem11 28512	. . . . . . 7 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No)
89	33	uneq2i 4112	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = (((bday‘𝐷) +no (bday‘𝐸)) ∪ ∅)
90		un0 4344	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ∅) = ((bday‘𝐷) +no (bday‘𝐸))
91	89, 90	eqtri 2784	. . . . . . . . . . . . 13 ⊢ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) = ((bday‘𝐷) +no (bday‘𝐸))
92		ssun2 4125	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))
93	92, 38	sstri 3940	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
94	93, 40	sstri 3940	. . . . . . . . . . . . 13 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
95	91, 94	eqsstri 3977	. . . . . . . . . . . 12 ⊢ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
96	95	sseli 3927	. . . . . . . . . . 11 ⊢ ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → (((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((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	96	imim1i 64	. . . . . . . . . 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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))) → ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
98	97	6ralimi 3137	. . . . . . . . 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 𝑒))))) → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
99	1, 98	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ 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‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
100	99, 5, 7	mulsproplem11 28512	. . . . . . 7 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No)
101	88, 100	subscld 28449	. . . . . 6 ⊢ (𝜑 → ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)) ∈ No)
102	101	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)) ∈ No)
103	1	mulsproplemcbv 28501	. . . . . . . 8 ⊢ (𝜑 → ∀𝑔 ∈ 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 𝑘))))))
104	103	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ 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 𝑘))))))
105		onelss 6405	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝐶) ∈ On → ((bday‘𝑥) ∈ (bday‘𝐶) → (bday‘𝑥) ⊆ (bday‘𝐶)))
106	66, 65, 105	mpsyl 69	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (bday‘𝑥) ⊆ (bday‘𝐶))
107		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (bday‘𝐶) = (bday‘𝐷))
108	106, 107	sseqtrd 3967	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (bday‘𝑥) ⊆ (bday‘𝐷))
109		bdayon 28138	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝑥) ∈ On
110		bdayon 28138	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝐷) ∈ On
111		bdayon 28138	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝐹) ∈ On
112		naddss1 8699	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝑥) ∈ On ∧ (bday‘𝐷) ∈ On ∧ (bday‘𝐹) ∈ On) → ((bday‘𝑥) ⊆ (bday‘𝐷) ↔ ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐷) +no (bday‘𝐹))))
113	109, 110, 111, 112	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝑥) ⊆ (bday‘𝐷) ↔ ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐷) +no (bday‘𝐹)))
114	108, 113	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐷) +no (bday‘𝐹)))
115		unss2 4133	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐷) +no (bday‘𝐹)) → (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝑥) +no (bday‘𝐹))) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))))
116	114, 115	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝑥) +no (bday‘𝐹))) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))))
117		bdayon 28138	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝐸) ∈ On
118		naddss1 8699	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝑥) ∈ On ∧ (bday‘𝐷) ∈ On ∧ (bday‘𝐸) ∈ On) → ((bday‘𝑥) ⊆ (bday‘𝐷) ↔ ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐷) +no (bday‘𝐸))))
119	109, 110, 117, 118	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝑥) ⊆ (bday‘𝐷) ↔ ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐷) +no (bday‘𝐸)))
120	108, 119	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐷) +no (bday‘𝐸)))
121		unss2 4133	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐷) +no (bday‘𝐸)) → (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝑥) +no (bday‘𝐸))) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
122	120, 121	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝑥) +no (bday‘𝐸))) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
123		unss12 4134	. . . . . . . . . . . 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‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
124	116, 122, 123	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐸)))))
125		unss2 4133	. . . . . . . . . . 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‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
126	124, 125	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
127	126	sseld 3930	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝑥) +no (bday‘𝐸))))) → (((bday‘𝑔) +no (bday‘ℎ)) ∪ ((((bday‘𝑖) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑙))) ∪ (((bday‘𝑖) +no (bday‘𝑙)) ∪ ((bday‘𝑗) +no (bday‘𝑘))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
128	127	imim1d 83	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) −s (𝑗 ·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‘𝐹)) ∪ ((bday‘𝑥) +no (bday‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) −s (𝑗 ·s 𝑘)))))))
129	128	ralimd6v 3216	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (∀𝑔 ∈ 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 𝑘))))) → ∀𝑔 ∈ 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 𝑘)))))))
130	104, 129	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ 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 𝑘))))))
131	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐶 ∈ No)
132		simprr2 1241	. . . . . . 7 ⊢ (((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → 𝐶 <s 𝑥)
133	132	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐶 <s 𝑥)
134	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐸 <s 𝐹)
135	65	olcd 888	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝐶) ∈ (bday‘𝑥) ∨ (bday‘𝑥) ∈ (bday‘𝐶)))
136	16	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
137	130, 131, 67, 74, 71, 133, 134, 135, 136	mulsproplem12 28513	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝑥 ·s 𝐹) −s (𝑥 ·s 𝐸)))
138		naddss1 8699	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝑥) ∈ On ∧ (bday‘𝐶) ∈ On ∧ (bday‘𝐸) ∈ On) → ((bday‘𝑥) ⊆ (bday‘𝐶) ↔ ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐶) +no (bday‘𝐸))))
139	109, 66, 117, 138	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝑥) ⊆ (bday‘𝐶) ↔ ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐶) +no (bday‘𝐸)))
140	106, 139	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐶) +no (bday‘𝐸)))
141		unss1 4131	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑥) +no (bday‘𝐸)) ⊆ ((bday‘𝐶) +no (bday‘𝐸)) → (((bday‘𝑥) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))))
142	140, 141	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((bday‘𝑥) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))))
143		naddss1 8699	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝑥) ∈ On ∧ (bday‘𝐶) ∈ On ∧ (bday‘𝐹) ∈ On) → ((bday‘𝑥) ⊆ (bday‘𝐶) ↔ ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐶) +no (bday‘𝐹))))
144	109, 66, 111, 143	mp3an 1490	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝑥) ⊆ (bday‘𝐶) ↔ ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐶) +no (bday‘𝐹)))
145	106, 144	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐶) +no (bday‘𝐹)))
146		unss1 4131	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑥) +no (bday‘𝐹)) ⊆ ((bday‘𝐶) +no (bday‘𝐹)) → (((bday‘𝑥) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
147	145, 146	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (((bday‘𝑥) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
148		unss12 4134	. . . . . . . . . . . 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‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
149	142, 147, 148	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐸)))))
150		unss2 4133	. . . . . . . . . . 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‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
151	149, 150	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
152	151	sseld 3930	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → (((bday‘𝑔) +no (bday‘ℎ)) ∪ ((((bday‘𝑖) +no (bday‘𝑘)) ∪ ((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	152	imim1d 83	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) −s (𝑗 ·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‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) −s (𝑗 ·s 𝑘)))))))
154	153	ralimd6v 3216	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (∀𝑔 ∈ 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 𝑘))))) → ∀𝑔 ∈ 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 𝑘)))))))
155	104, 154	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ∀𝑔 ∈ 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 𝑘))))))
156	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝐷 ∈ No)
157		simprr3 1242	. . . . . . 7 ⊢ (((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → 𝑥 <s 𝐷)
158	157	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → 𝑥 <s 𝐷)
159	65, 107	eleqtrd 2863	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → (bday‘𝑥) ∈ (bday‘𝐷))
160	159	orcd 887	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((bday‘𝑥) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝑥)))
161	155, 67, 156, 74, 71, 158, 134, 160, 136	mulsproplem12 28513	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) −s (𝑥 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
162	62, 76, 102, 137, 161	ltstrd 28120	. . . 4 ⊢ ((𝜑 ∧ ((bday‘𝐶) = (bday‘𝐷) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
163	162	anassrs 473	. . 3 ⊢ (((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) ∧ (𝑥 ∈ No ∧ ((bday‘𝑥) ∈ (bday‘𝐶) ∧ 𝐶 <s 𝑥 ∧ 𝑥 <s 𝐷))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
164	24, 163	rexlimddv 3170	. 2 ⊢ ((𝜑 ∧ (bday‘𝐶) = (bday‘𝐷)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
165	66	onordi 6476	. . . . 5 ⊢ Ord (bday‘𝐶)
166	110	onordi 6476	. . . . 5 ⊢ Ord (bday‘𝐷)
167		ordtri3or 6395	. . . . 5 ⊢ ((Ord (bday‘𝐶) ∧ Ord (bday‘𝐷)) → ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)))
168	165, 166, 167	mp2an 705	. . . 4 ⊢ ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶))
169		df-3or 1104	. . . . 5 ⊢ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ↔ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷)) ∨ (bday‘𝐷) ∈ (bday‘𝐶)))
170		or32 939	. . . . 5 ⊢ ((((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷)) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ↔ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ∨ (bday‘𝐶) = (bday‘𝐷)))
171	169, 170	bitri 278	. . . 4 ⊢ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐶) = (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ↔ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ∨ (bday‘𝐶) = (bday‘𝐷)))
172	168, 171	mpbi 233	. . 3 ⊢ (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ∨ (bday‘𝐶) = (bday‘𝐷))
173	172	a1i 11	. 2 ⊢ (𝜑 → (((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)) ∨ (bday‘𝐶) = (bday‘𝐷)))
174	18, 164, 173	mpjaodan 973	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103  Ord word 6361  Oncon0 6362  ‘cfv 6538  (class class class)co 7420   +no cnadd 8674  Nocsur 27997   <s clts 27998  bdaycbday 27999   0_s c0s 28191  Ocold 28209   −_s csubs 28406   ·_s cmuls 28492

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-1o 8476  df-2o 8477  df-nadd 8675  df-no 28000  df-lts 28001  df-bday 28002  df-les 28102  df-slts 28144  df-cuts 28146  df-0s 28193  df-made 28213  df-old 28214  df-left 28216  df-right 28217  df-norec 28324  df-norec2 28335  df-adds 28346  df-negs 28407  df-subs 28408  df-muls 28493

This theorem is used by:  mulsproplem14  28515