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