Metamath Proof Explorer

Theorem mulsproplem12

Description: Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming C and D are not the same age and E and F are not the same age. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses 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 mulsproplem12 ( 𝜑 → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )

Proof

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