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 
|- ( (/) e. CC -> (/) ~~> (/) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( (/) e. CC -> (/) e. CC )
2 0zd 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> 0 e. ZZ )
3 simpl 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> (/) e. CC )
4 subid 
 |-  ( (/) e. CC -> ( (/) - (/) ) = 0 )
5 4 fveq2d 
 |-  ( (/) e. CC -> ( abs ` ( (/) - (/) ) ) = ( abs ` 0 ) )
6 abs0 
 |-  ( abs ` 0 ) = 0
7 6 a1i 
 |-  ( (/) e. CC -> ( abs ` 0 ) = 0 )
8 5 7 eqtrd 
 |-  ( (/) e. CC -> ( abs ` ( (/) - (/) ) ) = 0 )
9 8 adantr 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> ( abs ` ( (/) - (/) ) ) = 0 )
10 rpgt0 
 |-  ( x e. RR+ -> 0 < x )
11 10 adantl 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> 0 < x )
12 9 11 eqbrtrd 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> ( abs ` ( (/) - (/) ) ) < x )
13 3 12 jca 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) )
14 13 ralrimivw 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> A. k e. ( ZZ>= ` 0 ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) )
15 fveq2 
 |-  ( m = 0 -> ( ZZ>= ` m ) = ( ZZ>= ` 0 ) )
16 15 raleqdv 
 |-  ( m = 0 -> ( A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) <-> A. k e. ( ZZ>= ` 0 ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) ) )
17 16 rspcev 
 |-  ( ( 0 e. ZZ /\ A. k e. ( ZZ>= ` 0 ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) ) -> E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) )
18 2 14 17 syl2anc 
 |-  ( ( (/) e. CC /\ x e. RR+ ) -> E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) )
19 18 ralrimiva 
 |-  ( (/) e. CC -> A. x e. RR+ E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) )
20 1 19 jca 
 |-  ( (/) e. CC -> ( (/) e. CC /\ A. x e. RR+ E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) ) )
21 0ex 
 |-  (/) e. _V
22 21 a1i 
 |-  ( T. -> (/) e. _V )
23 0fv 
 |-  ( (/) ` k ) = (/)
24 23 a1i 
 |-  ( ( T. /\ k e. ZZ ) -> ( (/) ` k ) = (/) )
25 22 24 clim 
 |-  ( T. -> ( (/) ~~> (/) <-> ( (/) e. CC /\ A. x e. RR+ E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) ) ) )
26 25 mptru 
 |-  ( (/) ~~> (/) <-> ( (/) e. CC /\ A. x e. RR+ E. m e. ZZ A. k e. ( ZZ>= ` m ) ( (/) e. CC /\ ( abs ` ( (/) - (/) ) ) < x ) ) )
27 20 26 sylibr 
 |-  ( (/) e. CC -> (/) ~~> (/) )