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 ( 𝐴 ∈ ℚ → ( ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) ∧ ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 qnumdencoprm ⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 )
2 1 oveq1d ⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
3 qnumcl ⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℤ )
4 qdencl ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )
5 4 nnzd ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℤ )
6 zgcdsq ⊢ ( ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℤ ) → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) gcd ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )
7 3 5 6 syl2anc ⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) gcd ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )
8 sq1 ⊢ ( 1 ↑ 2 ) = 1
9 8 a1i ⊢ ( 𝐴 ∈ ℚ → ( 1 ↑ 2 ) = 1 )
10 2 7 9 3eqtr3d ⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) ↑ 2 ) gcd ( ( denom ‘ 𝐴 ) ↑ 2 ) ) = 1 )
11 qeqnumdivden ⊢ ( 𝐴 ∈ ℚ → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )
12 11 oveq1d ⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ↑ 2 ) )
13 3 zcnd ⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℂ )
14 4 nncnd ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℂ )
15 4 nnne0d ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ≠ 0 )
16 13 14 15 sqdivd ⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) / ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )
17 12 16 eqtrd ⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) / ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )
18 qsqcl ⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ↑ 2 ) ∈ ℚ )
19 zsqcl ⊢ ( ( numer ‘ 𝐴 ) ∈ ℤ → ( ( numer ‘ 𝐴 ) ↑ 2 ) ∈ ℤ )
20 3 19 syl ⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ↑ 2 ) ∈ ℤ )
21 4 nnsqcld ⊢ ( 𝐴 ∈ ℚ → ( ( denom ‘ 𝐴 ) ↑ 2 ) ∈ ℕ )
22 qnumdenbi ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℚ ∧ ( ( numer ‘ 𝐴 ) ↑ 2 ) ∈ ℤ ∧ ( ( denom ‘ 𝐴 ) ↑ 2 ) ∈ ℕ ) → ( ( ( ( ( numer ‘ 𝐴 ) ↑ 2 ) gcd ( ( denom ‘ 𝐴 ) ↑ 2 ) ) = 1 ∧ ( 𝐴 ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) / ( ( denom ‘ 𝐴 ) ↑ 2 ) ) ) ↔ ( ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) ∧ ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) ) ) )
23 18 20 21 22 syl3anc ⊢ ( 𝐴 ∈ ℚ → ( ( ( ( ( numer ‘ 𝐴 ) ↑ 2 ) gcd ( ( denom ‘ 𝐴 ) ↑ 2 ) ) = 1 ∧ ( 𝐴 ↑ 2 ) = ( ( ( numer ‘ 𝐴 ) ↑ 2 ) / ( ( denom ‘ 𝐴 ) ↑ 2 ) ) ) ↔ ( ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) ∧ ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) ) ) )
24 10 17 23 mpbi2and ⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ ( 𝐴 ↑ 2 ) ) = ( ( numer ‘ 𝐴 ) ↑ 2 ) ∧ ( denom ‘ ( 𝐴 ↑ 2 ) ) = ( ( denom ‘ 𝐴 ) ↑ 2 ) ) )