MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsproplem12 Structured version   Visualization version   GIF version

Theorem mulsproplem12 27550
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.
StepHypRef 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 4150 . . . . . . . . . . . . . . . . 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 4150 . . . . . . . . . . . . . . . . . 18 ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
4 bday0s 27296 . . . . . . . . . . . . . . . . . . . 20 ( bday ‘ 0s ) = ∅
54, 4oveq12i 7408 . . . . . . . . . . . . . . . . . . 19 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
6 0elon 6410 . . . . . . . . . . . . . . . . . . . 20 ∅ ∈ On
7 naddrid 8670 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ On → (∅ +no ∅) = ∅)
86, 7ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∅ +no ∅) = ∅
95, 8eqtri 2761 . . . . . . . . . . . . . . . . . 18 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
103, 9eqtri 2761 . . . . . . . . . . . . . . . . 17 ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = ∅
112, 10eqtri 2761 . . . . . . . . . . . . . . . 16 (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
1211uneq2i 4158 . . . . . . . . . . . . . . 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 4388 . . . . . . . . . . . . . . 15 ((( bday 𝐷) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐹))
1412, 13eqtri 2761 . . . . . . . . . . . . . 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 4171 . . . . . . . . . . . . . . . 16 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
16 ssun1 4170 . . . . . . . . . . . . . . . 16 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
1715, 16sstri 3989 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
18 ssun2 4171 . . . . . . . . . . . . . . 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 𝐸)))))
1917, 18sstri 3989 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
2014, 19eqsstri 4014 . . . . . . . . . . . . 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 𝐸)))))
2120sseli 3976 . . . . . . . . . . . 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 𝐸))))))
2221imim1i 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 𝑒))))))
23226ralimi 3128 . . . . . . . . . 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 𝑒))))))
241, 23syl 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 )
2724, 25, 26mulsproplem10 27548 . . . . . . . 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 𝑤))})))
2827simp2d 1144 . . . . . . 7 (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ { ∣ ∃𝑟 ∈ ( R ‘𝐷)∃𝑠 ∈ ( R ‘𝐹) = (((𝑟 ·s 𝐹) +s (𝐷 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐷 ·s 𝐹)})
2928adantr 482 . . . . . 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 27245 . . . . . . . . . . . 12 ( bday 𝐷) ∈ On
32 mulsproplem.2 . . . . . . . . . . . . 13 (𝜑𝐶 No )
3332adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐶 No )
34 oldbday 27362 . . . . . . . . . . . 12 ((( bday 𝐷) ∈ On ∧ 𝐶 No ) → (𝐶 ∈ ( O ‘( bday 𝐷)) ↔ ( bday 𝐶) ∈ ( bday 𝐷)))
3531, 33, 34sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐶 ∈ ( O ‘( bday 𝐷)) ↔ ( bday 𝐶) ∈ ( bday 𝐷)))
3630, 35mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐶 ∈ ( O ‘( bday 𝐷)))
37 mulsproplem.6 . . . . . . . . . . 11 (𝜑𝐶 <s 𝐷)
3837adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐶 <s 𝐷)
39 breq1 5147 . . . . . . . . . . 11 (𝑥 = 𝐶 → (𝑥 <s 𝐷𝐶 <s 𝐷))
40 leftval 27325 . . . . . . . . . . 11 ( L ‘𝐷) = {𝑥 ∈ ( O ‘( bday 𝐷)) ∣ 𝑥 <s 𝐷}
4139, 40elrab2 3684 . . . . . . . . . 10 (𝐶 ∈ ( L ‘𝐷) ↔ (𝐶 ∈ ( O ‘( bday 𝐷)) ∧ 𝐶 <s 𝐷))
4236, 38, 41sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐶 ∈ ( L ‘𝐷))
43 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ( bday 𝐸) ∈ ( bday 𝐹))
44 bdayelon 27245 . . . . . . . . . . . 12 ( bday 𝐹) ∈ On
45 mulsproplem.4 . . . . . . . . . . . . 13 (𝜑𝐸 No )
4645adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 No )
47 oldbday 27362 . . . . . . . . . . . 12 ((( bday 𝐹) ∈ On ∧ 𝐸 No ) → (𝐸 ∈ ( O ‘( bday 𝐹)) ↔ ( bday 𝐸) ∈ ( bday 𝐹)))
4844, 46, 47sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐸 ∈ ( O ‘( bday 𝐹)) ↔ ( bday 𝐸) ∈ ( bday 𝐹)))
4943, 48mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 ∈ ( O ‘( bday 𝐹)))
50 mulsproplem.7 . . . . . . . . . . 11 (𝜑𝐸 <s 𝐹)
5150adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 <s 𝐹)
52 breq1 5147 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 <s 𝐹𝐸 <s 𝐹))
53 leftval 27325 . . . . . . . . . . 11 ( L ‘𝐹) = {𝑥 ∈ ( O ‘( bday 𝐹)) ∣ 𝑥 <s 𝐹}
5452, 53elrab2 3684 . . . . . . . . . 10 (𝐸 ∈ ( L ‘𝐹) ↔ (𝐸 ∈ ( O ‘( bday 𝐹)) ∧ 𝐸 <s 𝐹))
5549, 51, 54sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 ∈ ( L ‘𝐹))
56 eqid 2733 . . . . . . . . . 10 (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))
57 oveq1 7403 . . . . . . . . . . . . . 14 (𝑝 = 𝐶 → (𝑝 ·s 𝐹) = (𝐶 ·s 𝐹))
5857oveq1d 7411 . . . . . . . . . . . . 13 (𝑝 = 𝐶 → ((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)))
59 oveq1 7403 . . . . . . . . . . . . 13 (𝑝 = 𝐶 → (𝑝 ·s 𝑞) = (𝐶 ·s 𝑞))
6058, 59oveq12d 7414 . . . . . . . . . . . 12 (𝑝 = 𝐶 → (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)))
6160eqeq2d 2744 . . . . . . . . . . 11 (𝑝 = 𝐶 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞))))
62 oveq2 7404 . . . . . . . . . . . . . 14 (𝑞 = 𝐸 → (𝐷 ·s 𝑞) = (𝐷 ·s 𝐸))
6362oveq2d 7412 . . . . . . . . . . . . 13 (𝑞 = 𝐸 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
64 oveq2 7404 . . . . . . . . . . . . 13 (𝑞 = 𝐸 → (𝐶 ·s 𝑞) = (𝐶 ·s 𝐸))
6563, 64oveq12d 7414 . . . . . . . . . . . 12 (𝑞 = 𝐸 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)))
6665eqeq2d 2744 . . . . . . . . . . 11 (𝑞 = 𝐸 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝐶 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸))))
6761, 66rspc2ev 3622 . . . . . . . . . 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 𝑞)))
6856, 67mp3an3 1451 . . . . . . . . 9 ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
6942, 55, 68syl2anc 585 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)(((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)))
70 ovex 7429 . . . . . . . . 9 (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ V
71 eqeq1 2737 . . . . . . . . . 10 (𝑔 = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) → (𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))))
72712rexbidv 3220 . . . . . . . . 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 𝑞))))
7370, 72elab 3666 . . . . . . . 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 𝑞)))
7469, 73sylibr 233 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) ∈ {𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐷)∃𝑞 ∈ ( L ‘𝐹)𝑔 = (((𝑝 ·s 𝐹) +s (𝐷 ·s 𝑞)) -s (𝑝 ·s 𝑞))})
75 elun1 4174 . . . . . . 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 𝑠))}))
7674, 75syl 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 7429 . . . . . . . 8 (𝐷 ·s 𝐹) ∈ V
7877snid 4660 . . . . . . 7 (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)}
7978a1i 11 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐷 ·s 𝐹) ∈ {(𝐷 ·s 𝐹)})
8029, 76, 79ssltsepcd 27262 . . . . 5 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹))
8111uneq2i 4158 . . . . . . . . . . . . . . . . . . 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 4388 . . . . . . . . . . . . . . . . . . 19 ((( bday 𝐶) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐹))
8381, 82eqtri 2761 . . . . . . . . . . . . . . . . . 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 4170 . . . . . . . . . . . . . . . . . . . 20 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
85 ssun2 4171 . . . . . . . . . . . . . . . . . . . 20 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
8684, 85sstri 3989 . . . . . . . . . . . . . . . . . . 19 (( bday 𝐶) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
8786, 18sstri 3989 . . . . . . . . . . . . . . . . . 18 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8883, 87eqsstri 4014 . . . . . . . . . . . . . . . . 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 𝐸)))))
8988sseli 3976 . . . . . . . . . . . . . . . 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 𝐸))))))
9089imim1i 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 𝑒))))))
91906ralimi 3128 . . . . . . . . . . . . . 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 𝑒))))))
921, 91syl 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 𝑒))))))
9392, 32, 26mulsproplem10 27548 . . . . . . . . . . . 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 𝑤))})))
9493simp1d 1143 . . . . . . . . . . 11 (𝜑 → (𝐶 ·s 𝐹) ∈ No )
9511uneq2i 4158 . . . . . . . . . . . . . . . . . . 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 4388 . . . . . . . . . . . . . . . . . . 19 ((( bday 𝐷) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐸))
9795, 96eqtri 2761 . . . . . . . . . . . . . . . . . 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 4171 . . . . . . . . . . . . . . . . . . . 20 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
9998, 85sstri 3989 . . . . . . . . . . . . . . . . . . 19 (( bday 𝐷) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
10099, 18sstri 3989 . . . . . . . . . . . . . . . . . 18 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
10197, 100eqsstri 4014 . . . . . . . . . . . . . . . . 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 𝐸)))))
102101sseli 3976 . . . . . . . . . . . . . . . 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 𝐸))))))
103102imim1i 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 𝑒))))))
1041036ralimi 3128 . . . . . . . . . . . . . 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 𝑒))))))
1051, 104syl 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 𝑒))))))
106105, 25, 45mulsproplem10 27548 . . . . . . . . . . . 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 𝑤))})))
107106simp1d 1143 . . . . . . . . . . 11 (𝜑 → (𝐷 ·s 𝐸) ∈ No )
10894, 107addscomd 27418 . . . . . . . . . 10 (𝜑 → ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
109108oveq1d 7411 . . . . . . . . 9 (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)))
11011uneq2i 4158 . . . . . . . . . . . . . . . . . 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 4388 . . . . . . . . . . . . . . . . . 18 ((( bday 𝐶) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐸))
112110, 111eqtri 2761 . . . . . . . . . . . . . . . . 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 4170 . . . . . . . . . . . . . . . . . . 19 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
114113, 16sstri 3989 . . . . . . . . . . . . . . . . . 18 (( bday 𝐶) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
115114, 18sstri 3989 . . . . . . . . . . . . . . . . 17 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
116112, 115eqsstri 4014 . . . . . . . . . . . . . . . 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 𝐸)))))
117116sseli 3976 . . . . . . . . . . . . . . 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 𝐸))))))
118117imim1i 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 𝑒))))))
1191186ralimi 3128 . . . . . . . . . . . . 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 𝑒))))))
1201, 119syl 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 𝑒))))))
121120, 32, 45mulsproplem10 27548 . . . . . . . . . . 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 𝑤))})))
122121simp1d 1143 . . . . . . . . . 10 (𝜑 → (𝐶 ·s 𝐸) ∈ No )
123107, 94, 122addsubsassd 27515 . . . . . . . . 9 (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
124109, 123eqtrd 2773 . . . . . . . 8 (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) = ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))))
125124breq1d 5154 . . . . . . 7 (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹)))
12694, 122subscld 27502 . . . . . . . 8 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
12727simp1d 1143 . . . . . . . 8 (𝜑 → (𝐷 ·s 𝐹) ∈ No )
128107, 126, 127sltaddsub2d 27526 . . . . . . 7 (𝜑 → (((𝐷 ·s 𝐸) +s ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸))) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
129125, 128bitrd 279 . . . . . 6 (𝜑 → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
130129adantr 482 . . . . 5 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ((((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐶 ·s 𝐸)) <s (𝐷 ·s 𝐹) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
13180, 130mpbid 231 . . . 4 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
132131anassrs 469 . . 3 (((𝜑 ∧ ( bday 𝐶) ∈ ( bday 𝐷)) ∧ ( bday 𝐸) ∈ ( bday 𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
133106simp3d 1145 . . . . . . 7 (𝜑 → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
134133adantr 482 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → {(𝐷 ·s 𝐸)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐷)∃𝑤 ∈ ( L ‘𝐸)𝑗 = (((𝑣 ·s 𝐸) +s (𝐷 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
135 ovex 7429 . . . . . . . 8 (𝐷 ·s 𝐸) ∈ V
136135snid 4660 . . . . . . 7 (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)}
137136a1i 11 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐷 ·s 𝐸) ∈ {(𝐷 ·s 𝐸)})
138 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ( bday 𝐶) ∈ ( bday 𝐷))
13932adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 No )
14031, 139, 34sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐶 ∈ ( O ‘( bday 𝐷)) ↔ ( bday 𝐶) ∈ ( bday 𝐷)))
141138, 140mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 ∈ ( O ‘( bday 𝐷)))
14237adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 <s 𝐷)
143141, 142, 41sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 ∈ ( L ‘𝐷))
144 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ( bday 𝐹) ∈ ( bday 𝐸))
145 bdayelon 27245 . . . . . . . . . . . 12 ( bday 𝐸) ∈ On
14626adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 No )
147 oldbday 27362 . . . . . . . . . . . 12 ((( bday 𝐸) ∈ On ∧ 𝐹 No ) → (𝐹 ∈ ( O ‘( bday 𝐸)) ↔ ( bday 𝐹) ∈ ( bday 𝐸)))
148145, 146, 147sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐹 ∈ ( O ‘( bday 𝐸)) ↔ ( bday 𝐹) ∈ ( bday 𝐸)))
149144, 148mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 ∈ ( O ‘( bday 𝐸)))
15050adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐸 <s 𝐹)
151 breq2 5148 . . . . . . . . . . 11 (𝑥 = 𝐹 → (𝐸 <s 𝑥𝐸 <s 𝐹))
152 rightval 27326 . . . . . . . . . . 11 ( R ‘𝐸) = {𝑥 ∈ ( O ‘( bday 𝐸)) ∣ 𝐸 <s 𝑥}
153151, 152elrab2 3684 . . . . . . . . . 10 (𝐹 ∈ ( R ‘𝐸) ↔ (𝐹 ∈ ( O ‘( bday 𝐸)) ∧ 𝐸 <s 𝐹))
154149, 150, 153sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 ∈ ( R ‘𝐸))
155 eqid 2733 . . . . . . . . . 10 (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))
156 oveq1 7403 . . . . . . . . . . . . . 14 (𝑡 = 𝐶 → (𝑡 ·s 𝐸) = (𝐶 ·s 𝐸))
157156oveq1d 7411 . . . . . . . . . . . . 13 (𝑡 = 𝐶 → ((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)))
158 oveq1 7403 . . . . . . . . . . . . 13 (𝑡 = 𝐶 → (𝑡 ·s 𝑢) = (𝐶 ·s 𝑢))
159157, 158oveq12d 7414 . . . . . . . . . . . 12 (𝑡 = 𝐶 → (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)))
160159eqeq2d 2744 . . . . . . . . . . 11 (𝑡 = 𝐶 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢))))
161 oveq2 7404 . . . . . . . . . . . . . 14 (𝑢 = 𝐹 → (𝐷 ·s 𝑢) = (𝐷 ·s 𝐹))
162161oveq2d 7412 . . . . . . . . . . . . 13 (𝑢 = 𝐹 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
163 oveq2 7404 . . . . . . . . . . . . 13 (𝑢 = 𝐹 → (𝐶 ·s 𝑢) = (𝐶 ·s 𝐹))
164162, 163oveq12d 7414 . . . . . . . . . . . 12 (𝑢 = 𝐹 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
165164eqeq2d 2744 . . . . . . . . . . 11 (𝑢 = 𝐹 → ((((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝐶 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹))))
166160, 165rspc2ev 3622 . . . . . . . . . 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 𝑢)))
167155, 166mp3an3 1451 . . . . . . . . 9 ((𝐶 ∈ ( L ‘𝐷) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
168143, 154, 167syl2anc 585 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)(((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)))
169 ovex 7429 . . . . . . . . 9 (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ V
170 eqeq1 2737 . . . . . . . . . 10 (𝑖 = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) → (𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))))
1711702rexbidv 3220 . . . . . . . . 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 𝑢))))
172169, 171elab 3666 . . . . . . . 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 𝑢)))
173168, 172sylibr 233 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ∈ {𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐷)∃𝑢 ∈ ( R ‘𝐸)𝑖 = (((𝑡 ·s 𝐸) +s (𝐷 ·s 𝑢)) -s (𝑡 ·s 𝑢))})
174 elun1 4174 . . . . . . 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 𝑤))}))
175173, 174syl 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 𝑤))}))
176134, 137, 175ssltsepcd 27262 . . . . 5 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)))
177122, 127addscomd 27418 . . . . . . . . . . 11 (𝜑 → ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
178177oveq1d 7411 . . . . . . . . . 10 (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)))
179127, 122, 94addsubsassd 27515 . . . . . . . . . 10 (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
180178, 179eqtrd 2773 . . . . . . . . 9 (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) = ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
181180breq2d 5156 . . . . . . . 8 (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
182122, 94subscld 27502 . . . . . . . . 9 (𝜑 → ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ∈ No )
183107, 127, 182sltsubadd2d 27524 . . . . . . . 8 (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ (𝐷 ·s 𝐸) <s ((𝐷 ·s 𝐹) +s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)))))
184181, 183bitr4d 282 . . . . . . 7 (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
185107, 127, 122, 94sltsubsub2bd 27518 . . . . . . 7 (𝜑 → (((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
186184, 185bitrd 279 . . . . . 6 (𝜑 → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
187186adantr 482 . . . . 5 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ((𝐷 ·s 𝐸) <s (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐶 ·s 𝐹)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
188176, 187mpbid 231 . . . 4 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
189188anassrs 469 . . 3 (((𝜑 ∧ ( bday 𝐶) ∈ ( bday 𝐷)) ∧ ( bday 𝐹) ∈ ( bday 𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
190 mulsproplem12.2 . . . 4 (𝜑 → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
191190adantr 482 . . 3 ((𝜑 ∧ ( bday 𝐶) ∈ ( bday 𝐷)) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
192132, 189, 191mpjaodan 958 . 2 ((𝜑 ∧ ( bday 𝐶) ∈ ( bday 𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
19393simp3d 1145 . . . . . . 7 (𝜑 → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
194193adantr 482 . . . . . 6 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → {(𝐶 ·s 𝐹)} <<s ({𝑖 ∣ ∃𝑡 ∈ ( L ‘𝐶)∃𝑢 ∈ ( R ‘𝐹)𝑖 = (((𝑡 ·s 𝐹) +s (𝐶 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))
195 ovex 7429 . . . . . . . 8 (𝐶 ·s 𝐹) ∈ V
196195snid 4660 . . . . . . 7 (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)}
197196a1i 11 . . . . . 6 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐶 ·s 𝐹) ∈ {(𝐶 ·s 𝐹)})
198 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ( bday 𝐷) ∈ ( bday 𝐶))
199 bdayelon 27245 . . . . . . . . . . . 12 ( bday 𝐶) ∈ On
20025adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐷 No )
201 oldbday 27362 . . . . . . . . . . . 12 ((( bday 𝐶) ∈ On ∧ 𝐷 No ) → (𝐷 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝐷) ∈ ( bday 𝐶)))
202199, 200, 201sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐷 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝐷) ∈ ( bday 𝐶)))
203198, 202mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐷 ∈ ( O ‘( bday 𝐶)))
20437adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐶 <s 𝐷)
205 breq2 5148 . . . . . . . . . . 11 (𝑥 = 𝐷 → (𝐶 <s 𝑥𝐶 <s 𝐷))
206 rightval 27326 . . . . . . . . . . 11 ( R ‘𝐶) = {𝑥 ∈ ( O ‘( bday 𝐶)) ∣ 𝐶 <s 𝑥}
207205, 206elrab2 3684 . . . . . . . . . 10 (𝐷 ∈ ( R ‘𝐶) ↔ (𝐷 ∈ ( O ‘( bday 𝐶)) ∧ 𝐶 <s 𝐷))
208203, 204, 207sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐷 ∈ ( R ‘𝐶))
209 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ( bday 𝐸) ∈ ( bday 𝐹))
21045adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 No )
21144, 210, 47sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐸 ∈ ( O ‘( bday 𝐹)) ↔ ( bday 𝐸) ∈ ( bday 𝐹)))
212209, 211mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 ∈ ( O ‘( bday 𝐹)))
21350adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 <s 𝐹)
214212, 213, 54sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → 𝐸 ∈ ( L ‘𝐹))
215 eqid 2733 . . . . . . . . . 10 (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))
216 oveq1 7403 . . . . . . . . . . . . . 14 (𝑣 = 𝐷 → (𝑣 ·s 𝐹) = (𝐷 ·s 𝐹))
217216oveq1d 7411 . . . . . . . . . . . . 13 (𝑣 = 𝐷 → ((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)))
218 oveq1 7403 . . . . . . . . . . . . 13 (𝑣 = 𝐷 → (𝑣 ·s 𝑤) = (𝐷 ·s 𝑤))
219217, 218oveq12d 7414 . . . . . . . . . . . 12 (𝑣 = 𝐷 → (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)))
220219eqeq2d 2744 . . . . . . . . . . 11 (𝑣 = 𝐷 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤))))
221 oveq2 7404 . . . . . . . . . . . . . 14 (𝑤 = 𝐸 → (𝐶 ·s 𝑤) = (𝐶 ·s 𝐸))
222221oveq2d 7412 . . . . . . . . . . . . 13 (𝑤 = 𝐸 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) = ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)))
223 oveq2 7404 . . . . . . . . . . . . 13 (𝑤 = 𝐸 → (𝐷 ·s 𝑤) = (𝐷 ·s 𝐸))
224222, 223oveq12d 7414 . . . . . . . . . . . 12 (𝑤 = 𝐸 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
225224eqeq2d 2744 . . . . . . . . . . 11 (𝑤 = 𝐸 → ((((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝐷 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸))))
226220, 225rspc2ev 3622 . . . . . . . . . 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 𝑤)))
227215, 226mp3an3 1451 . . . . . . . . 9 ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐸 ∈ ( L ‘𝐹)) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
228208, 214, 227syl2anc 585 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)(((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)))
229 ovex 7429 . . . . . . . . 9 (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ V
230 eqeq1 2737 . . . . . . . . . 10 (𝑗 = (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) → (𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))))
2312302rexbidv 3220 . . . . . . . . 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 𝑤))))
232229, 231elab 3666 . . . . . . . 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 𝑤)))
233228, 232sylibr 233 . . . . . . 7 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ∈ {𝑗 ∣ ∃𝑣 ∈ ( R ‘𝐶)∃𝑤 ∈ ( L ‘𝐹)𝑗 = (((𝑣 ·s 𝐹) +s (𝐶 ·s 𝑤)) -s (𝑣 ·s 𝑤))})
234 elun2 4175 . . . . . . 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 𝑤))}))
235233, 234syl 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 𝑤))}))
236194, 197, 235ssltsepcd 27262 . . . . 5 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → (𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)))
237127, 122addscomd 27418 . . . . . . . . . 10 (𝜑 → ((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)))
238237oveq1d 7411 . . . . . . . . 9 (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)))
239122, 127, 107addsubsassd 27515 . . . . . . . . 9 (𝜑 → (((𝐶 ·s 𝐸) +s (𝐷 ·s 𝐹)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
240238, 239eqtrd 2773 . . . . . . . 8 (𝜑 → (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) = ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
241240breq2d 5156 . . . . . . 7 (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
242127, 107subscld 27502 . . . . . . . 8 (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
24394, 122, 242sltsubadd2d 27524 . . . . . . 7 (𝜑 → (((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ↔ (𝐶 ·s 𝐹) <s ((𝐶 ·s 𝐸) +s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
244241, 243bitr4d 282 . . . . . 6 (𝜑 → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
245244adantr 482 . . . . 5 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ((𝐶 ·s 𝐹) <s (((𝐷 ·s 𝐹) +s (𝐶 ·s 𝐸)) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
246236, 245mpbid 231 . . . 4 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐸) ∈ ( bday 𝐹))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
247246anassrs 469 . . 3 (((𝜑 ∧ ( bday 𝐷) ∈ ( bday 𝐶)) ∧ ( bday 𝐸) ∈ ( bday 𝐹)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
248121simp2d 1144 . . . . . . 7 (𝜑 → ({𝑔 ∣ ∃𝑝 ∈ ( L ‘𝐶)∃𝑞 ∈ ( L ‘𝐸)𝑔 = (((𝑝 ·s 𝐸) +s (𝐶 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ { ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐶 ·s 𝐸)})
249248adantr 482 . . . . . 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 𝐶))
25125adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐷 No )
252199, 251, 201sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐷 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝐷) ∈ ( bday 𝐶)))
253250, 252mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐷 ∈ ( O ‘( bday 𝐶)))
25437adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐶 <s 𝐷)
255253, 254, 207sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐷 ∈ ( R ‘𝐶))
256 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ( bday 𝐹) ∈ ( bday 𝐸))
25726adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 No )
258145, 257, 147sylancr 588 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐹 ∈ ( O ‘( bday 𝐸)) ↔ ( bday 𝐹) ∈ ( bday 𝐸)))
259256, 258mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 ∈ ( O ‘( bday 𝐸)))
26050adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐸 <s 𝐹)
261259, 260, 153sylanbrc 584 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → 𝐹 ∈ ( R ‘𝐸))
262 eqid 2733 . . . . . . . . . 10 (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))
263 oveq1 7403 . . . . . . . . . . . . . 14 (𝑟 = 𝐷 → (𝑟 ·s 𝐸) = (𝐷 ·s 𝐸))
264263oveq1d 7411 . . . . . . . . . . . . 13 (𝑟 = 𝐷 → ((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)))
265 oveq1 7403 . . . . . . . . . . . . 13 (𝑟 = 𝐷 → (𝑟 ·s 𝑠) = (𝐷 ·s 𝑠))
266264, 265oveq12d 7414 . . . . . . . . . . . 12 (𝑟 = 𝐷 → (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)))
267266eqeq2d 2744 . . . . . . . . . . 11 (𝑟 = 𝐷 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠))))
268 oveq2 7404 . . . . . . . . . . . . . 14 (𝑠 = 𝐹 → (𝐶 ·s 𝑠) = (𝐶 ·s 𝐹))
269268oveq2d 7412 . . . . . . . . . . . . 13 (𝑠 = 𝐹 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) = ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)))
270 oveq2 7404 . . . . . . . . . . . . 13 (𝑠 = 𝐹 → (𝐷 ·s 𝑠) = (𝐷 ·s 𝐹))
271269, 270oveq12d 7414 . . . . . . . . . . . 12 (𝑠 = 𝐹 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)))
272271eqeq2d 2744 . . . . . . . . . . 11 (𝑠 = 𝐹 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝐷 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹))))
273267, 272rspc2ev 3622 . . . . . . . . . 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 𝑠)))
274262, 273mp3an3 1451 . . . . . . . . 9 ((𝐷 ∈ ( R ‘𝐶) ∧ 𝐹 ∈ ( R ‘𝐸)) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
275255, 261, 274syl2anc 585 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸)(((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)))
276 ovex 7429 . . . . . . . . 9 (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ V
277 eqeq1 2737 . . . . . . . . . 10 ( = (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) → ( = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))))
2782772rexbidv 3220 . . . . . . . . 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 𝑠))))
279276, 278elab 3666 . . . . . . . 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 𝑠)))
280275, 279sylibr 233 . . . . . . 7 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) ∈ { ∣ ∃𝑟 ∈ ( R ‘𝐶)∃𝑠 ∈ ( R ‘𝐸) = (((𝑟 ·s 𝐸) +s (𝐶 ·s 𝑠)) -s (𝑟 ·s 𝑠))})
281 elun2 4175 . . . . . . 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 𝑠))}))
282280, 281syl 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 7429 . . . . . . . 8 (𝐶 ·s 𝐸) ∈ V
284283snid 4660 . . . . . . 7 (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)}
285284a1i 11 . . . . . 6 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (𝐶 ·s 𝐸) ∈ {(𝐶 ·s 𝐸)})
286249, 282, 285ssltsepcd 27262 . . . . 5 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸))
287107, 94addscomd 27418 . . . . . . . . . . 11 (𝜑 → ((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)))
288287oveq1d 7411 . . . . . . . . . 10 (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)))
28994, 107, 127addsubsassd 27515 . . . . . . . . . 10 (𝜑 → (((𝐶 ·s 𝐹) +s (𝐷 ·s 𝐸)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
290288, 289eqtrd 2773 . . . . . . . . 9 (𝜑 → (((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) = ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))))
291290breq1d 5154 . . . . . . . 8 (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸)))
292107, 127subscld 27502 . . . . . . . . 9 (𝜑 → ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) ∈ No )
29394, 292, 122sltaddsub2d 27526 . . . . . . . 8 (𝜑 → (((𝐶 ·s 𝐹) +s ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹))) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
294291, 293bitrd 279 . . . . . . 7 (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐷 ·s 𝐸) -s (𝐷 ·s 𝐹)) <s ((𝐶 ·s 𝐸) -s (𝐶 ·s 𝐹))))
295294, 185bitrd 279 . . . . . 6 (𝜑 → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
296295adantr 482 . . . . 5 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ((((𝐷 ·s 𝐸) +s (𝐶 ·s 𝐹)) -s (𝐷 ·s 𝐹)) <s (𝐶 ·s 𝐸) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
297286, 296mpbid 231 . . . 4 ((𝜑 ∧ (( bday 𝐷) ∈ ( bday 𝐶) ∧ ( bday 𝐹) ∈ ( bday 𝐸))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
298297anassrs 469 . . 3 (((𝜑 ∧ ( bday 𝐷) ∈ ( bday 𝐶)) ∧ ( bday 𝐹) ∈ ( bday 𝐸)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
299190adantr 482 . . 3 ((𝜑 ∧ ( bday 𝐷) ∈ ( bday 𝐶)) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
300247, 298, 299mpjaodan 958 . 2 ((𝜑 ∧ ( bday 𝐷) ∈ ( bday 𝐶)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
301 mulsproplem12.1 . 2 (𝜑 → (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
302192, 300, 301mpjaodan 958 1 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  {cab 2710  wral 3062  wrex 3071  cun 3944  c0 4320  {csn 4624   class class class wbr 5144  Oncon0 6356  cfv 6535  (class class class)co 7396   +no cnadd 8652   No csur 27110   <s cslt 27111   bday cbday 27112   <<s csslt 27249   0s c0s 27290   O cold 27305   L cleft 27307   R cright 27308   +s cadds 27410   -s csubs 27462   ·s cmuls 27529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-ot 4633  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-1o 8453  df-2o 8454  df-nadd 8653  df-no 27113  df-slt 27114  df-bday 27115  df-sle 27215  df-sslt 27250  df-scut 27252  df-0s 27292  df-made 27309  df-old 27310  df-left 27312  df-right 27313  df-norec 27389  df-norec2 27400  df-adds 27411  df-negs 27463  df-subs 27464  df-muls 27530
This theorem is referenced by:  mulsproplem13  27551
  Copyright terms: Public domain W3C validator