Proof of Theorem bezoutlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bezout.3 | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 2 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑧 = 𝐴 → (abs‘𝑧) = (abs‘𝐴)) | 
| 3 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑧 = 𝐴 → (𝑧 · 𝑥) = (𝐴 · 𝑥)) | 
| 4 | 2, 3 | eqeq12d 2753 | . . . . . 6
⊢ (𝑧 = 𝐴 → ((abs‘𝑧) = (𝑧 · 𝑥) ↔ (abs‘𝐴) = (𝐴 · 𝑥))) | 
| 5 | 4 | rexbidv 3179 | . . . . 5
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ ℤ (abs‘𝑧) = (𝑧 · 𝑥) ↔ ∃𝑥 ∈ ℤ (abs‘𝐴) = (𝐴 · 𝑥))) | 
| 6 |  | zre 12617 | . . . . . 6
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) | 
| 7 |  | 1z 12647 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 8 |  | ax-1rid 11225 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (𝑧 · 1) = 𝑧) | 
| 9 | 8 | eqcomd 2743 | . . . . . . . . 9
⊢ (𝑧 ∈ ℝ → 𝑧 = (𝑧 · 1)) | 
| 10 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑧 · 𝑥) = (𝑧 · 1)) | 
| 11 | 10 | rspceeqv 3645 | . . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝑧 =
(𝑧 · 1)) →
∃𝑥 ∈ ℤ
𝑧 = (𝑧 · 𝑥)) | 
| 12 | 7, 9, 11 | sylancr 587 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ →
∃𝑥 ∈ ℤ
𝑧 = (𝑧 · 𝑥)) | 
| 13 |  | eqeq1 2741 | . . . . . . . . 9
⊢
((abs‘𝑧) =
𝑧 → ((abs‘𝑧) = (𝑧 · 𝑥) ↔ 𝑧 = (𝑧 · 𝑥))) | 
| 14 | 13 | rexbidv 3179 | . . . . . . . 8
⊢
((abs‘𝑧) =
𝑧 → (∃𝑥 ∈ ℤ (abs‘𝑧) = (𝑧 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑧 = (𝑧 · 𝑥))) | 
| 15 | 12, 14 | syl5ibrcom 247 | . . . . . . 7
⊢ (𝑧 ∈ ℝ →
((abs‘𝑧) = 𝑧 → ∃𝑥 ∈ ℤ (abs‘𝑧) = (𝑧 · 𝑥))) | 
| 16 |  | neg1z 12653 | . . . . . . . . 9
⊢ -1 ∈
ℤ | 
| 17 |  | recn 11245 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) | 
| 18 | 17 | mulm1d 11715 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (-1
· 𝑧) = -𝑧) | 
| 19 |  | neg1cn 12380 | . . . . . . . . . . 11
⊢ -1 ∈
ℂ | 
| 20 |  | mulcom 11241 | . . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ 𝑧
∈ ℂ) → (-1 · 𝑧) = (𝑧 · -1)) | 
| 21 | 19, 17, 20 | sylancr 587 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (-1
· 𝑧) = (𝑧 · -1)) | 
| 22 | 18, 21 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝑧 ∈ ℝ → -𝑧 = (𝑧 · -1)) | 
| 23 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑥 = -1 → (𝑧 · 𝑥) = (𝑧 · -1)) | 
| 24 | 23 | rspceeqv 3645 | . . . . . . . . 9
⊢ ((-1
∈ ℤ ∧ -𝑧 =
(𝑧 · -1)) →
∃𝑥 ∈ ℤ
-𝑧 = (𝑧 · 𝑥)) | 
| 25 | 16, 22, 24 | sylancr 587 | . . . . . . . 8
⊢ (𝑧 ∈ ℝ →
∃𝑥 ∈ ℤ
-𝑧 = (𝑧 · 𝑥)) | 
| 26 |  | eqeq1 2741 | . . . . . . . . 9
⊢
((abs‘𝑧) =
-𝑧 → ((abs‘𝑧) = (𝑧 · 𝑥) ↔ -𝑧 = (𝑧 · 𝑥))) | 
| 27 | 26 | rexbidv 3179 | . . . . . . . 8
⊢
((abs‘𝑧) =
-𝑧 → (∃𝑥 ∈ ℤ (abs‘𝑧) = (𝑧 · 𝑥) ↔ ∃𝑥 ∈ ℤ -𝑧 = (𝑧 · 𝑥))) | 
| 28 | 25, 27 | syl5ibrcom 247 | . . . . . . 7
⊢ (𝑧 ∈ ℝ →
((abs‘𝑧) = -𝑧 → ∃𝑥 ∈ ℤ (abs‘𝑧) = (𝑧 · 𝑥))) | 
| 29 |  | absor 15339 | . . . . . . 7
⊢ (𝑧 ∈ ℝ →
((abs‘𝑧) = 𝑧 ∨ (abs‘𝑧) = -𝑧)) | 
| 30 | 15, 28, 29 | mpjaod 861 | . . . . . 6
⊢ (𝑧 ∈ ℝ →
∃𝑥 ∈ ℤ
(abs‘𝑧) = (𝑧 · 𝑥)) | 
| 31 | 6, 30 | syl 17 | . . . . 5
⊢ (𝑧 ∈ ℤ →
∃𝑥 ∈ ℤ
(abs‘𝑧) = (𝑧 · 𝑥)) | 
| 32 | 5, 31 | vtoclga 3577 | . . . 4
⊢ (𝐴 ∈ ℤ →
∃𝑥 ∈ ℤ
(abs‘𝐴) = (𝐴 · 𝑥)) | 
| 33 | 1, 32 | syl 17 | . . 3
⊢ (𝜑 → ∃𝑥 ∈ ℤ (abs‘𝐴) = (𝐴 · 𝑥)) | 
| 34 |  | bezout.4 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 35 | 34 | zcnd 12723 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐵 ∈ ℂ) | 
| 37 | 36 | mul01d 11460 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝐵 · 0) = 0) | 
| 38 | 37 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝐴 · 𝑥) + (𝐵 · 0)) = ((𝐴 · 𝑥) + 0)) | 
| 39 | 1 | zcnd 12723 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 40 |  | zcn 12618 | . . . . . . . . 9
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) | 
| 41 |  | mulcl 11239 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) | 
| 42 | 39, 40, 41 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝐴 · 𝑥) ∈ ℂ) | 
| 43 | 42 | addridd 11461 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝐴 · 𝑥) + 0) = (𝐴 · 𝑥)) | 
| 44 | 38, 43 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝐴 · 𝑥) + (𝐵 · 0)) = (𝐴 · 𝑥)) | 
| 45 | 44 | eqeq2d 2748 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 0)) ↔ (abs‘𝐴) = (𝐴 · 𝑥))) | 
| 46 |  | 0z 12624 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 47 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑦 = 0 → (𝐵 · 𝑦) = (𝐵 · 0)) | 
| 48 | 47 | oveq2d 7447 | . . . . . . 7
⊢ (𝑦 = 0 → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · 𝑥) + (𝐵 · 0))) | 
| 49 | 48 | rspceeqv 3645 | . . . . . 6
⊢ ((0
∈ ℤ ∧ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 0))) → ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | 
| 50 | 46, 49 | mpan 690 | . . . . 5
⊢
((abs‘𝐴) =
((𝐴 · 𝑥) + (𝐵 · 0)) → ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | 
| 51 | 45, 50 | biimtrrdi 254 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((abs‘𝐴) = (𝐴 · 𝑥) → ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | 
| 52 | 51 | reximdva 3168 | . . 3
⊢ (𝜑 → (∃𝑥 ∈ ℤ (abs‘𝐴) = (𝐴 · 𝑥) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | 
| 53 | 33, 52 | mpd 15 | . 2
⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | 
| 54 |  | nnabscl 15364 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℕ) | 
| 55 | 54 | ex 412 | . . 3
⊢ (𝐴 ∈ ℤ → (𝐴 ≠ 0 → (abs‘𝐴) ∈
ℕ)) | 
| 56 | 1, 55 | syl 17 | . 2
⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ ℕ)) | 
| 57 |  | eqeq1 2741 | . . . . 5
⊢ (𝑧 = (abs‘𝐴) → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | 
| 58 | 57 | 2rexbidv 3222 | . . . 4
⊢ (𝑧 = (abs‘𝐴) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | 
| 59 |  | bezout.1 | . . . 4
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} | 
| 60 | 58, 59 | elrab2 3695 | . . 3
⊢
((abs‘𝐴)
∈ 𝑀 ↔
((abs‘𝐴) ∈
ℕ ∧ ∃𝑥
∈ ℤ ∃𝑦
∈ ℤ (abs‘𝐴) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | 
| 61 | 60 | simplbi2com 502 | . 2
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ (abs‘𝐴) =
((𝐴 · 𝑥) + (𝐵 · 𝑦)) → ((abs‘𝐴) ∈ ℕ → (abs‘𝐴) ∈ 𝑀)) | 
| 62 | 53, 56, 61 | sylsyld 61 | 1
⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) |