Theorem abs1

Description: The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016)

	Ref	Expression
Assertion	abs1	$$⊢\left|1\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		0le1	$$⊢0\le 1$$
3		absid	$$⊢\left(1\in ℝ\wedge 0\le 1\right)\to \left|1\right|=1$$
4	1 2 3	mp2an	$$⊢\left|1\right|=1$$