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 ⊢ φ → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
mulsproplem.2 ⊢ φ → C ∈ No
mulsproplem.3 ⊢ φ → D ∈ No
mulsproplem.4 ⊢ φ → E ∈ No
mulsproplem.5 ⊢ φ → F ∈ No
mulsproplem.6 ⊢ φ → C < s D
mulsproplem.7 ⊢ φ → E < s F
mulsproplem12.1 ⊢ φ → bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C
mulsproplem12.2 ⊢ φ → bday ⁡ E ∈ bday ⁡ F ∨ bday ⁡ F ∈ bday ⁡ E
Assertion mulsproplem12 ⊢ φ → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E

Proof

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