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