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	$$⊢A\in ℝ\to \mathrm{i}A\notin {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		recn	$$⊢A\in ℝ\to A\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
4	1 2 3	sylancr	$$⊢A\in ℝ\to \mathrm{i}A\in ℂ$$
5		rpre	$$⊢\mathrm{i}A\in {ℝ}^{+}\to \mathrm{i}A\in ℝ$$
6		rereb	$$⊢\mathrm{i}A\in ℂ\to \left(\mathrm{i}A\in ℝ\leftrightarrow \Re \left(\mathrm{i}A\right)=\mathrm{i}A\right)$$
7	5 6	imbitrid	$$⊢\mathrm{i}A\in ℂ\to \left(\mathrm{i}A\in {ℝ}^{+}\to \Re \left(\mathrm{i}A\right)=\mathrm{i}A\right)$$
8	4 7	syl	$$⊢A\in ℝ\to \left(\mathrm{i}A\in {ℝ}^{+}\to \Re \left(\mathrm{i}A\right)=\mathrm{i}A\right)$$
9	4	addlidd	$$⊢A\in ℝ\to 0+\mathrm{i}A=\mathrm{i}A$$
10	9	fveq2d	$$⊢A\in ℝ\to \Re \left(0+\mathrm{i}A\right)=\Re \left(\mathrm{i}A\right)$$
11		0re	$$⊢0\in ℝ$$
12		crre	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \Re \left(0+\mathrm{i}A\right)=0$$
13	11 12	mpan	$$⊢A\in ℝ\to \Re \left(0+\mathrm{i}A\right)=0$$
14	10 13	eqtr3d	$$⊢A\in ℝ\to \Re \left(\mathrm{i}A\right)=0$$
15	14	eqeq1d	$$⊢A\in ℝ\to \left(\Re \left(\mathrm{i}A\right)=\mathrm{i}A\leftrightarrow 0=\mathrm{i}A\right)$$
16	8 15	sylibd	$$⊢A\in ℝ\to \left(\mathrm{i}A\in {ℝ}^{+}\to 0=\mathrm{i}A\right)$$
17		rpne0	$$⊢\mathrm{i}A\in {ℝ}^{+}\to \mathrm{i}A\ne 0$$
18	17	necon2bi	$$⊢\mathrm{i}A=0\to \neg \mathrm{i}A\in {ℝ}^{+}$$
19	18	eqcoms	$$⊢0=\mathrm{i}A\to \neg \mathrm{i}A\in {ℝ}^{+}$$
20	16 19	syl6	$$⊢A\in ℝ\to \left(\mathrm{i}A\in {ℝ}^{+}\to \neg \mathrm{i}A\in {ℝ}^{+}\right)$$
21	20	pm2.01d	$$⊢A\in ℝ\to \neg \mathrm{i}A\in {ℝ}^{+}$$
22		df-nel	$$⊢\mathrm{i}A\notin {ℝ}^{+}\leftrightarrow \neg \mathrm{i}A\in {ℝ}^{+}$$
23	21 22	sylibr	$$⊢A\in ℝ\to \mathrm{i}A\notin {ℝ}^{+}$$