Metamath Proof Explorer

Theorem mulsproplem6

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (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
mulsproplem6.1 ⊢ φ → A ∈ No
mulsproplem6.2 ⊢ φ → B ∈ No
mulsproplem6.3 ⊢ φ → P ∈ L ⁡ A
mulsproplem6.4 ⊢ φ → Q ∈ L ⁡ B
mulsproplem6.5 ⊢ φ → V ∈ R ⁡ A
mulsproplem6.6 ⊢ φ → W ∈ L ⁡ B
Assertion mulsproplem6 ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W

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 mulsproplem6.1 ⊢ φ → A ∈ No
3 mulsproplem6.2 ⊢ φ → B ∈ No
4 mulsproplem6.3 ⊢ φ → P ∈ L ⁡ A
5 mulsproplem6.4 ⊢ φ → Q ∈ L ⁡ B
6 mulsproplem6.5 ⊢ φ → V ∈ R ⁡ A
7 mulsproplem6.6 ⊢ φ → W ∈ L ⁡ B
8 5 leftnod ⊢ φ → Q ∈ No
9 7 leftnod ⊢ φ → W ∈ No
10 ltslin ⊢ Q ∈ No ∧ W ∈ No → Q < s W ∨ Q = W ∨ W < s Q
11 8 9 10 syl2anc ⊢ φ → Q < s W ∨ Q = W ∨ W < s Q
12 4 leftoldd ⊢ φ → P ∈ Old ⁡ bday ⁡ A
13 1 12 3 mulsproplem2 ⊢ φ → P ⋅ s B ∈ No
14 5 leftoldd ⊢ φ → Q ∈ Old ⁡ bday ⁡ B
15 1 2 14 mulsproplem3 ⊢ φ → A ⋅ s Q ∈ No
16 13 15 addscld ⊢ φ → P ⋅ s B + s A ⋅ s Q ∈ No
17 1 12 14 mulsproplem4 ⊢ φ → P ⋅ s Q ∈ No
18 16 17 subscld ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q ∈ No
19 18 adantr ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q ∈ No
20 7 leftoldd ⊢ φ → W ∈ Old ⁡ bday ⁡ B
21 1 2 20 mulsproplem3 ⊢ φ → A ⋅ s W ∈ No
22 13 21 addscld ⊢ φ → P ⋅ s B + s A ⋅ s W ∈ No
23 1 12 20 mulsproplem4 ⊢ φ → P ⋅ s W ∈ No
24 22 23 subscld ⊢ φ → P ⋅ s B + s A ⋅ s W - s P ⋅ s W ∈ No
25 24 adantr ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s W - s P ⋅ s W ∈ No
26 6 rightoldd ⊢ φ → V ∈ Old ⁡ bday ⁡ A
27 1 26 3 mulsproplem2 ⊢ φ → V ⋅ s B ∈ No
28 27 21 addscld ⊢ φ → V ⋅ s B + s A ⋅ s W ∈ No
29 1 26 20 mulsproplem4 ⊢ φ → V ⋅ s W ∈ No
30 28 29 subscld ⊢ φ → V ⋅ s B + s A ⋅ s W - s V ⋅ s W ∈ No
31 30 adantr ⊢ φ ∧ Q < s W → V ⋅ s B + s A ⋅ s W - s V ⋅ s W ∈ No
32 sltsleft ⊢ A ∈ No → L ⁡ A ≪ s A
33 2 32 syl ⊢ φ → L ⁡ A ≪ s A
34 snidg ⊢ A ∈ No → A ∈ A
35 2 34 syl ⊢ φ → A ∈ A
36 33 4 35 sltssepcd ⊢ φ → P < s A
37 0no ⊢ 0 s ∈ No
38 37 a1i ⊢ φ → 0 s ∈ No
39 4 leftnod ⊢ φ → P ∈ No
40 bday0 ⊢ bday ⁡ 0 s = ∅
41 40 40 oveq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅ + ∅
42 0elon ⊢ ∅ ∈ On
43 naddrid ⊢ ∅ ∈ On → ∅ + ∅ = ∅
44 42 43 ax-mp ⊢ ∅ + ∅ = ∅
45 41 44 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅
46 45 uneq1i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q = ∅ ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q
47 0un ⊢ ∅ ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q = bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q
48 46 47 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q = bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q
49 oldbdayim ⊢ P ∈ Old ⁡ bday ⁡ A → bday ⁡ P ∈ bday ⁡ A
50 12 49 syl ⊢ φ → bday ⁡ P ∈ bday ⁡ A
51 oldbdayim ⊢ Q ∈ Old ⁡ bday ⁡ B → bday ⁡ Q ∈ bday ⁡ B
52 14 51 syl ⊢ φ → bday ⁡ Q ∈ bday ⁡ B
53 bdayon ⊢ bday ⁡ A ∈ On
54 bdayon ⊢ bday ⁡ B ∈ On
55 naddel12 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ P ∈ bday ⁡ A ∧ bday ⁡ Q ∈ bday ⁡ B → bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
56 53 54 55 mp2an ⊢ bday ⁡ P ∈ bday ⁡ A ∧ bday ⁡ Q ∈ bday ⁡ B → bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
57 50 52 56 syl2anc ⊢ φ → bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
58 oldbdayim ⊢ W ∈ Old ⁡ bday ⁡ B → bday ⁡ W ∈ bday ⁡ B
59 20 58 syl ⊢ φ → bday ⁡ W ∈ bday ⁡ B
60 bdayon ⊢ bday ⁡ W ∈ On
61 naddel2 ⊢ bday ⁡ W ∈ On ∧ bday ⁡ B ∈ On ∧ bday ⁡ A ∈ On → bday ⁡ W ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
62 60 54 53 61 mp3an ⊢ bday ⁡ W ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
63 59 62 sylib ⊢ φ → bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
64 57 63 jca ⊢ φ → bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
65 naddel12 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ P ∈ bday ⁡ A ∧ bday ⁡ W ∈ bday ⁡ B → bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
66 53 54 65 mp2an ⊢ bday ⁡ P ∈ bday ⁡ A ∧ bday ⁡ W ∈ bday ⁡ B → bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
67 50 59 66 syl2anc ⊢ φ → bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
68 bdayon ⊢ bday ⁡ Q ∈ On
69 naddel2 ⊢ bday ⁡ Q ∈ On ∧ bday ⁡ B ∈ On ∧ bday ⁡ A ∈ On → bday ⁡ Q ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
70 68 54 53 69 mp3an ⊢ bday ⁡ Q ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
71 52 70 sylib ⊢ φ → bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
72 67 71 jca ⊢ φ → bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
73 bdayon ⊢ bday ⁡ P ∈ On
74 naddcl ⊢ bday ⁡ P ∈ On ∧ bday ⁡ Q ∈ On → bday ⁡ P + bday ⁡ Q ∈ On
75 73 68 74 mp2an ⊢ bday ⁡ P + bday ⁡ Q ∈ On
76 naddcl ⊢ bday ⁡ A ∈ On ∧ bday ⁡ W ∈ On → bday ⁡ A + bday ⁡ W ∈ On
77 53 60 76 mp2an ⊢ bday ⁡ A + bday ⁡ W ∈ On
78 75 77 onun2i ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ On
79 naddcl ⊢ bday ⁡ P ∈ On ∧ bday ⁡ W ∈ On → bday ⁡ P + bday ⁡ W ∈ On
80 73 60 79 mp2an ⊢ bday ⁡ P + bday ⁡ W ∈ On
81 naddcl ⊢ bday ⁡ A ∈ On ∧ bday ⁡ Q ∈ On → bday ⁡ A + bday ⁡ Q ∈ On
82 53 68 81 mp2an ⊢ bday ⁡ A + bday ⁡ Q ∈ On
83 80 82 onun2i ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ On
84 naddcl ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ A + bday ⁡ B ∈ On
85 53 54 84 mp2an ⊢ bday ⁡ A + bday ⁡ B ∈ On
86 onunel ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ On ∧ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
87 78 83 85 86 mp3an ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
88 onunel ⊢ bday ⁡ P + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
89 75 77 85 88 mp3an ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
90 onunel ⊢ bday ⁡ P + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
91 80 82 85 90 mp3an ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
92 89 91 anbi12i ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
93 87 92 bitri ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
94 64 72 93 sylanbrc ⊢ φ → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
95 elun1 ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
96 94 95 syl ⊢ φ → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
97 48 96 eqeltrid ⊢ φ → bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
98 1 38 38 39 2 8 9 97 mulsproplem1 ⊢ φ → 0 s ⋅ s 0 s ∈ No ∧ P < s A ∧ Q < s W → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q
99 98 simprd ⊢ φ → P < s A ∧ Q < s W → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q
100 36 99 mpand ⊢ φ → Q < s W → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q
101 100 imp ⊢ φ ∧ Q < s W → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q
102 23 21 17 15 ltsubsubs3bd ⊢ φ → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q ↔ A ⋅ s Q - s P ⋅ s Q < s A ⋅ s W - s P ⋅ s W
103 15 17 subscld ⊢ φ → A ⋅ s Q - s P ⋅ s Q ∈ No
104 21 23 subscld ⊢ φ → A ⋅ s W - s P ⋅ s W ∈ No
105 103 104 13 ltadds2d ⊢ φ → A ⋅ s Q - s P ⋅ s Q < s A ⋅ s W - s P ⋅ s W ↔ P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s P ⋅ s B + s A ⋅ s W - s P ⋅ s W
106 102 105 bitrd ⊢ φ → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q ↔ P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s P ⋅ s B + s A ⋅ s W - s P ⋅ s W
107 106 adantr ⊢ φ ∧ Q < s W → P ⋅ s W - s P ⋅ s Q < s A ⋅ s W - s A ⋅ s Q ↔ P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s P ⋅ s B + s A ⋅ s W - s P ⋅ s W
108 101 107 mpbid ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s P ⋅ s B + s A ⋅ s W - s P ⋅ s W
109 13 15 17 addsubsassd ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q = P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q
110 109 adantr ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q = P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q
111 13 21 23 addsubsassd ⊢ φ → P ⋅ s B + s A ⋅ s W - s P ⋅ s W = P ⋅ s B + s A ⋅ s W - s P ⋅ s W
112 111 adantr ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s W - s P ⋅ s W = P ⋅ s B + s A ⋅ s W - s P ⋅ s W
113 108 110 112 3brtr4d ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s P ⋅ s B + s A ⋅ s W - s P ⋅ s W
114 lltr ⊢ L ⁡ A ≪ s R ⁡ A
115 114 a1i ⊢ φ → L ⁡ A ≪ s R ⁡ A
116 115 4 6 sltssepcd ⊢ φ → P < s V
117 sltsleft ⊢ B ∈ No → L ⁡ B ≪ s B
118 3 117 syl ⊢ φ → L ⁡ B ≪ s B
119 snidg ⊢ B ∈ No → B ∈ B
120 3 119 syl ⊢ φ → B ∈ B
121 118 7 120 sltssepcd ⊢ φ → W < s B
122 6 rightnod ⊢ φ → V ∈ No
123 45 uneq1i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W = ∅ ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W
124 0un ⊢ ∅ ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W = bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W
125 123 124 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W = bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W
126 oldbdayim ⊢ V ∈ Old ⁡ bday ⁡ A → bday ⁡ V ∈ bday ⁡ A
127 26 126 syl ⊢ φ → bday ⁡ V ∈ bday ⁡ A
128 bdayon ⊢ bday ⁡ V ∈ On
129 naddel1 ⊢ bday ⁡ V ∈ On ∧ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ V ∈ bday ⁡ A ↔ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
130 128 53 54 129 mp3an ⊢ bday ⁡ V ∈ bday ⁡ A ↔ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
131 127 130 sylib ⊢ φ → bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
132 67 131 jca ⊢ φ → bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
133 naddel1 ⊢ bday ⁡ P ∈ On ∧ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ P ∈ bday ⁡ A ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
134 73 53 54 133 mp3an ⊢ bday ⁡ P ∈ bday ⁡ A ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
135 50 134 sylib ⊢ φ → bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
136 naddel12 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ V ∈ bday ⁡ A ∧ bday ⁡ W ∈ bday ⁡ B → bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
137 53 54 136 mp2an ⊢ bday ⁡ V ∈ bday ⁡ A ∧ bday ⁡ W ∈ bday ⁡ B → bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
138 127 59 137 syl2anc ⊢ φ → bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
139 135 138 jca ⊢ φ → bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
140 naddcl ⊢ bday ⁡ V ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ V + bday ⁡ B ∈ On
141 128 54 140 mp2an ⊢ bday ⁡ V + bday ⁡ B ∈ On
142 80 141 onun2i ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ On
143 naddcl ⊢ bday ⁡ P ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ B ∈ On
144 73 54 143 mp2an ⊢ bday ⁡ P + bday ⁡ B ∈ On
145 naddcl ⊢ bday ⁡ V ∈ On ∧ bday ⁡ W ∈ On → bday ⁡ V + bday ⁡ W ∈ On
146 128 60 145 mp2an ⊢ bday ⁡ V + bday ⁡ W ∈ On
147 144 146 onun2i ⊢ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ On
148 onunel ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ On ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
149 142 147 85 148 mp3an ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
150 onunel ⊢ bday ⁡ P + bday ⁡ W ∈ On ∧ bday ⁡ V + bday ⁡ B ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
151 80 141 85 150 mp3an ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
152 onunel ⊢ bday ⁡ P + bday ⁡ B ∈ On ∧ bday ⁡ V + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
153 144 146 85 152 mp3an ⊢ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
154 151 153 anbi12i ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
155 149 154 bitri ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
156 132 139 155 sylanbrc ⊢ φ → bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
157 elun1 ⊢ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B → bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
158 156 157 syl ⊢ φ → bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
159 125 158 eqeltrid ⊢ φ → bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ W ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
160 1 38 38 39 122 9 3 159 mulsproplem1 ⊢ φ → 0 s ⋅ s 0 s ∈ No ∧ P < s V ∧ W < s B → P ⋅ s B - s P ⋅ s W < s V ⋅ s B - s V ⋅ s W
161 160 simprd ⊢ φ → P < s V ∧ W < s B → P ⋅ s B - s P ⋅ s W < s V ⋅ s B - s V ⋅ s W
162 116 121 161 mp2and ⊢ φ → P ⋅ s B - s P ⋅ s W < s V ⋅ s B - s V ⋅ s W
163 13 23 subscld ⊢ φ → P ⋅ s B - s P ⋅ s W ∈ No
164 27 29 subscld ⊢ φ → V ⋅ s B - s V ⋅ s W ∈ No
165 163 164 21 ltadds1d ⊢ φ → P ⋅ s B - s P ⋅ s W < s V ⋅ s B - s V ⋅ s W ↔ P ⋅ s B - s P ⋅ s W + s A ⋅ s W < s V ⋅ s B - s V ⋅ s W + s A ⋅ s W
166 162 165 mpbid ⊢ φ → P ⋅ s B - s P ⋅ s W + s A ⋅ s W < s V ⋅ s B - s V ⋅ s W + s A ⋅ s W
167 13 21 23 addsubsd ⊢ φ → P ⋅ s B + s A ⋅ s W - s P ⋅ s W = P ⋅ s B - s P ⋅ s W + s A ⋅ s W
168 27 21 29 addsubsd ⊢ φ → V ⋅ s B + s A ⋅ s W - s V ⋅ s W = V ⋅ s B - s V ⋅ s W + s A ⋅ s W
169 166 167 168 3brtr4d ⊢ φ → P ⋅ s B + s A ⋅ s W - s P ⋅ s W < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
170 169 adantr ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s W - s P ⋅ s W < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
171 19 25 31 113 170 ltstrd ⊢ φ ∧ Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
172 171 ex ⊢ φ → Q < s W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
173 oveq2 ⊢ Q = W → A ⋅ s Q = A ⋅ s W
174 173 oveq2d ⊢ Q = W → P ⋅ s B + s A ⋅ s Q = P ⋅ s B + s A ⋅ s W
175 oveq2 ⊢ Q = W → P ⋅ s Q = P ⋅ s W
176 174 175 oveq12d ⊢ Q = W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q = P ⋅ s B + s A ⋅ s W - s P ⋅ s W
177 176 breq1d ⊢ Q = W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W ↔ P ⋅ s B + s A ⋅ s W - s P ⋅ s W < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
178 169 177 syl5ibrcom ⊢ φ → Q = W → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
179 18 adantr ⊢ φ ∧ W < s Q → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q ∈ No
180 27 15 addscld ⊢ φ → V ⋅ s B + s A ⋅ s Q ∈ No
181 1 26 14 mulsproplem4 ⊢ φ → V ⋅ s Q ∈ No
182 180 181 subscld ⊢ φ → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q ∈ No
183 182 adantr ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q ∈ No
184 30 adantr ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s W - s V ⋅ s W ∈ No
185 118 5 120 sltssepcd ⊢ φ → Q < s B
186 45 uneq1i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q = ∅ ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q
187 0un ⊢ ∅ ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q = bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q
188 186 187 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q = bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q
189 57 131 jca ⊢ φ → bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
190 naddel12 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ V ∈ bday ⁡ A ∧ bday ⁡ Q ∈ bday ⁡ B → bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
191 53 54 190 mp2an ⊢ bday ⁡ V ∈ bday ⁡ A ∧ bday ⁡ Q ∈ bday ⁡ B → bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
192 127 52 191 syl2anc ⊢ φ → bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
193 135 192 jca ⊢ φ → bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
194 75 141 onun2i ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ On
195 naddcl ⊢ bday ⁡ V ∈ On ∧ bday ⁡ Q ∈ On → bday ⁡ V + bday ⁡ Q ∈ On
196 128 68 195 mp2an ⊢ bday ⁡ V + bday ⁡ Q ∈ On
197 144 196 onun2i ⊢ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ On
198 onunel ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ On ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
199 194 197 85 198 mp3an ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
200 onunel ⊢ bday ⁡ P + bday ⁡ Q ∈ On ∧ bday ⁡ V + bday ⁡ B ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
201 75 141 85 200 mp3an ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B
202 onunel ⊢ bday ⁡ P + bday ⁡ B ∈ On ∧ bday ⁡ V + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
203 144 196 85 202 mp3an ⊢ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
204 201 203 anbi12i ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
205 199 204 bitri ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ P + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ P + bday ⁡ B ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
206 189 193 205 sylanbrc ⊢ φ → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
207 elun1 ⊢ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
208 206 207 syl ⊢ φ → bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
209 188 208 eqeltrid ⊢ φ → bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ P + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ B ∪ bday ⁡ P + bday ⁡ B ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
210 1 38 38 39 122 8 3 209 mulsproplem1 ⊢ φ → 0 s ⋅ s 0 s ∈ No ∧ P < s V ∧ Q < s B → P ⋅ s B - s P ⋅ s Q < s V ⋅ s B - s V ⋅ s Q
211 210 simprd ⊢ φ → P < s V ∧ Q < s B → P ⋅ s B - s P ⋅ s Q < s V ⋅ s B - s V ⋅ s Q
212 116 185 211 mp2and ⊢ φ → P ⋅ s B - s P ⋅ s Q < s V ⋅ s B - s V ⋅ s Q
213 13 17 subscld ⊢ φ → P ⋅ s B - s P ⋅ s Q ∈ No
214 27 181 subscld ⊢ φ → V ⋅ s B - s V ⋅ s Q ∈ No
215 213 214 15 ltadds1d ⊢ φ → P ⋅ s B - s P ⋅ s Q < s V ⋅ s B - s V ⋅ s Q ↔ P ⋅ s B - s P ⋅ s Q + s A ⋅ s Q < s V ⋅ s B - s V ⋅ s Q + s A ⋅ s Q
216 212 215 mpbid ⊢ φ → P ⋅ s B - s P ⋅ s Q + s A ⋅ s Q < s V ⋅ s B - s V ⋅ s Q + s A ⋅ s Q
217 13 15 17 addsubsd ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q = P ⋅ s B - s P ⋅ s Q + s A ⋅ s Q
218 27 15 181 addsubsd ⊢ φ → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q = V ⋅ s B - s V ⋅ s Q + s A ⋅ s Q
219 216 217 218 3brtr4d ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q
220 219 adantr ⊢ φ ∧ W < s Q → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q
221 sltsright ⊢ A ∈ No → A ≪ s R ⁡ A
222 2 221 syl ⊢ φ → A ≪ s R ⁡ A
223 222 35 6 sltssepcd ⊢ φ → A < s V
224 45 uneq1i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W = ∅ ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W
225 0un ⊢ ∅ ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W = bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W
226 224 225 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W = bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W
227 63 192 jca ⊢ φ → bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
228 71 138 jca ⊢ φ → bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
229 77 196 onun2i ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ On
230 82 146 onun2i ⊢ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ On
231 onunel ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
232 229 230 85 231 mp3an ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
233 onunel ⊢ bday ⁡ A + bday ⁡ W ∈ On ∧ bday ⁡ V + bday ⁡ Q ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
234 77 196 85 233 mp3an ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B
235 onunel ⊢ bday ⁡ A + bday ⁡ Q ∈ On ∧ bday ⁡ V + bday ⁡ W ∈ On ∧ bday ⁡ A + bday ⁡ B ∈ On → bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
236 82 146 85 235 mp3an ⊢ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
237 234 236 anbi12i ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
238 232 237 bitri ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ↔ bday ⁡ A + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ A + bday ⁡ Q ∈ bday ⁡ A + bday ⁡ B ∧ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
239 227 228 238 sylanbrc ⊢ φ → bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B
240 elun1 ⊢ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B → bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
241 239 240 syl ⊢ φ → bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
242 226 241 eqeltrid ⊢ φ → bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ A + bday ⁡ W ∪ bday ⁡ V + bday ⁡ Q ∪ bday ⁡ A + bday ⁡ Q ∪ bday ⁡ V + bday ⁡ W ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
243 1 38 38 2 122 9 8 242 mulsproplem1 ⊢ φ → 0 s ⋅ s 0 s ∈ No ∧ A < s V ∧ W < s Q → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W
244 243 simprd ⊢ φ → A < s V ∧ W < s Q → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W
245 223 244 mpand ⊢ φ → W < s Q → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W
246 245 imp ⊢ φ ∧ W < s Q → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W
247 15 181 21 29 ltsubsubsbd ⊢ φ → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W ↔ A ⋅ s Q - s V ⋅ s Q < s A ⋅ s W - s V ⋅ s W
248 15 181 subscld ⊢ φ → A ⋅ s Q - s V ⋅ s Q ∈ No
249 21 29 subscld ⊢ φ → A ⋅ s W - s V ⋅ s W ∈ No
250 248 249 27 ltadds2d ⊢ φ → A ⋅ s Q - s V ⋅ s Q < s A ⋅ s W - s V ⋅ s W ↔ V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
251 247 250 bitrd ⊢ φ → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W ↔ V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
252 251 adantr ⊢ φ ∧ W < s Q → A ⋅ s Q - s A ⋅ s W < s V ⋅ s Q - s V ⋅ s W ↔ V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
253 246 252 mpbid ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
254 27 15 181 addsubsassd ⊢ φ → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q = V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q
255 254 adantr ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q = V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q
256 27 21 29 addsubsassd ⊢ φ → V ⋅ s B + s A ⋅ s W - s V ⋅ s W = V ⋅ s B + s A ⋅ s W - s V ⋅ s W
257 256 adantr ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s W - s V ⋅ s W = V ⋅ s B + s A ⋅ s W - s V ⋅ s W
258 253 255 257 3brtr4d ⊢ φ ∧ W < s Q → V ⋅ s B + s A ⋅ s Q - s V ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
259 179 183 184 220 258 ltstrd ⊢ φ ∧ W < s Q → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
260 259 ex ⊢ φ → W < s Q → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
261 172 178 260 3jaod ⊢ φ → Q < s W ∨ Q = W ∨ W < s Q → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W
262 11 261 mpd ⊢ φ → P ⋅ s B + s A ⋅ s Q - s P ⋅ s Q < s V ⋅ s B + s A ⋅ s W - s V ⋅ s W