Metamath Proof Explorer

Theorem mulsproplem7

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