Metamath Proof Explorer

Theorem iconstr

Description: The imaginary unit _i is constructible. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Assertion iconstr 
|- _i e. Constr

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 1 a1i 
 |-  ( T. -> _i e. CC )
3 3nn0 
 |-  3 e. NN0
4 3 a1i 
 |-  ( T. -> 3 e. NN0 )
5 4 nn0red 
 |-  ( T. -> 3 e. RR )
6 4 nn0ge0d 
 |-  ( T. -> 0 <_ 3 )
7 5 6 resqrtcld 
 |-  ( T. -> ( sqrt ` 3 ) e. RR )
8 7 recnd 
 |-  ( T. -> ( sqrt ` 3 ) e. CC )
9 2 8 absmuld 
 |-  ( T. -> ( abs ` ( _i x. ( sqrt ` 3 ) ) ) = ( ( abs ` _i ) x. ( abs ` ( sqrt ` 3 ) ) ) )
10 absi 
 |-  ( abs ` _i ) = 1
11 7 mptru 
 |-  ( sqrt ` 3 ) e. RR
12 3re 
 |-  3 e. RR
13 6 mptru 
 |-  0 <_ 3
14 sqrtge0 
 |-  ( ( 3 e. RR /\ 0 <_ 3 ) -> 0 <_ ( sqrt ` 3 ) )
15 12 13 14 mp2an 
 |-  0 <_ ( sqrt ` 3 )
16 absid 
 |-  ( ( ( sqrt ` 3 ) e. RR /\ 0 <_ ( sqrt ` 3 ) ) -> ( abs ` ( sqrt ` 3 ) ) = ( sqrt ` 3 ) )
17 11 15 16 mp2an 
 |-  ( abs ` ( sqrt ` 3 ) ) = ( sqrt ` 3 )
18 10 17 oveq12i 
 |-  ( ( abs ` _i ) x. ( abs ` ( sqrt ` 3 ) ) ) = ( 1 x. ( sqrt ` 3 ) )
19 8 mptru 
 |-  ( sqrt ` 3 ) e. CC
20 19 mullidi 
 |-  ( 1 x. ( sqrt ` 3 ) ) = ( sqrt ` 3 )
21 18 20 eqtri 
 |-  ( ( abs ` _i ) x. ( abs ` ( sqrt ` 3 ) ) ) = ( sqrt ` 3 )
22 9 21 eqtrdi 
 |-  ( T. -> ( abs ` ( _i x. ( sqrt ` 3 ) ) ) = ( sqrt ` 3 ) )
23 22 oveq2d 
 |-  ( T. -> ( ( _i x. ( sqrt ` 3 ) ) / ( abs ` ( _i x. ( sqrt ` 3 ) ) ) ) = ( ( _i x. ( sqrt ` 3 ) ) / ( sqrt ` 3 ) ) )
24 4 nn0cnd 
 |-  ( T. -> 3 e. CC )
25 3ne0 
 |-  3 =/= 0
26 cnsqrt00 
 |-  ( 3 e. CC -> ( ( sqrt ` 3 ) = 0 <-> 3 = 0 ) )
27 26 necon3bid 
 |-  ( 3 e. CC -> ( ( sqrt ` 3 ) =/= 0 <-> 3 =/= 0 ) )
28 27 biimpar 
 |-  ( ( 3 e. CC /\ 3 =/= 0 ) -> ( sqrt ` 3 ) =/= 0 )
29 24 25 28 sylancl 
 |-  ( T. -> ( sqrt ` 3 ) =/= 0 )
30 29 mptru 
 |-  ( sqrt ` 3 ) =/= 0
31 1 19 30 divcan4i 
 |-  ( ( _i x. ( sqrt ` 3 ) ) / ( sqrt ` 3 ) ) = _i
32 23 31 eqtrdi 
 |-  ( T. -> ( ( _i x. ( sqrt ` 3 ) ) / ( abs ` ( _i x. ( sqrt ` 3 ) ) ) ) = _i )
33 1nn0 
 |-  1 e. NN0
34 33 a1i 
 |-  ( T. -> 1 e. NN0 )
35 34 nn0constr 
 |-  ( T. -> 1 e. Constr )
36 4 nn0constr 
 |-  ( T. -> 3 e. Constr )
37 35 constrnegcl 
 |-  ( T. -> -u 1 e. Constr )
38 2 8 mulcld 
 |-  ( T. -> ( _i x. ( sqrt ` 3 ) ) e. CC )
39 1nn 
 |-  1 e. NN
40 nnneneg 
 |-  ( 1 e. NN -> 1 =/= -u 1 )
41 39 40 mp1i 
 |-  ( T. -> 1 =/= -u 1 )
42 1cnd 
 |-  ( T. -> 1 e. CC )
43 42 38 subcld 
 |-  ( T. -> ( 1 - ( _i x. ( sqrt ` 3 ) ) ) e. CC )
44 43 abscld 
 |-  ( T. -> ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) e. RR )
45 2re 
 |-  2 e. RR
46 45 a1i 
 |-  ( T. -> 2 e. RR )
47 43 absge0d 
 |-  ( T. -> 0 <_ ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) )
48 0le2 
 |-  0 <_ 2
49 48 a1i 
 |-  ( T. -> 0 <_ 2 )
50 1red 
 |-  ( T. -> 1 e. RR )
51 7 50 pythagreim 
 |-  ( T. -> ( ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) ^ 2 ) = ( ( ( sqrt ` 3 ) ^ 2 ) + ( 1 ^ 2 ) ) )
52 24 sqsqrtd 
 |-  ( T. -> ( ( sqrt ` 3 ) ^ 2 ) = 3 )
53 sq1 
 |-  ( 1 ^ 2 ) = 1
54 53 a1i 
 |-  ( T. -> ( 1 ^ 2 ) = 1 )
55 52 54 oveq12d 
 |-  ( T. -> ( ( ( sqrt ` 3 ) ^ 2 ) + ( 1 ^ 2 ) ) = ( 3 + 1 ) )
56 3p1e4 
 |-  ( 3 + 1 ) = 4
57 sq2 
 |-  ( 2 ^ 2 ) = 4
58 56 57 eqtr4i 
 |-  ( 3 + 1 ) = ( 2 ^ 2 )
59 55 58 eqtrdi 
 |-  ( T. -> ( ( ( sqrt ` 3 ) ^ 2 ) + ( 1 ^ 2 ) ) = ( 2 ^ 2 ) )
60 51 59 eqtrd 
 |-  ( T. -> ( ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) ^ 2 ) = ( 2 ^ 2 ) )
61 44 46 47 49 60 sq11d 
 |-  ( T. -> ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) = 2 )
62 38 42 abssubd 
 |-  ( T. -> ( abs ` ( ( _i x. ( sqrt ` 3 ) ) - 1 ) ) = ( abs ` ( 1 - ( _i x. ( sqrt ` 3 ) ) ) ) )
63 5 50 resubcld 
 |-  ( T. -> ( 3 - 1 ) e. RR )
64 3m1e2 
 |-  ( 3 - 1 ) = 2
65 49 64 breqtrrdi 
 |-  ( T. -> 0 <_ ( 3 - 1 ) )
66 63 65 absidd 
 |-  ( T. -> ( abs ` ( 3 - 1 ) ) = ( 3 - 1 ) )
67 66 64 eqtrdi 
 |-  ( T. -> ( abs ` ( 3 - 1 ) ) = 2 )
68 61 62 67 3eqtr4d 
 |-  ( T. -> ( abs ` ( ( _i x. ( sqrt ` 3 ) ) - 1 ) ) = ( abs ` ( 3 - 1 ) ) )
69 42 negcld 
 |-  ( T. -> -u 1 e. CC )
70 69 38 subcld 
 |-  ( T. -> ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) e. CC )
71 70 abscld 
 |-  ( T. -> ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) e. RR )
72 70 absge0d 
 |-  ( T. -> 0 <_ ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) )
73 50 renegcld 
 |-  ( T. -> -u 1 e. RR )
74 7 73 pythagreim 
 |-  ( T. -> ( ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) ^ 2 ) = ( ( ( sqrt ` 3 ) ^ 2 ) + ( -u 1 ^ 2 ) ) )
75 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
76 75 a1i 
 |-  ( T. -> ( -u 1 ^ 2 ) = 1 )
77 52 76 oveq12d 
 |-  ( T. -> ( ( ( sqrt ` 3 ) ^ 2 ) + ( -u 1 ^ 2 ) ) = ( 3 + 1 ) )
78 77 58 eqtrdi 
 |-  ( T. -> ( ( ( sqrt ` 3 ) ^ 2 ) + ( -u 1 ^ 2 ) ) = ( 2 ^ 2 ) )
79 74 78 eqtrd 
 |-  ( T. -> ( ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) ^ 2 ) = ( 2 ^ 2 ) )
80 71 46 72 49 79 sq11d 
 |-  ( T. -> ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) = 2 )
81 38 69 abssubd 
 |-  ( T. -> ( abs ` ( ( _i x. ( sqrt ` 3 ) ) - -u 1 ) ) = ( abs ` ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) ) )
82 80 81 67 3eqtr4d 
 |-  ( T. -> ( abs ` ( ( _i x. ( sqrt ` 3 ) ) - -u 1 ) ) = ( abs ` ( 3 - 1 ) ) )
83 35 36 35 37 36 35 38 41 68 82 constrcccl 
 |-  ( T. -> ( _i x. ( sqrt ` 3 ) ) e. Constr )
84 ine0 
 |-  _i =/= 0
85 84 a1i 
 |-  ( T. -> _i =/= 0 )
86 2 8 85 29 mulne0d 
 |-  ( T. -> ( _i x. ( sqrt ` 3 ) ) =/= 0 )
87 83 86 constrdircl 
 |-  ( T. -> ( ( _i x. ( sqrt ` 3 ) ) / ( abs ` ( _i x. ( sqrt ` 3 ) ) ) ) e. Constr )
88 32 87 eqeltrrd 
 |-  ( T. -> _i e. Constr )
89 88 mptru 
 |-  _i e. Constr