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		ine0	$$⊢\mathrm{i}\ne 0$$
2	1	neii	$$⊢\neg \mathrm{i}=0$$
3		0lt1	$$⊢0<1$$
4		0re	$$⊢0\in ℝ$$
5		1re	$$⊢1\in ℝ$$
6	4 5	ltnsymi	$$⊢0<1\to \neg 1<0$$
7	3 6	ax-mp	$$⊢\neg 1<0$$
8		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
9	5	renegcli	$$⊢-1\in ℝ$$
10	8 9	eqeltri	$$⊢\mathrm{i}\mathrm{i}\in ℝ$$
11	4 10 5	ltadd1i	$$⊢0<\mathrm{i}\mathrm{i}\leftrightarrow 0+1<\mathrm{i}\mathrm{i}+1$$
12		ax-1cn	$$⊢1\in ℂ$$
13	12	addlidi	$$⊢0+1=1$$
14		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
15	13 14	breq12i	$$⊢0+1<\mathrm{i}\mathrm{i}+1\leftrightarrow 1<0$$
16	11 15	bitri	$$⊢0<\mathrm{i}\mathrm{i}\leftrightarrow 1<0$$
17	7 16	mtbir	$$⊢\neg 0<\mathrm{i}\mathrm{i}$$
18		msqgt0	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}\ne 0\right)\to 0<\mathrm{i}\mathrm{i}$$
19	18	ex	$$⊢\mathrm{i}\in ℝ\to \left(\mathrm{i}\ne 0\to 0<\mathrm{i}\mathrm{i}\right)$$
20	19	necon1bd	$$⊢\mathrm{i}\in ℝ\to \left(\neg 0<\mathrm{i}\mathrm{i}\to \mathrm{i}=0\right)$$
21	17 20	mpi	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}=0$$
22	2 21	mto	$$⊢\neg \mathrm{i}\in ℝ$$