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 ) )