Theorem mulsproplem12 28171

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 4180	. . . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
4		bday0s 27891	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( bday ‘ 0s ) = ∅
5	4, 4	oveq12i 7460	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
6		0elon 6449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
7		naddrid 8739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ On → (∅ +no ∅) = ∅)
8	6, 7	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ +no ∅) = ∅
9	5, 8	eqtri 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
10	3, 9	eqtri 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = ∅
11	2, 10	eqtri 2768	. . . . . . . . . . . . . . . 16 ⊢ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
12	11	uneq2i 4188	. . . . . . . . . . . . . . 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 4417	. . . . . . . . . . . . . . 15 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐹))
14	12, 13	eqtri 2768	. . . . . . . . . . . . . 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 4202	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
16		ssun1 4201	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
17	15, 16	sstri 4018	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
18		ssun2 4202	. . . . . . . . . . . . . . 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 4018	. . . . . . . . . . . . . 14 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
20	14, 19	eqsstri 4043	. . . . . . . . . . . . 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 4004	. . . . . . . . . . . 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 3133	. . . . . . . . . 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 28169	. . . . . . . 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 27839	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐷) ∈ On
32		mulsproplem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ No )
33	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ No )
34		oldbday 27957	. . . . . . . . . . . 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 5169	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 <s 𝐷 ↔ 𝐶 <s 𝐷))
40		leftval 27920	. . . . . . . . . . 11 ⊢ ( L ‘𝐷) = {𝑥 ∈ ( O ‘( bday ‘𝐷)) ∣ 𝑥 <s 𝐷}
41	39, 40	elrab2 3711	. . . . . . . . . 10 ⊢ (𝐶 ∈ ( L ‘𝐷) ↔ (𝐶 ∈ ( O ‘( bday ‘𝐷)) ∧ 𝐶 <s 𝐷))
42	36, 38, 41	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐶 ∈ ( L ‘𝐷))
43		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐸) ∈ ( bday ‘𝐹))
44		bdayelon 27839	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐹) ∈ On
45		mulsproplem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ No )
46	45	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ No )
47		oldbday 27957	. . . . . . . . . . . 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 5169	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 <s 𝐹 ↔ 𝐸 <s 𝐹))
53		leftval 27920	. . . . . . . . . . 11 ⊢ ( L ‘𝐹) = {𝑥 ∈ ( O ‘( bday ‘𝐹)) ∣ 𝑥 <s 𝐹}
54	52, 53	elrab2 3711	. . . . . . . . . 10 ⊢ (𝐸 ∈ ( L ‘𝐹) ↔ (𝐸 ∈ ( O ‘( bday ‘𝐹)) ∧ 𝐸 <s 𝐹))
55	49, 51, 54	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐸 ∈ ( L ‘𝐹))
56		eqid 2740	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))
57		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹))
58	57	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)))
59		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞))
60	58, 59	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)))
61	60	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞))))
62		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸))
63	62	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
64		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸))
65	63, 64	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)))
66	65	eqeq2d 2751	. . . . . . . . . . 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 3648	. . . . . . . . . 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 1450	. . . . . . . . 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 7481	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ V
71		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))))
72	71	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))))
73	70, 72	elab 3694	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))})
75		elun1 4205	. . . . . . 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 7481	. . . . . . . 8 ⊢ (𝐷 ·s 𝐹) ∈ V
78	77	snid 4684	. . . . . . 7 ⊢ (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}
79	78	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)})
80	29, 76, 79	ssltsepcd 27857	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹))
81	11	uneq2i 4188	. . . . . . . . . . . . . . . . . . 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 4417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐹))
83	81, 82	eqtri 2768	. . . . . . . . . . . . . . . . . 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 4201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
85		ssun2 4202	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
86	84, 85	sstri 4018	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
87	86, 18	sstri 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐹)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
88	83, 87	eqsstri 4043	. . . . . . . . . . . . . . . . 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 4004	. . . . . . . . . . . . . . . 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 3133	. . . . . . . . . . . . . 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 28169	. . . . . . . . . . . 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 1142	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ·s 𝐹) ∈ No )
95	11	uneq2i 4188	. . . . . . . . . . . . . . . . . . 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 4417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( bday ‘𝐷) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐷) +no ( bday ‘𝐸))
97	95, 96	eqtri 2768	. . . . . . . . . . . . . . . . . 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 4202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))
99	98, 85	sstri 4018	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
100	99, 18	sstri 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐷) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
101	97, 100	eqsstri 4043	. . . . . . . . . . . . . . . . 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 4004	. . . . . . . . . . . . . . . 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 3133	. . . . . . . . . . . . . 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 28169	. . . . . . . . . . . 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 1142	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 ·s 𝐸) ∈ No )
108	94, 107	addscomd 28018	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
109	108	oveq1d 7463	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)))
110	11	uneq2i 4188	. . . . . . . . . . . . . . . . . 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 4417	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ ∅) = (( bday ‘𝐶) +no ( bday ‘𝐸))
112	110, 111	eqtri 2768	. . . . . . . . . . . . . . . . 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 4201	. . . . . . . . . . . . . . . . . . 19 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹)))
114	113, 16	sstri 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
115	114, 18	sstri 4018	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝐶) +no ( bday ‘𝐸)) ⊆ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
116	112, 115	eqsstri 4043	. . . . . . . . . . . . . . . 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 4004	. . . . . . . . . . . . . . 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 3133	. . . . . . . . . . . . 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 28169	. . . . . . . . . . 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 1142	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ·s 𝐸) ∈ No )
123	107, 94, 122	addsubsassd 28129	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
124	109, 123	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
125	124	breq1d 5176	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹)))
126	94, 122	subscld 28111	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
127	27	simp1d 1142	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ·s 𝐹) ∈ No )
128	107, 126, 127	sltaddsub2d 28140	. . . . . . 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 232	. . . 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 1144	. . . . . . 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 7481	. . . . . . . 8 ⊢ (𝐷 ·s 𝐸) ∈ V
136	135	snid 4684	. . . . . . 7 ⊢ (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}
137	136	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)})
138		simprl 770	. . . . . . . . . . 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 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → ( bday ‘𝐹) ∈ ( bday ‘𝐸))
145		bdayelon 27839	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐸) ∈ On
146	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ No )
147		oldbday 27957	. . . . . . . . . . . 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 5170	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐹 → (𝐸 <s 𝑥 ↔ 𝐸 <s 𝐹))
152		rightval 27921	. . . . . . . . . . 11 ⊢ ( R ‘𝐸) = {𝑥 ∈ ( O ‘( bday ‘𝐸)) ∣ 𝐸 <s 𝑥}
153	151, 152	elrab2 3711	. . . . . . . . . 10 ⊢ (𝐹 ∈ ( R ‘𝐸) ↔ (𝐹 ∈ ( O ‘( bday ‘𝐸)) ∧ 𝐸 <s 𝐹))
154	149, 150, 153	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → 𝐹 ∈ ( R ‘𝐸))
155		eqid 2740	. . . . . . . . . 10 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))
156		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸))
157	156	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)))
158		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢))
159	157, 158	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)))
160	159	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢))))
161		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹))
162	161	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
163		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹))
164	162, 163	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
165	164	eqeq2d 2751	. . . . . . . . . . 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 3648	. . . . . . . . . 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 1450	. . . . . . . . 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 7481	. . . . . . . . 9 ⊢ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ V
170		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))))
171	170	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))))
172	169, 171	elab 3694	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))})
174		elun1 4205	. . . . . . 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 27857	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
177	122, 127	addscomd 28018	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
178	177	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)))
179	127, 122, 94	addsubsassd 28129	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
180	178, 179	eqtrd 2780	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
181	180	breq2d 5178	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
182	122, 94	subscld 28111	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ∈ No )
183	107, 127, 182	sltsubadd2d 28138	. . . . . . . 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 28132	. . . . . . 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 232	. . . 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 959	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐶) ∈ ( bday ‘𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
193	93	simp3d 1144	. . . . . . 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 7481	. . . . . . . 8 ⊢ (𝐶 ·s 𝐹) ∈ V
196	195	snid 4684	. . . . . . 7 ⊢ (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}
197	196	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)})
198		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → ( bday ‘𝐷) ∈ ( bday ‘𝐶))
199		bdayelon 27839	. . . . . . . . . . . 12 ⊢ ( bday ‘𝐶) ∈ On
200	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ No )
201		oldbday 27957	. . . . . . . . . . . 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 5170	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (𝐶 <s 𝑥 ↔ 𝐶 <s 𝐷))
206		rightval 27921	. . . . . . . . . . 11 ⊢ ( R ‘𝐶) = {𝑥 ∈ ( O ‘( bday ‘𝐶)) ∣ 𝐶 <s 𝑥}
207	205, 206	elrab2 3711	. . . . . . . . . 10 ⊢ (𝐷 ∈ ( R ‘𝐶) ↔ (𝐷 ∈ ( O ‘( bday ‘𝐶)) ∧ 𝐶 <s 𝐷))
208	203, 204, 207	sylanbrc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → 𝐷 ∈ ( R ‘𝐶))
209		simprr 772	. . . . . . . . . . 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 2740	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))
216		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹))
217	216	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)))
218		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤))
219	217, 218	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)))
220	219	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤))))
221		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸))
222	221	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
223		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸))
224	222, 223	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
225	224	eqeq2d 2751	. . . . . . . . . . 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 3648	. . . . . . . . . 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 1450	. . . . . . . . 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 7481	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ V
230		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))))
231	230	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))))
232	229, 231	elab 3694	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})
234		elun2 4206	. . . . . . 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 27857	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐸) ∈ ( bday ‘𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
237	127, 122	addscomd 28018	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
238	237	oveq1d 7463	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)))
239	122, 127, 107	addsubsassd 28129	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
240	238, 239	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
241	240	breq2d 5178	. . . . . . 7 ⊢ (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
242	127, 107	subscld 28111	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
243	94, 122, 242	sltsubadd2d 28138	. . . . . . 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 232	. . . 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 1143	. . . . . . 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 770	. . . . . . . . . . 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 772	. . . . . . . . . . 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 2740	. . . . . . . . . 10 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))
263		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸))
264	263	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)))
265		oveq1 7455	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠))
266	264, 265	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)))
267	266	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠))))
268		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹))
269	268	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
270		oveq2 7456	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹))
271	269, 270	oveq12d 7466	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)))
272	271	eqeq2d 2751	. . . . . . . . . . 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 3648	. . . . . . . . . 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 1450	. . . . . . . . 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 7481	. . . . . . . . 9 ⊢ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ V
277		eqeq1 2744	. . . . . . . . . 10 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))))
278	277	2rexbidv 3228	. . . . . . . . 9 ⊢ (ℎ = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → (∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))))
279	276, 278	elab 3694	. . . . . . . 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 234	. . . . . . 7 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ {ℎ ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)ℎ = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})
281		elun2 4206	. . . . . . 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 7481	. . . . . . . 8 ⊢ (𝐶 ·s 𝐸) ∈ V
284	283	snid 4684	. . . . . . 7 ⊢ (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}
285	284	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)})
286	249, 282, 285	ssltsepcd 27857	. . . . 5 ⊢ ((𝜑 ∧ (( bday ‘𝐷) ∈ ( bday ‘𝐶) ∧ ( bday ‘𝐹) ∈ ( bday ‘𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸))
287	107, 94	addscomd 28018	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
288	287	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)))
289	94, 107, 127	addsubsassd 28129	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
290	288, 289	eqtrd 2780	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
291	290	breq1d 5176	. . . . . . . 8 ⊢ (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸)))
292	107, 127	subscld 28111	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) ∈ No )
293	94, 292, 122	sltaddsub2d 28140	. . . . . . . 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 232	. . . 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 959	. 2 ⊢ ((𝜑 ∧ ( bday ‘𝐷) ∈ ( bday ‘𝐶)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
301		mulsproplem12.1	. 2 ⊢ (𝜑 → (( bday ‘𝐶) ∈ ( bday ‘𝐷) ∨ ( bday ‘𝐷) ∈ ( bday ‘𝐶)))
302	192, 300, 301	mpjaodan 959	1 ⊢ (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108  {cab 2717  ∀wral 3067  ∃wrex 3076   ∪ cun 3974  ∅c0 4352  {csn 4648   class class class wbr 5166  Oncon0 6395  ‘cfv 6573  (class class class)co 7448   +no cnadd 8721   No csur 27702   <s cslt 27703   bday cbday 27704   <<s csslt 27843   0_s c0s 27885   O cold 27900   L cleft 27902   R cright 27903   +_s cadds 28010   -_s csubs 28070   ·_s cmuls 28150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-ot 4657  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-1o 8522  df-2o 8523  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sle 27808  df-sslt 27844  df-scut 27846  df-0s 27887  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec 27989  df-norec2 28000  df-adds 28011  df-negs 28071  df-subs 28072  df-muls 28151

This theorem is referenced by:  mulsproplem13  28172