Metamath Proof Explorer

Theorem numdensq

Description: Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion numdensq 
|- ( A e. QQ -> ( ( numer ` ( A ^ 2 ) ) = ( ( numer ` A ) ^ 2 ) /\ ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 qnumdencoprm 
 |-  ( A e. QQ -> ( ( numer ` A ) gcd ( denom ` A ) ) = 1 )
2 1 oveq1d 
 |-  ( A e. QQ -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ 2 ) = ( 1 ^ 2 ) )
3 qnumcl 
 |-  ( A e. QQ -> ( numer ` A ) e. ZZ )
4 qdencl 
 |-  ( A e. QQ -> ( denom ` A ) e. NN )
5 4 nnzd 
 |-  ( A e. QQ -> ( denom ` A ) e. ZZ )
6 zgcdsq 
 |-  ( ( ( numer ` A ) e. ZZ /\ ( denom ` A ) e. ZZ ) -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) gcd ( ( denom ` A ) ^ 2 ) ) )
7 3 5 6 syl2anc 
 |-  ( A e. QQ -> ( ( ( numer ` A ) gcd ( denom ` A ) ) ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) gcd ( ( denom ` A ) ^ 2 ) ) )
8 sq1 
 |-  ( 1 ^ 2 ) = 1
9 8 a1i 
 |-  ( A e. QQ -> ( 1 ^ 2 ) = 1 )
10 2 7 9 3eqtr3d 
 |-  ( A e. QQ -> ( ( ( numer ` A ) ^ 2 ) gcd ( ( denom ` A ) ^ 2 ) ) = 1 )
11 qeqnumdivden 
 |-  ( A e. QQ -> A = ( ( numer ` A ) / ( denom ` A ) ) )
12 11 oveq1d 
 |-  ( A e. QQ -> ( A ^ 2 ) = ( ( ( numer ` A ) / ( denom ` A ) ) ^ 2 ) )
13 3 zcnd 
 |-  ( A e. QQ -> ( numer ` A ) e. CC )
14 4 nncnd 
 |-  ( A e. QQ -> ( denom ` A ) e. CC )
15 4 nnne0d 
 |-  ( A e. QQ -> ( denom ` A ) =/= 0 )
16 13 14 15 sqdivd 
 |-  ( A e. QQ -> ( ( ( numer ` A ) / ( denom ` A ) ) ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) / ( ( denom ` A ) ^ 2 ) ) )
17 12 16 eqtrd 
 |-  ( A e. QQ -> ( A ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) / ( ( denom ` A ) ^ 2 ) ) )
18 qsqcl 
 |-  ( A e. QQ -> ( A ^ 2 ) e. QQ )
19 zsqcl 
 |-  ( ( numer ` A ) e. ZZ -> ( ( numer ` A ) ^ 2 ) e. ZZ )
20 3 19 syl 
 |-  ( A e. QQ -> ( ( numer ` A ) ^ 2 ) e. ZZ )
21 4 nnsqcld 
 |-  ( A e. QQ -> ( ( denom ` A ) ^ 2 ) e. NN )
22 qnumdenbi 
 |-  ( ( ( A ^ 2 ) e. QQ /\ ( ( numer ` A ) ^ 2 ) e. ZZ /\ ( ( denom ` A ) ^ 2 ) e. NN ) -> ( ( ( ( ( numer ` A ) ^ 2 ) gcd ( ( denom ` A ) ^ 2 ) ) = 1 /\ ( A ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) / ( ( denom ` A ) ^ 2 ) ) ) <-> ( ( numer ` ( A ^ 2 ) ) = ( ( numer ` A ) ^ 2 ) /\ ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) ) ) )
23 18 20 21 22 syl3anc 
 |-  ( A e. QQ -> ( ( ( ( ( numer ` A ) ^ 2 ) gcd ( ( denom ` A ) ^ 2 ) ) = 1 /\ ( A ^ 2 ) = ( ( ( numer ` A ) ^ 2 ) / ( ( denom ` A ) ^ 2 ) ) ) <-> ( ( numer ` ( A ^ 2 ) ) = ( ( numer ` A ) ^ 2 ) /\ ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) ) ) )
24 10 17 23 mpbi2and 
 |-  ( A e. QQ -> ( ( numer ` ( A ^ 2 ) ) = ( ( numer ` A ) ^ 2 ) /\ ( denom ` ( A ^ 2 ) ) = ( ( denom ` A ) ^ 2 ) ) )