Theorem rpexp12i

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

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

Proof

Step	Hyp	Ref	Expression
1		rpexp1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 ) )
2	1	3adant3r	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 ) )
3		simp2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐵 ∈ ℤ )
4		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐴 ∈ ℤ )
5		simp3l	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
6		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℤ )
7	4 5 6	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℤ )
8		simp3r	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
9		rpexp1i	⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) = 1 → ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
10	3 7 8 9	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) = 1 → ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
11	7 3	gcdcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) )
12	11	eqeq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
13		zexpcl	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
14	3 8 13	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
15	7 14	gcdcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) )
16	15	eqeq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ↔ ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
17	10 12 16	3imtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
18	2 17	syld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )