Metamath Proof Explorer


Theorem coprimeprodsq

Description: If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion coprimeprodsq ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 nn0z ( 𝐴 ∈ ℕ0𝐴 ∈ ℤ )
2 nn0z ( 𝐶 ∈ ℕ0𝐶 ∈ ℤ )
3 gcdcl ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 gcd 𝐶 ) ∈ ℕ0 )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℕ0𝐶 ∈ ℕ0 ) → ( 𝐴 gcd 𝐶 ) ∈ ℕ0 )
5 4 3adant2 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 gcd 𝐶 ) ∈ ℕ0 )
6 5 3ad2ant1 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 gcd 𝐶 ) ∈ ℕ0 )
7 6 nn0cnd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 gcd 𝐶 ) ∈ ℂ )
8 7 sqvald ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) = ( ( 𝐴 gcd 𝐶 ) · ( 𝐴 gcd 𝐶 ) ) )
9 simp13 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐶 ∈ ℕ0 )
10 9 nn0cnd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐶 ∈ ℂ )
11 nn0cn ( 𝐴 ∈ ℕ0𝐴 ∈ ℂ )
12 11 3ad2ant1 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
13 12 3ad2ant1 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℂ )
14 10 13 mulcomd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐶 · 𝐴 ) = ( 𝐴 · 𝐶 ) )
15 simpl3 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → 𝐶 ∈ ℕ0 )
16 15 nn0cnd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → 𝐶 ∈ ℂ )
17 16 sqvald ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( 𝐶 ↑ 2 ) = ( 𝐶 · 𝐶 ) )
18 17 eqeq1d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ↔ ( 𝐶 · 𝐶 ) = ( 𝐴 · 𝐵 ) ) )
19 18 biimp3a ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐶 · 𝐶 ) = ( 𝐴 · 𝐵 ) )
20 14 19 oveq12d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) gcd ( 𝐴 · 𝐵 ) ) )
21 simp11 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℕ0 )
22 21 nn0zd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℤ )
23 9 nn0zd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐶 ∈ ℤ )
24 mulgcd ( ( 𝐶 ∈ ℕ0𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐶 ) ) = ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) )
25 9 22 23 24 syl3anc ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐶 ) ) = ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) )
26 simp12 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐵 ∈ ℤ )
27 mulgcd ( ( 𝐴 ∈ ℕ0𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 · 𝐶 ) gcd ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) )
28 21 23 26 27 syl3anc ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · 𝐶 ) gcd ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) )
29 20 25 28 3eqtr3d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) = ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) )
30 29 oveq2d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) ) = ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) ) )
31 mulgcdr ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ ( 𝐴 gcd 𝐶 ) ∈ ℕ0 ) → ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) ) = ( ( 𝐴 gcd 𝐶 ) · ( 𝐴 gcd 𝐶 ) ) )
32 22 23 6 31 syl3anc ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐶 · ( 𝐴 gcd 𝐶 ) ) ) = ( ( 𝐴 gcd 𝐶 ) · ( 𝐴 gcd 𝐶 ) ) )
33 6 nn0zd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 gcd 𝐶 ) ∈ ℤ )
34 gcdcl ( ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐶 gcd 𝐵 ) ∈ ℕ0 )
35 2 34 sylan ( ( 𝐶 ∈ ℕ0𝐵 ∈ ℤ ) → ( 𝐶 gcd 𝐵 ) ∈ ℕ0 )
36 35 ancoms ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd 𝐵 ) ∈ ℕ0 )
37 36 3adant1 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd 𝐵 ) ∈ ℕ0 )
38 37 3ad2ant1 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐶 gcd 𝐵 ) ∈ ℕ0 )
39 38 nn0zd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐶 gcd 𝐵 ) ∈ ℤ )
40 mulgcd ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐴 gcd 𝐶 ) ∈ ℤ ∧ ( 𝐶 gcd 𝐵 ) ∈ ℤ ) → ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) ) = ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) )
41 21 33 39 40 syl3anc ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 · ( 𝐴 gcd 𝐶 ) ) gcd ( 𝐴 · ( 𝐶 gcd 𝐵 ) ) ) = ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) )
42 30 32 41 3eqtr3d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( ( 𝐴 gcd 𝐶 ) · ( 𝐴 gcd 𝐶 ) ) = ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) )
43 2 3ad2ant3 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℤ )
44 gcdid ( 𝐶 ∈ ℤ → ( 𝐶 gcd 𝐶 ) = ( abs ‘ 𝐶 ) )
45 43 44 syl ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd 𝐶 ) = ( abs ‘ 𝐶 ) )
46 45 oveq1d ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 gcd 𝐶 ) gcd 𝐵 ) = ( ( abs ‘ 𝐶 ) gcd 𝐵 ) )
47 simp2 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐵 ∈ ℤ )
48 gcdabs1 ( ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( abs ‘ 𝐶 ) gcd 𝐵 ) = ( 𝐶 gcd 𝐵 ) )
49 43 47 48 syl2anc ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( abs ‘ 𝐶 ) gcd 𝐵 ) = ( 𝐶 gcd 𝐵 ) )
50 46 49 eqtrd ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 gcd 𝐶 ) gcd 𝐵 ) = ( 𝐶 gcd 𝐵 ) )
51 gcdass ( ( 𝐶 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐶 gcd 𝐶 ) gcd 𝐵 ) = ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) )
52 43 43 47 51 syl3anc ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 gcd 𝐶 ) gcd 𝐵 ) = ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) )
53 43 47 gcdcomd ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd 𝐵 ) = ( 𝐵 gcd 𝐶 ) )
54 50 52 53 3eqtr3d ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) = ( 𝐵 gcd 𝐶 ) )
55 54 oveq2d ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 gcd ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) ) = ( 𝐴 gcd ( 𝐵 gcd 𝐶 ) ) )
56 1 3ad2ant1 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
57 37 nn0zd ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 gcd 𝐵 ) ∈ ℤ )
58 gcdass ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ ( 𝐶 gcd 𝐵 ) ∈ ℤ ) → ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) = ( 𝐴 gcd ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) ) )
59 56 43 57 58 syl3anc ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) = ( 𝐴 gcd ( 𝐶 gcd ( 𝐶 gcd 𝐵 ) ) ) )
60 gcdass ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = ( 𝐴 gcd ( 𝐵 gcd 𝐶 ) ) )
61 56 47 43 60 syl3anc ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = ( 𝐴 gcd ( 𝐵 gcd 𝐶 ) ) )
62 55 59 61 3eqtr4d ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) = ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) )
63 62 eqeq1d ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) = 1 ↔ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) )
64 63 biimpar ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) = 1 )
65 64 oveq2d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) = ( 𝐴 · 1 ) )
66 65 3adant3 ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) = ( 𝐴 · 1 ) )
67 13 mulid1d ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 · 1 ) = 𝐴 )
68 66 67 eqtrd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → ( 𝐴 · ( ( 𝐴 gcd 𝐶 ) gcd ( 𝐶 gcd 𝐵 ) ) ) = 𝐴 )
69 8 42 68 3eqtrrd ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ∧ ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) ) → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) )
70 69 3expia ( ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ) )