Theorem mulsproplem12 28037

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 4123	. . . . . . . . . . . . . . . . 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 4123	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
4		bday0s 27747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( bday ‘ 0s ) = ∅
5	4, 4	oveq12i 7402	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
6		0elon 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
7		naddrid 8650	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ +no ∅) = ∅
9	5, 8	eqtri 2753	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
10	3, 9	eqtri 2753	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = ∅
11	2, 10	eqtri 2753	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
12	11	uneq2i 4131	. . . . . . . . . . . . . . 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 4360	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐹))
14	12, 13	eqtri 2753	. . . . . . . . . . . . . 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 4145	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
16		ssun1 4144	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
17	15, 16	sstri 3959	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
18		ssun2 4145	. . . . . . . . . . . . . . 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 3959	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
20	14, 19	eqsstri 3996	. . . . . . . . . . . . 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 3945	. . . . . . . . . . . 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 63	. . . . . . . . . . 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 3108	. . . . . . . . . 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 17	. . . . . . . . 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 28035	. . . . . . . 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 1143	. . . . . . 7 ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)})
29	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹)ℎ = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)})
30		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐶) ∈ ( bday ‘𝐷))
31		bdayelon 27695	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐷) ∈ On
32		mulsproplem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ No )
33	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ No )
34		oldbday 27819	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐷) ∈ On ∧ 𝐶 ∈ No ) → (𝐶 ∈ ( O ‘( bday ‘𝐷)) ↔ ( bday ‘𝐶) ∈ ( bday ‘𝐷)))
35	31, 33, 34	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ∈ ( O ‘( bday ‘𝐷)) ↔ ( bday ‘𝐶) ∈ ( bday ‘𝐷)))
36	30, 35	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ ( O ‘( bday ‘𝐷)))
37		mulsproplem.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 <s 𝐷)
38	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 <s 𝐷)
39		elleft 27780	. . . . . . . . . 10 ⊢ (𝐶 ∈ ( L ‘𝐷) ↔ (𝐶 ∈ ( O ‘( bday ‘𝐷)) ∧ 𝐶 <s 𝐷))
40	36, 38, 39	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ ( L ‘𝐷))
41		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐸) ∈ ( bday ‘𝐹))
42		bdayelon 27695	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐹) ∈ On
43		mulsproplem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ No )
44	43	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ No )
45		oldbday 27819	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐹) ∈ On ∧ 𝐸 ∈ No ) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
46	42, 44, 45	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
47	41, 46	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( O ‘( bday ‘𝐹)))
48		mulsproplem.7	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 <s 𝐹)
49	48	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 <s 𝐹)
50		elleft 27780	. . . . . . . . . 10 ⊢ (𝐸 ∈ ( L ‘𝐹) ↔ (𝐸 ∈ ( O ‘( bday ‘𝐹)) ∧ 𝐸 <s 𝐹))
51	47, 49, 50	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹))
52		eqid 2730	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))
53		oveq1 7397	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹))
54	53	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)))
55		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞))
56	54, 55	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)))
57	56	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞))))
58		oveq2 7398	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸))
59	58	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
60		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸))
61	59, 60	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)))
62	61	eqeq2d 2741	. . . . . . . . . . 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 3604	. . . . . . . . . 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 1452	. . . . . . . . 9 ⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
65	40, 51, 64	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
66		ovex 7423	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ V
67		eqeq1 2734	. . . . . . . . . 10 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))))
68	67	2rexbidv 3203	. . . . . . . . 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 3649	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))})
71		elun1 4148	. . . . . . 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 17	. . . . . 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 7423	. . . . . . . 8 ⊢ (𝐷 ·s 𝐹) ∈ V
74	73	snid 4629	. . . . . . 7 ⊢ (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}
75	74	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)})
76	29, 72, 75	ssltsepcd 27713	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹))
77	11	uneq2i 4131	. . . . . . . . . . . . . . . . . . 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 4360	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐹))
79	77, 78	eqtri 2753	. . . . . . . . . . . . . . . . . 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 4144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
81		ssun2 4145	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
82	80, 81	sstri 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
83	82, 18	sstri 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
84	79, 83	eqsstri 3996	. . . . . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . . . 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 63	. . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 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 28035	. . . . . . . . . . . 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 1142	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No )
91	11	uneq2i 4131	. . . . . . . . . . . . . . . . . . 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 4360	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐸))
93	91, 92	eqtri 2753	. . . . . . . . . . . . . . . . . 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 4145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
95	94, 81	sstri 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
96	95, 18	sstri 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
97	93, 96	eqsstri 3996	. . . . . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . . . 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 63	. . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 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 28035	. . . . . . . . . . . 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 1142	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No )
104	90, 103	addscomd 27881	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
105	104	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)))
106	11	uneq2i 4131	. . . . . . . . . . . . . . . . . 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 4360	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐸))
108	106, 107	eqtri 2753	. . . . . . . . . . . . . . . . 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 4144	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
110	109, 16	sstri 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
111	110, 18	sstri 3959	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
112	108, 111	eqsstri 3996	. . . . . . . . . . . . . . . 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 3945	. . . . . . . . . . . . . . 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 63	. . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . 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 17	. . . . . . . . . . . 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 28035	. . . . . . . . . . 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 1142	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No )
119	103, 90, 118	addsubsassd 27992	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
120	105, 119	eqtrd 2765	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
121	120	breq1d 5120	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹)))
122	90, 118	subscld 27974	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
123	27	simp1d 1142	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No )
124	103, 122, 123	sltaddsub2d 28003	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
125	121, 124	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
126	125	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
127	76, 126	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
128	127	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
129	102	simp3d 1144	. . . . . . 7 ⊢ (𝜑 → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
130	129	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
131		ovex 7423	. . . . . . . 8 ⊢ (𝐷 ·s 𝐸) ∈ V
132	131	snid 4629	. . . . . . 7 ⊢ (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}
133	132	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)})
134		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐶) ∈ ( bday ‘𝐷))
135	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ No )
136	31, 135, 34	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐶 ∈ ( O ‘( bday ‘𝐷)) ↔ ( bday ‘𝐶) ∈ ( bday ‘𝐷)))
137	134, 136	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ ( O ‘( bday ‘𝐷)))
138	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 <s 𝐷)
139	137, 138, 39	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ ( L ‘𝐷))
140		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐹) ∈ ( bday ‘𝐸))
141		bdayelon 27695	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐸) ∈ On
142	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ No )
143		oldbday 27819	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐸) ∈ On ∧ 𝐹 ∈ No ) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
144	141, 142, 143	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
145	140, 144	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( O ‘( bday ‘𝐸)))
146	48	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐸 <s 𝐹)
147		elright 27781	. . . . . . . . . 10 ⊢ (𝐹 ∈ ( R ‘𝐸) ↔ (𝐹 ∈ ( O ‘( bday ‘𝐸)) ∧ 𝐸 <s 𝐹))
148	145, 146, 147	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸))
149		eqid 2730	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))
150		oveq1 7397	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸))
151	150	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)))
152		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢))
153	151, 152	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)))
154	153	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢))))
155		oveq2 7398	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹))
156	155	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
157		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹))
158	156, 157	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
159	158	eqeq2d 2741	. . . . . . . . . . 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 3604	. . . . . . . . . 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 1452	. . . . . . . . 9 ⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
162	139, 148, 161	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
163		ovex 7423	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ V
164		eqeq1 2734	. . . . . . . . . 10 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))))
165	164	2rexbidv 3203	. . . . . . . . 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 3649	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))})
168		elun1 4148	. . . . . . 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 17	. . . . . 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	ssltsepcd 27713	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
171	118, 123	addscomd 27881	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
172	171	oveq1d 7405	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)))
173	123, 118, 90	addsubsassd 27992	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
174	172, 173	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
175	174	breq2d 5122	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
176	118, 90	subscld 27974	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ∈ No )
177	103, 123, 176	sltsubadd2d 28001	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
178	175, 177	bitr4d 282	. . . . . . 7 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
179	103, 123, 118, 90	sltsubsub2bd 27995	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
180	178, 179	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
181	180	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
182	170, 181	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
183	182	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
184		mulsproplem12.2	. . . 4 ⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
185	184	adantr 480	. . 3 ⊢ ((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
186	128, 183, 185	mpjaodan 960	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
187	89	simp3d 1144	. . . . . . 7 ⊢ (𝜑 → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
188	187	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
189		ovex 7423	. . . . . . . 8 ⊢ (𝐶 ·s 𝐹) ∈ V
190	189	snid 4629	. . . . . . 7 ⊢ (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}
191	190	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)})
192		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐷) ∈ ( bday ‘𝐶))
193		bdayelon 27695	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐶) ∈ On
194	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ No )
195		oldbday 27819	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐶) ∈ On ∧ 𝐷 ∈ No ) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
196	193, 194, 195	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
197	192, 196	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ ( O ‘( bday ‘𝐶)))
198	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 <s 𝐷)
199		elright 27781	. . . . . . . . . 10 ⊢ (𝐷 ∈ ( R ‘𝐶) ↔ (𝐷 ∈ ( O ‘( bday ‘𝐶)) ∧ 𝐶 <s 𝐷))
200	197, 198, 199	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ ( R ‘𝐶))
201		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐸) ∈ ( bday ‘𝐹))
202	43	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ No )
203	42, 202, 45	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
204	201, 203	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( O ‘( bday ‘𝐹)))
205	48	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 <s 𝐹)
206	204, 205, 50	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹))
207		eqid 2730	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))
208		oveq1 7397	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹))
209	208	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)))
210		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤))
211	209, 210	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)))
212	211	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤))))
213		oveq2 7398	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸))
214	213	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
215		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸))
216	214, 215	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
217	216	eqeq2d 2741	. . . . . . . . . . 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 3604	. . . . . . . . . 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 1452	. . . . . . . . 9 ⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
220	200, 206, 219	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
221		ovex 7423	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ V
222		eqeq1 2734	. . . . . . . . . 10 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))))
223	222	2rexbidv 3203	. . . . . . . . 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 3649	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})
226		elun2 4149	. . . . . . 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 17	. . . . . 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	ssltsepcd 27713	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
229	123, 118	addscomd 27881	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
230	229	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)))
231	118, 123, 103	addsubsassd 27992	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
232	230, 231	eqtrd 2765	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
233	232	breq2d 5122	. . . . . . 7 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
234	123, 103	subscld 27974	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
235	90, 118, 234	sltsubadd2d 28001	. . . . . . 7 ⊢ (𝜑 → (((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
236	233, 235	bitr4d 282	. . . . . 6 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
237	236	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
238	228, 237	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
239	238	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
240	117	simp2d 1143	. . . . . . 7 ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
241	240	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
242		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐷) ∈ ( bday ‘𝐶))
243	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ No )
244	193, 243, 195	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
245	242, 244	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ ( O ‘( bday ‘𝐶)))
246	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 <s 𝐷)
247	245, 246, 199	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ ( R ‘𝐶))
248		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐹) ∈ ( bday ‘𝐸))
249	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ No )
250	141, 249, 143	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
251	248, 250	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( O ‘( bday ‘𝐸)))
252	48	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐸 <s 𝐹)
253	251, 252, 147	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸))
254		eqid 2730	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))
255		oveq1 7397	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸))
256	255	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)))
257		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠))
258	256, 257	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)))
259	258	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠))))
260		oveq2 7398	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹))
261	260	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
262		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹))
263	261, 262	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)))
264	263	eqeq2d 2741	. . . . . . . . . . 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 3604	. . . . . . . . . 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 1452	. . . . . . . . 9 ⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
267	247, 253, 266	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
268		ovex 7423	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ V
269		eqeq1 2734	. . . . . . . . . 10 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))))
270	269	2rexbidv 3203	. . . . . . . . 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 3649	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})
273		elun2 4149	. . . . . . 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 17	. . . . . 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 7423	. . . . . . . 8 ⊢ (𝐶 ·s 𝐸) ∈ V
276	275	snid 4629	. . . . . . 7 ⊢ (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}
277	276	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)})
278	241, 274, 277	ssltsepcd 27713	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸))
279	103, 90	addscomd 27881	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
280	279	oveq1d 7405	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)))
281	90, 103, 123	addsubsassd 27992	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
282	280, 281	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
283	282	breq1d 5120	. . . . . . . 8 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸)))
284	103, 123	subscld 27974	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) ∈ No )
285	90, 284, 118	sltaddsub2d 28003	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
286	283, 285	bitrd 279	. . . . . . 7 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
287	286, 179	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
288	287	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
289	278, 288	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
290	289	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
291	184	adantr 480	. . 3 ⊢ ((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
292	239, 290, 291	mpjaodan 960	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
293		mulsproplem12.1	. 2 ⊢ (𝜑 → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
294	186, 292, 293	mpjaodan 960	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cab 2708  ∀wral 3045  ∃wrex 3054   ∪ cun 3915  ∅c0 4299  {csn 4592   class class class wbr 5110  Oncon0 6335  ‘cfv 6514  (class class class)co 7390   +no cnadd 8632   No csur 27558   <s cslt 27559   bday cbday 27560   <<s csslt 27699   0_s c0s 27741   O cold 27758   L cleft 27760   R cright 27761   +_s cadds 27873   -_s csubs 27933   ·_s cmuls 28016

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-ot 4601  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-1o 8437  df-2o 8438  df-nadd 8633  df-no 27561  df-slt 27562  df-bday 27563  df-sle 27664  df-sslt 27700  df-scut 27702  df-0s 27743  df-made 27762  df-old 27763  df-left 27765  df-right 27766  df-norec 27852  df-norec2 27863  df-adds 27874  df-negs 27934  df-subs 27935  df-muls 28017

This theorem is referenced by:  mulsproplem13  28038