Metamath Proof Explorer

Theorem constrdircl

Description: Constructible numbers are closed under taking the point on the unit circle having the same argument. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constrdircl.x 
|- ( ph -> X e. Constr )
constrdircl.1 
|- ( ph -> X =/= 0 )
Assertion constrdircl 
|- ( ph -> ( X / ( abs ` X ) ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrdircl.x 
 |-  ( ph -> X e. Constr )
2 constrdircl.1 
 |-  ( ph -> X =/= 0 )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( ph -> 0 e. NN0 )
5 4 nn0constr 
 |-  ( ph -> 0 e. Constr )
6 1nn0 
 |-  1 e. NN0
7 6 a1i 
 |-  ( ph -> 1 e. NN0 )
8 7 nn0constr 
 |-  ( ph -> 1 e. Constr )
9 1 constrcn 
 |-  ( ph -> X e. CC )
10 9 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
11 9 2 absne0d 
 |-  ( ph -> ( abs ` X ) =/= 0 )
12 10 11 rereccld 
 |-  ( ph -> ( 1 / ( abs ` X ) ) e. RR )
13 10 recnd 
 |-  ( ph -> ( abs ` X ) e. CC )
14 9 13 11 divcld 
 |-  ( ph -> ( X / ( abs ` X ) ) e. CC )
15 9 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
16 15 oveq2d 
 |-  ( ph -> ( ( 1 / ( abs ` X ) ) x. ( X - 0 ) ) = ( ( 1 / ( abs ` X ) ) x. X ) )
17 12 recnd 
 |-  ( ph -> ( 1 / ( abs ` X ) ) e. CC )
18 15 9 eqeltrd 
 |-  ( ph -> ( X - 0 ) e. CC )
19 17 18 mulcld 
 |-  ( ph -> ( ( 1 / ( abs ` X ) ) x. ( X - 0 ) ) e. CC )
20 19 addlidd 
 |-  ( ph -> ( 0 + ( ( 1 / ( abs ` X ) ) x. ( X - 0 ) ) ) = ( ( 1 / ( abs ` X ) ) x. ( X - 0 ) ) )
21 9 13 11 divrec2d 
 |-  ( ph -> ( X / ( abs ` X ) ) = ( ( 1 / ( abs ` X ) ) x. X ) )
22 16 20 21 3eqtr4rd 
 |-  ( ph -> ( X / ( abs ` X ) ) = ( 0 + ( ( 1 / ( abs ` X ) ) x. ( X - 0 ) ) ) )
23 1red 
 |-  ( ph -> 1 e. RR )
24 7 nn0ge0d 
 |-  ( ph -> 0 <_ 1 )
25 23 24 absidd 
 |-  ( ph -> ( abs ` 1 ) = 1 )
26 1m0e1 
 |-  ( 1 - 0 ) = 1
27 26 a1i 
 |-  ( ph -> ( 1 - 0 ) = 1 )
28 27 fveq2d 
 |-  ( ph -> ( abs ` ( 1 - 0 ) ) = ( abs ` 1 ) )
29 14 subid1d 
 |-  ( ph -> ( ( X / ( abs ` X ) ) - 0 ) = ( X / ( abs ` X ) ) )
30 29 fveq2d 
 |-  ( ph -> ( abs ` ( ( X / ( abs ` X ) ) - 0 ) ) = ( abs ` ( X / ( abs ` X ) ) ) )
31 9 13 11 absdivd 
 |-  ( ph -> ( abs ` ( X / ( abs ` X ) ) ) = ( ( abs ` X ) / ( abs ` ( abs ` X ) ) ) )
32 absidm 
 |-  ( X e. CC -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
33 9 32 syl 
 |-  ( ph -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
34 33 oveq2d 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` ( abs ` X ) ) ) = ( ( abs ` X ) / ( abs ` X ) ) )
35 13 11 dividd 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` X ) ) = 1 )
36 34 35 eqtrd 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` ( abs ` X ) ) ) = 1 )
37 30 31 36 3eqtrd 
 |-  ( ph -> ( abs ` ( ( X / ( abs ` X ) ) - 0 ) ) = 1 )
38 25 28 37 3eqtr4rd 
 |-  ( ph -> ( abs ` ( ( X / ( abs ` X ) ) - 0 ) ) = ( abs ` ( 1 - 0 ) ) )
39 5 1 5 8 5 12 14 22 38 constrlccl 
 |-  ( ph -> ( X / ( abs ` X ) ) e. Constr )