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

Metamath Proof Explorer

Theorem rennim

Description: A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013)

Ref Expression
Assertion rennim ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∉ ℝ+ )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4 1 2 3 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
5 rpre ⊢ ( ( i · 𝐴 ) ∈ ℝ+ → ( i · 𝐴 ) ∈ ℝ )
6 rereb ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ( i · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ ( i · 𝐴 ) ) = ( i · 𝐴 ) ) )
7 5 6 imbitrid ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ( i · 𝐴 ) ∈ ℝ+ → ( ℜ ‘ ( i · 𝐴 ) ) = ( i · 𝐴 ) ) )
8 4 7 syl ⊢ ( 𝐴 ∈ ℝ → ( ( i · 𝐴 ) ∈ ℝ+ → ( ℜ ‘ ( i · 𝐴 ) ) = ( i · 𝐴 ) ) )
9 4 addlidd ⊢ ( 𝐴 ∈ ℝ → ( 0 + ( i · 𝐴 ) ) = ( i · 𝐴 ) )
10 9 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( 0 + ( i · 𝐴 ) ) ) = ( ℜ ‘ ( i · 𝐴 ) ) )
11 0re ⊢ 0 ∈ ℝ
12 crre ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ℜ ‘ ( 0 + ( i · 𝐴 ) ) ) = 0 )
13 11 12 mpan ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( 0 + ( i · 𝐴 ) ) ) = 0 )
14 10 13 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( i · 𝐴 ) ) = 0 )
15 14 eqeq1d ⊢ ( 𝐴 ∈ ℝ → ( ( ℜ ‘ ( i · 𝐴 ) ) = ( i · 𝐴 ) ↔ 0 = ( i · 𝐴 ) ) )
16 8 15 sylibd ⊢ ( 𝐴 ∈ ℝ → ( ( i · 𝐴 ) ∈ ℝ+ → 0 = ( i · 𝐴 ) ) )
17 rpne0 ⊢ ( ( i · 𝐴 ) ∈ ℝ+ → ( i · 𝐴 ) ≠ 0 )
18 17 necon2bi ⊢ ( ( i · 𝐴 ) = 0 → ¬ ( i · 𝐴 ) ∈ ℝ+ )
19 18 eqcoms ⊢ ( 0 = ( i · 𝐴 ) → ¬ ( i · 𝐴 ) ∈ ℝ+ )
20 16 19 syl6 ⊢ ( 𝐴 ∈ ℝ → ( ( i · 𝐴 ) ∈ ℝ+ → ¬ ( i · 𝐴 ) ∈ ℝ+ ) )
21 20 pm2.01d ⊢ ( 𝐴 ∈ ℝ → ¬ ( i · 𝐴 ) ∈ ℝ+ )
22 df-nel ⊢ ( ( i · 𝐴 ) ∉ ℝ+ ↔ ¬ ( i · 𝐴 ) ∈ ℝ+ )
23 21 22 sylibr ⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∉ ℝ+ )