Theorem mulsproplem12 27823

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 4152	. . . . . . . . . . . . . . . . 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 4152	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
4		bday0s 27567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( bday ‘ 0s ) = ∅
5	4, 4	oveq12i 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
6		0elon 6418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
7		naddrid 8686	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ +no ∅) = ∅
9	5, 8	eqtri 2759	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
10	3, 9	eqtri 2759	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = ∅
11	2, 10	eqtri 2759	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
12	11	uneq2i 4160	. . . . . . . . . . . . . . 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 4390	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐹))
14	12, 13	eqtri 2759	. . . . . . . . . . . . . 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 4173	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
16		ssun1 4172	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
17	15, 16	sstri 3991	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
18		ssun2 4173	. . . . . . . . . . . . . . 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 3991	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
20	14, 19	eqsstri 4016	. . . . . . . . . . . . 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 3978	. . . . . . . . . . . 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 3126	. . . . . . . . . 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 27821	. . . . . . . 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 1142	. . . . . . 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 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐶) ∈ ( bday ‘𝐷))
31		bdayelon 27515	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐷) ∈ On
32		mulsproplem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ No )
33	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ No )
34		oldbday 27633	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐷) ∈ On ∧ 𝐶 ∈ No ) → (𝐶 ∈ ( O ‘( bday ‘𝐷)) ↔ ( bday ‘𝐶) ∈ ( bday ‘𝐷)))
35	31, 33, 34	sylancr 586	. . . . . . . . . . 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		breq1 5151	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 <s 𝐷 ↔ 𝐶 <s 𝐷))
40		leftval 27596	. . . . . . . . . . 11 ⊢ ( L ‘𝐷) = {𝑥 ∈ ( O ‘( bday ‘𝐷)) ∣ 𝑥 <s 𝐷}
41	39, 40	elrab2 3686	. . . . . . . . . 10 ⊢ (𝐶 ∈ ( L ‘𝐷) ↔ (𝐶 ∈ ( O ‘( bday ‘𝐷)) ∧ 𝐶 <s 𝐷))
42	36, 38, 41	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ ( L ‘𝐷))
43		simprr 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐸) ∈ ( bday ‘𝐹))
44		bdayelon 27515	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐹) ∈ On
45		mulsproplem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ No )
46	45	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ No )
47		oldbday 27633	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐹) ∈ On ∧ 𝐸 ∈ No ) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
48	44, 46, 47	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
49	43, 48	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( O ‘( bday ‘𝐹)))
50		mulsproplem.7	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 <s 𝐹)
51	50	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 <s 𝐹)
52		breq1 5151	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 <s 𝐹 ↔ 𝐸 <s 𝐹))
53		leftval 27596	. . . . . . . . . . 11 ⊢ ( L ‘𝐹) = {𝑥 ∈ ( O ‘( bday ‘𝐹)) ∣ 𝑥 <s 𝐹}
54	52, 53	elrab2 3686	. . . . . . . . . 10 ⊢ (𝐸 ∈ ( L ‘𝐹) ↔ (𝐸 ∈ ( O ‘( bday ‘𝐹)) ∧ 𝐸 <s 𝐹))
55	49, 51, 54	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹))
56		eqid 2731	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))
57		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹))
58	57	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)))
59		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞))
60	58, 59	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)))
61	60	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞))))
62		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸))
63	62	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
64		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸))
65	63, 64	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)))
66	65	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐸 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))))
67	61, 66	rspc2ev 3624	. . . . . . . . . 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 𝑞)))
68	56, 67	mp3an3 1449	. . . . . . . . 9 ⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
69	42, 55, 68	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
70		ovex 7445	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ V
71		eqeq1 2735	. . . . . . . . . 10 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))))
72	71	2rexbidv 3218	. . . . . . . . 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 𝑞))))
73	70, 72	elab 3668	. . . . . . . 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 𝑞)))
74	69, 73	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))})
75		elun1 4176	. . . . . . 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 𝑠))}))
76	74, 75	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 𝑠))}))
77		ovex 7445	. . . . . . . 8 ⊢ (𝐷 ·s 𝐹) ∈ V
78	77	snid 4664	. . . . . . 7 ⊢ (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}
79	78	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)})
80	29, 76, 79	ssltsepcd 27533	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹))
81	11	uneq2i 4160	. . . . . . . . . . . . . . . . . . 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 ‘𝐹)) ∪ ∅)
82		un0 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐹))
83	81, 82	eqtri 2759	. . . . . . . . . . . . . . . . . 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 ‘𝐹))
84		ssun1 4172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
85		ssun2 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
86	84, 85	sstri 3991	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
87	86, 18	sstri 3991	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
88	83, 87	eqsstri 4016	. . . . . . . . . . . . . . . . 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 ‘𝐸)))))
89	88	sseli 3978	. . . . . . . . . . . . . . . 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 ‘𝐸))))))
90	89	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 𝑒))))))
91	90	6ralimi 3126	. . . . . . . . . . . . . 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 𝑒))))))
92	1, 91	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 𝑒))))))
93	92, 32, 26	mulsproplem10 27821	. . . . . . . . . . . 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 𝑤))})))
94	93	simp1d 1141	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No )
95	11	uneq2i 4160	. . . . . . . . . . . . . . . . . . 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 ‘𝐸)) ∪ ∅)
96		un0 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐸))
97	95, 96	eqtri 2759	. . . . . . . . . . . . . . . . . 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 ‘𝐸))
98		ssun2 4173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
99	98, 85	sstri 3991	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
100	99, 18	sstri 3991	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
101	97, 100	eqsstri 4016	. . . . . . . . . . . . . . . . 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 ‘𝐸)))))
102	101	sseli 3978	. . . . . . . . . . . . . . . 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 ‘𝐸))))))
103	102	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 𝑒))))))
104	103	6ralimi 3126	. . . . . . . . . . . . . 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 𝑒))))))
105	1, 104	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 𝑒))))))
106	105, 25, 45	mulsproplem10 27821	. . . . . . . . . . . 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 𝑤))})))
107	106	simp1d 1141	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No )
108	94, 107	addscomd 27690	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
109	108	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)))
110	11	uneq2i 4160	. . . . . . . . . . . . . . . . . 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 ‘𝐸)) ∪ ∅)
111		un0 4390	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐸))
112	110, 111	eqtri 2759	. . . . . . . . . . . . . . . . 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 ‘𝐸))
113		ssun1 4172	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
114	113, 16	sstri 3991	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
115	114, 18	sstri 3991	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
116	112, 115	eqsstri 4016	. . . . . . . . . . . . . . . 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 ‘𝐸)))))
117	116	sseli 3978	. . . . . . . . . . . . . . 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 ‘𝐸))))))
118	117	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 𝑒))))))
119	118	6ralimi 3126	. . . . . . . . . . . . 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 𝑒))))))
120	1, 119	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 𝑒))))))
121	120, 32, 45	mulsproplem10 27821	. . . . . . . . . . 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 𝑤))})))
122	121	simp1d 1141	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No )
123	107, 94, 122	addsubsassd 27788	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
124	109, 123	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
125	124	breq1d 5158	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹)))
126	94, 122	subscld 27775	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
127	27	simp1d 1141	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No )
128	107, 126, 127	sltaddsub2d 27799	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
129	125, 128	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
130	129	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
131	80, 130	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
132	131	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
133	106	simp3d 1143	. . . . . . 7 ⊢ (𝜑 → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
134	133	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
135		ovex 7445	. . . . . . . 8 ⊢ (𝐷 ·s 𝐸) ∈ V
136	135	snid 4664	. . . . . . 7 ⊢ (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}
137	136	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)})
138		simprl 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐶) ∈ ( bday ‘𝐷))
139	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ No )
140	31, 139, 34	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐶 ∈ ( O ‘( bday ‘𝐷)) ↔ ( bday ‘𝐶) ∈ ( bday ‘𝐷)))
141	138, 140	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ ( O ‘( bday ‘𝐷)))
142	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 <s 𝐷)
143	141, 142, 41	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 ∈ ( L ‘𝐷))
144		simprr 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐹) ∈ ( bday ‘𝐸))
145		bdayelon 27515	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐸) ∈ On
146	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ No )
147		oldbday 27633	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐸) ∈ On ∧ 𝐹 ∈ No ) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
148	145, 146, 147	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
149	144, 148	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( O ‘( bday ‘𝐸)))
150	50	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐸 <s 𝐹)
151		breq2 5152	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐹 → (𝐸 <s 𝑥 ↔ 𝐸 <s 𝐹))
152		rightval 27597	. . . . . . . . . . 11 ⊢ ( R ‘𝐸) = {𝑥 ∈ ( O ‘( bday ‘𝐸)) ∣ 𝐸 <s 𝑥}
153	151, 152	elrab2 3686	. . . . . . . . . 10 ⊢ (𝐹 ∈ ( R ‘𝐸) ↔ (𝐹 ∈ ( O ‘( bday ‘𝐸)) ∧ 𝐸 <s 𝐹))
154	149, 150, 153	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸))
155		eqid 2731	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))
156		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸))
157	156	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)))
158		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢))
159	157, 158	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)))
160	159	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢))))
161		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹))
162	161	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
163		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹))
164	162, 163	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
165	164	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑢 = 𝐹 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))))
166	160, 165	rspc2ev 3624	. . . . . . . . . 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 𝑢)))
167	155, 166	mp3an3 1449	. . . . . . . . 9 ⊢ ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
168	143, 154, 167	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
169		ovex 7445	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ V
170		eqeq1 2735	. . . . . . . . . 10 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))))
171	170	2rexbidv 3218	. . . . . . . . 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 𝑢))))
172	169, 171	elab 3668	. . . . . . . 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 𝑢)))
173	168, 172	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))})
174		elun1 4176	. . . . . . 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 𝑤))}))
175	173, 174	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 𝑤))}))
176	134, 137, 175	ssltsepcd 27533	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
177	122, 127	addscomd 27690	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
178	177	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)))
179	127, 122, 94	addsubsassd 27788	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
180	178, 179	eqtrd 2771	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
181	180	breq2d 5160	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
182	122, 94	subscld 27775	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ∈ No )
183	107, 127, 182	sltsubadd2d 27797	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
184	181, 183	bitr4d 282	. . . . . . 7 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
185	107, 127, 122, 94	sltsubsub2bd 27791	. . . . . . 7 ⊢ (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
186	184, 185	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
187	186	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
188	176, 187	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
189	188	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
190		mulsproplem12.2	. . . 4 ⊢ (𝜑 → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
191	190	adantr 480	. . 3 ⊢ ((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
192	132, 189, 191	mpjaodan 956	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
193	93	simp3d 1143	. . . . . . 7 ⊢ (𝜑 → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
194	193	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
195		ovex 7445	. . . . . . . 8 ⊢ (𝐶 ·s 𝐹) ∈ V
196	195	snid 4664	. . . . . . 7 ⊢ (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}
197	196	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)})
198		simprl 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐷) ∈ ( bday ‘𝐶))
199		bdayelon 27515	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐶) ∈ On
200	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ No )
201		oldbday 27633	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝐶) ∈ On ∧ 𝐷 ∈ No ) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
202	199, 200, 201	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
203	198, 202	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ ( O ‘( bday ‘𝐶)))
204	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 <s 𝐷)
205		breq2 5152	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (𝐶 <s 𝑥 ↔ 𝐶 <s 𝐷))
206		rightval 27597	. . . . . . . . . . 11 ⊢ ( R ‘𝐶) = {𝑥 ∈ ( O ‘( bday ‘𝐶)) ∣ 𝐶 <s 𝑥}
207	205, 206	elrab2 3686	. . . . . . . . . 10 ⊢ (𝐷 ∈ ( R ‘𝐶) ↔ (𝐷 ∈ ( O ‘( bday ‘𝐶)) ∧ 𝐶 <s 𝐷))
208	203, 204, 207	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ ( R ‘𝐶))
209		simprr 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐸) ∈ ( bday ‘𝐹))
210	45	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ No )
211	44, 210, 47	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐸 ∈ ( O ‘( bday ‘𝐹)) ↔ ( bday ‘𝐸) ∈ ( bday ‘𝐹)))
212	209, 211	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( O ‘( bday ‘𝐹)))
213	50	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 <s 𝐹)
214	212, 213, 54	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹))
215		eqid 2731	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))
216		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹))
217	216	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)))
218		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤))
219	217, 218	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)))
220	219	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤))))
221		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸))
222	221	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
223		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸))
224	222, 223	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
225	224	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐸 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))))
226	220, 225	rspc2ev 3624	. . . . . . . . . 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 𝑤)))
227	215, 226	mp3an3 1449	. . . . . . . . 9 ⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
228	208, 214, 227	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
229		ovex 7445	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ V
230		eqeq1 2735	. . . . . . . . . 10 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))))
231	230	2rexbidv 3218	. . . . . . . . 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 𝑤))))
232	229, 231	elab 3668	. . . . . . . 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 𝑤)))
233	228, 232	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})
234		elun2 4177	. . . . . . 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 𝑤))}))
235	233, 234	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 𝑤))}))
236	194, 197, 235	ssltsepcd 27533	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
237	127, 122	addscomd 27690	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
238	237	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)))
239	122, 127, 107	addsubsassd 27788	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
240	238, 239	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
241	240	breq2d 5160	. . . . . . 7 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
242	127, 107	subscld 27775	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
243	94, 122, 242	sltsubadd2d 27797	. . . . . . 7 ⊢ (𝜑 → (((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
244	241, 243	bitr4d 282	. . . . . 6 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
245	244	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
246	236, 245	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
247	246	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
248	121	simp2d 1142	. . . . . . 7 ⊢ (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
249	248	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
250		simprl 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐷) ∈ ( bday ‘𝐶))
251	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ No )
252	199, 251, 201	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ∈ ( O ‘( bday ‘𝐶)) ↔ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
253	250, 252	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ ( O ‘( bday ‘𝐶)))
254	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐶 <s 𝐷)
255	253, 254, 207	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐷 ∈ ( R ‘𝐶))
256		simprr 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐹) ∈ ( bday ‘𝐸))
257	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ No )
258	145, 257, 147	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐹 ∈ ( O ‘( bday ‘𝐸)) ↔ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
259	256, 258	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( O ‘( bday ‘𝐸)))
260	50	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐸 <s 𝐹)
261	259, 260, 153	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸))
262		eqid 2731	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))
263		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸))
264	263	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)))
265		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠))
266	264, 265	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)))
267	266	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠))))
268		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹))
269	268	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
270		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹))
271	269, 270	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)))
272	271	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑠 = 𝐹 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))))
273	267, 272	rspc2ev 3624	. . . . . . . . . 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 𝑠)))
274	262, 273	mp3an3 1449	. . . . . . . . 9 ⊢ ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
275	255, 261, 274	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
276		ovex 7445	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ V
277		eqeq1 2735	. . . . . . . . . 10 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))))
278	277	2rexbidv 3218	. . . . . . . . 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 𝑠))))
279	276, 278	elab 3668	. . . . . . . 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 𝑠)))
280	275, 279	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})
281		elun2 4177	. . . . . . 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 𝑠))}))
282	280, 281	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 𝑠))}))
283		ovex 7445	. . . . . . . 8 ⊢ (𝐶 ·s 𝐸) ∈ V
284	283	snid 4664	. . . . . . 7 ⊢ (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}
285	284	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)})
286	249, 282, 285	ssltsepcd 27533	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸))
287	107, 94	addscomd 27690	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
288	287	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)))
289	94, 107, 127	addsubsassd 27788	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
290	288, 289	eqtrd 2771	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
291	290	breq1d 5158	. . . . . . . 8 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸)))
292	107, 127	subscld 27775	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) ∈ No )
293	94, 292, 122	sltaddsub2d 27799	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
294	291, 293	bitrd 279	. . . . . . 7 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
295	294, 185	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
296	295	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
297	286, 296	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
298	297	anassrs 467	. . 3 ⊢ (((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
299	190	adantr 480	. . 3 ⊢ ((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) → (( bday ‘𝐸) ∈ ( bday ‘𝐹) ∨ ( bday ‘𝐹) ∈ ( bday ‘𝐸)))
300	247, 298, 299	mpjaodan 956	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
301		mulsproplem12.1	. 2 ⊢ (𝜑 → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
302	192, 300, 301	mpjaodan 956	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105  {cab 2708  ∀wral 3060  ∃wrex 3069   ∪ cun 3946  ∅c0 4322  {csn 4628   class class class wbr 5148  Oncon0 6364  ‘cfv 6543  (class class class)co 7412   +no cnadd 8668   No csur 27380   <s cslt 27381   bday cbday 27382   <<s csslt 27519   0_s c0s 27561   O cold 27576   L cleft 27578   R cright 27579   +_s cadds 27682   -_s csubs 27735   ·_s cmuls 27802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-ot 4637  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-1o 8470  df-2o 8471  df-nadd 8669  df-no 27383  df-slt 27384  df-bday 27385  df-sle 27485  df-sslt 27520  df-scut 27522  df-0s 27563  df-made 27580  df-old 27581  df-left 27583  df-right 27584  df-norec 27661  df-norec2 27672  df-adds 27683  df-negs 27736  df-subs 27737  df-muls 27803

This theorem is referenced by:  mulsproplem13  27824