Step |
Hyp |
Ref |
Expression |
1 |
|
rplpwr |
⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐵 gcd 𝐴 ) = 1 → ( ( 𝐵 ↑ 𝑁 ) gcd 𝐴 ) = 1 ) ) |
2 |
1
|
3com12 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐵 gcd 𝐴 ) = 1 → ( ( 𝐵 ↑ 𝑁 ) gcd 𝐴 ) = 1 ) ) |
3 |
|
nnz |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ ) |
4 |
|
nnz |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ ) |
5 |
|
gcdcom |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) ) |
7 |
6
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) ) |
8 |
7
|
eqeq1d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd 𝐴 ) = 1 ) ) |
9 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℕ ) |
10 |
9
|
nnzd |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℤ ) |
11 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℕ ) |
12 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ ) |
13 |
12
|
nnnn0d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 ) |
14 |
11 13
|
nnexpcld |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ ) |
15 |
14
|
nnzd |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ ) |
16 |
10 15
|
gcdcomd |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐵 ↑ 𝑁 ) gcd 𝐴 ) ) |
17 |
16
|
eqeq1d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ↔ ( ( 𝐵 ↑ 𝑁 ) gcd 𝐴 ) = 1 ) ) |
18 |
2 8 17
|
3imtr4d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( 𝐴 gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) |