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

Metamath Proof Explorer

Theorem nn0expgcd

Description: Exponentiation distributes over GCD. nn0gcdsq extended to nonnegative exponents. expgcd extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023)

Ref Expression
Assertion nn0expgcd ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2 elnn0 ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
3 expgcd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
5 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
6 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
7 6 3ad2ant3 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ↑ 𝑁 ) = 0 )
8 7 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 0 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 0 gcd ( 𝐵 ↑ 𝑁 ) ) )
9 simp2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℕ )
10 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11 10 3ad2ant3 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
12 9 11 nnexpcld ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
13 12 nnzd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
14 gcd0id ⊢ ( ( 𝐵 ↑ 𝑁 ) ∈ ℤ → ( 0 gcd ( 𝐵 ↑ 𝑁 ) ) = ( abs ‘ ( 𝐵 ↑ 𝑁 ) ) )
15 13 14 syl ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 gcd ( 𝐵 ↑ 𝑁 ) ) = ( abs ‘ ( 𝐵 ↑ 𝑁 ) ) )
16 12 nnred ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℝ )
17 0red ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℝ )
18 12 nngt0d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐵 ↑ 𝑁 ) )
19 17 16 18 ltled ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( 𝐵 ↑ 𝑁 ) )
20 16 19 absidd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( abs ‘ ( 𝐵 ↑ 𝑁 ) ) = ( 𝐵 ↑ 𝑁 ) )
21 8 15 20 3eqtrrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) = ( ( 0 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
22 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 𝐵 ) )
23 22 3ad2ant1 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 𝐵 ) )
24 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
25 24 3ad2ant2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℤ )
26 gcd0id ⊢ ( 𝐵 ∈ ℤ → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
27 25 26 syl ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
28 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
29 0red ⊢ ( 𝐵 ∈ ℕ → 0 ∈ ℝ )
30 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
31 29 28 30 ltled ⊢ ( 𝐵 ∈ ℕ → 0 ≤ 𝐵 )
32 28 31 absidd ⊢ ( 𝐵 ∈ ℕ → ( abs ‘ 𝐵 ) = 𝐵 )
33 32 3ad2ant2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( abs ‘ 𝐵 ) = 𝐵 )
34 23 27 33 3eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = 𝐵 )
35 34 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
36 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
37 36 3ad2ant1 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
38 37 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 0 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
39 21 35 38 3eqtr4d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
40 39 3expia ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
41 1z ⊢ 1 ∈ ℤ
42 gcd1 ⊢ ( 1 ∈ ℤ → ( 1 gcd 1 ) = 1 )
43 41 42 ax-mp ⊢ ( 1 gcd 1 ) = 1
44 43 eqcomi ⊢ 1 = ( 1 gcd 1 )
45 simp1 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → 𝐴 = 0 )
46 45 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 𝐵 ) )
47 simp2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → 𝐵 ∈ ℕ )
48 47 nnzd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → 𝐵 ∈ ℤ )
49 48 26 syl ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
50 32 3ad2ant2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( abs ‘ 𝐵 ) = 𝐵 )
51 46 49 50 3eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐴 gcd 𝐵 ) = 𝐵 )
52 simp3 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → 𝑁 = 0 )
53 51 52 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
54 47 nncnd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → 𝐵 ∈ ℂ )
55 54 exp0d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 0 ) = 1 )
56 53 55 eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = 1 )
57 45 52 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
58 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
59 58 a1i ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 0 ↑ 0 ) = 1 )
60 57 59 eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
61 52 oveq2d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
62 61 55 eqtrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = 1 )
63 60 62 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 1 gcd 1 ) )
64 44 56 63 3eqtr4a ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
65 64 3expia ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝑁 = 0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
66 40 65 jaod ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
67 5 66 biimtrid ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
68 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
69 68 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℕ0 )
70 10 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
71 69 70 nn0expcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 )
72 nn0gcdid0 ⊢ ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 → ( ( 𝐴 ↑ 𝑁 ) gcd 0 ) = ( 𝐴 ↑ 𝑁 ) )
73 71 72 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd 0 ) = ( 𝐴 ↑ 𝑁 ) )
74 simp2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → 𝐵 = 0 )
75 74 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
76 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 0 ↑ 𝑁 ) = 0 )
77 75 76 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) = 0 )
78 77 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) gcd 0 ) )
79 74 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = ( 𝐴 gcd 0 ) )
80 nn0gcdid0 ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 gcd 0 ) = 𝐴 )
81 68 80 syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 gcd 0 ) = 𝐴 )
82 81 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 0 ) = 𝐴 )
83 79 82 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = 𝐴 )
84 83 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
85 73 78 84 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
86 85 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
87 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
88 87 exp0d ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 0 ) = 1 )
89 88 43 eqtr4di ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ↑ 0 ) = ( 1 gcd 1 ) )
90 81 oveq1d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 gcd 0 ) ↑ 0 ) = ( 𝐴 ↑ 0 ) )
91 58 a1i ⊢ ( 𝐴 ∈ ℕ → ( 0 ↑ 0 ) = 1 )
92 88 91 oveq12d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 ↑ 0 ) gcd ( 0 ↑ 0 ) ) = ( 1 gcd 1 ) )
93 89 90 92 3eqtr4d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐴 gcd 0 ) ↑ 0 ) = ( ( 𝐴 ↑ 0 ) gcd ( 0 ↑ 0 ) ) )
94 93 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 0 ) ↑ 0 ) = ( ( 𝐴 ↑ 0 ) gcd ( 0 ↑ 0 ) ) )
95 simp2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → 𝐵 = 0 )
96 95 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 𝐴 gcd 0 ) )
97 simp3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
98 96 97 oveq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 gcd 0 ) ↑ 0 ) )
99 97 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
100 95 97 oveq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
101 99 100 oveq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 0 ) gcd ( 0 ↑ 0 ) ) )
102 94 98 101 3eqtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
103 102 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( 𝑁 = 0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
104 86 103 jaod ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
105 5 104 biimtrid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
106 gcd0val ⊢ ( 0 gcd 0 ) = 0
107 6 106 eqtr4di ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = ( 0 gcd 0 ) )
108 106 a1i ⊢ ( 𝑁 ∈ ℕ → ( 0 gcd 0 ) = 0 )
109 108 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 gcd 0 ) ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
110 6 6 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ↑ 𝑁 ) gcd ( 0 ↑ 𝑁 ) ) = ( 0 gcd 0 ) )
111 107 109 110 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 gcd 0 ) ↑ 𝑁 ) = ( ( 0 ↑ 𝑁 ) gcd ( 0 ↑ 𝑁 ) ) )
112 111 3ad2ant3 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 0 gcd 0 ) ↑ 𝑁 ) = ( ( 0 ↑ 𝑁 ) gcd ( 0 ↑ 𝑁 ) ) )
113 simp1 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → 𝐴 = 0 )
114 simp2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → 𝐵 = 0 )
115 113 114 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
116 115 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 0 gcd 0 ) ↑ 𝑁 ) )
117 113 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
118 114 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
119 117 118 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 0 ↑ 𝑁 ) gcd ( 0 ↑ 𝑁 ) ) )
120 112 116 119 3eqtr4d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
121 120 3expia ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
122 58 43 eqtr4i ⊢ ( 0 ↑ 0 ) = ( 1 gcd 1 )
123 106 oveq1i ⊢ ( ( 0 gcd 0 ) ↑ 0 ) = ( 0 ↑ 0 )
124 58 58 oveq12i ⊢ ( ( 0 ↑ 0 ) gcd ( 0 ↑ 0 ) ) = ( 1 gcd 1 )
125 122 123 124 3eqtr4i ⊢ ( ( 0 gcd 0 ) ↑ 0 ) = ( ( 0 ↑ 0 ) gcd ( 0 ↑ 0 ) )
126 simp1 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → 𝐴 = 0 )
127 simp2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → 𝐵 = 0 )
128 126 127 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
129 simp3 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
130 128 129 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 0 gcd 0 ) ↑ 0 ) )
131 126 129 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
132 127 129 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
133 131 132 oveq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( ( 0 ↑ 0 ) gcd ( 0 ↑ 0 ) ) )
134 125 130 133 3eqtr4a ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
135 134 3expia ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝑁 = 0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
136 121 135 jaod ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
137 5 136 biimtrid ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
138 4 67 105 137 ccase ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
139 1 2 138 syl2anb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) ) )
140 139 3impia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )