Theorem inelr

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

	Ref	Expression
Assertion	inelr	|- -. _i e. RR

Proof

Step	Hyp	Ref	Expression
1		ine0	|- _i =/= 0
2	1	neii	|- -. _i = 0
3		0lt1	|- 0 < 1
4		0re	|- 0 e. RR
5		1re	|- 1 e. RR
6	4 5	ltnsymi	|- ( 0 < 1 -> -. 1 < 0 )
7	3 6	ax-mp	|- -. 1 < 0
8		ixi	|- ( _i x. _i ) = -u 1
9	5	renegcli	|- -u 1 e. RR
10	8 9	eqeltri	|- ( _i x. _i ) e. RR
11	4 10 5	ltadd1i	|- ( 0 < ( _i x. _i ) <-> ( 0 + 1 ) < ( ( _i x. _i ) + 1 ) )
12		ax-1cn	|- 1 e. CC
13	12	addlidi	|- ( 0 + 1 ) = 1
14		ax-i2m1	|- ( ( _i x. _i ) + 1 ) = 0
15	13 14	breq12i	|- ( ( 0 + 1 ) < ( ( _i x. _i ) + 1 ) <-> 1 < 0 )
16	11 15	bitri	|- ( 0 < ( _i x. _i ) <-> 1 < 0 )
17	7 16	mtbir	|- -. 0 < ( _i x. _i )
18		msqgt0	|- ( ( _i e. RR /\ _i =/= 0 ) -> 0 < ( _i x. _i ) )
19	18	ex	|- ( _i e. RR -> ( _i =/= 0 -> 0 < ( _i x. _i ) ) )
20	19	necon1bd	|- ( _i e. RR -> ( -. 0 < ( _i x. _i ) -> _i = 0 ) )
21	17 20	mpi	|- ( _i e. RR -> _i = 0 )
22	2 21	mto	|- -. _i e. RR