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	$$⊢\mathrm{i}=\sqrt{-1}$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		0le1	$$⊢0\le 1$$
3		sqrtneg	$$⊢\left(1\in ℝ\wedge 0\le 1\right)\to \sqrt{-1}=\mathrm{i}\sqrt{1}$$
4	1 2 3	mp2an	$$⊢\sqrt{-1}=\mathrm{i}\sqrt{1}$$
5		sqrt1	$$⊢\sqrt{1}=1$$
6	5	oveq2i	$$⊢\mathrm{i}\sqrt{1}=\mathrm{i}\cdot 1$$
7		ax-icn	$$⊢\mathrm{i}\in ℂ$$
8	7	mulid1i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
9	4 6 8	3eqtrri	$$⊢\mathrm{i}=\sqrt{-1}$$