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	syl5bb	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ 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	syl5bb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ 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 ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ) )

Metamath Proof Explorer

Theorem lmclim

Proof