Metamath Proof Explorer

Theorem divgcdodd

Description: Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014)

Ref Expression
Assertion divgcdodd 
|- ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )

Proof

Step Hyp Ref Expression
1 n2dvds1 
 |-  -. 2 || 1
2 2z 
 |-  2 e. ZZ
3 nnz 
 |-  ( A e. NN -> A e. ZZ )
4 nnz 
 |-  ( B e. NN -> B e. ZZ )
5 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
6 3 4 5 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
7 6 simpld 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) || A )
8 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
9 8 nnzd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. ZZ )
10 8 nnne0d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) =/= 0 )
11 3 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> A e. ZZ )
12 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
13 9 10 11 12 syl3anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
14 7 13 mpbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A / ( A gcd B ) ) e. ZZ )
15 6 simprd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) || B )
16 4 adantl 
 |-  ( ( A e. NN /\ B e. NN ) -> B e. ZZ )
17 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
18 9 10 16 17 syl3anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
19 15 18 mpbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( B / ( A gcd B ) ) e. ZZ )
20 dvdsgcdb 
 |-  ( ( 2 e. ZZ /\ ( A / ( A gcd B ) ) e. ZZ /\ ( B / ( A gcd B ) ) e. ZZ ) -> ( ( 2 || ( A / ( A gcd B ) ) /\ 2 || ( B / ( A gcd B ) ) ) <-> 2 || ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) ) )
21 2 14 19 20 mp3an2i 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( 2 || ( A / ( A gcd B ) ) /\ 2 || ( B / ( A gcd B ) ) ) <-> 2 || ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) ) )
22 gcddiv 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( A gcd B ) e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
23 11 16 8 6 22 syl31anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
24 8 nncnd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. CC )
25 24 10 dividd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
26 23 25 eqtr3d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
27 26 breq2d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( 2 || ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) <-> 2 || 1 ) )
28 27 biimpd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( 2 || ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) -> 2 || 1 ) )
29 21 28 sylbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( 2 || ( A / ( A gcd B ) ) /\ 2 || ( B / ( A gcd B ) ) ) -> 2 || 1 ) )
30 29 expdimp 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ 2 || ( A / ( A gcd B ) ) ) -> ( 2 || ( B / ( A gcd B ) ) -> 2 || 1 ) )
31 1 30 mtoi 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ 2 || ( A / ( A gcd B ) ) ) -> -. 2 || ( B / ( A gcd B ) ) )
32 31 ex 
 |-  ( ( A e. NN /\ B e. NN ) -> ( 2 || ( A / ( A gcd B ) ) -> -. 2 || ( B / ( A gcd B ) ) ) )
33 imor 
 |-  ( ( 2 || ( A / ( A gcd B ) ) -> -. 2 || ( B / ( A gcd B ) ) ) <-> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
34 32 33 sylib 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )