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 ⊢ ∅ ∈ ℂ → ∅ ⇝ ∅