# Metamath Proof Explorer

## 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↔\sqrt{1}<\sqrt{2}\right)$
8 3 4 5 6 7 mp4an ${⊢}1<2↔\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↔\sqrt{2}<\sqrt{4}\right)$
17 5 6 12 15 16 mp4an ${⊢}2<4↔\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)$