Metamath Proof Explorer

Theorem mulsproplem13

Description: Lemma for surreal multiplication. Remove the restriction on C and D from mulsproplem12 . (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
mulsproplem13.1 ⊢ φ → bday ⁡ E ∈ bday ⁡ F ∨ bday ⁡ F ∈ bday ⁡ E
Assertion mulsproplem13 ⊢ φ → 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 mulsproplem13.1 ⊢ φ → bday ⁡ E ∈ bday ⁡ F ∨ bday ⁡ F ∈ bday ⁡ E
9 1 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → ∀ 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
10 2 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → C ∈ No
11 3 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → D ∈ No
12 4 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → E ∈ No
13 5 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → F ∈ No
14 6 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → C < s D
15 7 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → E < s F
16 simpr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C
17 8 adantr ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → bday ⁡ E ∈ bday ⁡ F ∨ bday ⁡ F ∈ bday ⁡ E
18 9 10 11 12 13 14 15 16 17 mulsproplem12 ⊢ φ ∧ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E
19 2 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D → C ∈ No
20 3 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D → D ∈ No
21 simpr ⊢ φ ∧ bday ⁡ C = bday ⁡ D → bday ⁡ C = bday ⁡ D
22 6 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D → C < s D
23 nodense ⊢ C ∈ No ∧ D ∈ No ∧ bday ⁡ C = bday ⁡ D ∧ C < s D → ∃ x ∈ No bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D
24 19 20 21 22 23 syl22anc ⊢ φ ∧ bday ⁡ C = bday ⁡ D → ∃ x ∈ No bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D
25 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
26 unidm ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = bday ⁡ 0 s + bday ⁡ 0 s
27 bday0s ⊢ bday ⁡ 0 s = ∅
28 27 27 oveq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅ + ∅
29 0elon ⊢ ∅ ∈ On
30 naddrid ⊢ ∅ ∈ On → ∅ + ∅ = ∅
31 29 30 ax-mp ⊢ ∅ + ∅ = ∅
32 28 31 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅
33 25 26 32 3eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅
34 33 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 ∪ ∅
35 un0 ⊢ bday ⁡ C + bday ⁡ F ∪ ∅ = bday ⁡ C + bday ⁡ F
36 34 35 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
37 ssun1 ⊢ bday ⁡ C + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
38 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
39 37 38 sstri ⊢ bday ⁡ C + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
40 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
41 39 40 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
42 36 41 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
43 42 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
44 43 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
45 44 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
46 1 45 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
47 46 2 5 mulsproplem11 ⊢ φ → C ⋅ s F ∈ No
48 33 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 ∪ ∅
49 un0 ⊢ bday ⁡ C + bday ⁡ E ∪ ∅ = bday ⁡ C + bday ⁡ E
50 48 49 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
51 ssun1 ⊢ bday ⁡ C + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
52 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
53 51 52 sstri ⊢ bday ⁡ C + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
54 53 40 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
55 50 54 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
56 55 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
57 56 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
58 57 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
59 1 58 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
60 59 2 4 mulsproplem11 ⊢ φ → C ⋅ s E ∈ No
61 47 60 subscld ⊢ φ → C ⋅ s F - s C ⋅ s E ∈ No
62 61 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C ⋅ s F - s C ⋅ s E ∈ No
63 46 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ 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
64 simprr1 ⊢ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ∈ bday ⁡ C
65 64 adantl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ∈ bday ⁡ C
66 bdayelon ⊢ bday ⁡ C ∈ On
67 simprrl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ∈ No
68 oldbday ⊢ bday ⁡ C ∈ On ∧ x ∈ No → x ∈ Old ⁡ bday ⁡ C ↔ bday ⁡ x ∈ bday ⁡ C
69 66 67 68 sylancr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ∈ Old ⁡ bday ⁡ C ↔ bday ⁡ x ∈ bday ⁡ C
70 65 69 mpbird ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ∈ Old ⁡ bday ⁡ C
71 5 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → F ∈ No
72 63 70 71 mulsproplem2 ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ⋅ s F ∈ No
73 59 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ 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
74 4 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → E ∈ No
75 73 70 74 mulsproplem2 ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ⋅ s E ∈ No
76 72 75 subscld ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ⋅ s F - s x ⋅ s E ∈ No
77 33 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 ∪ ∅
78 un0 ⊢ bday ⁡ D + bday ⁡ F ∪ ∅ = bday ⁡ D + bday ⁡ F
79 77 78 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
80 ssun2 ⊢ bday ⁡ D + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
81 80 52 sstri ⊢ bday ⁡ D + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
82 81 40 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
83 79 82 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
84 83 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
85 84 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
86 85 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
87 1 86 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
88 87 3 5 mulsproplem11 ⊢ φ → D ⋅ s F ∈ No
89 33 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 ∪ ∅
90 un0 ⊢ bday ⁡ D + bday ⁡ E ∪ ∅ = bday ⁡ D + bday ⁡ E
91 89 90 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
92 ssun2 ⊢ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
93 92 38 sstri ⊢ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
94 93 40 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
95 91 94 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
96 95 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
97 96 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
98 97 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
99 1 98 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
100 99 3 4 mulsproplem11 ⊢ φ → D ⋅ s E ∈ No
101 88 100 subscld ⊢ φ → D ⋅ s F - s D ⋅ s E ∈ No
102 101 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → D ⋅ s F - s D ⋅ s E ∈ No
103 1 mulsproplemcbv ⊢ φ → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
104 103 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
105 onelss ⊢ bday ⁡ C ∈ On → bday ⁡ x ∈ bday ⁡ C → bday ⁡ x ⊆ bday ⁡ C
106 66 65 105 mpsyl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ⊆ bday ⁡ C
107 simprl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ C = bday ⁡ D
108 106 107 sseqtrd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ⊆ bday ⁡ D
109 bdayelon ⊢ bday ⁡ x ∈ On
110 bdayelon ⊢ bday ⁡ D ∈ On
111 bdayelon ⊢ bday ⁡ F ∈ On
112 naddss1 ⊢ bday ⁡ x ∈ On ∧ bday ⁡ D ∈ On ∧ bday ⁡ F ∈ On → bday ⁡ x ⊆ bday ⁡ D ↔ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ D + bday ⁡ F
113 109 110 111 112 mp3an ⊢ bday ⁡ x ⊆ bday ⁡ D ↔ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ D + bday ⁡ F
114 108 113 sylib ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ F ⊆ bday ⁡ D + bday ⁡ F
115 unss2 ⊢ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ D + bday ⁡ F → bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
116 114 115 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
117 bdayelon ⊢ bday ⁡ E ∈ On
118 naddss1 ⊢ bday ⁡ x ∈ On ∧ bday ⁡ D ∈ On ∧ bday ⁡ E ∈ On → bday ⁡ x ⊆ bday ⁡ D ↔ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ D + bday ⁡ E
119 109 110 117 118 mp3an ⊢ bday ⁡ x ⊆ bday ⁡ D ↔ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ D + bday ⁡ E
120 108 119 sylib ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ E ⊆ bday ⁡ D + bday ⁡ E
121 unss2 ⊢ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ D + bday ⁡ E → bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
122 120 121 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
123 unss12 ⊢ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∧ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
124 116 122 123 syl2anc ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
125 unss2 ⊢ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ 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 ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
126 124 125 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
127 126 sseld ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
128 127 imim1d ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
129 128 ralimd6v ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
130 104 129 mpd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ x + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
131 2 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C ∈ No
132 simprr2 ⊢ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C < s x
133 132 adantl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C < s x
134 7 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → E < s F
135 65 olcd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ C ∈ bday ⁡ x ∨ bday ⁡ x ∈ bday ⁡ C
136 8 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ E ∈ bday ⁡ F ∨ bday ⁡ F ∈ bday ⁡ E
137 130 131 67 74 71 133 134 135 136 mulsproplem12 ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C ⋅ s F - s C ⋅ s E < s x ⋅ s F - s x ⋅ s E
138 naddss1 ⊢ bday ⁡ x ∈ On ∧ bday ⁡ C ∈ On ∧ bday ⁡ E ∈ On → bday ⁡ x ⊆ bday ⁡ C ↔ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E
139 109 66 117 138 mp3an ⊢ bday ⁡ x ⊆ bday ⁡ C ↔ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E
140 106 139 sylib ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E
141 unss1 ⊢ bday ⁡ x + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E → bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
142 140 141 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F
143 naddss1 ⊢ bday ⁡ x ∈ On ∧ bday ⁡ C ∈ On ∧ bday ⁡ F ∈ On → bday ⁡ x ⊆ bday ⁡ C ↔ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ F
144 109 66 111 143 mp3an ⊢ bday ⁡ x ⊆ bday ⁡ C ↔ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ F
145 106 144 sylib ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ F
146 unss1 ⊢ bday ⁡ x + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ F → bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
147 145 146 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
148 unss12 ⊢ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∧ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
149 142 147 148 syl2anc ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
150 unss2 ⊢ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ⊆ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + 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
151 149 150 syl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + 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
152 151 sseld ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
153 152 imim1d ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
154 153 ralimd6v ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
155 104 154 mpd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No ∀ k ∈ No ∀ l ∈ No bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ x + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ x + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → g ⋅ s h ∈ No ∧ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
156 3 adantr ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → D ∈ No
157 simprr3 ⊢ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x < s D
158 157 adantl ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x < s D
159 65 107 eleqtrd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ∈ bday ⁡ D
160 159 orcd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → bday ⁡ x ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ x
161 155 67 156 74 71 158 134 160 136 mulsproplem12 ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → x ⋅ s F - s x ⋅ s E < s D ⋅ s F - s D ⋅ s E
162 62 76 102 137 161 slttrd ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E
163 162 anassrs ⊢ φ ∧ bday ⁡ C = bday ⁡ D ∧ x ∈ No ∧ bday ⁡ x ∈ bday ⁡ C ∧ C < s x ∧ x < s D → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E
164 24 163 rexlimddv ⊢ φ ∧ bday ⁡ C = bday ⁡ D → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E
165 66 onordi ⊢ Ord ⁡ bday ⁡ C
166 110 onordi ⊢ Ord ⁡ bday ⁡ D
167 ordtri3or ⊢ Ord ⁡ bday ⁡ C ∧ Ord ⁡ bday ⁡ D → bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C
168 165 166 167 mp2an ⊢ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C
169 df-3or ⊢ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ↔ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C
170 or32 ⊢ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ↔ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ∨ bday ⁡ C = bday ⁡ D
171 169 170 bitri ⊢ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ C = bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ↔ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ∨ bday ⁡ C = bday ⁡ D
172 168 171 mpbi ⊢ bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ∨ bday ⁡ C = bday ⁡ D
173 172 a1i ⊢ φ → bday ⁡ C ∈ bday ⁡ D ∨ bday ⁡ D ∈ bday ⁡ C ∨ bday ⁡ C = bday ⁡ D
174 18 164 173 mpjaodan ⊢ φ → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E