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		ine0	⊢ i ≠ 0
2	1	neii	⊢ ¬ i = 0
3		0lt1	⊢ 0 < 1
4		0re	⊢ 0 ∈ ℝ
5		1re	⊢ 1 ∈ ℝ
6	4 5	ltnsymi	⊢ ( 0 < 1 → ¬ 1 < 0 )
7	3 6	ax-mp	⊢ ¬ 1 < 0
8		ixi	⊢ ( i · i ) = - 1
9	5	renegcli	⊢ - 1 ∈ ℝ
10	8 9	eqeltri	⊢ ( i · i ) ∈ ℝ
11	4 10 5	ltadd1i	⊢ ( 0 < ( i · i ) ↔ ( 0 + 1 ) < ( ( i · i ) + 1 ) )
12		ax-1cn	⊢ 1 ∈ ℂ
13	12	addlidi	⊢ ( 0 + 1 ) = 1
14		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
15	13 14	breq12i	⊢ ( ( 0 + 1 ) < ( ( i · i ) + 1 ) ↔ 1 < 0 )
16	11 15	bitri	⊢ ( 0 < ( i · i ) ↔ 1 < 0 )
17	7 16	mtbir	⊢ ¬ 0 < ( i · i )
18		msqgt0	⊢ ( ( i ∈ ℝ ∧ i ≠ 0 ) → 0 < ( i · i ) )
19	18	ex	⊢ ( i ∈ ℝ → ( i ≠ 0 → 0 < ( i · i ) ) )
20	19	necon1bd	⊢ ( i ∈ ℝ → ( ¬ 0 < ( i · i ) → i = 0 ) )
21	17 20	mpi	⊢ ( i ∈ ℝ → i = 0 )
22	2 21	mto	⊢ ¬ i ∈ ℝ