This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqrtm1

Description: The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of _i , but the definition of sqrt df-sqrt has already been crafted with _i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 or i2 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Assertion sqrtm1 ⊢ i = − 1

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 0le1 ⊢ 0 ≤ 1
3 sqrtneg ⊢ 1 ∈ ℝ ∧ 0 ≤ 1 → − 1 = i ⁢ 1
4 1 2 3 mp2an ⊢ − 1 = i ⁢ 1
5 sqrt1 ⊢ 1 = 1
6 5 oveq2i ⊢ i ⁢ 1 = i ⋅ 1
7 ax-icn ⊢ i ∈ ℂ
8 7 mulridi ⊢ i ⋅ 1 = i
9 4 6 8 3eqtrri ⊢ i = − 1