Metamath Proof Explorer


Theorem gcdaddmlem

Description: Lemma for gcdaddm . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses gcdaddmlem.1 K
gcdaddmlem.2 M
gcdaddmlem.3 N
Assertion gcdaddmlem M gcd N = M gcd K M + N

Proof

Step Hyp Ref Expression
1 gcdaddmlem.1 K
2 gcdaddmlem.2 M
3 gcdaddmlem.3 N
4 gcddvds M N M gcd N M M gcd N N
5 2 3 4 mp2an M gcd N M M gcd N N
6 5 simpli M gcd N M
7 gcdcl M N M gcd N 0
8 2 3 7 mp2an M gcd N 0
9 8 nn0zi M gcd N
10 1z 1
11 dvds2ln K 1 M gcd N M N M gcd N M M gcd N N M gcd N K M + 1 N
12 1 10 11 mpanl12 M gcd N M N M gcd N M M gcd N N M gcd N K M + 1 N
13 9 2 3 12 mp3an M gcd N M M gcd N N M gcd N K M + 1 N
14 5 13 ax-mp M gcd N K M + 1 N
15 zcn N N
16 3 15 ax-mp N
17 16 mulid2i 1 N = N
18 17 oveq2i K M + 1 N = K M + N
19 14 18 breqtri M gcd N K M + N
20 zmulcl K M K M
21 1 2 20 mp2an K M
22 zaddcl K M N K M + N
23 21 3 22 mp2an K M + N
24 dvdslegcd M gcd N M K M + N ¬ M = 0 K M + N = 0 M gcd N M M gcd N K M + N M gcd N M gcd K M + N
25 24 ex M gcd N M K M + N ¬ M = 0 K M + N = 0 M gcd N M M gcd N K M + N M gcd N M gcd K M + N
26 9 2 23 25 mp3an ¬ M = 0 K M + N = 0 M gcd N M M gcd N K M + N M gcd N M gcd K M + N
27 6 19 26 mp2ani ¬ M = 0 K M + N = 0 M gcd N M gcd K M + N
28 gcddvds M K M + N M gcd K M + N M M gcd K M + N K M + N
29 2 23 28 mp2an M gcd K M + N M M gcd K M + N K M + N
30 29 simpli M gcd K M + N M
31 gcdcl M K M + N M gcd K M + N 0
32 2 23 31 mp2an M gcd K M + N 0
33 32 nn0zi M gcd K M + N
34 znegcl K K
35 1 34 ax-mp K
36 dvds2ln K 1 M gcd K M + N M K M + N M gcd K M + N M M gcd K M + N K M + N M gcd K M + N K M + 1 K M + N
37 35 10 36 mpanl12 M gcd K M + N M K M + N M gcd K M + N M M gcd K M + N K M + N M gcd K M + N K M + 1 K M + N
38 33 2 23 37 mp3an M gcd K M + N M M gcd K M + N K M + N M gcd K M + N K M + 1 K M + N
39 29 38 ax-mp M gcd K M + N K M + 1 K M + N
40 zcn K K
41 1 40 ax-mp K
42 zcn M M
43 2 42 ax-mp M
44 41 43 mulneg1i K M = K M
45 zcn K M + N K M + N
46 23 45 ax-mp K M + N
47 46 mulid2i 1 K M + N = K M + N
48 44 47 oveq12i K M + 1 K M + N = K M + K M + N
49 41 43 mulcli K M
50 49 negcli K M
51 49 negidi K M + K M = 0
52 49 50 51 addcomli - K M + K M = 0
53 52 oveq1i K M + K M + N = 0 + N
54 50 49 16 addassi K M + K M + N = K M + K M + N
55 16 addid2i 0 + N = N
56 53 54 55 3eqtr3i K M + K M + N = N
57 48 56 eqtri K M + 1 K M + N = N
58 39 57 breqtri M gcd K M + N N
59 dvdslegcd M gcd K M + N M N ¬ M = 0 N = 0 M gcd K M + N M M gcd K M + N N M gcd K M + N M gcd N
60 59 ex M gcd K M + N M N ¬ M = 0 N = 0 M gcd K M + N M M gcd K M + N N M gcd K M + N M gcd N
61 33 2 3 60 mp3an ¬ M = 0 N = 0 M gcd K M + N M M gcd K M + N N M gcd K M + N M gcd N
62 30 58 61 mp2ani ¬ M = 0 N = 0 M gcd K M + N M gcd N
63 27 62 anim12i ¬ M = 0 K M + N = 0 ¬ M = 0 N = 0 M gcd N M gcd K M + N M gcd K M + N M gcd N
64 9 zrei M gcd N
65 33 zrei M gcd K M + N
66 64 65 letri3i M gcd N = M gcd K M + N M gcd N M gcd K M + N M gcd K M + N M gcd N
67 63 66 sylibr ¬ M = 0 K M + N = 0 ¬ M = 0 N = 0 M gcd N = M gcd K M + N
68 pm4.57 ¬ ¬ M = 0 K M + N = 0 ¬ M = 0 N = 0 M = 0 K M + N = 0 M = 0 N = 0
69 oveq2 M = 0 K M = K 0
70 41 mul01i K 0 = 0
71 69 70 eqtrdi M = 0 K M = 0
72 71 oveq1d M = 0 K M + N = 0 + N
73 72 55 eqtrdi M = 0 K M + N = N
74 73 eqeq1d M = 0 K M + N = 0 N = 0
75 74 pm5.32i M = 0 K M + N = 0 M = 0 N = 0
76 oveq12 M = 0 N = 0 M gcd N = 0 gcd 0
77 oveq12 M = 0 K M + N = 0 M gcd K M + N = 0 gcd 0
78 75 77 sylbir M = 0 N = 0 M gcd K M + N = 0 gcd 0
79 76 78 eqtr4d M = 0 N = 0 M gcd N = M gcd K M + N
80 75 79 sylbi M = 0 K M + N = 0 M gcd N = M gcd K M + N
81 80 79 jaoi M = 0 K M + N = 0 M = 0 N = 0 M gcd N = M gcd K M + N
82 68 81 sylbi ¬ ¬ M = 0 K M + N = 0 ¬ M = 0 N = 0 M gcd N = M gcd K M + N
83 67 82 pm2.61i M gcd N = M gcd K M + N