Metamath Proof Explorer

Theorem iscmet3lem3

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion iscmet3lem3 ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 simpl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
3 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℝ+ )
4 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
5 4 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
6 5 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
7 oveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 1 / 2 ) ↑ 𝑛 ) = ( ( 1 / 2 ) ↑ 𝑘 ) )
8 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) )
9 ovex ⊢ ( ( 1 / 2 ) ↑ 𝑘 ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 2 ) ↑ 𝑘 ) )
11 6 10 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 2 ) ↑ 𝑘 ) )
12 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
13 12 reseq2i ⊢ ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ℕ0 ) = ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ( ℤ≥ ‘ 0 ) )
14 nn0ssz ⊢ ℕ0 ⊆ ℤ
15 resmpt ⊢ ( ℕ0 ⊆ ℤ → ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ℕ0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) )
16 14 15 ax-mp ⊢ ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ℕ0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑛 ) )
17 13 16 eqtr3i ⊢ ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ( ℤ≥ ‘ 0 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑛 ) )
18 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
19 18 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( 1 / 2 ) ∈ ℂ )
20 halfre ⊢ ( 1 / 2 ) ∈ ℝ
21 halfge0 ⊢ 0 ≤ ( 1 / 2 )
22 absid ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ) → ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 ) )
23 20 21 22 mp2an ⊢ ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 )
24 halflt1 ⊢ ( 1 / 2 ) < 1
25 23 24 eqbrtri ⊢ ( abs ‘ ( 1 / 2 ) ) < 1
26 25 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( abs ‘ ( 1 / 2 ) ) < 1 )
27 19 26 expcnv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ⇝ 0 )
28 17 27 eqbrtrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ( ℤ≥ ‘ 0 ) ) ⇝ 0 )
29 0z ⊢ 0 ∈ ℤ
30 zex ⊢ ℤ ∈ V
31 30 mptex ⊢ ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ∈ V
32 31 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ∈ V )
33 climres ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ∈ V ) → ( ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ( ℤ≥ ‘ 0 ) ) ⇝ 0 ↔ ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ⇝ 0 ) )
34 29 32 33 sylancr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( ( ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ↾ ( ℤ≥ ‘ 0 ) ) ⇝ 0 ↔ ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ⇝ 0 ) )
35 28 34 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑛 ∈ ℤ ↦ ( ( 1 / 2 ) ↑ 𝑛 ) ) ⇝ 0 )
36 1 2 3 11 35 climi0 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 )
37 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
38 1rp ⊢ 1 ∈ ℝ+
39 rphalfcl ⊢ ( 1 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
40 38 39 ax-mp ⊢ ( 1 / 2 ) ∈ ℝ+
41 rpexpcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
42 40 6 41 sylancr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
43 rpre ⊢ ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ )
44 rpge0 ⊢ ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ → 0 ≤ ( ( 1 / 2 ) ↑ 𝑘 ) )
45 43 44 absidd ⊢ ( ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ → ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) = ( ( 1 / 2 ) ↑ 𝑘 ) )
46 42 45 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) = ( ( 1 / 2 ) ↑ 𝑘 ) )
47 46 breq1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 ↔ ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 ) )
48 37 47 sylan2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 ↔ ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 ) )
49 48 anassrs ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 ↔ ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 ) )
50 49 ralbidva ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 ) )
51 50 rexbidva ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 1 / 2 ) ↑ 𝑘 ) ) < 𝑅 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 ) )
52 36 51 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑅 )