Theorem mulsproplem1 28511

Description: Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-Mar-2025.)

Hypotheses

Ref	Expression
mulsproplem.1	⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
mulsproplem1.1	⊢ (𝜑 → 𝑋 ∈ No)
mulsproplem1.2	⊢ (𝜑 → 𝑌 ∈ No)
mulsproplem1.3	⊢ (𝜑 → 𝑍 ∈ No)
mulsproplem1.4	⊢ (𝜑 → 𝑊 ∈ No)
mulsproplem1.5	⊢ (𝜑 → 𝑇 ∈ No)
mulsproplem1.6	⊢ (𝜑 → 𝑈 ∈ No)
mulsproplem1.7	⊢ (𝜑 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑈))) ∪ (((bday‘𝑍) +no (bday‘𝑈)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))

Assertion

Ref	Expression
mulsproplem1	⊢ (𝜑 → ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇)))))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑇,𝑒,𝑓   𝑈,𝑓   𝑊,𝑑,𝑒,𝑓   𝑋,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑌,𝑏,𝑐,𝑑,𝑒,𝑓   𝑍,𝑐,𝑑,𝑒,𝑓

Allowed substitution hints:   𝜑(𝑒, 𝑓, 𝑎, 𝑏, 𝑐, 𝑑)   𝑇(𝑎, 𝑏, 𝑐, 𝑑)   𝑈(𝑒, 𝑎, 𝑏, 𝑐, 𝑑)   𝑊(𝑎, 𝑏, 𝑐)   𝑌(𝑎)   𝑍(𝑎, 𝑏)

Proof of Theorem mulsproplem1

Step	Hyp	Ref	Expression
1		mulsproplem.1	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 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		mulsproplem1.7	. 2 ⊢ (𝜑 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑈))) ∪ (((bday‘𝑍) +no (bday‘𝑈)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))))
3		mulsproplem1.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ No)
4		mulsproplem1.2	. . 3 ⊢ (𝜑 → 𝑌 ∈ No)
5		mulsproplem1.3	. . 3 ⊢ (𝜑 → 𝑍 ∈ No)
6		mulsproplem1.4	. . 3 ⊢ (𝜑 → 𝑊 ∈ No)
7		mulsproplem1.5	. . 3 ⊢ (𝜑 → 𝑇 ∈ No)
8		mulsproplem1.6	. . 3 ⊢ (𝜑 → 𝑈 ∈ No)
9		fveq2 6890	. . . . . . . 8 ⊢ (𝑎 = 𝑋 → (bday‘𝑎) = (bday‘𝑋))
10	9	oveq1d 7439	. . . . . . 7 ⊢ (𝑎 = 𝑋 → ((bday‘𝑎) +no (bday‘𝑏)) = ((bday‘𝑋) +no (bday‘𝑏)))
11	10	uneq1d 4165	. . . . . 6 ⊢ (𝑎 = 𝑋 → (((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) = (((bday‘𝑋) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))))
12	11	eleq1d 2845	. . . . 5 ⊢ (𝑎 = 𝑋 → ((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
13		oveq1 7431	. . . . . . 7 ⊢ (𝑎 = 𝑋 → (𝑎 ·s 𝑏) = (𝑋 ·s 𝑏))
14	13	eleq1d 2845	. . . . . 6 ⊢ (𝑎 = 𝑋 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑋 ·s 𝑏) ∈ No))
15	14	anbi1d 643	. . . . 5 ⊢ (𝑎 = 𝑋 → (((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)))) ↔ ((𝑋 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
16	12, 15	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝑋 → (((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((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 𝑒)))))))
17		fveq2 6890	. . . . . . . 8 ⊢ (𝑏 = 𝑌 → (bday‘𝑏) = (bday‘𝑌))
18	17	oveq2d 7440	. . . . . . 7 ⊢ (𝑏 = 𝑌 → ((bday‘𝑋) +no (bday‘𝑏)) = ((bday‘𝑋) +no (bday‘𝑌)))
19	18	uneq1d 4165	. . . . . 6 ⊢ (𝑏 = 𝑌 → (((bday‘𝑋) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) = (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))))
20	19	eleq1d 2845	. . . . 5 ⊢ (𝑏 = 𝑌 → ((((bday‘𝑋) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
21		oveq2 7432	. . . . . . 7 ⊢ (𝑏 = 𝑌 → (𝑋 ·s 𝑏) = (𝑋 ·s 𝑌))
22	21	eleq1d 2845	. . . . . 6 ⊢ (𝑏 = 𝑌 → ((𝑋 ·s 𝑏) ∈ No ↔ (𝑋 ·s 𝑌) ∈ No))
23	22	anbi1d 643	. . . . 5 ⊢ (𝑏 = 𝑌 → (((𝑋 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)))) ↔ ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
24	20, 23	imbi12d 347	. . . 4 ⊢ (𝑏 = 𝑌 → (((((bday‘𝑋) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((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 𝑒)))))))
25		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑐 = 𝑍 → (bday‘𝑐) = (bday‘𝑍))
26	25	oveq1d 7439	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → ((bday‘𝑐) +no (bday‘𝑒)) = ((bday‘𝑍) +no (bday‘𝑒)))
27	26	uneq1d 4165	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → (((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) = (((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))))
28	25	oveq1d 7439	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → ((bday‘𝑐) +no (bday‘𝑓)) = ((bday‘𝑍) +no (bday‘𝑓)))
29	28	uneq1d 4165	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))) = (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))
30	27, 29	uneq12d 4167	. . . . . . 7 ⊢ (𝑐 = 𝑍 → ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒)))) = ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒)))))
31	30	uneq2d 4166	. . . . . 6 ⊢ (𝑐 = 𝑍 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) = (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))))
32	31	eleq1d 2845	. . . . 5 ⊢ (𝑐 = 𝑍 → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
33		breq1 5105	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → (𝑐 <s 𝑑 ↔ 𝑍 <s 𝑑))
34	33	anbi1d 643	. . . . . . 7 ⊢ (𝑐 = 𝑍 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓)))
35		oveq1 7431	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (𝑐 ·s 𝑓) = (𝑍 ·s 𝑓))
36		oveq1 7431	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (𝑐 ·s 𝑒) = (𝑍 ·s 𝑒))
37	35, 36	oveq12d 7442	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) = ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)))
38	37	breq1d 5112	. . . . . . 7 ⊢ (𝑐 = 𝑍 → (((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))
39	34, 38	imbi12d 347	. . . . . 6 ⊢ (𝑐 = 𝑍 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))) ↔ ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)))))
40	39	anbi2d 642	. . . . 5 ⊢ (𝑐 = 𝑍 → (((𝑋 ·s 𝑌) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)))) ↔ ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))))))
41	32, 40	imbi12d 347	. . . 4 ⊢ (𝑐 = 𝑍 → (((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((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 𝑒)))))))
42		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑑 = 𝑊 → (bday‘𝑑) = (bday‘𝑊))
43	42	oveq1d 7439	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → ((bday‘𝑑) +no (bday‘𝑓)) = ((bday‘𝑊) +no (bday‘𝑓)))
44	43	uneq2d 4166	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → (((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) = (((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))))
45	42	oveq1d 7439	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → ((bday‘𝑑) +no (bday‘𝑒)) = ((bday‘𝑊) +no (bday‘𝑒)))
46	45	uneq2d 4166	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))) = (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))))
47	44, 46	uneq12d 4167	. . . . . . 7 ⊢ (𝑑 = 𝑊 → ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒)))) = ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒)))))
48	47	uneq2d 4166	. . . . . 6 ⊢ (𝑑 = 𝑊 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) = (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))))))
49	48	eleq1d 2845	. . . . 5 ⊢ (𝑑 = 𝑊 → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
50		breq2 5106	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → (𝑍 <s 𝑑 ↔ 𝑍 <s 𝑊))
51	50	anbi1d 643	. . . . . . 7 ⊢ (𝑑 = 𝑊 → ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓)))
52		oveq1 7431	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (𝑑 ·s 𝑓) = (𝑊 ·s 𝑓))
53		oveq1 7431	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (𝑑 ·s 𝑒) = (𝑊 ·s 𝑒))
54	52, 53	oveq12d 7442	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)) = ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒)))
55	54	breq2d 5114	. . . . . . 7 ⊢ (𝑑 = 𝑊 → (((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒))))
56	51, 55	imbi12d 347	. . . . . 6 ⊢ (𝑑 = 𝑊 → (((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒))) ↔ ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒)))))
57	56	anbi2d 642	. . . . 5 ⊢ (𝑑 = 𝑊 → (((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)))) ↔ ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒))))))
58	49, 57	imbi12d 347	. . . 4 ⊢ (𝑑 = 𝑊 → (((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((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 𝑒)))))))
59		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑒 = 𝑇 → (bday‘𝑒) = (bday‘𝑇))
60	59	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → ((bday‘𝑍) +no (bday‘𝑒)) = ((bday‘𝑍) +no (bday‘𝑇)))
61	60	uneq1d 4165	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → (((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) = (((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))))
62	59	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → ((bday‘𝑊) +no (bday‘𝑒)) = ((bday‘𝑊) +no (bday‘𝑇)))
63	62	uneq2d 4166	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))) = (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))
64	61, 63	uneq12d 4167	. . . . . . 7 ⊢ (𝑒 = 𝑇 → ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒)))) = ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇)))))
65	64	uneq2d 4166	. . . . . 6 ⊢ (𝑒 = 𝑇 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))))) = (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))))
66	65	eleq1d 2845	. . . . 5 ⊢ (𝑒 = 𝑇 → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))))
67		breq1 5105	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → (𝑒 <s 𝑓 ↔ 𝑇 <s 𝑓))
68	67	anbi2d 642	. . . . . . 7 ⊢ (𝑒 = 𝑇 → ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓)))
69		oveq2 7432	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (𝑍 ·s 𝑒) = (𝑍 ·s 𝑇))
70	69	oveq2d 7440	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) = ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)))
71		oveq2 7432	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (𝑊 ·s 𝑒) = (𝑊 ·s 𝑇))
72	71	oveq2d 7440	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒)) = ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇)))
73	70, 72	breq12d 5115	. . . . . . 7 ⊢ (𝑒 = 𝑇 → (((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇))))
74	68, 73	imbi12d 347	. . . . . 6 ⊢ (𝑒 = 𝑇 → (((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒))) ↔ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇)))))
75	74	anbi2d 642	. . . . 5 ⊢ (𝑒 = 𝑇 → (((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑒)))) ↔ ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇))))))
76	66, 75	imbi12d 347	. . . 4 ⊢ (𝑒 = 𝑇 → (((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑒)) ∪ ((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 𝑇)))))))
77		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑓 = 𝑈 → (bday‘𝑓) = (bday‘𝑈))
78	77	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → ((bday‘𝑊) +no (bday‘𝑓)) = ((bday‘𝑊) +no (bday‘𝑈)))
79	78	uneq2d 4166	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → (((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) = (((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑈))))
80	77	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → ((bday‘𝑍) +no (bday‘𝑓)) = ((bday‘𝑍) +no (bday‘𝑈)))
81	80	uneq1d 4165	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))) = (((bday‘𝑍) +no (bday‘𝑈)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))
82	79, 81	uneq12d 4167	. . . . . . 7 ⊢ (𝑓 = 𝑈 → ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇)))) = ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑈))) ∪ (((bday‘𝑍) +no (bday‘𝑈)) ∪ ((bday‘𝑊) +no (bday‘𝑇)))))
83	82	uneq2d 4166	. . . . . 6 ⊢ (𝑓 = 𝑈 → (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))) = (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑈))) ∪ (((bday‘𝑍) +no (bday‘𝑈)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))))
84	83	eleq1d 2845	. . . . 5 ⊢ (𝑓 = 𝑈 → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((bday‘𝑊) +no (bday‘𝑓))) ∪ (((bday‘𝑍) +no (bday‘𝑓)) ∪ ((bday‘𝑊) +no (bday‘𝑇))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ↔ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((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		breq2 5106	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → (𝑇 <s 𝑓 ↔ 𝑇 <s 𝑈))
86	85	anbi2d 642	. . . . . . 7 ⊢ (𝑓 = 𝑈 → ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈)))
87		oveq2 7432	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (𝑍 ·s 𝑓) = (𝑍 ·s 𝑈))
88	87	oveq1d 7439	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) = ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)))
89		oveq2 7432	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (𝑊 ·s 𝑓) = (𝑊 ·s 𝑈))
90	89	oveq1d 7439	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇)) = ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇)))
91	88, 90	breq12d 5115	. . . . . . 7 ⊢ (𝑓 = 𝑈 → (((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇)) ↔ ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇))))
92	86, 91	imbi12d 347	. . . . . 6 ⊢ (𝑓 = 𝑈 → (((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇))) ↔ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇)))))
93	92	anbi2d 642	. . . . 5 ⊢ (𝑓 = 𝑈 → (((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) −s (𝑊 ·s 𝑇)))) ↔ ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇))))))
94	84, 93	imbi12d 347	. . . 4 ⊢ (𝑓 = 𝑈 → (((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((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 𝑇)))))))
95	16, 24, 41, 58, 76, 94	rspc6v 3596	. . 3 ⊢ (((𝑋 ∈ No ∧ 𝑌 ∈ No) ∧ (𝑍 ∈ No ∧ 𝑊 ∈ No) ∧ (𝑇 ∈ No ∧ 𝑈 ∈ No)) → (∀𝑎 ∈ 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 𝑒))))) → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((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 𝑇)))))))
96	3, 4, 5, 6, 7, 8, 95	syl222anc 1413	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 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 𝑒))))) → ((((bday‘𝑋) +no (bday‘𝑌)) ∪ ((((bday‘𝑍) +no (bday‘𝑇)) ∪ ((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 𝑇)))))))
97	1, 2, 96	mp2d 50	1 ⊢ (𝜑 → ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) −s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) −s (𝑊 ·s 𝑇)))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ∪ cun 4148   class class class wbr 5102  ‘cfv 6543  (class class class)co 7424   +no cnadd 8682  Nocsur 28006   <s clts 28007  bdaycbday 28008   −_s csubs 28415   ·_s cmuls 28501

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427

This theorem is used by:  mulsproplem2  28512  mulsproplem3  28513  mulsproplem4  28514  mulsproplem5  28515  mulsproplem6  28516  mulsproplem7  28517  mulsproplem8  28518