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 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
constrinvcl.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion constrinvcl ( 𝜑 → ( 1 / 𝑋 ) ∈ Constr )

Proof

Step Hyp Ref Expression
1 constrinvcl.1 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
2 constrinvcl.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ ) → 𝑋 ∈ Constr )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ ) → 𝑋 ≠ 0 )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ ) → 𝑋 ∈ ℝ )
6 3 4 5 constrreinvcl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ ) → ( 1 / 𝑋 ) ∈ Constr )
7 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
8 1 constrcn ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
9 7 8 2 absdivd ⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝑋 ) ) = ( ( abs ‘ 1 ) / ( abs ‘ 𝑋 ) ) )
10 abs1 ⊢ ( abs ‘ 1 ) = 1
11 10 oveq1i ⊢ ( ( abs ‘ 1 ) / ( abs ‘ 𝑋 ) ) = ( 1 / ( abs ‘ 𝑋 ) )
12 9 11 eqtr2di ⊢ ( 𝜑 → ( 1 / ( abs ‘ 𝑋 ) ) = ( abs ‘ ( 1 / 𝑋 ) ) )
13 8 2 reccld ⊢ ( 𝜑 → ( 1 / 𝑋 ) ∈ ℂ )
14 8 2 recne0d ⊢ ( 𝜑 → ( 1 / 𝑋 ) ≠ 0 )
15 13 14 efiargd ⊢ ( 𝜑 → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) = ( ( 1 / 𝑋 ) / ( abs ‘ ( 1 / 𝑋 ) ) ) )
16 12 15 oveq12d ⊢ ( 𝜑 → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) ) = ( ( abs ‘ ( 1 / 𝑋 ) ) · ( ( 1 / 𝑋 ) / ( abs ‘ ( 1 / 𝑋 ) ) ) ) )
17 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝑋 ) ) ∈ ℝ )
18 17 recnd ⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝑋 ) ) ∈ ℂ )
19 13 14 absne0d ⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝑋 ) ) ≠ 0 )
20 13 18 19 divcan2d ⊢ ( 𝜑 → ( ( abs ‘ ( 1 / 𝑋 ) ) · ( ( 1 / 𝑋 ) / ( abs ‘ ( 1 / 𝑋 ) ) ) ) = ( 1 / 𝑋 ) )
21 16 20 eqtrd ⊢ ( 𝜑 → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) ) = ( 1 / 𝑋 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) ) = ( 1 / 𝑋 ) )
23 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
24 23 zconstr ⊢ ( 𝜑 → 0 ∈ Constr )
25 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
26 25 zconstr ⊢ ( 𝜑 → 1 ∈ Constr )
27 8 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
28 27 recnd ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
29 7 subid1d ⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
30 29 7 eqeltrd ⊢ ( 𝜑 → ( 1 − 0 ) ∈ ℂ )
31 28 30 mulcld ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ∈ ℂ )
32 31 addlidd ⊢ ( 𝜑 → ( 0 + ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ) = ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) )
33 29 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) = ( ( abs ‘ 𝑋 ) · 1 ) )
34 28 mulridd ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · 1 ) = ( abs ‘ 𝑋 ) )
35 32 33 34 3eqtrrd ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) = ( 0 + ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ) )
36 8 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑋 ) )
37 27 36 absidd ⊢ ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
38 28 subid1d ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) − 0 ) = ( abs ‘ 𝑋 ) )
39 38 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( abs ‘ 𝑋 ) ) )
40 8 subid1d ⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
41 40 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) )
42 37 39 41 3eqtr4d ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( 𝑋 − 0 ) ) )
43 24 26 24 1 24 27 28 35 42 constrlccl ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ Constr )
44 8 2 absne0d ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≠ 0 )
45 43 44 27 constrreinvcl ⊢ ( 𝜑 → ( 1 / ( abs ‘ 𝑋 ) ) ∈ Constr )
46 45 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ Constr )
47 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → 𝑋 ∈ ℂ )
48 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → 𝑋 ≠ 0 )
49 8 adantr ⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℂ )
50 simpr ⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℝ+ ) → - 𝑋 ∈ ℝ+ )
51 50 rpred ⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℝ+ ) → - 𝑋 ∈ ℝ )
52 49 51 negrebd ⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℝ )
53 52 stoic1a ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ¬ - 𝑋 ∈ ℝ+ )
54 47 48 53 arginv ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) = - ( ℑ ‘ ( log ‘ 𝑋 ) ) )
55 47 48 53 argcj ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) = - ( ℑ ‘ ( log ‘ 𝑋 ) ) )
56 54 55 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) = ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) )
57 56 oveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) = ( i · ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) ) )
58 57 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) = ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) ) ) )
59 8 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ∈ ℂ )
60 8 2 cjne0d ⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ≠ 0 )
61 59 60 efiargd ⊢ ( 𝜑 → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( abs ‘ ( ∗ ‘ 𝑋 ) ) ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝑋 ) ) ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( abs ‘ ( ∗ ‘ 𝑋 ) ) ) )
63 58 62 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( abs ‘ ( ∗ ‘ 𝑋 ) ) ) )
64 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → 𝑋 ∈ Constr )
65 64 constrcjcl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ∗ ‘ 𝑋 ) ∈ Constr )
66 60 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ∗ ‘ 𝑋 ) ≠ 0 )
67 65 66 constrdircl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ( ∗ ‘ 𝑋 ) / ( abs ‘ ( ∗ ‘ 𝑋 ) ) ) ∈ Constr )
68 63 67 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) ∈ Constr )
69 46 68 constrmulcl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( 1 / 𝑋 ) ) ) ) ) ) ∈ Constr )
70 22 69 eqeltrrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ℝ ) → ( 1 / 𝑋 ) ∈ Constr )
71 6 70 pm2.61dan ⊢ ( 𝜑 → ( 1 / 𝑋 ) ∈ Constr )