Theorem sqrt2gt1lt2

Description: The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005) (Revised by Mario Carneiro, 6-Sep-2013)

	Ref	Expression
Assertion	sqrt2gt1lt2	$$⊢\left(1<\sqrt{2}\wedge \sqrt{2}<2\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrt1	$$⊢\sqrt{1}=1$$
2		1lt2	$$⊢1<2$$
3		1re	$$⊢1\in ℝ$$
4		0le1	$$⊢0\le 1$$
5		2re	$$⊢2\in ℝ$$
6		0le2	$$⊢0\le 2$$
7		sqrtlt	$$⊢\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left(2\in ℝ\wedge 0\le 2\right)\right)\to \left(1<2\leftrightarrow \sqrt{1}<\sqrt{2}\right)$$
8	3 4 5 6 7	mp4an	$$⊢1<2\leftrightarrow \sqrt{1}<\sqrt{2}$$
9	2 8	mpbi	$$⊢\sqrt{1}<\sqrt{2}$$
10	1 9	eqbrtrri	$$⊢1<\sqrt{2}$$
11		2lt4	$$⊢2<4$$
12		4re	$$⊢4\in ℝ$$
13		0re	$$⊢0\in ℝ$$
14		4pos	$$⊢0<4$$
15	13 12 14	ltleii	$$⊢0\le 4$$
16		sqrtlt	$$⊢\left(\left(2\in ℝ\wedge 0\le 2\right)\wedge \left(4\in ℝ\wedge 0\le 4\right)\right)\to \left(2<4\leftrightarrow \sqrt{2}<\sqrt{4}\right)$$
17	5 6 12 15 16	mp4an	$$⊢2<4\leftrightarrow \sqrt{2}<\sqrt{4}$$
18	11 17	mpbi	$$⊢\sqrt{2}<\sqrt{4}$$
19		sqrt4	$$⊢\sqrt{4}=2$$
20	18 19	breqtri	$$⊢\sqrt{2}<2$$
21	10 20	pm3.2i	$$⊢\left(1<\sqrt{2}\wedge \sqrt{2}<2\right)$$