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 ) )