Metamath Proof Explorer

Theorem constrinvcl

Description: Constructible numbers are closed under complex inverse. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypotheses constrinvcl.1 
|- ( ph -> X e. Constr )
constrinvcl.2 
|- ( ph -> X =/= 0 )
Assertion constrinvcl 
|- ( ph -> ( 1 / X ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrinvcl.1 
 |-  ( ph -> X e. Constr )
2 constrinvcl.2 
 |-  ( ph -> X =/= 0 )
3 1 adantr 
 |-  ( ( ph /\ X e. RR ) -> X e. Constr )
4 2 adantr 
 |-  ( ( ph /\ X e. RR ) -> X =/= 0 )
5 simpr 
 |-  ( ( ph /\ X e. RR ) -> X e. RR )
6 3 4 5 constrreinvcl 
 |-  ( ( ph /\ X e. RR ) -> ( 1 / X ) e. Constr )
7 1cnd 
 |-  ( ph -> 1 e. CC )
8 1 constrcn 
 |-  ( ph -> X e. CC )
9 7 8 2 absdivd 
 |-  ( ph -> ( abs ` ( 1 / X ) ) = ( ( abs ` 1 ) / ( abs ` X ) ) )
10 abs1 
 |-  ( abs ` 1 ) = 1
11 10 oveq1i 
 |-  ( ( abs ` 1 ) / ( abs ` X ) ) = ( 1 / ( abs ` X ) )
12 9 11 eqtr2di 
 |-  ( ph -> ( 1 / ( abs ` X ) ) = ( abs ` ( 1 / X ) ) )
13 8 2 reccld 
 |-  ( ph -> ( 1 / X ) e. CC )
14 8 2 recne0d 
 |-  ( ph -> ( 1 / X ) =/= 0 )
15 13 14 efiargd 
 |-  ( ph -> ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) = ( ( 1 / X ) / ( abs ` ( 1 / X ) ) ) )
16 12 15 oveq12d 
 |-  ( ph -> ( ( 1 / ( abs ` X ) ) x. ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) ) = ( ( abs ` ( 1 / X ) ) x. ( ( 1 / X ) / ( abs ` ( 1 / X ) ) ) ) )
17 13 abscld 
 |-  ( ph -> ( abs ` ( 1 / X ) ) e. RR )
18 17 recnd 
 |-  ( ph -> ( abs ` ( 1 / X ) ) e. CC )
19 13 14 absne0d 
 |-  ( ph -> ( abs ` ( 1 / X ) ) =/= 0 )
20 13 18 19 divcan2d 
 |-  ( ph -> ( ( abs ` ( 1 / X ) ) x. ( ( 1 / X ) / ( abs ` ( 1 / X ) ) ) ) = ( 1 / X ) )
21 16 20 eqtrd 
 |-  ( ph -> ( ( 1 / ( abs ` X ) ) x. ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) ) = ( 1 / X ) )
22 21 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( ( 1 / ( abs ` X ) ) x. ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) ) = ( 1 / X ) )
23 0zd 
 |-  ( ph -> 0 e. ZZ )
24 23 zconstr 
 |-  ( ph -> 0 e. Constr )
25 1zzd 
 |-  ( ph -> 1 e. ZZ )
26 25 zconstr 
 |-  ( ph -> 1 e. Constr )
27 8 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
28 27 recnd 
 |-  ( ph -> ( abs ` X ) e. CC )
29 7 subid1d 
 |-  ( ph -> ( 1 - 0 ) = 1 )
30 29 7 eqeltrd 
 |-  ( ph -> ( 1 - 0 ) e. CC )
31 28 30 mulcld 
 |-  ( ph -> ( ( abs ` X ) x. ( 1 - 0 ) ) e. CC )
32 31 addlidd 
 |-  ( ph -> ( 0 + ( ( abs ` X ) x. ( 1 - 0 ) ) ) = ( ( abs ` X ) x. ( 1 - 0 ) ) )
33 29 oveq2d 
 |-  ( ph -> ( ( abs ` X ) x. ( 1 - 0 ) ) = ( ( abs ` X ) x. 1 ) )
34 28 mulridd 
 |-  ( ph -> ( ( abs ` X ) x. 1 ) = ( abs ` X ) )
35 32 33 34 3eqtrrd 
 |-  ( ph -> ( abs ` X ) = ( 0 + ( ( abs ` X ) x. ( 1 - 0 ) ) ) )
36 8 absge0d 
 |-  ( ph -> 0 <_ ( abs ` X ) )
37 27 36 absidd 
 |-  ( ph -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
38 28 subid1d 
 |-  ( ph -> ( ( abs ` X ) - 0 ) = ( abs ` X ) )
39 38 fveq2d 
 |-  ( ph -> ( abs ` ( ( abs ` X ) - 0 ) ) = ( abs ` ( abs ` X ) ) )
40 8 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
41 40 fveq2d 
 |-  ( ph -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
42 37 39 41 3eqtr4d 
 |-  ( ph -> ( abs ` ( ( abs ` X ) - 0 ) ) = ( abs ` ( X - 0 ) ) )
43 24 26 24 1 24 27 28 35 42 constrlccl 
 |-  ( ph -> ( abs ` X ) e. Constr )
44 8 2 absne0d 
 |-  ( ph -> ( abs ` X ) =/= 0 )
45 43 44 27 constrreinvcl 
 |-  ( ph -> ( 1 / ( abs ` X ) ) e. Constr )
46 45 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( 1 / ( abs ` X ) ) e. Constr )
47 8 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> X e. CC )
48 2 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> X =/= 0 )
49 8 adantr 
 |-  ( ( ph /\ -u X e. RR+ ) -> X e. CC )
50 simpr 
 |-  ( ( ph /\ -u X e. RR+ ) -> -u X e. RR+ )
51 50 rpred 
 |-  ( ( ph /\ -u X e. RR+ ) -> -u X e. RR )
52 49 51 negrebd 
 |-  ( ( ph /\ -u X e. RR+ ) -> X e. RR )
53 52 stoic1a 
 |-  ( ( ph /\ -. X e. RR ) -> -. -u X e. RR+ )
54 47 48 53 arginv 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( log ` ( 1 / X ) ) ) = -u ( Im ` ( log ` X ) ) )
55 47 48 53 argcj 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( log ` ( * ` X ) ) ) = -u ( Im ` ( log ` X ) ) )
56 54 55 eqtr4d 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( log ` ( 1 / X ) ) ) = ( Im ` ( log ` ( * ` X ) ) ) )
57 56 oveq2d 
 |-  ( ( ph /\ -. X e. RR ) -> ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) = ( _i x. ( Im ` ( log ` ( * ` X ) ) ) ) )
58 57 fveq2d 
 |-  ( ( ph /\ -. X e. RR ) -> ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) = ( exp ` ( _i x. ( Im ` ( log ` ( * ` X ) ) ) ) ) )
59 8 cjcld 
 |-  ( ph -> ( * ` X ) e. CC )
60 8 2 cjne0d 
 |-  ( ph -> ( * ` X ) =/= 0 )
61 59 60 efiargd 
 |-  ( ph -> ( exp ` ( _i x. ( Im ` ( log ` ( * ` X ) ) ) ) ) = ( ( * ` X ) / ( abs ` ( * ` X ) ) ) )
62 61 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( exp ` ( _i x. ( Im ` ( log ` ( * ` X ) ) ) ) ) = ( ( * ` X ) / ( abs ` ( * ` X ) ) ) )
63 58 62 eqtrd 
 |-  ( ( ph /\ -. X e. RR ) -> ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) = ( ( * ` X ) / ( abs ` ( * ` X ) ) ) )
64 1 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> X e. Constr )
65 64 constrcjcl 
 |-  ( ( ph /\ -. X e. RR ) -> ( * ` X ) e. Constr )
66 60 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( * ` X ) =/= 0 )
67 65 66 constrdircl 
 |-  ( ( ph /\ -. X e. RR ) -> ( ( * ` X ) / ( abs ` ( * ` X ) ) ) e. Constr )
68 63 67 eqeltrd 
 |-  ( ( ph /\ -. X e. RR ) -> ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) e. Constr )
69 46 68 constrmulcl 
 |-  ( ( ph /\ -. X e. RR ) -> ( ( 1 / ( abs ` X ) ) x. ( exp ` ( _i x. ( Im ` ( log ` ( 1 / X ) ) ) ) ) ) e. Constr )
70 22 69 eqeltrrd 
 |-  ( ( ph /\ -. X e. RR ) -> ( 1 / X ) e. Constr )
71 6 70 pm2.61dan 
 |-  ( ph -> ( 1 / X ) e. Constr )