Metamath Proof Explorer


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 addid2i ( 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 ∈ ℝ