This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpexp1i

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

Ref Expression
Assertion rpexp1i ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 ) )

Proof

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