Step | Hyp | Ref
| Expression |
1 | | iscmet3.1 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | simpl 472 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ 𝑀 ∈
ℤ) |
3 | | simpr 476 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℝ+) |
4 | | eluzelz 11573 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
5 | 4, 1 | eleq2s 2706 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
6 | 5 | adantl 481 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
7 | | oveq2 6557 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘)) |
8 | | eqid 2610 |
. . . . 5
⊢ (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) = (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) |
9 | | ovex 6577 |
. . . . 5
⊢ ((1 /
2)↑𝑘) ∈
V |
10 | 7, 8, 9 | fvmpt 6191 |
. . . 4
⊢ (𝑘 ∈ ℤ → ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
11 | 6, 10 | syl 17 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
12 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
13 | 12 | reseq2i 5314 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ↾
ℕ0) = ((𝑛
∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾
(ℤ≥‘0)) |
14 | | nn0ssz 11275 |
. . . . . . 7
⊢
ℕ0 ⊆ ℤ |
15 | | resmpt 5369 |
. . . . . . 7
⊢
(ℕ0 ⊆ ℤ → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ ℕ0)
= (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ↾
ℕ0) = (𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛)) |
17 | 13, 16 | eqtr3i 2634 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ↾
(ℤ≥‘0)) = (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛)) |
18 | | halfcn 11124 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (1 / 2) ∈ ℂ) |
20 | | halfre 11123 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
21 | | 1rp 11712 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ+ |
22 | | rphalfcl 11734 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℝ+ |
24 | | rpge0 11721 |
. . . . . . . . . 10
⊢ ((1 / 2)
∈ ℝ+ → 0 ≤ (1 / 2)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 2) |
26 | | absid 13884 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
27 | 20, 25, 26 | mp2an 704 |
. . . . . . . 8
⊢
(abs‘(1 / 2)) = (1 / 2) |
28 | | halflt1 11127 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
29 | 27, 28 | eqbrtri 4604 |
. . . . . . 7
⊢
(abs‘(1 / 2)) < 1 |
30 | 29 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (abs‘(1 / 2)) < 1) |
31 | 19, 30 | expcnv 14435 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) ⇝ 0) |
32 | 17, 31 | syl5eqbr 4618 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ((𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
↾ (ℤ≥‘0)) ⇝ 0) |
33 | | 0z 11265 |
. . . . 5
⊢ 0 ∈
ℤ |
34 | | zex 11263 |
. . . . . . 7
⊢ ℤ
∈ V |
35 | 34 | mptex 6390 |
. . . . . 6
⊢ (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ∈
V |
36 | 35 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
∈ V) |
37 | | climres 14154 |
. . . . 5
⊢ ((0
∈ ℤ ∧ (𝑛
∈ ℤ ↦ ((1 / 2)↑𝑛)) ∈ V) → (((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾
(ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0)) |
38 | 33, 36, 37 | sylancr 694 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (((𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
↾ (ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0)) |
39 | 32, 38 | mpbid 221 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
⇝ 0) |
40 | 1, 2, 3, 11, 39 | climi0 14091 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅) |
41 | 1 | uztrn2 11581 |
. . . . . 6
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
42 | | rpexpcl 12741 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈
ℝ+) |
43 | 23, 6, 42 | sylancr 694 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈
ℝ+) |
44 | | rpre 11715 |
. . . . . . . . 9
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → ((1 / 2)↑𝑘) ∈ ℝ) |
45 | | rpge0 11721 |
. . . . . . . . 9
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → 0 ≤ ((1 / 2)↑𝑘)) |
46 | 44, 45 | absidd 14009 |
. . . . . . . 8
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → (abs‘((1 / 2)↑𝑘)) = ((1 / 2)↑𝑘)) |
47 | 43, 46 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → (abs‘((1 /
2)↑𝑘)) = ((1 /
2)↑𝑘)) |
48 | 47 | breq1d 4593 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
49 | 41, 48 | sylan2 490 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
50 | 49 | anassrs 678 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
51 | 50 | ralbidva 2968 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)) |
52 | 51 | rexbidva 3031 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)) |
53 | 40, 52 | mpbid 221 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅) |