Step |
Hyp |
Ref |
Expression |
1 |
|
fltabcoprmex.a |
⊢ ( 𝜑 → 𝐴 ∈ ℕ ) |
2 |
|
fltabcoprmex.b |
⊢ ( 𝜑 → 𝐵 ∈ ℕ ) |
3 |
|
fltabcoprmex.c |
⊢ ( 𝜑 → 𝐶 ∈ ℕ ) |
4 |
|
fltabcoprmex.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
5 |
|
fltabcoprmex.1 |
⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) ) |
6 |
|
fltaccoprm.1 |
⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 ) |
7 |
2 4
|
nnexpcld |
⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℕ ) |
8 |
7
|
nncnd |
⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ ) |
9 |
1 4
|
nnexpcld |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℕ ) |
10 |
9
|
nncnd |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ ) |
11 |
8 10
|
addcomd |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) ) |
12 |
11 5
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) ) |
13 |
2
|
nnzd |
⊢ ( 𝜑 → 𝐵 ∈ ℤ ) |
14 |
1
|
nnzd |
⊢ ( 𝜑 → 𝐴 ∈ ℤ ) |
15 |
13 14
|
gcdcomd |
⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = ( 𝐴 gcd 𝐵 ) ) |
16 |
15 6
|
eqtrd |
⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = 1 ) |
17 |
2 1 3 4 12 16
|
fltaccoprm |
⊢ ( 𝜑 → ( 𝐵 gcd 𝐶 ) = 1 ) |