Metamath Proof Explorer

Theorem zexpgcd

Description: Exponentiation distributes over GCD. zgcdsq extended to nonnegative exponents. nn0expgcd extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023)

Ref Expression
Assertion zexpgcd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B N = A N gcd B N

Proof

Step Hyp Ref Expression
1 gcdabs ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = A gcd B
2 1 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B = A gcd B
3 2 eqcomd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B = A gcd B
4 3 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B N = A gcd B N
5 nn0abscl ⊢ A ∈ ℤ → A ∈ ℕ 0
6 nn0abscl ⊢ B ∈ ℤ → B ∈ ℕ 0
7 id ⊢ N ∈ ℕ 0 → N ∈ ℕ 0
8 nn0expgcd ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ N ∈ ℕ 0 → A gcd B N = A N gcd B N
9 5 6 7 8 syl3an ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B N = A N gcd B N
10 zcn ⊢ A ∈ ℤ → A ∈ ℂ
11 10 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A ∈ ℂ
12 simp3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → N ∈ ℕ 0
13 11 12 absexpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N = A N
14 13 eqcomd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N = A N
15 zcn ⊢ B ∈ ℤ → B ∈ ℂ
16 15 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → B ∈ ℂ
17 16 12 absexpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → B N = B N
18 17 eqcomd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → B N = B N
19 14 18 oveq12d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N gcd B N = A N gcd B N
20 zexpcl ⊢ A ∈ ℤ ∧ N ∈ ℕ 0 → A N ∈ ℤ
21 20 3adant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N ∈ ℤ
22 zexpcl ⊢ B ∈ ℤ ∧ N ∈ ℕ 0 → B N ∈ ℤ
23 22 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → B N ∈ ℤ
24 gcdabs ⊢ A N ∈ ℤ ∧ B N ∈ ℤ → A N gcd B N = A N gcd B N
25 21 23 24 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N gcd B N = A N gcd B N
26 19 25 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A N gcd B N = A N gcd B N
27 4 9 26 3eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ 0 → A gcd B N = A N gcd B N