# 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( A e. NN /\ B e. ZZ ) -> A e. RR )`
` |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> ( ( A gcd B ) <_ A /\ A <_ ( A gcd B ) ) ) )`
` |-  ( ( A e. NN /\ B e. ZZ ) -> ( A || B -> ( A gcd B ) = A ) )`
` |-  ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )`