Metamath Proof Explorer


Theorem constrsscn

Description: Closure of the constructible points in the complex numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
constrsscn.1 φ N On
Assertion constrsscn φ C N

Proof

Step Hyp Ref Expression
1 constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
2 constrsscn.1 φ N On
3 fveq2 m = C m = C
4 3 sseq1d m = C m C
5 fveq2 m = n C m = C n
6 5 sseq1d m = n C m C n
7 fveq2 m = suc n C m = C suc n
8 7 sseq1d m = suc n C m C suc n
9 fveq2 m = N C m = C N
10 9 sseq1d m = N C m C N
11 1 constr0 C = 0 1
12 0cn 0
13 ax-1cn 1
14 prssi 0 1 0 1
15 12 13 14 mp2an 0 1
16 11 15 eqsstri C
17 simpl n On C n n On
18 eqid C n = C n
19 1 17 18 constrsuc n On C n x C suc n x a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
20 19 biimpa n On C n x C suc n x a C n b C n c C n d C n t r x = a + t b a x = c + r d c b a d c 0 a C n b C n c C n e C n f C n t x = a + t b a x c = e f a C n b C n c C n d C n e C n f C n a d x a = b c x d = e f
21 20 simpld n On C n x C suc n x
22 21 ex n On C n x C suc n x
23 22 ssrdv n On C n C suc n
24 23 ex n On C n C suc n
25 vex m V
26 25 a1i Lim m n m C n m V
27 simpl Lim m n m C n Lim m
28 1 26 27 constrlim Lim m n m C n C m = o m C o
29 fveq2 n = o C n = C o
30 29 sseq1d n = o C n C o
31 simplr Lim m n m C n o m n m C n
32 simpr Lim m n m C n o m o m
33 30 31 32 rspcdva Lim m n m C n o m C o
34 33 iunssd Lim m n m C n o m C o
35 28 34 eqsstrd Lim m n m C n C m
36 35 ex Lim m n m C n C m
37 4 6 8 10 16 24 36 tfinds N On C N
38 2 37 syl φ C N