Proof of Theorem jm2.24
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 𝐴 ∈
(ℤ≥‘2)) |
2 | | peano2zm 11297 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
3 | 2 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝑁 − 1) ∈ ℤ) |
4 | | frmy 36497 |
. . . . . . 7
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
5 | 4 | fovcl 6663 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 − 1) ∈ ℤ) → (𝐴 Yrm (𝑁 − 1)) ∈
ℤ) |
6 | 1, 3, 5 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm (𝑁 − 1)) ∈
ℤ) |
7 | 6 | zred 11358 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm (𝑁 − 1)) ∈
ℝ) |
8 | 4 | fovcl 6663 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) |
9 | 8 | zred 11358 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℝ) |
10 | 9 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm 𝑁) ∈ ℝ) |
11 | 7, 10 | readdcld 9948 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) ∈ ℝ) |
12 | | 0red 9920 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 ∈
ℝ) |
13 | | frmx 36496 |
. . . . . 6
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
14 | 13 | fovcl 6663 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
15 | 14 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Xrm 𝑁) ∈
ℕ0) |
16 | 15 | nn0red 11229 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Xrm 𝑁) ∈ ℝ) |
17 | | znegcl 11289 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → -𝑁 ∈
ℤ) |
18 | 17 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → -𝑁 ∈ ℤ) |
19 | 18 | peano2zd 11361 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (-𝑁 + 1) ∈ ℤ) |
20 | 4 | fovcl 6663 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (-𝑁 + 1) ∈ ℤ) → (𝐴 Yrm (-𝑁 + 1)) ∈
ℤ) |
21 | 1, 19, 20 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm (-𝑁 + 1)) ∈ ℤ) |
22 | 21 | zred 11358 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm (-𝑁 + 1)) ∈ ℝ) |
23 | 4 | fovcl 6663 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ -𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) ∈ ℤ) |
24 | 1, 18, 23 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm -𝑁) ∈ ℤ) |
25 | 24 | zred 11358 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm -𝑁) ∈ ℝ) |
26 | | rmy0 36512 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
27 | 26 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm 0) = 0) |
28 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 𝑁 ≤ 0) |
29 | | zre 11258 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
30 | 29 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 𝑁 ∈ ℝ) |
31 | 30 | le0neg1d 10478 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝑁 ≤ 0 ↔ 0 ≤ -𝑁)) |
32 | 28, 31 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 ≤ -𝑁) |
33 | | 0zd 11266 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 ∈
ℤ) |
34 | | zleltp1 11305 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ -𝑁
∈ ℤ) → (0 ≤ -𝑁 ↔ 0 < (-𝑁 + 1))) |
35 | 33, 18, 34 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (0 ≤ -𝑁 ↔ 0 < (-𝑁 + 1))) |
36 | 32, 35 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 < (-𝑁 + 1)) |
37 | | ltrmy 36537 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (-𝑁 + 1) ∈ ℤ) → (0
< (-𝑁 + 1) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (-𝑁 + 1)))) |
38 | 1, 33, 19, 37 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (0 < (-𝑁 + 1) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (-𝑁 + 1)))) |
39 | 36, 38 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm 0) < (𝐴 Yrm (-𝑁 + 1))) |
40 | 27, 39 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 < (𝐴 Yrm (-𝑁 + 1))) |
41 | | lermy 36540 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (0 ≤
-𝑁 ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm -𝑁))) |
42 | 1, 33, 18, 41 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (0 ≤ -𝑁 ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm -𝑁))) |
43 | 32, 42 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm 0) ≤ (𝐴 Yrm -𝑁)) |
44 | 27, 43 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 ≤ (𝐴 Yrm -𝑁)) |
45 | | addgtge0 10395 |
. . . . . 6
⊢ ((((𝐴 Yrm (-𝑁 + 1)) ∈ ℝ ∧
(𝐴 Yrm -𝑁) ∈ ℝ) ∧ (0 <
(𝐴 Yrm (-𝑁 + 1)) ∧ 0 ≤ (𝐴 Yrm -𝑁))) → 0 < ((𝐴 Yrm (-𝑁 + 1)) + (𝐴 Yrm -𝑁))) |
46 | 22, 25, 40, 44, 45 | syl22anc 1319 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 < ((𝐴 Yrm (-𝑁 + 1)) + (𝐴 Yrm -𝑁))) |
47 | 7 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm (𝑁 − 1)) ∈
ℂ) |
48 | 10 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm 𝑁) ∈ ℂ) |
49 | 47, 48 | negdid 10284 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → -((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) = (-(𝐴 Yrm (𝑁 − 1)) + -(𝐴 Yrm 𝑁))) |
50 | | rmyneg 36511 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑁 − 1) ∈ ℤ) → (𝐴 Yrm -(𝑁 − 1)) = -(𝐴 Yrm (𝑁 − 1))) |
51 | 1, 3, 50 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm -(𝑁 − 1)) = -(𝐴 Yrm (𝑁 − 1))) |
52 | | rmyneg 36511 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) |
53 | 52 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) |
54 | 51, 53 | oveq12d 6567 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → ((𝐴 Yrm -(𝑁 − 1)) + (𝐴 Yrm -𝑁)) = (-(𝐴 Yrm (𝑁 − 1)) + -(𝐴 Yrm 𝑁))) |
55 | | zcn 11259 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
56 | 55 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 𝑁 ∈ ℂ) |
57 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
58 | | negsubdi 10216 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝑁 −
1) = (-𝑁 +
1)) |
59 | 56, 57, 58 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → -(𝑁 − 1) = (-𝑁 + 1)) |
60 | 59 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (𝐴 Yrm -(𝑁 − 1)) = (𝐴 Yrm (-𝑁 + 1))) |
61 | 60 | oveq1d 6564 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → ((𝐴 Yrm -(𝑁 − 1)) + (𝐴 Yrm -𝑁)) = ((𝐴 Yrm (-𝑁 + 1)) + (𝐴 Yrm -𝑁))) |
62 | 49, 54, 61 | 3eqtr2d 2650 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → -((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) = ((𝐴 Yrm (-𝑁 + 1)) + (𝐴 Yrm -𝑁))) |
63 | 46, 62 | breqtrrd 4611 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 < -((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁))) |
64 | 11 | lt0neg1d 10476 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → (((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < 0 ↔ 0 < -((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)))) |
65 | 63, 64 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < 0) |
66 | 15 | nn0ge0d 11231 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → 0 ≤ (𝐴 Xrm 𝑁)) |
67 | 11, 12, 16, 65, 66 | ltletrd 10076 |
. 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≤ 0) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) |
68 | | simpll 786 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → 𝐴 ∈
(ℤ≥‘2)) |
69 | | elnnz 11264 |
. . . . 5
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
70 | 69 | biimpri 217 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 0 <
𝑁) → 𝑁 ∈ ℕ) |
71 | 70 | adantll 746 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ) |
72 | | jm2.24nn 36544 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) |
73 | 68, 71, 72 | syl2anc 691 |
. 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) |
74 | 29 | adantl 481 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ) |
75 | | 0re 9919 |
. . 3
⊢ 0 ∈
ℝ |
76 | | lelttric 10023 |
. . 3
⊢ ((𝑁 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑁 ≤ 0
∨ 0 < 𝑁)) |
77 | 74, 75, 76 | sylancl 693 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 0 ∨ 0 < 𝑁)) |
78 | 67, 73, 77 | mpjaodan 823 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) |