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 < ( sqrt ` 2 ) /\ ( sqrt ` 2 ) < 2 )

Proof

Step Hyp Ref Expression
1 sqrt1 
 |-  ( sqrt ` 1 ) = 1
2 1lt2 
 |-  1 < 2
3 1re 
 |-  1 e. RR
4 0le1 
 |-  0 <_ 1
5 2re 
 |-  2 e. RR
6 0le2 
 |-  0 <_ 2
7 sqrtlt 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( 2 e. RR /\ 0 <_ 2 ) ) -> ( 1 < 2 <-> ( sqrt ` 1 ) < ( sqrt ` 2 ) ) )
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 e. RR
13 0re 
 |-  0 e. RR
14 4pos 
 |-  0 < 4
15 13 12 14 ltleii 
 |-  0 <_ 4
16 sqrtlt 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( 4 e. RR /\ 0 <_ 4 ) ) -> ( 2 < 4 <-> ( sqrt ` 2 ) < ( sqrt ` 4 ) ) )
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 
 |-  ( 1 < ( sqrt ` 2 ) /\ ( sqrt ` 2 ) < 2 )