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