Metamath Proof Explorer

Theorem constr0

Description: The first step of the construction of constructible numbers is the pair { 0 , 1 } . In this theorem and the following, we use ( CN ) for the N -th intermediate iteration of the constructible number. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypothesis 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 } )
Assertion constr0 
|- ( C ` (/) ) = { 0 , 1 }

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 1 fveq1i 
 |-  ( 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 } ) ` (/) )
3 prex 
 |-  { 0 , 1 } e. _V
4 3 rdg0 
 |-  ( 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 } ) ` (/) ) = { 0 , 1 }
5 2 4 eqtri 
 |-  ( C ` (/) ) = { 0 , 1 }