Metamath Proof Explorer

Theorem constrimcl

Description: Constructible numbers are closed under taking the imaginary part. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypothesis constrcjcl.1 
|- ( ph -> X e. Constr )
Assertion constrimcl 
|- ( ph -> ( Im ` X ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrcjcl.1 
 |-  ( ph -> X e. Constr )
2 0zd 
 |-  ( ph -> 0 e. ZZ )
3 2 zconstr 
 |-  ( ph -> 0 e. Constr )
4 1zzd 
 |-  ( ph -> 1 e. ZZ )
5 4 zconstr 
 |-  ( ph -> 1 e. Constr )
6 1 constrcn 
 |-  ( ph -> X e. CC )
7 6 recld 
 |-  ( ph -> ( Re ` X ) e. RR )
8 7 recnd 
 |-  ( ph -> ( Re ` X ) e. CC )
9 ax-icn 
 |-  _i e. CC
10 9 a1i 
 |-  ( ph -> _i e. CC )
11 6 imcld 
 |-  ( ph -> ( Im ` X ) e. RR )
12 11 recnd 
 |-  ( ph -> ( Im ` X ) e. CC )
13 10 12 mulcld 
 |-  ( ph -> ( _i x. ( Im ` X ) ) e. CC )
14 6 replimd 
 |-  ( ph -> X = ( ( Re ` X ) + ( _i x. ( Im ` X ) ) ) )
15 8 13 14 mvrladdd 
 |-  ( ph -> ( X - ( Re ` X ) ) = ( _i x. ( Im ` X ) ) )
16 6 8 negsubd 
 |-  ( ph -> ( X + -u ( Re ` X ) ) = ( X - ( Re ` X ) ) )
17 1 constrrecl 
 |-  ( ph -> ( Re ` X ) e. Constr )
18 17 constrnegcl 
 |-  ( ph -> -u ( Re ` X ) e. Constr )
19 1 18 constraddcl 
 |-  ( ph -> ( X + -u ( Re ` X ) ) e. Constr )
20 16 19 eqeltrrd 
 |-  ( ph -> ( X - ( Re ` X ) ) e. Constr )
21 15 20 eqeltrrd 
 |-  ( ph -> ( _i x. ( Im ` X ) ) e. Constr )
22 1m0e1 
 |-  ( 1 - 0 ) = 1
23 1cnd 
 |-  ( ph -> 1 e. CC )
24 22 23 eqeltrid 
 |-  ( ph -> ( 1 - 0 ) e. CC )
25 12 24 mulcld 
 |-  ( ph -> ( ( Im ` X ) x. ( 1 - 0 ) ) e. CC )
26 25 addlidd 
 |-  ( ph -> ( 0 + ( ( Im ` X ) x. ( 1 - 0 ) ) ) = ( ( Im ` X ) x. ( 1 - 0 ) ) )
27 22 a1i 
 |-  ( ph -> ( 1 - 0 ) = 1 )
28 27 oveq2d 
 |-  ( ph -> ( ( Im ` X ) x. ( 1 - 0 ) ) = ( ( Im ` X ) x. 1 ) )
29 12 mulridd 
 |-  ( ph -> ( ( Im ` X ) x. 1 ) = ( Im ` X ) )
30 26 28 29 3eqtrrd 
 |-  ( ph -> ( Im ` X ) = ( 0 + ( ( Im ` X ) x. ( 1 - 0 ) ) ) )
31 10 12 absmuld 
 |-  ( ph -> ( abs ` ( _i x. ( Im ` X ) ) ) = ( ( abs ` _i ) x. ( abs ` ( Im ` X ) ) ) )
32 absi 
 |-  ( abs ` _i ) = 1
33 32 a1i 
 |-  ( ph -> ( abs ` _i ) = 1 )
34 33 oveq1d 
 |-  ( ph -> ( ( abs ` _i ) x. ( abs ` ( Im ` X ) ) ) = ( 1 x. ( abs ` ( Im ` X ) ) ) )
35 12 abscld 
 |-  ( ph -> ( abs ` ( Im ` X ) ) e. RR )
36 35 recnd 
 |-  ( ph -> ( abs ` ( Im ` X ) ) e. CC )
37 36 mullidd 
 |-  ( ph -> ( 1 x. ( abs ` ( Im ` X ) ) ) = ( abs ` ( Im ` X ) ) )
38 31 34 37 3eqtrd 
 |-  ( ph -> ( abs ` ( _i x. ( Im ` X ) ) ) = ( abs ` ( Im ` X ) ) )
39 13 subid1d 
 |-  ( ph -> ( ( _i x. ( Im ` X ) ) - 0 ) = ( _i x. ( Im ` X ) ) )
40 39 fveq2d 
 |-  ( ph -> ( abs ` ( ( _i x. ( Im ` X ) ) - 0 ) ) = ( abs ` ( _i x. ( Im ` X ) ) ) )
41 12 subid1d 
 |-  ( ph -> ( ( Im ` X ) - 0 ) = ( Im ` X ) )
42 41 fveq2d 
 |-  ( ph -> ( abs ` ( ( Im ` X ) - 0 ) ) = ( abs ` ( Im ` X ) ) )
43 38 40 42 3eqtr4rd 
 |-  ( ph -> ( abs ` ( ( Im ` X ) - 0 ) ) = ( abs ` ( ( _i x. ( Im ` X ) ) - 0 ) ) )
44 3 5 3 21 3 11 12 30 43 constrlccl 
 |-  ( ph -> ( Im ` X ) e. Constr )