Proof of Theorem bezoutlem2
Step | Hyp | Ref
| Expression |
1 | | bezout.2 |
. 2
⊢ 𝐺 = inf(𝑀, ℝ, < ) |
2 | | bezout.1 |
. . . . 5
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} |
3 | | ssrab2 3650 |
. . . . 5
⊢ {𝑧 ∈ ℕ ∣
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} ⊆ ℕ |
4 | 2, 3 | eqsstri 3598 |
. . . 4
⊢ 𝑀 ⊆
ℕ |
5 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
6 | 4, 5 | sseqtri 3600 |
. . 3
⊢ 𝑀 ⊆
(ℤ≥‘1) |
7 | | bezout.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) |
8 | | bezout.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℤ) |
9 | 2, 7, 8 | bezoutlem1 15094 |
. . . . 5
⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) |
10 | | ne0i 3880 |
. . . . 5
⊢
((abs‘𝐴)
∈ 𝑀 → 𝑀 ≠ ∅) |
11 | 9, 10 | syl6 34 |
. . . 4
⊢ (𝜑 → (𝐴 ≠ 0 → 𝑀 ≠ ∅)) |
12 | | eqid 2610 |
. . . . . . 7
⊢ {𝑧 ∈ ℕ ∣
∃𝑦 ∈ ℤ
∃𝑥 ∈ ℤ
𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} |
13 | 12, 8, 7 | bezoutlem1 15094 |
. . . . . 6
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
14 | | rexcom 3080 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) |
15 | 7 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐴 ∈ ℂ) |
17 | | zcn 11259 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
18 | 17 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑥 ∈ ℂ) |
19 | 16, 18 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐴 · 𝑥) ∈ ℂ) |
20 | 8 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ℂ) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐵 ∈ ℂ) |
22 | | zcn 11259 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
23 | 22 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑦 ∈ ℂ) |
24 | 21, 23 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℂ) |
25 | 19, 24 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐵 · 𝑦) + (𝐴 · 𝑥))) |
26 | 25 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
27 | 26 | 2rexbidva 3038 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
28 | 14, 27 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
29 | 28 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝜑 → {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
30 | 2, 29 | syl5eq 2656 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
31 | 30 | eleq2d 2673 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐵) ∈ 𝑀 ↔ (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
32 | 13, 31 | sylibrd 248 |
. . . . 5
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ 𝑀)) |
33 | | ne0i 3880 |
. . . . 5
⊢
((abs‘𝐵)
∈ 𝑀 → 𝑀 ≠ ∅) |
34 | 32, 33 | syl6 34 |
. . . 4
⊢ (𝜑 → (𝐵 ≠ 0 → 𝑀 ≠ ∅)) |
35 | | bezout.5 |
. . . . 5
⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
36 | | neorian 2876 |
. . . . 5
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
37 | 35, 36 | sylibr 223 |
. . . 4
⊢ (𝜑 → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) |
38 | 11, 34, 37 | mpjaod 395 |
. . 3
⊢ (𝜑 → 𝑀 ≠ ∅) |
39 | | infssuzcl 11648 |
. . 3
⊢ ((𝑀 ⊆
(ℤ≥‘1) ∧ 𝑀 ≠ ∅) → inf(𝑀, ℝ, < ) ∈ 𝑀) |
40 | 6, 38, 39 | sylancr 694 |
. 2
⊢ (𝜑 → inf(𝑀, ℝ, < ) ∈ 𝑀) |
41 | 1, 40 | syl5eqel 2692 |
1
⊢ (𝜑 → 𝐺 ∈ 𝑀) |