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 e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 
|- ( ph -> N e. On )
Assertion constrsscn 
|- ( ph -> ( C ` N ) C_ CC )

Proof

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