Theorem mulsproplem1 27811

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 7426	. . . . . . 7 ⊢ (𝑎 = 𝑋 → (( bday ‘𝑎) +no ( bday ‘𝑏)) = (( bday ‘𝑋) +no ( bday ‘𝑏)))
11	10	uneq1d 4161	. . . . . 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 2816	. . . . 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 7418	. . . . . . 7 ⊢ (𝑎 = 𝑋 → (𝑎 ·s 𝑏) = (𝑋 ·s 𝑏))
14	13	eleq1d 2816	. . . . . 6 ⊢ (𝑎 = 𝑋 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑋 ·s 𝑏) ∈ No ))
15	14	anbi1d 628	. . . . 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 343	. . . 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 7427	. . . . . . 7 ⊢ (𝑏 = 𝑌 → (( bday ‘𝑋) +no ( bday ‘𝑏)) = (( bday ‘𝑋) +no ( bday ‘𝑌)))
19	18	uneq1d 4161	. . . . . 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 2816	. . . . 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 7419	. . . . . . 7 ⊢ (𝑏 = 𝑌 → (𝑋 ·s 𝑏) = (𝑋 ·s 𝑌))
22	21	eleq1d 2816	. . . . . 6 ⊢ (𝑏 = 𝑌 → ((𝑋 ·s 𝑏) ∈ No ↔ (𝑋 ·s 𝑌) ∈ No ))
23	22	anbi1d 628	. . . . 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 343	. . . 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 7426	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (( bday ‘𝑐) +no ( bday ‘𝑒)) = (( bday ‘𝑍) +no ( bday ‘𝑒)))
27	26	uneq1d 4161	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → ((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑍) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))))
28	25	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (( bday ‘𝑐) +no ( bday ‘𝑓)) = (( bday ‘𝑍) +no ( bday ‘𝑓)))
29	28	uneq1d 4161	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))
30	27, 29	uneq12d 4163	. . . . . . 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 4162	. . . . . 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 2816	. . . . 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 5150	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → (𝑐 <s 𝑑 ↔ 𝑍 <s 𝑑))
34	33	anbi1d 628	. . . . . . 7 ⊢ (𝑐 = 𝑍 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓)))
35		oveq1 7418	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (𝑐 ·s 𝑓) = (𝑍 ·s 𝑓))
36		oveq1 7418	. . . . . . . . 9 ⊢ (𝑐 = 𝑍 → (𝑐 ·s 𝑒) = (𝑍 ·s 𝑒))
37	35, 36	oveq12d 7429	. . . . . . . 8 ⊢ (𝑐 = 𝑍 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)))
38	37	breq1d 5157	. . . . . . 7 ⊢ (𝑐 = 𝑍 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))
39	34, 38	imbi12d 343	. . . . . 6 ⊢ (𝑐 = 𝑍 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))
40	39	anbi2d 627	. . . . 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 343	. . . 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 7426	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (( bday ‘𝑑) +no ( bday ‘𝑓)) = (( bday ‘𝑊) +no ( bday ‘𝑓)))
44	43	uneq2d 4162	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → ((( bday ‘𝑍) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑍) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑓))))
45	42	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (( bday ‘𝑑) +no ( bday ‘𝑒)) = (( bday ‘𝑊) +no ( bday ‘𝑒)))
46	45	uneq2d 4162	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑒))))
47	44, 46	uneq12d 4163	. . . . . . 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 4162	. . . . . 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 2816	. . . . 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 5151	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → (𝑍 <s 𝑑 ↔ 𝑍 <s 𝑊))
51	50	anbi1d 628	. . . . . . 7 ⊢ (𝑑 = 𝑊 → ((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓)))
52		oveq1 7418	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (𝑑 ·s 𝑓) = (𝑊 ·s 𝑓))
53		oveq1 7418	. . . . . . . . 9 ⊢ (𝑑 = 𝑊 → (𝑑 ·s 𝑒) = (𝑊 ·s 𝑒))
54	52, 53	oveq12d 7429	. . . . . . . 8 ⊢ (𝑑 = 𝑊 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒)))
55	54	breq2d 5159	. . . . . . 7 ⊢ (𝑑 = 𝑊 → (((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒))))
56	51, 55	imbi12d 343	. . . . . 6 ⊢ (𝑑 = 𝑊 → (((𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒)))))
57	56	anbi2d 627	. . . . 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 343	. . . 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 7427	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (( bday ‘𝑍) +no ( bday ‘𝑒)) = (( bday ‘𝑍) +no ( bday ‘𝑇)))
61	60	uneq1d 4161	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((( bday ‘𝑍) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑓))) = ((( bday ‘𝑍) +no ( bday ‘𝑇)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑓))))
62	59	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (( bday ‘𝑊) +no ( bday ‘𝑒)) = (( bday ‘𝑊) +no ( bday ‘𝑇)))
63	62	uneq2d 4162	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑒))) = ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑇))))
64	61, 63	uneq12d 4163	. . . . . . 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 4162	. . . . . 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 2816	. . . . 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 5150	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → (𝑒 <s 𝑓 ↔ 𝑇 <s 𝑓))
68	67	anbi2d 627	. . . . . . 7 ⊢ (𝑒 = 𝑇 → ((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓)))
69		oveq2 7419	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (𝑍 ·s 𝑒) = (𝑍 ·s 𝑇))
70	69	oveq2d 7427	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) = ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)))
71		oveq2 7419	. . . . . . . . 9 ⊢ (𝑒 = 𝑇 → (𝑊 ·s 𝑒) = (𝑊 ·s 𝑇))
72	71	oveq2d 7427	. . . . . . . 8 ⊢ (𝑒 = 𝑇 → ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒)) = ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇)))
73	70, 72	breq12d 5160	. . . . . . 7 ⊢ (𝑒 = 𝑇 → (((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒)) ↔ ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇))))
74	68, 73	imbi12d 343	. . . . . 6 ⊢ (𝑒 = 𝑇 → (((𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑒)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑒))) ↔ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇)))))
75	74	anbi2d 627	. . . . 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 343	. . . 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 7427	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (( bday ‘𝑊) +no ( bday ‘𝑓)) = (( bday ‘𝑊) +no ( bday ‘𝑈)))
79	78	uneq2d 4162	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((( bday ‘𝑍) +no ( bday ‘𝑇)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑓))) = ((( bday ‘𝑍) +no ( bday ‘𝑇)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑈))))
80	77	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (( bday ‘𝑍) +no ( bday ‘𝑓)) = (( bday ‘𝑍) +no ( bday ‘𝑈)))
81	80	uneq1d 4161	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((( bday ‘𝑍) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑇))) = ((( bday ‘𝑍) +no ( bday ‘𝑈)) ∪ (( bday ‘𝑊) +no ( bday ‘𝑇))))
82	79, 81	uneq12d 4163	. . . . . . 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 4162	. . . . . 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 2816	. . . . 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 5151	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → (𝑇 <s 𝑓 ↔ 𝑇 <s 𝑈))
86	85	anbi2d 627	. . . . . . 7 ⊢ (𝑓 = 𝑈 → ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) ↔ (𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈)))
87		oveq2 7419	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (𝑍 ·s 𝑓) = (𝑍 ·s 𝑈))
88	87	oveq1d 7426	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)) = ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)))
89		oveq2 7419	. . . . . . . . 9 ⊢ (𝑓 = 𝑈 → (𝑊 ·s 𝑓) = (𝑊 ·s 𝑈))
90	89	oveq1d 7426	. . . . . . . 8 ⊢ (𝑓 = 𝑈 → ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇)) = ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇)))
91	88, 90	breq12d 5160	. . . . . . 7 ⊢ (𝑓 = 𝑈 → (((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇)) ↔ ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇))))
92	86, 91	imbi12d 343	. . . . . 6 ⊢ (𝑓 = 𝑈 → (((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓) → ((𝑍 ·s 𝑓) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑓) -s (𝑊 ·s 𝑇))) ↔ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇)))))
93	92	anbi2d 627	. . . . 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 343	. . . 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 3630	. . 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 1384	. 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 49	1 ⊢ (𝜑 → ((𝑋 ·s 𝑌) ∈ No ∧ ((𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈) → ((𝑍 ·s 𝑈) -s (𝑍 ·s 𝑇)) <s ((𝑊 ·s 𝑈) -s (𝑊 ·s 𝑇)))))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∀wral 3059   ∪ cun 3945   class class class wbr 5147  ‘cfv 6542  (class class class)co 7411   +no cnadd 8666   No csur 27379   <s cslt 27380   bday cbday 27381   -_s csubs 27734   ·_s cmuls 27801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  mulsproplem2  27812  mulsproplem3  27813  mulsproplem4  27814  mulsproplem5  27815  mulsproplem6  27816  mulsproplem7  27817  mulsproplem8  27818