Metamath Proof Explorer

Theorem zsqrtelqelz

Description: If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion zsqrtelqelz 
|- ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( sqrt ` A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 qdencl 
 |-  ( ( sqrt ` A ) e. QQ -> ( denom ` ( sqrt ` A ) ) e. NN )
2 1 adantl 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( sqrt ` A ) ) e. NN )
3 2 nnred 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( sqrt ` A ) ) e. RR )
4 1red 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> 1 e. RR )
5 2 nnnn0d 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( sqrt ` A ) ) e. NN0 )
6 5 nn0ge0d 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> 0 <_ ( denom ` ( sqrt ` A ) ) )
7 0le1 
 |-  0 <_ 1
8 7 a1i 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> 0 <_ 1 )
9 sq1 
 |-  ( 1 ^ 2 ) = 1
10 9 a1i 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( 1 ^ 2 ) = 1 )
11 zcn 
 |-  ( A e. ZZ -> A e. CC )
12 11 sqsqrtd 
 |-  ( A e. ZZ -> ( ( sqrt ` A ) ^ 2 ) = A )
13 12 adantr 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( ( sqrt ` A ) ^ 2 ) = A )
14 13 fveq2d 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( ( sqrt ` A ) ^ 2 ) ) = ( denom ` A ) )
15 simpl 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> A e. ZZ )
16 zq 
 |-  ( A e. ZZ -> A e. QQ )
17 16 adantr 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> A e. QQ )
18 qden1elz 
 |-  ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )
19 17 18 syl 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )
20 15 19 mpbird 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` A ) = 1 )
21 14 20 eqtrd 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( ( sqrt ` A ) ^ 2 ) ) = 1 )
22 densq 
 |-  ( ( sqrt ` A ) e. QQ -> ( denom ` ( ( sqrt ` A ) ^ 2 ) ) = ( ( denom ` ( sqrt ` A ) ) ^ 2 ) )
23 22 adantl 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( ( sqrt ` A ) ^ 2 ) ) = ( ( denom ` ( sqrt ` A ) ) ^ 2 ) )
24 10 21 23 3eqtr2rd 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( ( denom ` ( sqrt ` A ) ) ^ 2 ) = ( 1 ^ 2 ) )
25 3 4 6 8 24 sq11d 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( denom ` ( sqrt ` A ) ) = 1 )
26 qden1elz 
 |-  ( ( sqrt ` A ) e. QQ -> ( ( denom ` ( sqrt ` A ) ) = 1 <-> ( sqrt ` A ) e. ZZ ) )
27 26 adantl 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( ( denom ` ( sqrt ` A ) ) = 1 <-> ( sqrt ` A ) e. ZZ ) )
28 25 27 mpbid 
 |-  ( ( A e. ZZ /\ ( sqrt ` A ) e. QQ ) -> ( sqrt ` A ) e. ZZ )