Description: The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | inelr | ⊢ ¬ i ∈ ℝ |
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 ∈ ℝ |