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 
|- ( ph -> X e. Constr )
constrinvcl.2 
|- ( ph -> X =/= 0 )
constrreinvcl.3 
|- ( ph -> X e. RR )
Assertion constrreinvcl 
|- ( ph -> ( 1 / X ) e. Constr )

Proof

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