Proof of Theorem gcdaddm
Step | Hyp | Ref
| Expression |
1 | | oveq1 7282 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℤ, 𝐾, 0) → (𝐾 · 𝑀) = (if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀)) |
2 | 1 | oveq1d 7290 |
. . . . 5
⊢ (𝐾 = if(𝐾 ∈ ℤ, 𝐾, 0) → ((𝐾 · 𝑀) + 𝑁) = ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁)) |
3 | 2 | oveq2d 7291 |
. . . 4
⊢ (𝐾 = if(𝐾 ∈ ℤ, 𝐾, 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (𝑀 gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁))) |
4 | 3 | eqeq2d 2749 |
. . 3
⊢ (𝐾 = if(𝐾 ∈ ℤ, 𝐾, 0) → ((𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ↔ (𝑀 gcd 𝑁) = (𝑀 gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁)))) |
5 | | oveq1 7282 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → (𝑀 gcd 𝑁) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd 𝑁)) |
6 | | id 22 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → 𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0)) |
7 | | oveq2 7283 |
. . . . . 6
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → (if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) = (if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0))) |
8 | 7 | oveq1d 7290 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁) = ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁)) |
9 | 6, 8 | oveq12d 7293 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → (𝑀 gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁)) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁))) |
10 | 5, 9 | eqeq12d 2754 |
. . 3
⊢ (𝑀 = if(𝑀 ∈ ℤ, 𝑀, 0) → ((𝑀 gcd 𝑁) = (𝑀 gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · 𝑀) + 𝑁)) ↔ (if(𝑀 ∈ ℤ, 𝑀, 0) gcd 𝑁) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁)))) |
11 | | oveq2 7283 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℤ, 𝑁, 0) → (if(𝑀 ∈ ℤ, 𝑀, 0) gcd 𝑁) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd if(𝑁 ∈ ℤ, 𝑁, 0))) |
12 | | oveq2 7283 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℤ, 𝑁, 0) → ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁) = ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + if(𝑁 ∈ ℤ, 𝑁, 0))) |
13 | 12 | oveq2d 7291 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℤ, 𝑁, 0) → (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁)) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + if(𝑁 ∈ ℤ, 𝑁, 0)))) |
14 | 11, 13 | eqeq12d 2754 |
. . 3
⊢ (𝑁 = if(𝑁 ∈ ℤ, 𝑁, 0) → ((if(𝑀 ∈ ℤ, 𝑀, 0) gcd 𝑁) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + 𝑁)) ↔ (if(𝑀 ∈ ℤ, 𝑀, 0) gcd if(𝑁 ∈ ℤ, 𝑁, 0)) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + if(𝑁 ∈ ℤ, 𝑁, 0))))) |
15 | | 0z 12330 |
. . . . 5
⊢ 0 ∈
ℤ |
16 | 15 | elimel 4528 |
. . . 4
⊢ if(𝐾 ∈ ℤ, 𝐾, 0) ∈
ℤ |
17 | 15 | elimel 4528 |
. . . 4
⊢ if(𝑀 ∈ ℤ, 𝑀, 0) ∈
ℤ |
18 | 15 | elimel 4528 |
. . . 4
⊢ if(𝑁 ∈ ℤ, 𝑁, 0) ∈
ℤ |
19 | 16, 17, 18 | gcdaddmlem 16231 |
. . 3
⊢ (if(𝑀 ∈ ℤ, 𝑀, 0) gcd if(𝑁 ∈ ℤ, 𝑁, 0)) = (if(𝑀 ∈ ℤ, 𝑀, 0) gcd ((if(𝐾 ∈ ℤ, 𝐾, 0) · if(𝑀 ∈ ℤ, 𝑀, 0)) + if(𝑁 ∈ ℤ, 𝑁, 0))) |
20 | 4, 10, 14, 19 | dedth3h 4519 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
21 | | zcn 12324 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
22 | | zcn 12324 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
23 | | mulcl 10955 |
. . . . . 6
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 · 𝑀) ∈ ℂ) |
24 | 21, 22, 23 | syl2an 596 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℂ) |
25 | | zcn 12324 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
26 | | addcom 11161 |
. . . . 5
⊢ (((𝐾 · 𝑀) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 · 𝑀) + 𝑁) = (𝑁 + (𝐾 · 𝑀))) |
27 | 24, 25, 26 | syl2an 596 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) = (𝑁 + (𝐾 · 𝑀))) |
28 | 27 | 3impa 1109 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) = (𝑁 + (𝐾 · 𝑀))) |
29 | 28 | oveq2d 7291 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))) |
30 | 20, 29 | eqtrd 2778 |
1
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))) |