This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmclim

Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmclim.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
lmclim.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion lmclim ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 lmclim.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 lmclim.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 3anass ⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ) )
4 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
5 3anass ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) )
6 simplr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) → 𝑍 ⊆ dom 𝐹 )
7 6 sselda ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
8 7 biantrurd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ) )
9 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
10 9 cnmetdval ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) )
11 10 ancoms ⊢ ( ( 𝑃 ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) )
12 11 breq1d ⊢ ( ( 𝑃 ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) )
13 12 pm5.32da ⊢ ( 𝑃 ∈ ℂ → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
14 13 ad2antlr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
15 8 14 bitr3d ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
16 5 15 bitrid ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
17 4 16 sylan2 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
18 17 anassrs ⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
19 18 ralbidva ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
20 19 rexbidva ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
21 20 ralbidv ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝑃 ∈ ℂ ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) )
22 21 pm5.32da ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ↔ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) ) )
23 22 anbi2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) ) ) )
24 3 23 bitrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) ) ) )
25 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
26 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
27 26 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
28 simpl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → 𝑀 ∈ ℤ )
29 25 27 2 28 lmmbr3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑘 ) ( abs ∘ − ) 𝑃 ) < 𝑥 ) ) ) )
30 simpll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) → 𝑀 ∈ ℤ )
31 simpr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
32 eqidd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
33 2 30 31 32 clim2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) → ( 𝐹 ⇝ 𝑃 ↔ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) ) )
34 33 pm5.32da ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ ( 𝑃 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝑃 ) ) < 𝑥 ) ) ) ) )
35 24 29 34 3bitr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ) )