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

Metamath Proof Explorer

Theorem rei

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

Ref Expression
Assertion rei ⊢ ℜ ⁡ i = 0

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 fveq2i ⊢ ℜ ⁡ 0 + i ⋅ 1 = ℜ ⁡ i ⋅ 1
6 0re ⊢ 0 ∈ ℝ
7 1re ⊢ 1 ∈ ℝ
8 crre ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ → ℜ ⁡ 0 + i ⋅ 1 = 0
9 6 7 8 mp2an ⊢ ℜ ⁡ 0 + i ⋅ 1 = 0
10 1 mulridi ⊢ i ⋅ 1 = i
11 10 fveq2i ⊢ ℜ ⁡ i ⋅ 1 = ℜ ⁡ i
12 5 9 11 3eqtr3ri ⊢ ℜ ⁡ i = 0