Theorem mulsproplemcbv 28510

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025.)

Hypothesis

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 𝑒))))))

Assertion

Ref

Expression

mulsproplemcbv

⊢ (𝜑 → ∀𝑔 ∈ 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 𝑘))))))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐴,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝐶,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝐷,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝑔,𝐸,ℎ,𝑖,𝑗,𝑘,𝑙   𝑔,𝐹,ℎ,𝑖,𝑗,𝑘,𝑙

Allowed substitution hints:   𝜑(𝑒, 𝑓, 𝑔, ℎ, 𝑖, 𝑗, 𝑘, 𝑎, 𝑏, 𝑐, 𝑑, 𝑙)

Proof of Theorem mulsproplemcbv

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076   ∪ cun 4148   class class class wbr 5102  ‘cfv 6543  (class class class)co 7424   +no cnadd 8681  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:  mulsproplem13  28523  mulsproplem14  28524