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 ⊢ ⊤ → i ⁢ 3 = i ⁢ 3
10 absi ⊢ 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 → 3 = 3
17 11 15 16 mp2an ⊢ 3 = 3
18 10 17 oveq12i ⊢ i ⁢ 3 = 1 ⁢ 3
19 8 mptru ⊢ 3 ∈ ℂ
20 19 mullidi ⊢ 1 ⁢ 3 = 3
21 18 20 eqtri ⊢ i ⁢ 3 = 3
22 9 21 eqtrdi ⊢ ⊤ → i ⁢ 3 = 3
23 22 oveq2d ⊢ ⊤ → i ⁢ 3 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 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 ⊢ ⊤ → 1 − i ⁢ 3 ∈ ℝ
45 2re ⊢ 2 ∈ ℝ
46 45 a1i ⊢ ⊤ → 2 ∈ ℝ
47 43 absge0d ⊢ ⊤ → 0 ≤ 1 − i ⁢ 3
48 0le2 ⊢ 0 ≤ 2
49 48 a1i ⊢ ⊤ → 0 ≤ 2
50 1red ⊢ ⊤ → 1 ∈ ℝ
51 7 50 pythagreim ⊢ ⊤ → 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 ⊢ ⊤ → 1 − i ⁢ 3 2 = 2 2
61 44 46 47 49 60 sq11d ⊢ ⊤ → 1 − i ⁢ 3 = 2
62 38 42 abssubd ⊢ ⊤ → i ⁢ 3 − 1 = 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 ⊢ ⊤ → 3 − 1 = 3 − 1
67 66 64 eqtrdi ⊢ ⊤ → 3 − 1 = 2
68 61 62 67 3eqtr4d ⊢ ⊤ → i ⁢ 3 − 1 = 3 − 1
69 42 negcld ⊢ ⊤ → − 1 ∈ ℂ
70 69 38 subcld ⊢ ⊤ → - 1 - i ⁢ 3 ∈ ℂ
71 70 abscld ⊢ ⊤ → - 1 - i ⁢ 3 ∈ ℝ
72 70 absge0d ⊢ ⊤ → 0 ≤ - 1 - i ⁢ 3
73 50 renegcld ⊢ ⊤ → − 1 ∈ ℝ
74 7 73 pythagreim ⊢ ⊤ → - 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 ⊢ ⊤ → - 1 - i ⁢ 3 2 = 2 2
80 71 46 72 49 79 sq11d ⊢ ⊤ → - 1 - i ⁢ 3 = 2
81 38 69 abssubd ⊢ ⊤ → i ⁢ 3 − -1 = - 1 - i ⁢ 3
82 80 81 67 3eqtr4d ⊢ ⊤ → i ⁢ 3 − -1 = 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 i ⁢ 3 ∈ Constr
88 32 87 eqeltrrd ⊢ ⊤ → i ∈ Constr
89 88 mptru ⊢ i ∈ Constr