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