Proof of Theorem coprimeprodsq
Step | Hyp | Ref
| Expression |
1 | | nn0z 12326 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
2 | | nn0z 12326 |
. . . . . . . 8
⊢ (𝐶 ∈ ℕ0
→ 𝐶 ∈
ℤ) |
3 | | gcdcl 16194 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 gcd 𝐶) ∈
ℕ0) |
4 | 1, 2, 3 | syl2an 595 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝐴 gcd 𝐶) ∈
ℕ0) |
5 | 4 | 3adant2 1129 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐴 gcd 𝐶) ∈
ℕ0) |
6 | 5 | 3ad2ant1 1131 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 gcd 𝐶) ∈
ℕ0) |
7 | 6 | nn0cnd 12278 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 gcd 𝐶) ∈ ℂ) |
8 | 7 | sqvald 13842 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 gcd 𝐶)↑2) = ((𝐴 gcd 𝐶) · (𝐴 gcd 𝐶))) |
9 | | simp13 1203 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐶 ∈
ℕ0) |
10 | 9 | nn0cnd 12278 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐶 ∈ ℂ) |
11 | | nn0cn 12226 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
12 | 11 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → 𝐴 ∈ ℂ) |
13 | 12 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐴 ∈ ℂ) |
14 | 10, 13 | mulcomd 10980 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐶 · 𝐴) = (𝐴 · 𝐶)) |
15 | | simpl3 1191 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → 𝐶 ∈
ℕ0) |
16 | 15 | nn0cnd 12278 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → 𝐶 ∈ ℂ) |
17 | 16 | sqvald 13842 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → (𝐶↑2) = (𝐶 · 𝐶)) |
18 | 17 | eqeq1d 2741 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) ↔ (𝐶 · 𝐶) = (𝐴 · 𝐵))) |
19 | 18 | biimp3a 1467 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐶 · 𝐶) = (𝐴 · 𝐵)) |
20 | 14, 19 | oveq12d 7286 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐶 · 𝐴) gcd (𝐶 · 𝐶)) = ((𝐴 · 𝐶) gcd (𝐴 · 𝐵))) |
21 | | simp11 1201 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐴 ∈
ℕ0) |
22 | 21 | nn0zd 12406 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐴 ∈ ℤ) |
23 | 9 | nn0zd 12406 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐶 ∈ ℤ) |
24 | | mulgcd 16237 |
. . . . . . 7
⊢ ((𝐶 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐶 ∈ ℤ)
→ ((𝐶 · 𝐴) gcd (𝐶 · 𝐶)) = (𝐶 · (𝐴 gcd 𝐶))) |
25 | 9, 22, 23, 24 | syl3anc 1369 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐶 · 𝐴) gcd (𝐶 · 𝐶)) = (𝐶 · (𝐴 gcd 𝐶))) |
26 | | simp12 1202 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐵 ∈ ℤ) |
27 | | mulgcd 16237 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐶 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐴 · 𝐶) gcd (𝐴 · 𝐵)) = (𝐴 · (𝐶 gcd 𝐵))) |
28 | 21, 23, 26, 27 | syl3anc 1369 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 · 𝐶) gcd (𝐴 · 𝐵)) = (𝐴 · (𝐶 gcd 𝐵))) |
29 | 20, 25, 28 | 3eqtr3d 2787 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐶 · (𝐴 gcd 𝐶)) = (𝐴 · (𝐶 gcd 𝐵))) |
30 | 29 | oveq2d 7284 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐶 · (𝐴 gcd 𝐶))) = ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐴 · (𝐶 gcd 𝐵)))) |
31 | | mulgcdr 16239 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ (𝐴 gcd 𝐶) ∈ ℕ0) → ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐶 · (𝐴 gcd 𝐶))) = ((𝐴 gcd 𝐶) · (𝐴 gcd 𝐶))) |
32 | 22, 23, 6, 31 | syl3anc 1369 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐶 · (𝐴 gcd 𝐶))) = ((𝐴 gcd 𝐶) · (𝐴 gcd 𝐶))) |
33 | 6 | nn0zd 12406 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 gcd 𝐶) ∈ ℤ) |
34 | | gcdcl 16194 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐶 gcd 𝐵) ∈
ℕ0) |
35 | 2, 34 | sylan 579 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℕ0
∧ 𝐵 ∈ ℤ)
→ (𝐶 gcd 𝐵) ∈
ℕ0) |
36 | 35 | ancoms 458 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0)
→ (𝐶 gcd 𝐵) ∈
ℕ0) |
37 | 36 | 3adant1 1128 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 gcd 𝐵) ∈
ℕ0) |
38 | 37 | 3ad2ant1 1131 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐶 gcd 𝐵) ∈
ℕ0) |
39 | 38 | nn0zd 12406 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐶 gcd 𝐵) ∈ ℤ) |
40 | | mulgcd 16237 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ (𝐴 gcd 𝐶) ∈ ℤ ∧ (𝐶 gcd 𝐵) ∈ ℤ) → ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐴 · (𝐶 gcd 𝐵))) = (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)))) |
41 | 21, 33, 39, 40 | syl3anc 1369 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 · (𝐴 gcd 𝐶)) gcd (𝐴 · (𝐶 gcd 𝐵))) = (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)))) |
42 | 30, 32, 41 | 3eqtr3d 2787 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → ((𝐴 gcd 𝐶) · (𝐴 gcd 𝐶)) = (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)))) |
43 | 2 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → 𝐶 ∈ ℤ) |
44 | | gcdid 16215 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ ℤ → (𝐶 gcd 𝐶) = (abs‘𝐶)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 gcd 𝐶) = (abs‘𝐶)) |
46 | 45 | oveq1d 7283 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐶 gcd 𝐶) gcd 𝐵) = ((abs‘𝐶) gcd 𝐵)) |
47 | | simp2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → 𝐵 ∈ ℤ) |
48 | | gcdabs1 16217 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
((abs‘𝐶) gcd 𝐵) = (𝐶 gcd 𝐵)) |
49 | 43, 47, 48 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((abs‘𝐶) gcd 𝐵) = (𝐶 gcd 𝐵)) |
50 | 46, 49 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐶 gcd 𝐶) gcd 𝐵) = (𝐶 gcd 𝐵)) |
51 | | gcdass 16236 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐶 gcd 𝐶) gcd 𝐵) = (𝐶 gcd (𝐶 gcd 𝐵))) |
52 | 43, 43, 47, 51 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐶 gcd 𝐶) gcd 𝐵) = (𝐶 gcd (𝐶 gcd 𝐵))) |
53 | 43, 47 | gcdcomd 16202 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 gcd 𝐵) = (𝐵 gcd 𝐶)) |
54 | 50, 52, 53 | 3eqtr3d 2787 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 gcd (𝐶 gcd 𝐵)) = (𝐵 gcd 𝐶)) |
55 | 54 | oveq2d 7284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐴 gcd (𝐶 gcd (𝐶 gcd 𝐵))) = (𝐴 gcd (𝐵 gcd 𝐶))) |
56 | 1 | 3ad2ant1 1131 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → 𝐴 ∈ ℤ) |
57 | 37 | nn0zd 12406 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 gcd 𝐵) ∈ ℤ) |
58 | | gcdass 16236 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝐵) ∈ ℤ) → ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)) = (𝐴 gcd (𝐶 gcd (𝐶 gcd 𝐵)))) |
59 | 56, 43, 57, 58 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)) = (𝐴 gcd (𝐶 gcd (𝐶 gcd 𝐵)))) |
60 | | gcdass 16236 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = (𝐴 gcd (𝐵 gcd 𝐶))) |
61 | 56, 47, 43, 60 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐴 gcd 𝐵) gcd 𝐶) = (𝐴 gcd (𝐵 gcd 𝐶))) |
62 | 55, 59, 61 | 3eqtr4d 2789 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)) = ((𝐴 gcd 𝐵) gcd 𝐶)) |
63 | 62 | eqeq1d 2741 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) gcd 𝐶) = 1)) |
64 | 63 | biimpar 477 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵)) = 1) |
65 | 64 | oveq2d 7284 |
. . . . 5
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵))) = (𝐴 · 1)) |
66 | 65 | 3adant3 1130 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵))) = (𝐴 · 1)) |
67 | 13 | mulid1d 10976 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 · 1) = 𝐴) |
68 | 66, 67 | eqtrd 2779 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → (𝐴 · ((𝐴 gcd 𝐶) gcd (𝐶 gcd 𝐵))) = 𝐴) |
69 | 8, 42, 68 | 3eqtrrd 2784 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1 ∧ (𝐶↑2) = (𝐴 · 𝐵)) → 𝐴 = ((𝐴 gcd 𝐶)↑2)) |
70 | 69 | 3expia 1119 |
1
⊢ (((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈
ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) → 𝐴 = ((𝐴 gcd 𝐶)↑2))) |