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 ( 1 < ( √ ‘ 2 ) ∧ ( √ ‘ 2 ) < 2 )

Proof

Step Hyp Ref Expression
1 sqrt1 ⊢ ( √ ‘ 1 ) = 1
2 1lt2 ⊢ 1 < 2
3 1re ⊢ 1 ∈ ℝ
4 0le1 ⊢ 0 ≤ 1
5 2re ⊢ 2 ∈ ℝ
6 0le2 ⊢ 0 ≤ 2
7 sqrtlt ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ) → ( 1 < 2 ↔ ( √ ‘ 1 ) < ( √ ‘ 2 ) ) )
8 3 4 5 6 7 mp4an ⊢ ( 1 < 2 ↔ ( √ ‘ 1 ) < ( √ ‘ 2 ) )
9 2 8 mpbi ⊢ ( √ ‘ 1 ) < ( √ ‘ 2 )
10 1 9 eqbrtrri ⊢ 1 < ( √ ‘ 2 )
11 2lt4 ⊢ 2 < 4
12 4re ⊢ 4 ∈ ℝ
13 0re ⊢ 0 ∈ ℝ
14 4pos ⊢ 0 < 4
15 13 12 14 ltleii ⊢ 0 ≤ 4
16 sqrtlt ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 4 ∈ ℝ ∧ 0 ≤ 4 ) ) → ( 2 < 4 ↔ ( √ ‘ 2 ) < ( √ ‘ 4 ) ) )
17 5 6 12 15 16 mp4an ⊢ ( 2 < 4 ↔ ( √ ‘ 2 ) < ( √ ‘ 4 ) )
18 11 17 mpbi ⊢ ( √ ‘ 2 ) < ( √ ‘ 4 )
19 sqrt4 ⊢ ( √ ‘ 4 ) = 2
20 18 19 breqtri ⊢ ( √ ‘ 2 ) < 2
21 10 20 pm3.2i ⊢ ( 1 < ( √ ‘ 2 ) ∧ ( √ ‘ 2 ) < 2 )