Metamath Proof Explorer

Theorem divgcdcoprm0

Description: Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021)

Ref Expression
Assertion divgcdcoprm0 
|- ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
2 1 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
3 gcdcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
4 3 nn0zd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. ZZ )
5 simpl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
6 4 5 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) e. ZZ /\ A e. ZZ ) )
7 6 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) e. ZZ /\ A e. ZZ ) )
8 divides 
 |-  ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> E. a e. ZZ ( a x. ( A gcd B ) ) = A ) )
9 7 8 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) || A <-> E. a e. ZZ ( a x. ( A gcd B ) ) = A ) )
10 simpr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
11 4 10 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) e. ZZ /\ B e. ZZ ) )
12 11 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) e. ZZ /\ B e. ZZ ) )
13 divides 
 |-  ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> E. b e. ZZ ( b x. ( A gcd B ) ) = B ) )
14 12 13 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) || B <-> E. b e. ZZ ( b x. ( A gcd B ) ) = B ) )
15 9 14 anbi12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) <-> ( E. a e. ZZ ( a x. ( A gcd B ) ) = A /\ E. b e. ZZ ( b x. ( A gcd B ) ) = B ) ) )
16 bezout 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> E. m e. ZZ E. n e. ZZ ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) )
17 16 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> E. m e. ZZ E. n e. ZZ ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) )
18 oveq1 
 |-  ( ( a x. ( A gcd B ) ) = A -> ( ( a x. ( A gcd B ) ) x. m ) = ( A x. m ) )
19 oveq1 
 |-  ( ( b x. ( A gcd B ) ) = B -> ( ( b x. ( A gcd B ) ) x. n ) = ( B x. n ) )
20 18 19 oveqan12rd 
 |-  ( ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) -> ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) = ( ( A x. m ) + ( B x. n ) ) )
21 20 eqeq2d 
 |-  ( ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) -> ( ( A gcd B ) = ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) <-> ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) ) )
22 21 bicomd 
 |-  ( ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) <-> ( A gcd B ) = ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) ) )
23 simpl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. ZZ )
24 23 zcnd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. CC )
25 24 adantl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
26 3 nn0cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. CC )
27 26 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) e. CC )
28 27 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) e. CC )
29 simpl 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> m e. ZZ )
30 29 zcnd 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> m e. CC )
31 30 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> m e. CC )
32 25 28 31 mul32d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. ( A gcd B ) ) x. m ) = ( ( a x. m ) x. ( A gcd B ) ) )
33 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
34 33 zcnd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. CC )
35 34 adantl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
36 simpr 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> n e. ZZ )
37 36 zcnd 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> n e. CC )
38 37 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> n e. CC )
39 35 28 38 mul32d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) x. n ) = ( ( b x. n ) x. ( A gcd B ) ) )
40 32 39 oveq12d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) = ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) )
41 40 eqeq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A gcd B ) = ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) <-> ( A gcd B ) = ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) ) )
42 23 adantl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
43 29 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> m e. ZZ )
44 42 43 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a x. m ) e. ZZ )
45 4 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) e. ZZ )
46 45 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) e. ZZ )
47 44 46 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. m ) x. ( A gcd B ) ) e. ZZ )
48 33 adantl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
49 36 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> n e. ZZ )
50 48 49 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. n ) e. ZZ )
51 3 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) e. NN0 )
52 51 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) e. NN0 )
53 52 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) e. ZZ )
54 50 53 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. n ) x. ( A gcd B ) ) e. ZZ )
55 47 54 zaddcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) e. ZZ )
56 55 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) e. CC )
57 gcd2n0cl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) e. NN )
58 nnrp 
 |-  ( ( A gcd B ) e. NN -> ( A gcd B ) e. RR+ )
59 58 rpcnne0d 
 |-  ( ( A gcd B ) e. NN -> ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) )
60 57 59 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) )
61 60 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) )
62 div11 
 |-  ( ( ( A gcd B ) e. CC /\ ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) e. CC /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( ( ( A gcd B ) / ( A gcd B ) ) = ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) <-> ( A gcd B ) = ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) ) )
63 28 56 61 62 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( A gcd B ) / ( A gcd B ) ) = ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) <-> ( A gcd B ) = ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) ) )
64 divid 
 |-  ( ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
65 61 64 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
66 47 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. m ) x. ( A gcd B ) ) e. CC )
67 54 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. n ) x. ( A gcd B ) ) e. CC )
68 divdir 
 |-  ( ( ( ( a x. m ) x. ( A gcd B ) ) e. CC /\ ( ( b x. n ) x. ( A gcd B ) ) e. CC /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) = ( ( ( ( a x. m ) x. ( A gcd B ) ) / ( A gcd B ) ) + ( ( ( b x. n ) x. ( A gcd B ) ) / ( A gcd B ) ) ) )
69 66 67 61 68 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) = ( ( ( ( a x. m ) x. ( A gcd B ) ) / ( A gcd B ) ) + ( ( ( b x. n ) x. ( A gcd B ) ) / ( A gcd B ) ) ) )
70 44 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a x. m ) e. CC )
71 51 nn0cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) e. CC )
72 71 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) e. CC )
73 57 nnne0d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A gcd B ) =/= 0 )
74 73 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A gcd B ) =/= 0 )
75 70 72 74 divcan4d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a x. m ) x. ( A gcd B ) ) / ( A gcd B ) ) = ( a x. m ) )
76 50 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. n ) e. CC )
77 76 28 74 divcan4d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( b x. n ) x. ( A gcd B ) ) / ( A gcd B ) ) = ( b x. n ) )
78 75 77 oveq12d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( ( a x. m ) x. ( A gcd B ) ) / ( A gcd B ) ) + ( ( ( b x. n ) x. ( A gcd B ) ) / ( A gcd B ) ) ) = ( ( a x. m ) + ( b x. n ) ) )
79 69 78 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) = ( ( a x. m ) + ( b x. n ) ) )
80 65 79 eqeq12d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( A gcd B ) / ( A gcd B ) ) = ( ( ( ( a x. m ) x. ( A gcd B ) ) + ( ( b x. n ) x. ( A gcd B ) ) ) / ( A gcd B ) ) <-> 1 = ( ( a x. m ) + ( b x. n ) ) ) )
81 41 63 80 3bitr2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A gcd B ) = ( ( ( a x. ( A gcd B ) ) x. m ) + ( ( b x. ( A gcd B ) ) x. n ) ) <-> 1 = ( ( a x. m ) + ( b x. n ) ) ) )
82 22 81 sylan9bbr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) <-> 1 = ( ( a x. m ) + ( b x. n ) ) ) )
83 eqcom 
 |-  ( 1 = ( ( a x. m ) + ( b x. n ) ) <-> ( ( a x. m ) + ( b x. n ) ) = 1 )
84 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( m e. ZZ /\ n e. ZZ ) )
85 84 anim1ci 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. ZZ /\ b e. ZZ ) /\ ( m e. ZZ /\ n e. ZZ ) ) )
86 bezoutr1 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( ( a x. m ) + ( b x. n ) ) = 1 -> ( a gcd b ) = 1 ) )
87 85 86 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a x. m ) + ( b x. n ) ) = 1 -> ( a gcd b ) = 1 ) )
88 87 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( ( ( a x. m ) + ( b x. n ) ) = 1 -> ( a gcd b ) = 1 ) )
89 83 88 biimtrid 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( 1 = ( ( a x. m ) + ( b x. n ) ) -> ( a gcd b ) = 1 ) )
90 simpll1 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> A e. ZZ )
91 90 zcnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> A e. CC )
92 divmul3 
 |-  ( ( A e. CC /\ a e. CC /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( ( A / ( A gcd B ) ) = a <-> A = ( a x. ( A gcd B ) ) ) )
93 91 25 61 92 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A / ( A gcd B ) ) = a <-> A = ( a x. ( A gcd B ) ) ) )
94 eqcom 
 |-  ( a = ( A / ( A gcd B ) ) <-> ( A / ( A gcd B ) ) = a )
95 eqcom 
 |-  ( ( a x. ( A gcd B ) ) = A <-> A = ( a x. ( A gcd B ) ) )
96 93 94 95 3bitr4g 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a = ( A / ( A gcd B ) ) <-> ( a x. ( A gcd B ) ) = A ) )
97 96 biimprd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. ( A gcd B ) ) = A -> a = ( A / ( A gcd B ) ) ) )
98 97 a1d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> a = ( A / ( A gcd B ) ) ) ) )
99 98 imp32 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> a = ( A / ( A gcd B ) ) )
100 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> B e. ZZ )
101 100 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> B e. CC )
102 101 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> B e. CC )
103 divmul3 
 |-  ( ( B e. CC /\ b e. CC /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( ( B / ( A gcd B ) ) = b <-> B = ( b x. ( A gcd B ) ) ) )
104 102 35 61 103 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B / ( A gcd B ) ) = b <-> B = ( b x. ( A gcd B ) ) ) )
105 eqcom 
 |-  ( b = ( B / ( A gcd B ) ) <-> ( B / ( A gcd B ) ) = b )
106 eqcom 
 |-  ( ( b x. ( A gcd B ) ) = B <-> B = ( b x. ( A gcd B ) ) )
107 104 105 106 3bitr4g 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b = ( B / ( A gcd B ) ) <-> ( b x. ( A gcd B ) ) = B ) )
108 107 biimprd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) = B -> b = ( B / ( A gcd B ) ) ) )
109 108 a1dd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> b = ( B / ( A gcd B ) ) ) ) )
110 109 imp32 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> b = ( B / ( A gcd B ) ) )
111 99 110 oveq12d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( a gcd b ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
112 111 eqeq1d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( ( a gcd b ) = 1 <-> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
113 89 112 sylibd 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( 1 = ( ( a x. m ) + ( b x. n ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
114 82 113 sylbid 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( ( b x. ( A gcd B ) ) = B /\ ( a x. ( A gcd B ) ) = A ) ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
115 114 exp32 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) )
116 115 com34 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) )
117 116 com23 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) )
118 117 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( a e. ZZ /\ b e. ZZ ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) ) )
119 118 com23 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( a e. ZZ /\ b e. ZZ ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) ) )
120 119 rexlimdvva 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( E. m e. ZZ E. n e. ZZ ( A gcd B ) = ( ( A x. m ) + ( B x. n ) ) -> ( ( a e. ZZ /\ b e. ZZ ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) ) )
121 17 120 mpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( a e. ZZ /\ b e. ZZ ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) ) )
122 121 impl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) )
123 122 rexlimdva 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ a e. ZZ ) -> ( E. b e. ZZ ( b x. ( A gcd B ) ) = B -> ( ( a x. ( A gcd B ) ) = A -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) )
124 123 com23 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) /\ a e. ZZ ) -> ( ( a x. ( A gcd B ) ) = A -> ( E. b e. ZZ ( b x. ( A gcd B ) ) = B -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) )
125 124 rexlimdva 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( E. a e. ZZ ( a x. ( A gcd B ) ) = A -> ( E. b e. ZZ ( b x. ( A gcd B ) ) = B -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) ) )
126 125 impd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( E. a e. ZZ ( a x. ( A gcd B ) ) = A /\ E. b e. ZZ ( b x. ( A gcd B ) ) = B ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
127 15 126 sylbid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 ) )
128 2 127 mpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )