Theorem mulsproplem12 28513

Description: Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming 𝐶 and 𝐷 are not the same age and 𝐸 and 𝐹 are not the same age. (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 𝐹)
mulsproplem12.1	⊢ (𝜑 → ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)))
mulsproplem12.2	⊢ (𝜑 → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))

Assertion

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

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

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

Proof of Theorem mulsproplem12

Dummy variables 𝑔 ℎ 𝑖 𝑗 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mulsproplem.1	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 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		unidm 4104	. . . . . . . . . . . . . . . . 17 ⊢ ((((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 )))
3		unidm 4104	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) = ((bday‘ 0s ) +no (bday‘ 0s ))
4		bday0 28197	. . . . . . . . . . . . . . . . . . . 20 ⊢ (bday‘ 0s ) = ∅
5	4, 4	oveq12i 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((bday‘ 0s ) +no (bday‘ 0s )) = (∅ +no ∅)
6		0elon 6418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
7		naddrid 8693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ +no ∅) = ∅
9	5, 8	eqtri 2784	. . . . . . . . . . . . . . . . . 18 ⊢ ((bday‘ 0s ) +no (bday‘ 0s )) = ∅
10	3, 9	eqtri 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) = ∅
11	2, 10	eqtri 2784	. . . . . . . . . . . . . . . 16 ⊢ ((((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s ))) ∪ (((bday‘ 0s ) +no (bday‘ 0s )) ∪ ((bday‘ 0s ) +no (bday‘ 0s )))) = ∅
12	11	uneq2i 4112	. . . . . . . . . . . . . . 15 ⊢ (((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‘𝐹)) ∪ ∅)
13		un0 4344	. . . . . . . . . . . . . . 15 ⊢ (((bday‘𝐷) +no (bday‘𝐹)) ∪ ∅) = ((bday‘𝐷) +no (bday‘𝐹))
14	12, 13	eqtri 2784	. . . . . . . . . . . . . 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‘𝐹))
15		ssun2 4125	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹)))
16		ssun1 4124	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
17	15, 16	sstri 3940	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
18		ssun2 4125	. . . . . . . . . . . . . . 15 ⊢ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
19	17, 18	sstri 3940	. . . . . . . . . . . . . 14 ⊢ ((bday‘𝐷) +no (bday‘𝐹)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
20	14, 19	eqsstri 3977	. . . . . . . . . . . . 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‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
21	20	sseli 3927	. . . . . . . . . . . 12 ⊢ ((((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‘𝐸))))))
22	21	imim1i 64	. . . . . . . . . . 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‘𝐸))))) → ((𝑎 ·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 𝑒))))))
23	22	6ralimi 3137	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ 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 𝑒))))))
24	1, 23	syl 18	. . . . . . . . 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‘ 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 𝑒))))))
25		mulsproplem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ No)
26		mulsproplem.5	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ No)
27	24, 25, 26	mulsproplem10 28511	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐹) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)} ∧ {(𝐷 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))})))
28	27	simp2d 1161	. . . . . . 7 ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)})
29	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)})
30		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (bday‘𝐶) ∈ (bday‘𝐷))
31		bdayon 28138	. . . . . . . . . . . 12 ⊢ (bday‘𝐷) ∈ On
32		mulsproplem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ No)
33	32	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐶 ∈ No)
34		oldbday 28287	. . . . . . . . . . . 12 ⊢ (((bday‘𝐷) ∈ On ∧ 𝐶 ∈ No) → (𝐶 ∈ (O‘(bday‘𝐷)) ↔ (bday‘𝐶) ∈ (bday‘𝐷)))
35	31, 33, 34	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐶 ∈ (O‘(bday‘𝐷)) ↔ (bday‘𝐶) ∈ (bday‘𝐷)))
36	30, 35	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐶 ∈ (O‘(bday‘𝐷)))
37		mulsproplem.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 <s 𝐷)
38	37	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐶 <s 𝐷)
39		elleft 28237	. . . . . . . . . 10 ⊢ (𝐶 ∈ (L‘𝐷) ↔ (𝐶 ∈ (O‘(bday‘𝐷)) ∧ 𝐶 <s 𝐷))
40	36, 38, 39	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐶 ∈ (L‘𝐷))
41		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (bday‘𝐸) ∈ (bday‘𝐹))
42		bdayon 28138	. . . . . . . . . . . 12 ⊢ (bday‘𝐹) ∈ On
43		mulsproplem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ No)
44	43	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ No)
45		oldbday 28287	. . . . . . . . . . . 12 ⊢ (((bday‘𝐹) ∈ On ∧ 𝐸 ∈ No) → (𝐸 ∈ (O‘(bday‘𝐹)) ↔ (bday‘𝐸) ∈ (bday‘𝐹)))
46	42, 44, 45	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐸 ∈ (O‘(bday‘𝐹)) ↔ (bday‘𝐸) ∈ (bday‘𝐹)))
47	41, 46	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ (O‘(bday‘𝐹)))
48		mulsproplem.7	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 <s 𝐹)
49	48	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 <s 𝐹)
50		elleft 28237	. . . . . . . . . 10 ⊢ (𝐸 ∈ (L‘𝐹) ↔ (𝐸 ∈ (O‘(bday‘𝐹)) ∧ 𝐸 <s 𝐹))
51	47, 49, 50	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ (L‘𝐹))
52		eqid 2761	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸))
53		oveq1 7427	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹))
54	53	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)))
55		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞))
56	54, 55	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝐶 ·s 𝑞)))
57	56	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝐶 ·s 𝑞))))
58		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸))
59	58	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
60		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸))
61	59, 60	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)))
62	61	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐸 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝐶 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸))))
63	57, 62	rspc2ev 3589	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (L‘𝐷) ∧ 𝐸 ∈ (L‘𝐹) ∧ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸))) → ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)))
64	52, 63	mp3an3 1479	. . . . . . . . 9 ⊢ ((𝐶 ∈ (L‘𝐷) ∧ 𝐸 ∈ (L‘𝐹)) → ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)))
65	40, 51, 64	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)))
66		ovex 7453	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ V
67		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))))
68	67	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) → (∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))))
69	66, 68	elab 3633	. . . . . . . 8 ⊢ ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ↔ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞)))
70	65, 69	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))})
71		elun1 4128	. . . . . . 7 ⊢ ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}))
72	70, 71	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) ∈ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}))
73		ovex 7453	. . . . . . . 8 ⊢ (𝐷 ·s 𝐹) ∈ V
74	73	snid 4623	. . . . . . 7 ⊢ (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}
75	74	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)})
76	29, 72, 75	sltssepcd 28158	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹))
77	11	uneq2i 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((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	. . . . . . . . . . . . . . . . . . 19 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ∅) = ((bday‘𝐶) +no (bday‘𝐹))
79	77, 78	eqtri 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (((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		ssun1 4124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))
81		ssun2 4125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
82	80, 81	sstri 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
83	82, 18	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ ((bday‘𝐶) +no (bday‘𝐹)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
84	79, 83	eqsstri 3977	. . . . . . . . . . . . . . . . 17 ⊢ (((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‘𝐸)))))
85	84	sseli 3927	. . . . . . . . . . . . . . . 16 ⊢ ((((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‘𝐸))))))
86	85	imim1i 64	. . . . . . . . . . . . . . 15 ⊢ (((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·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 𝑒))))))
87	86	6ralimi 3137	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ 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 𝑒))))))
88	1, 87	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ 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 𝑒))))))
89	88, 32, 26	mulsproplem10 28511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 ·s 𝐹) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐹)} ∧ {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))})))
90	89	simp1d 1160	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No)
91	11	uneq2i 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((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		un0 4344	. . . . . . . . . . . . . . . . . . 19 ⊢ (((bday‘𝐷) +no (bday‘𝐸)) ∪ ∅) = ((bday‘𝐷) +no (bday‘𝐸))
93	91, 92	eqtri 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (((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‘𝐸))
94		ssun2 4125	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))
95	94, 81	sstri 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
96	95, 18	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ ((bday‘𝐷) +no (bday‘𝐸)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
97	93, 96	eqsstri 3977	. . . . . . . . . . . . . . . . 17 ⊢ (((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‘𝐸)))))
98	97	sseli 3927	. . . . . . . . . . . . . . . 16 ⊢ ((((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‘𝐸))))))
99	98	imim1i 64	. . . . . . . . . . . . . . 15 ⊢ (((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·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 𝑒))))))
100	99	6ralimi 3137	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ 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 𝑒))))))
101	1, 100	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ 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 𝑒))))))
102	101, 25, 43	mulsproplem10 28511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐷 ·s 𝐸) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐷)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐷 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐷)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐷 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐸)} ∧ {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))})))
103	102	simp1d 1160	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No)
104	90, 103	addscomd 28353	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
105	104	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐶 ·s 𝐸)))
106	11	uneq2i 4112	. . . . . . . . . . . . . . . . . 18 ⊢ (((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‘𝐸)) ∪ ∅)
107		un0 4344	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ∅) = ((bday‘𝐶) +no (bday‘𝐸))
108	106, 107	eqtri 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((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‘𝐸))
109		ssun1 4124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹)))
110	109, 16	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
111	110, 18	sstri 3940	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝐶) +no (bday‘𝐸)) ⊆ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))))
112	108, 111	eqsstri 3977	. . . . . . . . . . . . . . . 16 ⊢ (((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‘𝐸)))))
113	112	sseli 3927	. . . . . . . . . . . . . . 15 ⊢ ((((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‘𝐸))))))
114	113	imim1i 64	. . . . . . . . . . . . . 14 ⊢ (((((bday‘𝑎) +no (bday‘𝑏)) ∪ ((((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) ∪ (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))) ∈ (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) → ((𝑎 ·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 𝑒))))))
115	114	6ralimi 3137	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ 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 𝑒))))))
116	1, 115	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑎 ∈ 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 𝑒))))))
117	116, 32, 43	mulsproplem10 28511	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 ·s 𝐸) ∈ No ∧ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)} ∧ {(𝐶 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))})))
118	117	simp1d 1160	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No)
119	103, 90, 118	addsubsassd 28467	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸))))
120	105, 119	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸))))
121	120	breq1d 5113	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹)))
122	90, 118	subscld 28449	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) ∈ No)
123	27	simp1d 1160	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No)
124	103, 122, 123	ltaddsubs2d 28478	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
125	121, 124	bitrd 282	. . . . . 6 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
126	125	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
127	76, 126	mpbid 235	. . . 4 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
128	127	anassrs 473	. . 3 ⊢ (((𝜑 ∧ (bday‘𝐶) ∈ (bday‘𝐷)) ∧ (bday‘𝐸) ∈ (bday‘𝐹)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
129	102	simp3d 1162	. . . . . . 7 ⊢ (𝜑 → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
130	129	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
131		ovex 7453	. . . . . . . 8 ⊢ (𝐷 ·s 𝐸) ∈ V
132	131	snid 4623	. . . . . . 7 ⊢ (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}
133	132	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)})
134		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (bday‘𝐶) ∈ (bday‘𝐷))
135	32	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐶 ∈ No)
136	31, 135, 34	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐶 ∈ (O‘(bday‘𝐷)) ↔ (bday‘𝐶) ∈ (bday‘𝐷)))
137	134, 136	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐶 ∈ (O‘(bday‘𝐷)))
138	37	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐶 <s 𝐷)
139	137, 138, 39	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐶 ∈ (L‘𝐷))
140		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (bday‘𝐹) ∈ (bday‘𝐸))
141		bdayon 28138	. . . . . . . . . . . 12 ⊢ (bday‘𝐸) ∈ On
142	26	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ No)
143		oldbday 28287	. . . . . . . . . . . 12 ⊢ (((bday‘𝐸) ∈ On ∧ 𝐹 ∈ No) → (𝐹 ∈ (O‘(bday‘𝐸)) ↔ (bday‘𝐹) ∈ (bday‘𝐸)))
144	141, 142, 143	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐹 ∈ (O‘(bday‘𝐸)) ↔ (bday‘𝐹) ∈ (bday‘𝐸)))
145	140, 144	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ (O‘(bday‘𝐸)))
146	48	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐸 <s 𝐹)
147		elright 28238	. . . . . . . . . 10 ⊢ (𝐹 ∈ (R‘𝐸) ↔ (𝐹 ∈ (O‘(bday‘𝐸)) ∧ 𝐸 <s 𝐹))
148	145, 146, 147	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ (R‘𝐸))
149		eqid 2761	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹))
150		oveq1 7427	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸))
151	150	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)))
152		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢))
153	151, 152	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝐶 ·s 𝑢)))
154	153	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝐶 ·s 𝑢))))
155		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹))
156	155	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
157		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹))
158	156, 157	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)))
159	158	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑢 = 𝐹 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝐶 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹))))
160	154, 159	rspc2ev 3589	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (L‘𝐷) ∧ 𝐹 ∈ (R‘𝐸) ∧ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹))) → ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
161	149, 160	mp3an3 1479	. . . . . . . . 9 ⊢ ((𝐶 ∈ (L‘𝐷) ∧ 𝐹 ∈ (R‘𝐸)) → ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
162	139, 148, 161	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
163		ovex 7453	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ V
164		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))))
165	164	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) → (∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)) ↔ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))))
166	163, 165	elab 3633	. . . . . . . 8 ⊢ ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ↔ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
167	162, 166	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))})
168		elun1 4128	. . . . . . 7 ⊢ ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
169	167, 168	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ∈ ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐷)∃𝑢 ∈ (R‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐷)∃𝑤 ∈ (L‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
170	130, 133, 169	sltssepcd 28158	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)))
171	118, 123	addscomd 28353	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
172	171	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐶 ·s 𝐹)))
173	123, 118, 90	addsubsassd 28467	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹))))
174	172, 173	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹))))
175	174	breq2d 5115	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹)))))
176	118, 90	subscld 28449	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹)) ∈ No)
177	103, 123, 176	ltsubadds2d 28476	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹)))))
178	175, 177	bitr4d 285	. . . . . . 7 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ↔ ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹))))
179	103, 123, 118, 90	ltsubsubs2bd 28470	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
180	178, 179	bitrd 282	. . . . . 6 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
181	180	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
182	170, 181	mpbid 235	. . . 4 ⊢ ((𝜑 ∧ ((bday‘𝐶) ∈ (bday‘𝐷) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
183	182	anassrs 473	. . 3 ⊢ (((𝜑 ∧ (bday‘𝐶) ∈ (bday‘𝐷)) ∧ (bday‘𝐹) ∈ (bday‘𝐸)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
184		mulsproplem12.2	. . . 4 ⊢ (𝜑 → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
185	184	adantr 486	. . 3 ⊢ ((𝜑 ∧ (bday‘𝐶) ∈ (bday‘𝐷)) → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
186	128, 183, 185	mpjaodan 973	. 2 ⊢ ((𝜑 ∧ (bday‘𝐶) ∈ (bday‘𝐷)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
187	89	simp3d 1162	. . . . . . 7 ⊢ (𝜑 → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
188	187	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
189		ovex 7453	. . . . . . . 8 ⊢ (𝐶 ·s 𝐹) ∈ V
190	189	snid 4623	. . . . . . 7 ⊢ (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}
191	190	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)})
192		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (bday‘𝐷) ∈ (bday‘𝐶))
193		bdayon 28138	. . . . . . . . . . . 12 ⊢ (bday‘𝐶) ∈ On
194	25	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐷 ∈ No)
195		oldbday 28287	. . . . . . . . . . . 12 ⊢ (((bday‘𝐶) ∈ On ∧ 𝐷 ∈ No) → (𝐷 ∈ (O‘(bday‘𝐶)) ↔ (bday‘𝐷) ∈ (bday‘𝐶)))
196	193, 194, 195	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐷 ∈ (O‘(bday‘𝐶)) ↔ (bday‘𝐷) ∈ (bday‘𝐶)))
197	192, 196	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐷 ∈ (O‘(bday‘𝐶)))
198	37	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐶 <s 𝐷)
199		elright 28238	. . . . . . . . . 10 ⊢ (𝐷 ∈ (R‘𝐶) ↔ (𝐷 ∈ (O‘(bday‘𝐶)) ∧ 𝐶 <s 𝐷))
200	197, 198, 199	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐷 ∈ (R‘𝐶))
201		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (bday‘𝐸) ∈ (bday‘𝐹))
202	43	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ No)
203	42, 202, 45	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐸 ∈ (O‘(bday‘𝐹)) ↔ (bday‘𝐸) ∈ (bday‘𝐹)))
204	201, 203	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ (O‘(bday‘𝐹)))
205	48	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 <s 𝐹)
206	204, 205, 50	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → 𝐸 ∈ (L‘𝐹))
207		eqid 2761	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸))
208		oveq1 7427	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹))
209	208	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)))
210		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤))
211	209, 210	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝐷 ·s 𝑤)))
212	211	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝐷 ·s 𝑤))))
213		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸))
214	213	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
215		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸))
216	214, 215	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)))
217	216	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐸 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝐷 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸))))
218	212, 217	rspc2ev 3589	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (R‘𝐶) ∧ 𝐸 ∈ (L‘𝐹) ∧ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸))) → ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)))
219	207, 218	mp3an3 1479	. . . . . . . . 9 ⊢ ((𝐷 ∈ (R‘𝐶) ∧ 𝐸 ∈ (L‘𝐹)) → ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)))
220	200, 206, 219	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)))
221		ovex 7453	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ V
222		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))))
223	222	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) → (∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))))
224	221, 223	elab 3633	. . . . . . . 8 ⊢ ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))} ↔ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤)))
225	220, 224	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))})
226		elun2 4129	. . . . . . 7 ⊢ ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))} → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
227	225, 226	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ∈ ({𝑖 ∣ ∃𝑡 ∈ (L‘𝐶)∃𝑢 ∈ (R‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) −s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ (R‘𝐶)∃𝑤 ∈ (L‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) −s (𝑣 ·s 𝑤))}))
228	188, 191, 227	sltssepcd 28158	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)))
229	123, 118	addscomd 28353	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
230	229	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐷 ·s 𝐸)))
231	118, 123, 103	addsubsassd 28467	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) −s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
232	230, 231	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
233	232	breq2d 5115	. . . . . . 7 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))))
234	123, 103	subscld 28449	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)) ∈ No)
235	90, 118, 234	ltsubadds2d 28476	. . . . . . 7 ⊢ (𝜑 → (((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))))
236	233, 235	bitr4d 285	. . . . . 6 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
237	236	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) −s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
238	228, 237	mpbid 235	. . . 4 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐸) ∈ (bday‘𝐹))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
239	238	anassrs 473	. . 3 ⊢ (((𝜑 ∧ (bday‘𝐷) ∈ (bday‘𝐶)) ∧ (bday‘𝐸) ∈ (bday‘𝐹)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
240	117	simp2d 1161	. . . . . . 7 ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
241	240	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
242		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (bday‘𝐷) ∈ (bday‘𝐶))
243	25	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐷 ∈ No)
244	193, 243, 195	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐷 ∈ (O‘(bday‘𝐶)) ↔ (bday‘𝐷) ∈ (bday‘𝐶)))
245	242, 244	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐷 ∈ (O‘(bday‘𝐶)))
246	37	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐶 <s 𝐷)
247	245, 246, 199	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐷 ∈ (R‘𝐶))
248		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (bday‘𝐹) ∈ (bday‘𝐸))
249	26	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ No)
250	141, 249, 143	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐹 ∈ (O‘(bday‘𝐸)) ↔ (bday‘𝐹) ∈ (bday‘𝐸)))
251	248, 250	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ (O‘(bday‘𝐸)))
252	48	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐸 <s 𝐹)
253	251, 252, 147	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → 𝐹 ∈ (R‘𝐸))
254		eqid 2761	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹))
255		oveq1 7427	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸))
256	255	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)))
257		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠))
258	256, 257	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝐷 ·s 𝑠)))
259	258	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝐷 ·s 𝑠))))
260		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹))
261	260	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
262		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹))
263	261, 262	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)))
264	263	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑠 = 𝐹 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝐷 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹))))
265	259, 264	rspc2ev 3589	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (R‘𝐶) ∧ 𝐹 ∈ (R‘𝐸) ∧ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹))) → ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
266	254, 265	mp3an3 1479	. . . . . . . . 9 ⊢ ((𝐷 ∈ (R‘𝐶) ∧ 𝐹 ∈ (R‘𝐸)) → ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
267	247, 253, 266	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
268		ovex 7453	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ V
269		eqeq1 2765	. . . . . . . . . 10 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) → (ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))))
270	269	2rexbidv 3228	. . . . . . . . 9 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) → (∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))))
271	268, 270	elab 3633	. . . . . . . 8 ⊢ ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))} ↔ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
272	267, 271	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))})
273		elun2 4129	. . . . . . 7 ⊢ ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))} → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}))
274	272, 273	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) ∈ ({𝑔 ∣ ∃𝑝 ∈ (L‘𝐶)∃𝑞 ∈ (L‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) −s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ (R‘𝐶)∃𝑠 ∈ (R‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) −s (𝑟 ·s 𝑠))}))
275		ovex 7453	. . . . . . . 8 ⊢ (𝐶 ·s 𝐸) ∈ V
276	275	snid 4623	. . . . . . 7 ⊢ (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}
277	276	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)})
278	241, 274, 277	sltssepcd 28158	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸))
279	103, 90	addscomd 28353	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
280	279	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐷 ·s 𝐹)))
281	90, 103, 123	addsubsassd 28467	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) −s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹))))
282	280, 281	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹))))
283	282	breq1d 5113	. . . . . . . 8 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸)))
284	103, 123	subscld 28449	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) ∈ No)
285	90, 284, 118	ltaddsubs2d 28478	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹))))
286	283, 285	bitrd 282	. . . . . . 7 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) −s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) −s (𝐶 ·s 𝐹))))
287	286, 179	bitrd 282	. . . . . 6 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
288	287	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) −s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸))))
289	278, 288	mpbid 235	. . . 4 ⊢ ((𝜑 ∧ ((bday‘𝐷) ∈ (bday‘𝐶) ∧ (bday‘𝐹) ∈ (bday‘𝐸))) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
290	289	anassrs 473	. . 3 ⊢ (((𝜑 ∧ (bday‘𝐷) ∈ (bday‘𝐶)) ∧ (bday‘𝐹) ∈ (bday‘𝐸)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
291	184	adantr 486	. . 3 ⊢ ((𝜑 ∧ (bday‘𝐷) ∈ (bday‘𝐶)) → ((bday‘𝐸) ∈ (bday‘𝐹) ∨ (bday‘𝐹) ∈ (bday‘𝐸)))
292	239, 290, 291	mpjaodan 973	. 2 ⊢ ((𝜑 ∧ (bday‘𝐷) ∈ (bday‘𝐶)) → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
293		mulsproplem12.1	. 2 ⊢ (𝜑 → ((bday‘𝐶) ∈ (bday‘𝐷) ∨ (bday‘𝐷) ∈ (bday‘𝐶)))
294	186, 292, 293	mpjaodan 973	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cab 2739  ∀wral 3077  ∃wrex 3087   ∪ cun 3897  ∅c0 4279  {csn 4584   class class class wbr 5103  Oncon0 6362  ‘cfv 6538  (class class class)co 7420   +no cnadd 8674  Nocsur 27997   <s clts 27998  bdaycbday 27999   <<s cslts 28143   0_s c0s 28191  Ocold 28209  Lcleft 28211  Rcright 28212   +_s cadds 28345   −_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:  mulsproplem13  28514