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