Metamath Proof Explorer

Theorem lmnn

Description: A condition that implies convergence. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmnn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
lmnn.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
lmnn.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
lmnn.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
lmnn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < ( 1 / 𝑘 ) )
Assertion lmnn ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 lmnn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 lmnn.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 lmnn.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
4 lmnn.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
5 lmnn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < ( 1 / 𝑘 ) )
6 rpreccl ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
8 7 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ )
9 7 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( 1 / 𝑥 ) )
10 flge0nn0 ⊢ ( ( ( 1 / 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝑥 ) ) → ( ⌊ ‘ ( 1 / 𝑥 ) ) ∈ ℕ0 )
11 8 9 10 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ ( 1 / 𝑥 ) ) ∈ ℕ0 )
12 nn0p1nn ⊢ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℕ )
13 11 12 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℕ )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝐹 : ℕ ⟶ 𝑋 )
16 eluznn ⊢ ( ( ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑘 ∈ ℕ )
17 13 16 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑘 ∈ ℕ )
18 15 17 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
19 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑃 ∈ 𝑋 )
20 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) ∈ ℝ* )
21 14 18 19 20 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) ∈ ℝ* )
22 17 nnrecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
23 22 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ* )
24 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
25 24 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑥 ∈ ℝ* )
26 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < ( 1 / 𝑘 ) )
27 17 26 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < ( 1 / 𝑘 ) )
28 8 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑥 ) ∈ ℝ )
29 13 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℝ )
31 17 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑘 ∈ ℝ )
32 flltp1 ⊢ ( ( 1 / 𝑥 ) ∈ ℝ → ( 1 / 𝑥 ) < ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) )
33 28 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑥 ) < ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) )
34 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ≤ 𝑘 )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ≤ 𝑘 )
36 28 30 31 33 35 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑥 ) < 𝑘 )
37 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → 𝑥 ∈ ℝ+ )
38 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
39 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
40 39 rpregt0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
41 ltrec1 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 1 / 𝑥 ) < 𝑘 ↔ ( 1 / 𝑘 ) < 𝑥 ) )
42 38 40 41 syl2an ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑥 ) < 𝑘 ↔ ( 1 / 𝑘 ) < 𝑥 ) )
43 37 17 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( 1 / 𝑥 ) < 𝑘 ↔ ( 1 / 𝑘 ) < 𝑥 ) )
44 36 43 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( 1 / 𝑘 ) < 𝑥 )
45 21 23 25 27 44 xrlttrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 )
46 45 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 )
47 fveq2 ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) )
48 47 raleqdv ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) )
49 48 rspcev ⊢ ( ( ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / 𝑥 ) ) + 1 ) ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 )
50 13 46 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 )
51 50 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 )
52 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
53 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
54 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
55 1 2 52 53 54 4 lmmbrf ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
56 3 51 55 mpbir2and ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )