Proof of Theorem mulsproplem5
Step | Hyp | Ref
| Expression |
1 | | leftssno 27723 |
. . . 4
⊢ ( L
‘𝐴) ⊆ No |
2 | | mulsproplem5.3 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ( L ‘𝐴)) |
3 | 1, 2 | sselid 3972 |
. . 3
⊢ (𝜑 → 𝑃 ∈ No
) |
4 | | mulsproplem5.5 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴)) |
5 | 1, 4 | sselid 3972 |
. . 3
⊢ (𝜑 → 𝑇 ∈ No
) |
6 | | sltlin 27598 |
. . 3
⊢ ((𝑃 ∈
No ∧ 𝑇 ∈
No ) → (𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃)) |
7 | 3, 5, 6 | syl2anc 583 |
. 2
⊢ (𝜑 → (𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃)) |
8 | | mulsproplem.1 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑎 ∈ No
∀𝑏 ∈ No ∀𝑐 ∈ No
∀𝑑 ∈ No ∀𝑒 ∈ No
∀𝑓 ∈ No (((( bday ‘𝑎) +no (
bday ‘𝑏))
∪ (((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) |
9 | | leftssold 27721 |
. . . . . . . . . 10
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
10 | 9, 2 | sselid 3972 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ( O ‘(
bday ‘𝐴))) |
11 | | mulsproplem5.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ No
) |
12 | 8, 10, 11 | mulsproplem2 27933 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ·s 𝐵) ∈ No
) |
13 | | mulsproplem5.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ No
) |
14 | | leftssold 27721 |
. . . . . . . . . 10
⊢ ( L
‘𝐵) ⊆ ( O
‘( bday ‘𝐵)) |
15 | | mulsproplem5.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ( L ‘𝐵)) |
16 | 14, 15 | sselid 3972 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ( O ‘(
bday ‘𝐵))) |
17 | 8, 13, 16 | mulsproplem3 27934 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑄) ∈ No
) |
18 | 12, 17 | addscld 27813 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No
) |
19 | 8, 10, 16 | mulsproplem4 27935 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ·s 𝑄) ∈ No
) |
20 | 18, 19 | subscld 27889 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
22 | 9, 4 | sselid 3972 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ( O ‘(
bday ‘𝐴))) |
23 | 8, 22, 11 | mulsproplem2 27933 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ·s 𝐵) ∈ No
) |
24 | 23, 17 | addscld 27813 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) ∈ No
) |
25 | 8, 22, 16 | mulsproplem4 27935 |
. . . . . . 7
⊢ (𝜑 → (𝑇 ·s 𝑄) ∈ No
) |
26 | 24, 25 | subscld 27889 |
. . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) ∈ No
) |
27 | 26 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) ∈ No
) |
28 | | rightssold 27722 |
. . . . . . . . . 10
⊢ ( R
‘𝐵) ⊆ ( O
‘( bday ‘𝐵)) |
29 | | mulsproplem5.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵)) |
30 | 28, 29 | sselid 3972 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ( O ‘(
bday ‘𝐵))) |
31 | 8, 13, 30 | mulsproplem3 27934 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑈) ∈ No
) |
32 | 23, 31 | addscld 27813 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈ No
) |
33 | 8, 22, 30 | mulsproplem4 27935 |
. . . . . . 7
⊢ (𝜑 → (𝑇 ·s 𝑈) ∈ No
) |
34 | 32, 33 | subscld 27889 |
. . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No
) |
35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No
) |
36 | | ssltleft 27713 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No → ( L ‘𝐵) <<s {𝐵}) |
37 | 11, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐵) <<s {𝐵}) |
38 | | snidg 4654 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No → 𝐵 ∈
{𝐵}) |
39 | 11, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
40 | 37, 15, 39 | ssltsepcd 27643 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 <s 𝐵) |
41 | | 0sno 27675 |
. . . . . . . . . . . 12
⊢
0s ∈ No |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0s ∈ No ) |
43 | | leftssno 27723 |
. . . . . . . . . . . 12
⊢ ( L
‘𝐵) ⊆ No |
44 | 43, 15 | sselid 3972 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ No
) |
45 | | bday0s 27677 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘ 0s ) = ∅ |
46 | 45, 45 | oveq12i 7413 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) |
47 | | 0elon 6408 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ On |
48 | | naddrid 8678 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ On → (∅ +no ∅) = ∅) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (∅
+no ∅) = ∅ |
50 | 46, 49 | eqtri 2752 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ |
51 | 50 | uneq1i 4151 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))))) =
(∅ ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))))) |
52 | | 0un 4384 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) |
53 | 51, 52 | eqtri 2752 |
. . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) |
54 | | oldbdayim 27731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑃) ∈
( bday ‘𝐴)) |
55 | 10, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑃)
∈ ( bday ‘𝐴)) |
56 | | oldbdayim 27731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑄) ∈
( bday ‘𝐵)) |
57 | 16, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑄)
∈ ( bday ‘𝐵)) |
58 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐴) ∈ On |
59 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐵) ∈ On |
60 | | naddel12 8695 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑃) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
61 | 58, 59, 60 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
62 | 55, 57, 61 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
63 | | oldbdayim 27731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑇) ∈
( bday ‘𝐴)) |
64 | 22, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑇)
∈ ( bday ‘𝐴)) |
65 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑇) ∈ On |
66 | | naddel1 8682 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑇)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
67 | 65, 58, 59, 66 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑇) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
68 | 64, 67 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
69 | 62, 68 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
70 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑃) ∈ On |
71 | | naddel1 8682 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑃)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
72 | 70, 58, 59, 71 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑃) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
73 | 55, 72 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
74 | | naddel12 8695 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑇) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
75 | 58, 59, 74 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑄) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
76 | 64, 57, 75 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
77 | 73, 76 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑇) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
78 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . . 18
⊢ ( bday ‘𝑄) ∈ On |
79 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
On) |
80 | 70, 78, 79 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
On |
81 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
On) |
82 | 65, 59, 81 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
On |
83 | 80, 82 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
On |
84 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
On) |
85 | 70, 59, 84 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
On |
86 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
On) |
87 | 65, 78, 86 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
On |
88 | 85, 87 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
On |
89 | | naddcl 8672 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) |
90 | 58, 59, 89 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On |
91 | | onunel 6459 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
On ∧ ((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
92 | 83, 88, 90, 91 | mp3an 1457 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
93 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝑇) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
94 | 80, 82, 90, 93 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
95 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑇) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
96 | 85, 87, 90, 95 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
97 | 94, 96 | anbi12i 626 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
98 | 92, 97 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
99 | 69, 77, 98 | sylanbrc 582 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝑇) +no ( bday ‘𝐵))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑇) +no ( bday ‘𝑄)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
100 | | elun1 4168 |
. . . . . . . . . . . . 13
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝑇) +no ( bday
‘𝐵))) ∪
((( bday ‘𝑃) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑇) +no ( bday
‘𝑄)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝑇) +no ( bday ‘𝐵))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑇) +no ( bday ‘𝑄)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
102 | 53, 101 | eqeltrid 2829 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday
‘𝑇) +no ( bday ‘𝐵))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑇) +no ( bday ‘𝑄))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
103 | 8, 42, 42, 3, 5, 44, 11, 102 | mulsproplem1 27932 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑃 <s 𝑇 ∧ 𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄))))) |
104 | 103 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 <s 𝑇 ∧ 𝑄 <s 𝐵) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)))) |
105 | 40, 104 | mpan2d 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 <s 𝑇 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)))) |
106 | 105 | imp 406 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄))) |
107 | 12, 19 | subscld 27889 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) ∈ No
) |
108 | 23, 25 | subscld 27889 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ∈ No
) |
109 | 107, 108,
17 | sltadd1d 27831 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄)))) |
110 | 109 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄)))) |
111 | 106, 110 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
112 | 12, 17, 19 | addsubsd 27906 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
113 | 112 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
114 | 23, 17, 25 | addsubsd 27906 |
. . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
115 | 114 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑄)) +s (𝐴 ·s 𝑄))) |
116 | 111, 113,
115 | 3brtr4d 5170 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄))) |
117 | | ssltleft 27713 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → ( L ‘𝐴) <<s {𝐴}) |
118 | 13, 117 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴}) |
119 | | snidg 4654 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → 𝐴 ∈
{𝐴}) |
120 | 13, 119 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
121 | 118, 4, 120 | ssltsepcd 27643 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 <s 𝐴) |
122 | | lltropt 27715 |
. . . . . . . . . . 11
⊢ ( L
‘𝐵) <<s ( R
‘𝐵) |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵)) |
124 | 123, 15, 29 | ssltsepcd 27643 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 <s 𝑈) |
125 | | rightssno 27724 |
. . . . . . . . . . . 12
⊢ ( R
‘𝐵) ⊆ No |
126 | 125, 29 | sselid 3972 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ No
) |
127 | 50 | uneq1i 4151 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(∅ ∪ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) |
128 | | 0un 4384 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) |
129 | 127, 128 | eqtri 2752 |
. . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) |
130 | | oldbdayim 27731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑈) ∈
( bday ‘𝐵)) |
131 | 30, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑈)
∈ ( bday ‘𝐵)) |
132 | | bdayelon 27625 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑈) ∈ On |
133 | | naddel2 8683 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑈) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑈)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
134 | 132, 59, 58, 133 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑈) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
135 | 131, 134 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
136 | 76, 135 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
137 | | naddel12 8695 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑇) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
138 | 58, 59, 137 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
139 | 64, 131, 138 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
140 | | naddel2 8683 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑄) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑄)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
141 | 78, 59, 58, 140 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑄) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
142 | 57, 141 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
143 | 139, 142 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
144 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
On) |
145 | 58, 132, 144 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
On |
146 | 87, 145 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On |
147 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
On) |
148 | 65, 132, 147 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
On |
149 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑄)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
On) |
150 | 58, 78, 149 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
On |
151 | 148, 150 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On |
152 | | onunel 6459 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On ∧ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
153 | 146, 151,
90, 152 | mp3an 1457 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
154 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
155 | 87, 145, 90, 154 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
156 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
157 | 148, 150,
90, 156 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
158 | 155, 157 | anbi12i 626 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
159 | 153, 158 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
160 | 136, 143,
159 | sylanbrc 582 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
161 | | elun1 4168 |
. . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑇) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
163 | 129, 162 | eqeltrid 2829 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑇) +no ( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
164 | 8, 42, 42, 5, 13, 44, 126, 163 | mulsproplem1 27932 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))))) |
165 | 164 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))) |
166 | 121, 124,
165 | mp2and 696 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))) |
167 | 33, 31, 25, 17 | sltsubsub3bd 27909 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) |
168 | 17, 25 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) ∈ No
) |
169 | 31, 33 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ∈ No
) |
170 | 168, 169,
23 | sltadd2d 27830 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))) |
171 | 167, 170 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))) |
172 | 166, 171 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) |
173 | 23, 17, 25 | addsubsassd 27905 |
. . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑇 ·s 𝑄)))) |
174 | 23, 31, 33 | addsubsassd 27905 |
. . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) |
175 | 172, 173,
174 | 3brtr4d 5170 |
. . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |
176 | 175 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |
177 | 21, 27, 35, 116, 176 | slttrd 27608 |
. . . 4
⊢ ((𝜑 ∧ 𝑃 <s 𝑇) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |
178 | 177 | ex 412 |
. . 3
⊢ (𝜑 → (𝑃 <s 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) |
179 | | oveq1 7408 |
. . . . . . 7
⊢ (𝑃 = 𝑇 → (𝑃 ·s 𝐵) = (𝑇 ·s 𝐵)) |
180 | 179 | oveq1d 7416 |
. . . . . 6
⊢ (𝑃 = 𝑇 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) = ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄))) |
181 | | oveq1 7408 |
. . . . . 6
⊢ (𝑃 = 𝑇 → (𝑃 ·s 𝑄) = (𝑇 ·s 𝑄)) |
182 | 180, 181 | oveq12d 7419 |
. . . . 5
⊢ (𝑃 = 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄))) |
183 | 182 | breq1d 5148 |
. . . 4
⊢ (𝑃 = 𝑇 → ((((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ↔ (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑇 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) |
184 | 175, 183 | syl5ibrcom 246 |
. . 3
⊢ (𝜑 → (𝑃 = 𝑇 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) |
185 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) ∈ No
) |
186 | 12, 31 | addscld 27813 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈ No
) |
187 | 8, 10, 30 | mulsproplem4 27935 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ·s 𝑈) ∈ No
) |
188 | 186, 187 | subscld 27889 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) ∈ No
) |
189 | 188 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) ∈ No
) |
190 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈ No
) |
191 | 118, 2, 120 | ssltsepcd 27643 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 <s 𝐴) |
192 | 50 | uneq1i 4151 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(∅ ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) |
193 | | 0un 4384 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) |
194 | 192, 193 | eqtri 2752 |
. . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))))) =
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) |
195 | 62, 135 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
196 | | naddel12 8695 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑃) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
197 | 58, 59, 196 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) |
198 | 55, 131, 197 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑃) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
199 | 198, 142 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑃) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑄)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
200 | 80, 145 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On |
201 | | naddcl 8672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑃) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
On) |
202 | 70, 132, 201 | mp2an 689 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
On |
203 | 202, 150 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On |
204 | | onunel 6459 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On ∧ ((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
205 | 200, 203,
90, 204 | mp3an 1457 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
206 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
207 | 80, 145, 90, 206 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
208 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑄)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
209 | 202, 150,
90, 208 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
210 | 207, 209 | anbi12i 626 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
211 | 205, 210 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑄)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
212 | 195, 199,
211 | sylanbrc 582 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
213 | | elun1 4168 |
. . . . . . . . . . . . 13
⊢
((((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑃) +no ( bday
‘𝑄)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑃) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑄)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑃) +no
( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
215 | 194, 214 | eqeltrid 2829 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑃) +no ( bday ‘𝑄)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑃) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑄))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
216 | 8, 42, 42, 3, 13, 44, 126, 215 | mulsproplem1 27932 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))))) |
217 | 216 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 <s 𝐴 ∧ 𝑄 <s 𝑈) → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)))) |
218 | 191, 124,
217 | mp2and 696 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄))) |
219 | 187, 31, 19, 17 | sltsubsub3bd 27909 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)))) |
220 | 17, 19 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) ∈ No
) |
221 | 31, 187 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)) ∈ No
) |
222 | 220, 221,
12 | sltadd2d 27830 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈))))) |
223 | 219, 222 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 ·s 𝑈) -s (𝑃 ·s 𝑄)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑄)) ↔ ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈))))) |
224 | 218, 223 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄))) <s ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)))) |
225 | 12, 17, 19 | addsubsassd 27905 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑄) -s (𝑃 ·s 𝑄)))) |
226 | 12, 31, 187 | addsubsassd 27905 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = ((𝑃 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑃 ·s 𝑈)))) |
227 | 224, 225,
226 | 3brtr4d 5170 |
. . . . . 6
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈))) |
228 | 227 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈))) |
229 | | ssltright 27714 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No → {𝐵}
<<s ( R ‘𝐵)) |
230 | 11, 229 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵)) |
231 | 230, 39, 29 | ssltsepcd 27643 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 <s 𝑈) |
232 | 50 | uneq1i 4151 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))))) =
(∅ ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))))) |
233 | | 0un 4384 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) |
234 | 232, 233 | eqtri 2752 |
. . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) |
235 | | onunel 6459 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑃) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
236 | 82, 202, 90, 235 | mp3an 1457 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
237 | 68, 198, 236 | sylanbrc 582 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑃) +no ( bday ‘𝑈))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
238 | 139, 73 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑃) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
239 | 82, 202 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
On |
240 | 148, 85 | onun2i 6476 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
On |
241 | | onunel 6459 |
. . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
On ∧ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
242 | 239, 240,
90, 241 | mp3an 1457 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
243 | | onunel 6459 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝑃) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
244 | 148, 85, 90, 243 | mp3an 1457 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) |
245 | 244 | anbi2i 622 |
. . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
246 | 242, 245 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑃) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) |
247 | 237, 238,
246 | sylanbrc 582 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑃) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑃) +no ( bday ‘𝐵)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) |
248 | | elun1 4168 |
. . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑃) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑃) +no ( bday
‘𝐵)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) |
249 | 247, 248 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑃) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑃) +no ( bday ‘𝐵)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
250 | 234, 249 | eqeltrid 2829 |
. . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑃) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑃) +no ( bday ‘𝐵))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) |
251 | 8, 42, 42, 5, 3, 11, 126, 250 | mulsproplem1 27932 |
. . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈ No
∧ ((𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵))))) |
252 | 251 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 <s 𝑃 ∧ 𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)))) |
253 | 231, 252 | mpan2d 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 <s 𝑃 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)))) |
254 | 253 | imp 406 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵))) |
255 | 33, 23, 187, 12 | sltsubsub2bd 27908 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)))) |
256 | 12, 187 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) ∈ No
) |
257 | 23, 33 | subscld 27889 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ∈ No
) |
258 | 256, 257,
31 | sltadd1d 27831 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))) |
259 | 255, 258 | bitrd 279 |
. . . . . . . 8
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))) |
260 | 259 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑃 ·s 𝑈) -s (𝑃 ·s 𝐵)) ↔ (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))) |
261 | 254, 260 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))) |
262 | 12, 31, 187 | addsubsd 27906 |
. . . . . . 7
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈))) |
263 | 262 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) = (((𝑃 ·s 𝐵) -s (𝑃 ·s 𝑈)) +s (𝐴 ·s 𝑈))) |
264 | 23, 31, 33 | addsubsd 27906 |
. . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))) |
265 | 264 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))) |
266 | 261, 263,
265 | 3brtr4d 5170 |
. . . . 5
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑃 ·s 𝑈)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |
267 | 185, 189,
190, 228, 266 | slttrd 27608 |
. . . 4
⊢ ((𝜑 ∧ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |
268 | 267 | ex 412 |
. . 3
⊢ (𝜑 → (𝑇 <s 𝑃 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) |
269 | 178, 184,
268 | 3jaod 1425 |
. 2
⊢ (𝜑 → ((𝑃 <s 𝑇 ∨ 𝑃 = 𝑇 ∨ 𝑇 <s 𝑃) → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) |
270 | 7, 269 | mpd 15 |
1
⊢ (𝜑 → (((𝑃 ·s 𝐵) +s (𝐴 ·s 𝑄)) -s (𝑃 ·s 𝑄)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |