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

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 ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 0 ∈ ℤ )
3 simpl ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∅ ∈ ℂ )
4 subid ⊢ ( ∅ ∈ ℂ → ( ∅ − ∅ ) = 0 )
5 4 fveq2d ⊢ ( ∅ ∈ ℂ → ( abs ‘ ( ∅ − ∅ ) ) = ( abs ‘ 0 ) )
6 abs0 ⊢ ( abs ‘ 0 ) = 0
7 6 a1i ⊢ ( ∅ ∈ ℂ → ( abs ‘ 0 ) = 0 )
8 5 7 eqtrd ⊢ ( ∅ ∈ ℂ → ( abs ‘ ( ∅ − ∅ ) ) = 0 )
9 8 adantr ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ∅ − ∅ ) ) = 0 )
10 rpgt0 ⊢ ( 𝑥 ∈ ℝ+ → 0 < 𝑥 )
11 10 adantl ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 0 < 𝑥 )
12 9 11 eqbrtrd ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 )
13 3 12 jca ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) )
14 13 ralrimivw ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) )
15 fveq2 ⊢ ( 𝑚 = 0 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 0 ) )
16 15 raleqdv ⊢ ( 𝑚 = 0 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ) )
17 16 rspcev ⊢ ( ( 0 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ) → ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) )
18 2 14 17 syl2anc ⊢ ( ( ∅ ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) )
19 18 ralrimiva ⊢ ( ∅ ∈ ℂ → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) )
20 1 19 jca ⊢ ( ∅ ∈ ℂ → ( ∅ ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ) )
21 0ex ⊢ ∅ ∈ V
22 21 a1i ⊢ ( ⊤ → ∅ ∈ V )
23 0fv ⊢ ( ∅ ‘ 𝑘 ) = ∅
24 23 a1i ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℤ ) → ( ∅ ‘ 𝑘 ) = ∅ )
25 22 24 clim ⊢ ( ⊤ → ( ∅ ⇝ ∅ ↔ ( ∅ ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ) ) )
26 25 mptru ⊢ ( ∅ ⇝ ∅ ↔ ( ∅ ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ∅ ∈ ℂ ∧ ( abs ‘ ( ∅ − ∅ ) ) < 𝑥 ) ) )
27 20 26 sylibr ⊢ ( ∅ ∈ ℂ → ∅ ⇝ ∅ )