Metamath Proof Explorer

Theorem 0cnv

Description: If (/) is a complex number, then it converges to itself. See 0ncn and its comment; see also the comment in climlimsupcex . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion 0cnv ⊢∅∈ℂ→∅⇝∅

Proof

Step Hyp Ref Expression
1 id ⊢∅∈ℂ→∅∈ℂ
2 0zd ⊢∅∈ℂ∧x∈ℝ+→0∈ℤ
3 simpl ⊢∅∈ℂ∧x∈ℝ+→∅∈ℂ
4 subid ⊢∅∈ℂ→∅−∅=0
5 4 fveq2d ⊢∅∈ℂ→∅−∅=0
6 abs0 ⊢0=0
7 6 a1i ⊢∅∈ℂ→0=0
8 5 7 eqtrd ⊢∅∈ℂ→∅−∅=0
9 8 adantr ⊢∅∈ℂ∧x∈ℝ+→∅−∅=0
10 rpgt0 ⊢x∈ℝ+→0<x
11 10 adantl ⊢∅∈ℂ∧x∈ℝ+→0<x
12 9 11 eqbrtrd ⊢∅∈ℂ∧x∈ℝ+→∅−∅<x
13 3 12 jca ⊢∅∈ℂ∧x∈ℝ+→∅∈ℂ∧∅−∅<x
14 13 ralrimivw ⊢∅∈ℂ∧x∈ℝ+→∀k∈ℤ≥0∅∈ℂ∧∅−∅<x
15 fveq2 ⊢m=0→ℤ≥m=ℤ≥0
16 15 raleqdv ⊢m=0→∀k∈ℤ≥m∅∈ℂ∧∅−∅<x↔∀k∈ℤ≥0∅∈ℂ∧∅−∅<x
17 16 rspcev ⊢0∈ℤ∧∀k∈ℤ≥0∅∈ℂ∧∅−∅<x→∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
18 2 14 17 syl2anc ⊢∅∈ℂ∧x∈ℝ+→∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
19 18 ralrimiva ⊢∅∈ℂ→∀x∈ℝ+∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
20 1 19 jca ⊢∅∈ℂ→∅∈ℂ∧∀x∈ℝ+∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
21 0ex ⊢∅∈V
22 21 a1i ⊢⊤→∅∈V
23 0fv ⊢∅⁡k=∅
24 23 a1i ⊢⊤∧k∈ℤ→∅⁡k=∅
25 22 24 clim ⊢⊤→∅⇝∅↔∅∈ℂ∧∀x∈ℝ+∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
26 25 mptru ⊢∅⇝∅↔∅∈ℂ∧∀x∈ℝ+∃m∈ℤ∀k∈ℤ≥m∅∈ℂ∧∅−∅<x
27 20 26 sylibr ⊢∅∈ℂ→∅⇝∅