Theorem inelr

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

	Ref	Expression
Assertion	inelr	⊢ ¬ i ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		neg1lt0	⊢ - 1 < 0
2		neg1rr	⊢ - 1 ∈ ℝ
3		0re	⊢ 0 ∈ ℝ
4	2 3	ltnsymi	⊢ ( - 1 < 0 → ¬ 0 < - 1 )
5	1 4	ax-mp	⊢ ¬ 0 < - 1
6		ixi	⊢ ( i · i ) = - 1
7	6	breq2i	⊢ ( 0 < ( i · i ) ↔ 0 < - 1 )
8	5 7	mtbir	⊢ ¬ 0 < ( i · i )
9		ine0	⊢ i ≠ 0
10		msqgt0	⊢ ( ( i ∈ ℝ ∧ i ≠ 0 ) → 0 < ( i · i ) )
11	9 10	mpan2	⊢ ( i ∈ ℝ → 0 < ( i · i ) )
12	8 11	mto	⊢ ¬ i ∈ ℝ