Metamath Proof Explorer

Theorem nonsq

Description: Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion nonsq 
|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> -. ( sqrt ` A ) e. QQ )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
2 1 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> B e. ZZ )
3 simprl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( B ^ 2 ) < A )
4 nn0re 
 |-  ( A e. NN0 -> A e. RR )
5 4 ad2antrr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> A e. RR )
6 5 recnd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> A e. CC )
7 6 sqsqrtd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( ( sqrt ` A ) ^ 2 ) = A )
8 3 7 breqtrrd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( B ^ 2 ) < ( ( sqrt ` A ) ^ 2 ) )
9 nn0re 
 |-  ( B e. NN0 -> B e. RR )
10 9 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> B e. RR )
11 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
12 11 ad2antrr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> 0 <_ A )
13 5 12 resqrtcld 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( sqrt ` A ) e. RR )
14 nn0ge0 
 |-  ( B e. NN0 -> 0 <_ B )
15 14 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> 0 <_ B )
16 5 12 sqrtge0d 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> 0 <_ ( sqrt ` A ) )
17 10 13 15 16 lt2sqd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( B < ( sqrt ` A ) <-> ( B ^ 2 ) < ( ( sqrt ` A ) ^ 2 ) ) )
18 8 17 mpbird 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> B < ( sqrt ` A ) )
19 simprr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> A < ( ( B + 1 ) ^ 2 ) )
20 7 19 eqbrtrd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( ( sqrt ` A ) ^ 2 ) < ( ( B + 1 ) ^ 2 ) )
21 peano2re 
 |-  ( B e. RR -> ( B + 1 ) e. RR )
22 10 21 syl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( B + 1 ) e. RR )
23 peano2nn0 
 |-  ( B e. NN0 -> ( B + 1 ) e. NN0 )
24 nn0ge0 
 |-  ( ( B + 1 ) e. NN0 -> 0 <_ ( B + 1 ) )
25 23 24 syl 
 |-  ( B e. NN0 -> 0 <_ ( B + 1 ) )
26 25 ad2antlr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> 0 <_ ( B + 1 ) )
27 13 22 16 26 lt2sqd 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( ( sqrt ` A ) < ( B + 1 ) <-> ( ( sqrt ` A ) ^ 2 ) < ( ( B + 1 ) ^ 2 ) ) )
28 20 27 mpbird 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( sqrt ` A ) < ( B + 1 ) )
29 btwnnz 
 |-  ( ( B e. ZZ /\ B < ( sqrt ` A ) /\ ( sqrt ` A ) < ( B + 1 ) ) -> -. ( sqrt ` A ) e. ZZ )
30 2 18 28 29 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> -. ( sqrt ` A ) e. ZZ )
31 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
32 31 ad2antrr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> A e. ZZ )
33 zsqrtelqelz 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( sqrt ` A ) e. ZZ )
34 33 ex 
 |-  ( A e. ZZ -> ( ( sqrt ` A ) e. QQ -> ( sqrt ` A ) e. ZZ ) )
35 32 34 syl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> ( ( sqrt ` A ) e. QQ -> ( sqrt ` A ) e. ZZ ) )
36 30 35 mtod 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( ( B ^ 2 ) < A /\ A < ( ( B + 1 ) ^ 2 ) ) ) -> -. ( sqrt ` A ) e. QQ )