Metamath Proof Explorer

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 gcdcom ⊢ ( ( ( 𝐴 ↑ 𝑀 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) )
12 7 3 11 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) )
13 12 eqeq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
14 zexpcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
15 3 8 14 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
16 gcdcom ⊢ ( ( ( 𝐴 ↑ 𝑀 ) ∈ ℤ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℤ ) → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) )
17 7 15 16 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) )
18 17 eqeq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ↔ ( ( 𝐵 ↑ 𝑁 ) gcd ( 𝐴 ↑ 𝑀 ) ) = 1 ) )
19 10 13 18 3imtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( 𝐴 ↑ 𝑀 ) gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
20 2 19 syld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑀 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )