This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imi

Description: The imaginary part of _i . (Contributed by Scott Fenton, 9-Jun-2006)

Ref Expression
Assertion imi ⊢ ℑ ⁡ i = 1

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 ax-1cn ⊢ 1 ∈ ℂ
3 1 2 mulcli ⊢ i ⋅ 1 ∈ ℂ
4 3 addlidi ⊢ 0 + i ⋅ 1 = i ⋅ 1
5 4 eqcomi ⊢ i ⋅ 1 = 0 + i ⋅ 1
6 5 fveq2i ⊢ ℑ ⁡ i ⋅ 1 = ℑ ⁡ 0 + i ⋅ 1
7 1 mulridi ⊢ i ⋅ 1 = i
8 7 fveq2i ⊢ ℑ ⁡ i ⋅ 1 = ℑ ⁡ i
9 0re ⊢ 0 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 crim ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ → ℑ ⁡ 0 + i ⋅ 1 = 1
12 9 10 11 mp2an ⊢ ℑ ⁡ 0 + i ⋅ 1 = 1
13 6 8 12 3eqtr3i ⊢ ℑ ⁡ i = 1