Metamath Proof Explorer

Theorem divgcdoddALTV

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

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

Proof

Step Hyp Ref Expression
1 divgcdodd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
2 nnz 
 |-  ( A e. NN -> A e. ZZ )
3 nnz 
 |-  ( B e. NN -> B e. ZZ )
4 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
5 2 3 4 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
6 5 simpld 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) || A )
7 2 3 anim12i 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A e. ZZ /\ B e. ZZ ) )
8 nnne0 
 |-  ( A e. NN -> A =/= 0 )
9 8 neneqd 
 |-  ( A e. NN -> -. A = 0 )
10 9 intnanrd 
 |-  ( A e. NN -> -. ( A = 0 /\ B = 0 ) )
11 10 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> -. ( A = 0 /\ B = 0 ) )
12 gcdn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
13 7 11 12 syl2anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
14 13 nnzd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. ZZ )
15 13 nnne0d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) =/= 0 )
16 2 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> A e. ZZ )
17 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
18 14 15 16 17 syl3anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
19 6 18 mpbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A / ( A gcd B ) ) e. ZZ )
20 19 biantrurd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) <-> ( ( A / ( A gcd B ) ) e. ZZ /\ -. 2 || ( A / ( A gcd B ) ) ) ) )
21 5 simprd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) || B )
22 3 adantl 
 |-  ( ( A e. NN /\ B e. NN ) -> B e. ZZ )
23 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
24 14 15 22 23 syl3anc 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
25 21 24 mpbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( B / ( A gcd B ) ) e. ZZ )
26 25 biantrurd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( B / ( A gcd B ) ) <-> ( ( B / ( A gcd B ) ) e. ZZ /\ -. 2 || ( B / ( A gcd B ) ) ) ) )
27 20 26 orbi12d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) <-> ( ( ( A / ( A gcd B ) ) e. ZZ /\ -. 2 || ( A / ( A gcd B ) ) ) \/ ( ( B / ( A gcd B ) ) e. ZZ /\ -. 2 || ( B / ( A gcd B ) ) ) ) ) )
28 1 27 mpbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( ( A / ( A gcd B ) ) e. ZZ /\ -. 2 || ( A / ( A gcd B ) ) ) \/ ( ( B / ( A gcd B ) ) e. ZZ /\ -. 2 || ( B / ( A gcd B ) ) ) ) )
29 isodd3 
 |-  ( ( A / ( A gcd B ) ) e. Odd <-> ( ( A / ( A gcd B ) ) e. ZZ /\ -. 2 || ( A / ( A gcd B ) ) ) )
30 isodd3 
 |-  ( ( B / ( A gcd B ) ) e. Odd <-> ( ( B / ( A gcd B ) ) e. ZZ /\ -. 2 || ( B / ( A gcd B ) ) ) )
31 29 30 orbi12i 
 |-  ( ( ( A / ( A gcd B ) ) e. Odd \/ ( B / ( A gcd B ) ) e. Odd ) <-> ( ( ( A / ( A gcd B ) ) e. ZZ /\ -. 2 || ( A / ( A gcd B ) ) ) \/ ( ( B / ( A gcd B ) ) e. ZZ /\ -. 2 || ( B / ( A gcd B ) ) ) ) )
32 28 31 sylibr 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A / ( A gcd B ) ) e. Odd \/ ( B / ( A gcd B ) ) e. Odd ) )