gcdaddm - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > gcdaddm		GIF version

Theorem gcdaddm 12763

Description: Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.)

**Assertion**
Ref	Expression
gcdaddm	⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀))))

**Proof of Theorem gcdaddm**
Step	Hyp	Ref	Expression
1		gcddvds 12742	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
2	1	3adant1 1046	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
3	2	simpld 112	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑀)
4		simp1 1028	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℤ)
5		1zzd 9673	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈ ℤ)
6		gcdcl 12745	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
7	6	3adant1 1046	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ₀)
8	7	nn0zd 9768	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℤ)
9		simp2 1029	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
10		simp3 1030	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
11		dvds2ln 12593	. . . . . . . . . 10 ⊢ (((𝐾 ∈ ℤ ∧ 1 ∈ ℤ) ∧ ((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁))))
12	4, 5, 8, 9, 10, 11	syl23anc 1285	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁))))
13	2, 12	mpd 13	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁)))
14	10	zcnd 9771	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℂ)
15	14	mullidd 8344	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 · 𝑁) = 𝑁)
16	15	oveq2d 6101	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + (1 · 𝑁)) = ((𝐾 · 𝑀) + 𝑁))
17	13, 16	breqtrd 4156	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁))
18	3, 17	jca 306	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)))
19	4, 9	zmulcld 9776	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℤ)
20	19, 10	zaddcld 9774	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) ∈ ℤ)
21		dvdslegcd 12743	. . . . . . . 8 ⊢ ((((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0)) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
22	21	ex 115	. . . . . . 7 ⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))))
23	8, 9, 20, 22	syl3anc 1278	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))))
24	18, 23	mpid 42	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
25		gcddvds 12742	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)))
26	9, 20, 25	syl2anc 415	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)))
27	26	simpld 112	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀)
28	4	znegcld 9772	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → -𝐾 ∈ ℤ)
29	9, 20	gcdcld 12747	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℕ₀)
30	29	nn0zd 9768	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ)
31		dvds2ln 12593	. . . . . . . . . 10 ⊢ (((-𝐾 ∈ ℤ ∧ 1 ∈ ℤ) ∧ ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ)) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁)))))
32	28, 5, 30, 9, 20, 31	syl23anc 1285	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁)))))
33	26, 32	mpd 13	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))))
34	4	zcnd 9771	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℂ)
35	9	zcnd 9771	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
36	34, 35	mulneg1d 8738	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝐾 · 𝑀) = -(𝐾 · 𝑀))
37	20	zcnd 9771	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) ∈ ℂ)
38	37	mullidd 8344	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 · ((𝐾 · 𝑀) + 𝑁)) = ((𝐾 · 𝑀) + 𝑁))
39	36, 38	oveq12d 6103	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)))
40	34, 35	mulcld 8346	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℂ)
41	40	negcld 8624	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → -(𝐾 · 𝑀) ∈ ℂ)
42	40, 41	addcomd 8477	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + -(𝐾 · 𝑀)) = (-(𝐾 · 𝑀) + (𝐾 · 𝑀)))
43	40	negidd 8627	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + -(𝐾 · 𝑀)) = 0)
44	42, 43	eqtr3d 2273	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-(𝐾 · 𝑀) + (𝐾 · 𝑀)) = 0)
45	44	oveq1d 6100	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (0 + 𝑁))
46	41, 40, 14	addassd 8348	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)))
47	14	addlidd 8476	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 + 𝑁) = 𝑁)
48	45, 46, 47	3eqtr3d 2279	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) = 𝑁)
49	39, 48	eqtrd 2271	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = 𝑁)
50	33, 49	breqtrd 4156	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁)
51	27, 50	jca 306	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁))
52		dvdslegcd 12743	. . . . . . . 8 ⊢ ((((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)))
53	52	ex 115	. . . . . . 7 ⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))))
54	30, 53	syld3an1 1324	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))))
55	51, 54	mpid 42	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)))
56	24, 55	anim12d 335	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))))
57	7	nn0red 9623	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℝ)
58	29	nn0red 9623	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℝ)
59	57, 58	letri3d 8441	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ↔ ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))))
60	56, 59	sylibrd 169	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
61		0zd 9658	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
62		zdceq 9722	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑀 = 0)
63	9, 61, 62	syl2anc 415	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 = 0)
64		zdceq 9722	. . . . . . 7 ⊢ ((((𝐾 · 𝑀) + 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → DECID ((𝐾 · 𝑀) + 𝑁) = 0)
65	20, 61, 64	syl2anc 415	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID ((𝐾 · 𝑀) + 𝑁) = 0)
66	63, 65	dcand 945	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0))
67		zdceq 9722	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
68	10, 61, 67	syl2anc 415	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
69	63, 68	dcand 945	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
70		orandc 952	. . . . 5 ⊢ ((DECID (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ DECID (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0)) ↔ ¬ (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))))
71	66, 69, 70	syl2anc 415	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0)) ↔ ¬ (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))))
72		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → 𝑀 = 0)
73	72	oveq2d 6101	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐾 · 𝑀) = (𝐾 · 0))
74	34	mul01d 8720	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 0) = 0)
75	74	adantr 276	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐾 · 0) = 0)
76	73, 75	eqtrd 2271	. . . . . . . . . 10 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐾 · 𝑀) = 0)
77	76	oveq1d 6100	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝐾 · 𝑀) + 𝑁) = (0 + 𝑁))
78	47	adantr 276	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (0 + 𝑁) = 𝑁)
79	77, 78	eqtrd 2271	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝐾 · 𝑀) + 𝑁) = 𝑁)
80	79	eqeq1d 2247	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (((𝐾 · 𝑀) + 𝑁) = 0 ↔ 𝑁 = 0))
81	80	pm5.32da 456	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ↔ (𝑀 = 0 ∧ 𝑁 = 0)))
82		oveq12 6094	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (0 gcd 0))
83	82	adantl 277	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (0 gcd 0))
84		oveq12 6094	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0))
85	81, 84	biimtrrdi 164	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0)))
86	85	imp 124	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0))
87	83, 86	eqtr4d 2274	. . . . . . 7 ⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))
88	87	ex 115	. . . . . 6 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
89	81, 88	sylbid 150	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
90	89, 88	jaod 729	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
91	71, 90	sylbird 170	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))
92		dcn 854	. . . . . 6 ⊢ (DECID (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → DECID ¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0))
93	66, 92	syl 14	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID ¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0))
94		dcn 854	. . . . . 6 ⊢ (DECID (𝑀 = 0 ∧ 𝑁 = 0) → DECID ¬ (𝑀 = 0 ∧ 𝑁 = 0))
95	69, 94	syl 14	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID ¬ (𝑀 = 0 ∧ 𝑁 = 0))
96	93, 95	dcand 945	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)))
97		exmiddc 848	. . . 4 ⊢ (DECID (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∨ ¬ (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))))
98	96, 97	syl 14	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∨ ¬ (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))))
99	60, 91, 98	mpjaod 730	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))
100	40, 14	addcomd 8477	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) = (𝑁 + (𝐾 · 𝑀)))
101	100	oveq2d 6101	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀))))
102	99, 101	eqtrd 2271	1 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀))))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 class class class wbr 4130 (class class class)co 6085 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 ≤ cle 8361 -cneg 8498 ℕ₀cn0 9565 ℤcz 9646 ∥ cdvds 12556 gcd cgcd 12732

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-sup 7324 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-n0 9566 df-z 9647 df-uz 9924 df-q 10022 df-rp 10057 df-fz 10414 df-fzo 10552 df-fl 10707 df-mod 10762 df-seqfrec 10887 df-exp 10978 df-cj 11609 df-re 11610 df-im 11611 df-rsqrt 11766 df-abs 11767 df-dvds 12557 df-gcd 12733

This theorem is used by: gcdadd 12764 gcdid 12765 modgcd 12770 gcdmultipled 12772 gcdmultiple 12799 pythagtriplem4 13049 gcdi 13201

W3C validator