Metamath Proof Explorer

Theorem iconstr

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

Ref Expression
Assertion iconstr i ∈ Constr

Proof

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