Metamath Proof Explorer

Theorem mulsproplem5

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

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