Metamath Proof Explorer

Theorem gcdzeq

Description: A positive integer A is equal to its gcd with an integer B if and only if A divides B . Generalization of gcdeq . (Contributed by AV, 1-Jul-2020)

Ref Expression
Assertion gcdzeq 
|- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( A e. NN -> A e. ZZ )
2 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
3 1 2 sylan 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
4 3 simprd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) || B )
5 breq1 
 |-  ( ( A gcd B ) = A -> ( ( A gcd B ) || B <-> A || B ) )
6 4 5 syl5ibcom 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A -> A || B ) )
7 1 adantr 
 |-  ( ( A e. NN /\ B e. ZZ ) -> A e. ZZ )
8 iddvds 
 |-  ( A e. ZZ -> A || A )
9 7 8 syl 
 |-  ( ( A e. NN /\ B e. ZZ ) -> A || A )
10 simpr 
 |-  ( ( A e. NN /\ B e. ZZ ) -> B e. ZZ )
11 nnne0 
 |-  ( A e. NN -> A =/= 0 )
12 simpl 
 |-  ( ( A = 0 /\ B = 0 ) -> A = 0 )
13 12 necon3ai 
 |-  ( A =/= 0 -> -. ( A = 0 /\ B = 0 ) )
14 11 13 syl 
 |-  ( A e. NN -> -. ( A = 0 /\ B = 0 ) )
15 14 adantr 
 |-  ( ( A e. NN /\ B e. ZZ ) -> -. ( A = 0 /\ B = 0 ) )
16 dvdslegcd 
 |-  ( ( ( A e. ZZ /\ A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( ( A || A /\ A || B ) -> A <_ ( A gcd B ) ) )
17 7 7 10 15 16 syl31anc 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A || A /\ A || B ) -> A <_ ( A gcd B ) ) )
18 9 17 mpand 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A || B -> A <_ ( A gcd B ) ) )
19 3 simpld 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) || A )
20 gcdcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
21 1 20 sylan 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
22 21 nn0zd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) e. ZZ )
23 simpl 
 |-  ( ( A e. NN /\ B e. ZZ ) -> A e. NN )
24 dvdsle 
 |-  ( ( ( A gcd B ) e. ZZ /\ A e. NN ) -> ( ( A gcd B ) || A -> ( A gcd B ) <_ A ) )
25 22 23 24 syl2anc 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) || A -> ( A gcd B ) <_ A ) )
26 19 25 mpd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) <_ A )
27 18 26 jctild 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A || B -> ( ( A gcd B ) <_ A /\ A <_ ( A gcd B ) ) ) )
28 21 nn0red 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) e. RR )
29 nnre 
 |-  ( A e. NN -> A e. RR )
30 29 adantr 
 |-  ( ( A e. NN /\ B e. ZZ ) -> A e. RR )
31 28 30 letri3d 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> ( ( A gcd B ) <_ A /\ A <_ ( A gcd B ) ) ) )
32 27 31 sylibrd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A || B -> ( A gcd B ) = A ) )
33 6 32 impbid 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )