Theorem gcdaddmlem

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

	Ref	Expression
Hypotheses	gcdaddmlem.1	⊢ 𝐾 ∈ ℤ
	gcdaddmlem.2	⊢ 𝑀 ∈ ℤ
	gcdaddmlem.3	⊢ 𝑁 ∈ ℤ
Assertion	gcdaddmlem	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) )

Proof

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