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 · 𝐴 ) ∉ ℝ+ )