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 ⊢ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C 2 = A ⁢ B → A = A gcd C 2

Proof

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