Metamath Proof Explorer

Theorem rpexp1i

Description: Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014)

Ref Expression
Assertion rpexp1i ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ 0 → A gcd B = 1 → A M gcd B = 1

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ M ∈ ℕ 0 ↔ M ∈ ℕ ∨ M = 0
2 rpexp ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A M gcd B = 1 ↔ A gcd B = 1
3 2 biimprd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A gcd B = 1 → A M gcd B = 1
4 3 3expa ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A gcd B = 1 → A M gcd B = 1
5 simpr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → M = 0
6 5 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A M = A 0
7 zcn ⊢ A ∈ ℤ → A ∈ ℂ
8 7 ad2antrr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A ∈ ℂ
9 8 exp0d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A 0 = 1
10 6 9 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A M = 1
11 10 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A M gcd B = 1 gcd B
12 1gcd ⊢ B ∈ ℤ → 1 gcd B = 1
13 12 ad2antlr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → 1 gcd B = 1
14 11 13 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A M gcd B = 1
15 14 a1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M = 0 → A gcd B = 1 → A M gcd B = 1
16 4 15 jaodan ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ ∨ M = 0 → A gcd B = 1 → A M gcd B = 1
17 1 16 sylan2b ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ 0 → A gcd B = 1 → A M gcd B = 1
18 17 3impa ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ 0 → A gcd B = 1 → A M gcd B = 1