Description: The imaginary part of _i . (Contributed by Scott Fenton, 9-Jun-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | imi | ⊢ ( ℑ ‘ i ) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-icn | ⊢ i ∈ ℂ | |
2 | ax-1cn | ⊢ 1 ∈ ℂ | |
3 | 1 2 | mulcli | ⊢ ( i · 1 ) ∈ ℂ |
4 | 3 | addid2i | ⊢ ( 0 + ( i · 1 ) ) = ( i · 1 ) |
5 | 4 | eqcomi | ⊢ ( i · 1 ) = ( 0 + ( i · 1 ) ) |
6 | 5 | fveq2i | ⊢ ( ℑ ‘ ( i · 1 ) ) = ( ℑ ‘ ( 0 + ( i · 1 ) ) ) |
7 | 1 | mulid1i | ⊢ ( 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 |