Theorem inelr

Description: The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999)

	Ref	Expression
Assertion	inelr	$$⊢\neg \mathrm{i}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		neg1lt0	$$⊢-1<0$$
2		neg1rr	$$⊢-1\in ℝ$$
3		0re	$$⊢0\in ℝ$$
4	2 3	ltnsymi	$$⊢-1<0\to \neg 0<-1$$
5	1 4	ax-mp	$$⊢\neg 0<-1$$
6		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
7	6	breq2i	$$⊢0<\mathrm{i}\mathrm{i}\leftrightarrow 0<-1$$
8	5 7	mtbir	$$⊢\neg 0<\mathrm{i}\mathrm{i}$$
9		ine0	$$⊢\mathrm{i}\ne 0$$
10		msqgt0	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}\ne 0\right)\to 0<\mathrm{i}\mathrm{i}$$
11	9 10	mpan2	$$⊢\mathrm{i}\in ℝ\to 0<\mathrm{i}\mathrm{i}$$
12	8 11	mto	$$⊢\neg \mathrm{i}\in ℝ$$