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