Theorem absi

Description: The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005)

	Ref	Expression
Assertion	absi	$$⊢\left|\mathrm{i}\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		absval	$$⊢\mathrm{i}\in ℂ\to \left|\mathrm{i}\right|=\sqrt{\mathrm{i}\bar{\mathrm{i}}}$$
3	1 2	ax-mp	$$⊢\left|\mathrm{i}\right|=\sqrt{\mathrm{i}\bar{\mathrm{i}}}$$
4		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
5	4	oveq2i	$$⊢\mathrm{i}\bar{\mathrm{i}}=\mathrm{i}\left(-\mathrm{i}\right)$$
6	1 1	mulneg2i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=-\mathrm{i}\mathrm{i}$$
7		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
8	7	negeqi	$$⊢-\mathrm{i}\mathrm{i}=--1$$
9		negneg1e1	$$⊢--1=1$$
10	8 9	eqtri	$$⊢-\mathrm{i}\mathrm{i}=1$$
11	5 6 10	3eqtri	$$⊢\mathrm{i}\bar{\mathrm{i}}=1$$
12	11	fveq2i	$$⊢\sqrt{\mathrm{i}\bar{\mathrm{i}}}=\sqrt{1}$$
13		sqrt1	$$⊢\sqrt{1}=1$$
14	3 12 13	3eqtri	$$⊢\left|\mathrm{i}\right|=1$$