Metamath Proof Explorer

Theorem modgcd

Description: The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion modgcd 
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) gcd N ) = ( M gcd N ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( M e. ZZ -> M e. RR )
2 nnrp 
 |-  ( N e. NN -> N e. RR+ )
3 modval 
 |-  ( ( M e. RR /\ N e. RR+ ) -> ( M mod N ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M mod N ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
5 zcn 
 |-  ( M e. ZZ -> M e. CC )
6 5 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. CC )
7 nncn 
 |-  ( N e. NN -> N e. CC )
8 7 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. CC )
9 nnre 
 |-  ( N e. NN -> N e. RR )
10 nnne0 
 |-  ( N e. NN -> N =/= 0 )
11 redivcl 
 |-  ( ( M e. RR /\ N e. RR /\ N =/= 0 ) -> ( M / N ) e. RR )
12 1 9 10 11 syl3an 
 |-  ( ( M e. ZZ /\ N e. NN /\ N e. NN ) -> ( M / N ) e. RR )
13 12 3anidm23 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. RR )
14 13 flcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. ZZ )
15 14 zcnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. CC )
16 mulneg1 
 |-  ( ( ( |_ ` ( M / N ) ) e. CC /\ N e. CC ) -> ( -u ( |_ ` ( M / N ) ) x. N ) = -u ( ( |_ ` ( M / N ) ) x. N ) )
17 mulcom 
 |-  ( ( ( |_ ` ( M / N ) ) e. CC /\ N e. CC ) -> ( ( |_ ` ( M / N ) ) x. N ) = ( N x. ( |_ ` ( M / N ) ) ) )
18 17 negeqd 
 |-  ( ( ( |_ ` ( M / N ) ) e. CC /\ N e. CC ) -> -u ( ( |_ ` ( M / N ) ) x. N ) = -u ( N x. ( |_ ` ( M / N ) ) ) )
19 16 18 eqtrd 
 |-  ( ( ( |_ ` ( M / N ) ) e. CC /\ N e. CC ) -> ( -u ( |_ ` ( M / N ) ) x. N ) = -u ( N x. ( |_ ` ( M / N ) ) ) )
20 19 ancoms 
 |-  ( ( N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( -u ( |_ ` ( M / N ) ) x. N ) = -u ( N x. ( |_ ` ( M / N ) ) ) )
21 20 3adant1 
 |-  ( ( M e. CC /\ N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( -u ( |_ ` ( M / N ) ) x. N ) = -u ( N x. ( |_ ` ( M / N ) ) ) )
22 21 oveq2d 
 |-  ( ( M e. CC /\ N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) = ( M + -u ( N x. ( |_ ` ( M / N ) ) ) ) )
23 mulcl 
 |-  ( ( N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( N x. ( |_ ` ( M / N ) ) ) e. CC )
24 negsub 
 |-  ( ( M e. CC /\ ( N x. ( |_ ` ( M / N ) ) ) e. CC ) -> ( M + -u ( N x. ( |_ ` ( M / N ) ) ) ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
25 23 24 sylan2 
 |-  ( ( M e. CC /\ ( N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) ) -> ( M + -u ( N x. ( |_ ` ( M / N ) ) ) ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
26 25 3impb 
 |-  ( ( M e. CC /\ N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( M + -u ( N x. ( |_ ` ( M / N ) ) ) ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
27 22 26 eqtrd 
 |-  ( ( M e. CC /\ N e. CC /\ ( |_ ` ( M / N ) ) e. CC ) -> ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
28 6 8 15 27 syl3anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) = ( M - ( N x. ( |_ ` ( M / N ) ) ) ) )
29 4 28 eqtr4d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M mod N ) = ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) )
30 29 oveq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd ( M mod N ) ) = ( N gcd ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) ) )
31 14 znegcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> -u ( |_ ` ( M / N ) ) e. ZZ )
32 nnz 
 |-  ( N e. NN -> N e. ZZ )
33 32 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. ZZ )
34 simpl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. ZZ )
35 gcdaddm 
 |-  ( ( -u ( |_ ` ( M / N ) ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( N gcd M ) = ( N gcd ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) ) )
36 31 33 34 35 syl3anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd M ) = ( N gcd ( M + ( -u ( |_ ` ( M / N ) ) x. N ) ) ) )
37 30 36 eqtr4d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd ( M mod N ) ) = ( N gcd M ) )
38 zmodcl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M mod N ) e. NN0 )
39 38 nn0zd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M mod N ) e. ZZ )
40 33 39 gcdcomd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd ( M mod N ) ) = ( ( M mod N ) gcd N ) )
41 33 34 gcdcomd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd M ) = ( M gcd N ) )
42 37 40 41 3eqtr3d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) gcd N ) = ( M gcd N ) )