This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdslegcd

Description: An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdslegcd 
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { n e. ZZ | A. z e. { M , N } n || z } = { n e. ZZ | A. z e. { M , N } n || z }
2 eqid 
 |-  { n e. ZZ | ( n || M /\ n || N ) } = { n e. ZZ | ( n || M /\ n || N ) }
3 1 2 gcdcllem3 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) e. NN /\ ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || M /\ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || N ) /\ ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) ) )
4 3 simp3d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
5 gcdn0val 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
6 5 breq2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( K <_ ( M gcd N ) <-> K <_ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
7 4 6 sylibrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ ( M gcd N ) ) )
8 7 com12 
 |-  ( ( K e. ZZ /\ K || M /\ K || N ) -> ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> K <_ ( M gcd N ) ) )
9 8 3expb 
 |-  ( ( K e. ZZ /\ ( K || M /\ K || N ) ) -> ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> K <_ ( M gcd N ) ) )
10 9 com12 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K e. ZZ /\ ( K || M /\ K || N ) ) -> K <_ ( M gcd N ) ) )
11 10 exp4b 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( K e. ZZ -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) ) ) )
12 11 com23 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ -> ( -. ( M = 0 /\ N = 0 ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) ) ) )
13 12 impcom 
 |-  ( ( K e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) ) )
14 13 3impb 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) ) )
15 14 imp 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) )