Metamath Proof Explorer

Theorem constrreinvcl

Description: If a real number X is constructible, then, so is its inverse. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypotheses constrinvcl.1 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
constrinvcl.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
constrreinvcl.3 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion constrreinvcl ( 𝜑 → ( 1 / 𝑋 ) ∈ Constr )

Proof

Step Hyp Ref Expression
1 constrinvcl.1 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
2 constrinvcl.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3 constrreinvcl.3 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4 iconstr ⊢ i ∈ Constr
5 4 a1i ⊢ ( 𝜑 → i ∈ Constr )
6 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
7 5 1 constrmulcl ⊢ ( 𝜑 → ( i · 𝑋 ) ∈ Constr )
8 7 constrcn ⊢ ( 𝜑 → ( i · 𝑋 ) ∈ ℂ )
9 6 8 negsubd ⊢ ( 𝜑 → ( 1 + - ( i · 𝑋 ) ) = ( 1 − ( i · 𝑋 ) ) )
10 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
11 10 zconstr ⊢ ( 𝜑 → 1 ∈ Constr )
12 7 constrnegcl ⊢ ( 𝜑 → - ( i · 𝑋 ) ∈ Constr )
13 11 12 constraddcl ⊢ ( 𝜑 → ( 1 + - ( i · 𝑋 ) ) ∈ Constr )
14 9 13 eqeltrrd ⊢ ( 𝜑 → ( 1 − ( i · 𝑋 ) ) ∈ Constr )
15 5 14 constraddcl ⊢ ( 𝜑 → ( i + ( 1 − ( i · 𝑋 ) ) ) ∈ Constr )
16 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
17 16 zconstr ⊢ ( 𝜑 → 0 ∈ Constr )
18 3 2 rereccld ⊢ ( 𝜑 → ( 1 / 𝑋 ) ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → ( 1 / 𝑋 ) ∈ ℂ )
20 5 constrcn ⊢ ( 𝜑 → i ∈ ℂ )
21 6 8 subcld ⊢ ( 𝜑 → ( 1 − ( i · 𝑋 ) ) ∈ ℂ )
22 20 21 pncan2d ⊢ ( 𝜑 → ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) = ( 1 − ( i · 𝑋 ) ) )
23 22 oveq2d ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) = ( ( 1 / 𝑋 ) · ( 1 − ( i · 𝑋 ) ) ) )
24 23 oveq2d ⊢ ( 𝜑 → ( i + ( ( 1 / 𝑋 ) · ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) ) = ( i + ( ( 1 / 𝑋 ) · ( 1 − ( i · 𝑋 ) ) ) ) )
25 19 6 8 subdid ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( 1 − ( i · 𝑋 ) ) ) = ( ( ( 1 / 𝑋 ) · 1 ) − ( ( 1 / 𝑋 ) · ( i · 𝑋 ) ) ) )
26 19 mulridd ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · 1 ) = ( 1 / 𝑋 ) )
27 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
28 6 27 8 2 div32d ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( i · 𝑋 ) ) = ( 1 · ( ( i · 𝑋 ) / 𝑋 ) ) )
29 8 27 2 divcld ⊢ ( 𝜑 → ( ( i · 𝑋 ) / 𝑋 ) ∈ ℂ )
30 29 mullidd ⊢ ( 𝜑 → ( 1 · ( ( i · 𝑋 ) / 𝑋 ) ) = ( ( i · 𝑋 ) / 𝑋 ) )
31 20 27 2 divcan4d ⊢ ( 𝜑 → ( ( i · 𝑋 ) / 𝑋 ) = i )
32 28 30 31 3eqtrd ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( i · 𝑋 ) ) = i )
33 26 32 oveq12d ⊢ ( 𝜑 → ( ( ( 1 / 𝑋 ) · 1 ) − ( ( 1 / 𝑋 ) · ( i · 𝑋 ) ) ) = ( ( 1 / 𝑋 ) − i ) )
34 25 33 eqtrd ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( 1 − ( i · 𝑋 ) ) ) = ( ( 1 / 𝑋 ) − i ) )
35 34 oveq2d ⊢ ( 𝜑 → ( i + ( ( 1 / 𝑋 ) · ( 1 − ( i · 𝑋 ) ) ) ) = ( i + ( ( 1 / 𝑋 ) − i ) ) )
36 20 19 pncan3d ⊢ ( 𝜑 → ( i + ( ( 1 / 𝑋 ) − i ) ) = ( 1 / 𝑋 ) )
37 24 35 36 3eqtrrd ⊢ ( 𝜑 → ( 1 / 𝑋 ) = ( i + ( ( 1 / 𝑋 ) · ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) ) )
38 6 subid1d ⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
39 38 6 eqeltrd ⊢ ( 𝜑 → ( 1 − 0 ) ∈ ℂ )
40 19 39 mulcld ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( 1 − 0 ) ) ∈ ℂ )
41 40 addlidd ⊢ ( 𝜑 → ( 0 + ( ( 1 / 𝑋 ) · ( 1 − 0 ) ) ) = ( ( 1 / 𝑋 ) · ( 1 − 0 ) ) )
42 38 oveq2d ⊢ ( 𝜑 → ( ( 1 / 𝑋 ) · ( 1 − 0 ) ) = ( ( 1 / 𝑋 ) · 1 ) )
43 41 42 26 3eqtrrd ⊢ ( 𝜑 → ( 1 / 𝑋 ) = ( 0 + ( ( 1 / 𝑋 ) · ( 1 − 0 ) ) ) )
44 38 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · ( 1 − 0 ) ) = ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · 1 ) )
45 15 constrcn ⊢ ( 𝜑 → ( i + ( 1 − ( i · 𝑋 ) ) ) ∈ ℂ )
46 45 20 subcld ⊢ ( 𝜑 → ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ∈ ℂ )
47 46 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) ∈ ℂ )
48 47 mulridd ⊢ ( 𝜑 → ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · 1 ) = ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) )
49 22 fveq2d ⊢ ( 𝜑 → ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) = ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) )
50 44 48 49 3eqtrd ⊢ ( 𝜑 → ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · ( 1 − 0 ) ) = ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) )
51 50 fveq2d ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · ( 1 − 0 ) ) ) = ( ℑ ‘ ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) ) )
52 6 8 cjsubd ⊢ ( 𝜑 → ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝑋 ) ) ) )
53 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
54 53 cjred ⊢ ( 𝜑 → ( ∗ ‘ 1 ) = 1 )
55 20 27 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( i · 𝑋 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝑋 ) ) )
56 cji ⊢ ( ∗ ‘ i ) = - i
57 56 a1i ⊢ ( 𝜑 → ( ∗ ‘ i ) = - i )
58 3 cjred ⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) = 𝑋 )
59 57 58 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ i ) · ( ∗ ‘ 𝑋 ) ) = ( - i · 𝑋 ) )
60 20 27 mulneg1d ⊢ ( 𝜑 → ( - i · 𝑋 ) = - ( i · 𝑋 ) )
61 55 59 60 3eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( i · 𝑋 ) ) = - ( i · 𝑋 ) )
62 54 61 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝑋 ) ) ) = ( 1 − - ( i · 𝑋 ) ) )
63 6 8 subnegd ⊢ ( 𝜑 → ( 1 − - ( i · 𝑋 ) ) = ( 1 + ( i · 𝑋 ) ) )
64 52 62 63 3eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) = ( 1 + ( i · 𝑋 ) ) )
65 64 fveq2d ⊢ ( 𝜑 → ( ℑ ‘ ( ∗ ‘ ( 1 − ( i · 𝑋 ) ) ) ) = ( ℑ ‘ ( 1 + ( i · 𝑋 ) ) ) )
66 53 3 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 1 + ( i · 𝑋 ) ) ) = 𝑋 )
67 51 65 66 3eqtrd ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · ( 1 − 0 ) ) ) = 𝑋 )
68 67 2 eqnetrd ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( ( i + ( 1 − ( i · 𝑋 ) ) ) − i ) ) · ( 1 − 0 ) ) ) ≠ 0 )
69 5 15 17 11 18 18 19 37 43 68 constrllcl ⊢ ( 𝜑 → ( 1 / 𝑋 ) ∈ Constr )