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

Metamath Proof Explorer

Theorem rpexp

Description: If two numbers A and B are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion rpexp ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
2 1 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ↑ 𝑁 ) gcd 0 ) = ( 0 gcd 0 ) )
3 2 eqeq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 0 ↑ 𝑁 ) gcd 0 ) = 1 ↔ ( 0 gcd 0 ) = 1 ) )
4 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
5 oveq12 ⊢ ( ( ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = ( ( 0 ↑ 𝑁 ) gcd 0 ) )
6 4 5 sylan ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = ( ( 0 ↑ 𝑁 ) gcd 0 ) )
7 6 eqeq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( ( 0 ↑ 𝑁 ) gcd 0 ) = 1 ) )
8 oveq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
9 8 eqeq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 ↔ ( 0 gcd 0 ) = 1 ) )
10 7 9 bibi12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ↔ ( ( ( 0 ↑ 𝑁 ) gcd 0 ) = 1 ↔ ( 0 gcd 0 ) = 1 ) ) )
11 3 10 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ) )
13 exprmfct ⊢ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) )
14 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝐴 ∈ ℤ )
15 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝑁 ∈ ℕ )
16 15 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝑁 ∈ ℕ0 )
17 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
18 14 16 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
19 18 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
20 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝐵 ∈ ℤ )
21 20 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
22 gcddvds ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ 𝐵 ) )
23 19 21 22 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ 𝐵 ) )
24 23 simpld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) )
25 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
26 25 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
27 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
28 14 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 𝐴 ∈ ℂ )
29 expeq0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) )
30 28 15 29 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ↑ 𝑁 ) = 0 ↔ 𝐴 = 0 ) )
31 30 anbi1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) = 0 ∧ 𝐵 = 0 ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
32 27 31 mtbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ¬ ( ( 𝐴 ↑ 𝑁 ) = 0 ∧ 𝐵 = 0 ) )
33 gcdn0cl ⊢ ( ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( ( 𝐴 ↑ 𝑁 ) = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℕ )
34 18 20 32 33 syl21anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℕ )
35 34 nnzd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℤ )
36 35 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℤ )
37 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → ( ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
38 26 36 19 37 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
39 24 38 mpan2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
40 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
41 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
42 15 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
43 prmdvdsexp ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ↔ 𝑝 ∥ 𝐴 ) )
44 40 41 42 43 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ↔ 𝑝 ∥ 𝐴 ) )
45 39 44 sylibd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → 𝑝 ∥ 𝐴 ) )
46 23 simprd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ 𝐵 )
47 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ 𝐵 ) → 𝑝 ∥ 𝐵 ) )
48 26 36 21 47 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∥ 𝐵 ) → 𝑝 ∥ 𝐵 ) )
49 46 48 mpan2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → 𝑝 ∥ 𝐵 ) )
50 45 49 jcad ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) )
51 dvdsgcd ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ) )
52 26 41 21 51 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ) )
53 nprmdvds1 ⊢ ( 𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1 )
54 breq2 ⊢ ( ( 𝐴 gcd 𝐵 ) = 1 → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ↔ 𝑝 ∥ 1 ) )
55 54 notbid ⊢ ( ( 𝐴 gcd 𝐵 ) = 1 → ( ¬ 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ↔ ¬ 𝑝 ∥ 1 ) )
56 53 55 syl5ibrcom ⊢ ( 𝑝 ∈ ℙ → ( ( 𝐴 gcd 𝐵 ) = 1 → ¬ 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ) )
57 56 necon2ad ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
58 57 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
59 50 52 58 3syld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
60 59 rexlimdva ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
61 gcdn0cl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
62 61 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
63 eluz2b3 ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝐴 gcd 𝐵 ) ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
64 63 baib ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
65 62 64 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
66 60 65 sylibrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ) )
67 13 66 syl5 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ) )
68 exprmfct ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐴 gcd 𝐵 ) )
69 62 nnzd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
70 69 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
71 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
72 41 21 71 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
73 72 simpld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
74 iddvdsexp ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∥ ( 𝐴 ↑ 𝑁 ) )
75 41 42 74 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∥ ( 𝐴 ↑ 𝑁 ) )
76 70 41 19 73 75 dvdstrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) )
77 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ∧ ( 𝐴 gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
78 26 70 19 77 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ∧ ( 𝐴 gcd 𝐵 ) ∥ ( 𝐴 ↑ 𝑁 ) ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
79 76 78 mpan2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ) )
80 72 simprd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
81 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → 𝑝 ∥ 𝐵 ) )
82 26 70 21 81 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → 𝑝 ∥ 𝐵 ) )
83 80 82 mpan2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → 𝑝 ∥ 𝐵 ) )
84 79 83 jcad ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ∧ 𝑝 ∥ 𝐵 ) ) )
85 dvdsgcd ⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ) )
86 26 19 21 85 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( 𝐴 ↑ 𝑁 ) ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ) )
87 breq2 ⊢ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ↔ 𝑝 ∥ 1 ) )
88 87 notbid ⊢ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 → ( ¬ 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ↔ ¬ 𝑝 ∥ 1 ) )
89 53 88 syl5ibrcom ⊢ ( 𝑝 ∈ ℙ → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 → ¬ 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ) )
90 89 necon2ad ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
91 90 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
92 84 86 91 3syld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
93 92 rexlimdva ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
94 eluz2b3 ⊢ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℕ ∧ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
95 94 baib ⊢ ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ℕ → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
96 34 95 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ) )
97 93 96 sylibrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝐴 gcd 𝐵 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ) )
98 68 97 syl5 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ) )
99 67 98 impbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 gcd 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ) )
100 99 96 65 3bitr3d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) ≠ 1 ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
101 100 necon4bid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
102 101 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ) )
103 12 102 pm2.61d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )