This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mulridd ⊢ ( ( ( 𝐴 ∈ ℕ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 ) ) )