Metamath Proof Explorer

Theorem mulsproplem8

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