Metamath Proof Explorer

Theorem mulsproplem14

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