Step | Hyp | Ref
| Expression |
1 | | iscmet3.1 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | simpl 486 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ 𝑀 ∈
ℤ) |
3 | | simpr 488 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℝ+) |
4 | | eluzelz 12448 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
5 | 4, 1 | eleq2s 2856 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
6 | 5 | adantl 485 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
7 | | oveq2 7221 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘)) |
8 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) = (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) |
9 | | ovex 7246 |
. . . . 5
⊢ ((1 /
2)↑𝑘) ∈
V |
10 | 7, 8, 9 | fvmpt 6818 |
. . . 4
⊢ (𝑘 ∈ ℤ → ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
11 | 6, 10 | syl 17 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
12 | | nn0uz 12476 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
13 | 12 | reseq2i 5848 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ↾
ℕ0) = ((𝑛
∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾
(ℤ≥‘0)) |
14 | | nn0ssz 12198 |
. . . . . . 7
⊢
ℕ0 ⊆ ℤ |
15 | | resmpt 5905 |
. . . . . . 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 2767 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ↾
(ℤ≥‘0)) = (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛)) |
18 | | halfcn 12045 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (1 / 2) ∈ ℂ) |
20 | | halfre 12044 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
21 | | halfge0 12047 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 2) |
22 | | absid 14860 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
23 | 20, 21, 22 | mp2an 692 |
. . . . . . . 8
⊢
(abs‘(1 / 2)) = (1 / 2) |
24 | | halflt1 12048 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
25 | 23, 24 | eqbrtri 5074 |
. . . . . . 7
⊢
(abs‘(1 / 2)) < 1 |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (abs‘(1 / 2)) < 1) |
27 | 19, 26 | expcnv 15428 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) ⇝ 0) |
28 | 17, 27 | eqbrtrid 5088 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ((𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
↾ (ℤ≥‘0)) ⇝ 0) |
29 | | 0z 12187 |
. . . . 5
⊢ 0 ∈
ℤ |
30 | | zex 12185 |
. . . . . . 7
⊢ ℤ
∈ V |
31 | 30 | mptex 7039 |
. . . . . 6
⊢ (𝑛 ∈ ℤ ↦ ((1 /
2)↑𝑛)) ∈
V |
32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
∈ V) |
33 | | climres 15136 |
. . . . 5
⊢ ((0
∈ ℤ ∧ (𝑛
∈ ℤ ↦ ((1 / 2)↑𝑛)) ∈ V) → (((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾
(ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0)) |
34 | 29, 32, 33 | sylancr 590 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (((𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
↾ (ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0)) |
35 | 28, 34 | mpbid 235 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (𝑛 ∈ ℤ
↦ ((1 / 2)↑𝑛))
⇝ 0) |
36 | 1, 2, 3, 11, 35 | climi0 15073 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅) |
37 | 1 | uztrn2 12457 |
. . . . . 6
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
38 | | 1rp 12590 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
39 | | rphalfcl 12613 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ+ |
41 | | rpexpcl 13654 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈
ℝ+) |
42 | 40, 6, 41 | sylancr 590 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈
ℝ+) |
43 | | rpre 12594 |
. . . . . . . . 9
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → ((1 / 2)↑𝑘) ∈ ℝ) |
44 | | rpge0 12599 |
. . . . . . . . 9
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → 0 ≤ ((1 / 2)↑𝑘)) |
45 | 43, 44 | absidd 14986 |
. . . . . . . 8
⊢ (((1 /
2)↑𝑘) ∈
ℝ+ → (abs‘((1 / 2)↑𝑘)) = ((1 / 2)↑𝑘)) |
46 | 42, 45 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → (abs‘((1 /
2)↑𝑘)) = ((1 /
2)↑𝑘)) |
47 | 46 | breq1d 5063 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑘 ∈ 𝑍) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
48 | 37, 47 | sylan2 596 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
49 | 48 | anassrs 471 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘((1 /
2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅)) |
50 | 49 | ralbidva 3117 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)) |
51 | 50 | rexbidva 3215 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ (∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)) |
52 | 36, 51 | mpbid 235 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+)
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅) |