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 
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A ^ N ) gcd B ) = 1 <-> ( A gcd B ) = 1 ) )

Proof

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