Step | Hyp | Ref
| Expression |
1 | | bezoutlemzz 11957 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
2 | 1 | ancoms 266 |
. . 3
⊢ ((𝐵 ∈ ℕ0
∧ 𝐴 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
3 | 2 | adantll 473 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ 𝐴 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
4 | | bezoutlemzz 11957 |
. . . . 5
⊢ ((-𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑡 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)))) |
5 | 4 | ancoms 266 |
. . . 4
⊢ ((𝐵 ∈ ℕ0
∧ -𝐴 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑡 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)))) |
6 | 5 | adantll 473 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑡 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)))) |
7 | | simpr 109 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ 𝑧 ∈
ℤ) |
8 | | simpll 524 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) → 𝐴 ∈ ℤ) |
9 | 8 | ad2antrr 485 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
10 | | dvdsnegb 11770 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑧 ∥ 𝐴 ↔ 𝑧 ∥ -𝐴)) |
11 | 7, 9, 10 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ (𝑧 ∥ 𝐴 ↔ 𝑧 ∥ -𝐴)) |
12 | 11 | biimprd 157 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ (𝑧 ∥ -𝐴 → 𝑧 ∥ 𝐴)) |
13 | 12 | anim1d 334 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ ((𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵) → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) |
14 | 13 | imim2d 54 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑧 ∈ ℤ)
→ ((𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) → (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))) |
15 | 14 | ralimdva 2537 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) ∧ 𝑑 ∈ ℕ0) →
(∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))) |
16 | 8 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
17 | 16 | zcnd 9335 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ 𝐴 ∈
ℂ) |
18 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ 𝑡 ∈
ℤ) |
19 | 18 | zcnd 9335 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ 𝑡 ∈
ℂ) |
20 | | mulneg12 8316 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (-𝐴 · 𝑡) = (𝐴 · -𝑡)) |
21 | 17, 19, 20 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ (-𝐴 · 𝑡) = (𝐴 · -𝑡)) |
22 | 21 | oveq1d 5868 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ ((-𝐴 · 𝑡) + (𝐵 · 𝑦)) = ((𝐴 · -𝑡) + (𝐵 · 𝑦))) |
23 | 22 | eqeq2d 2182 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ (𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)) ↔ 𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)))) |
24 | 23 | rexbidv 2471 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ (∃𝑦 ∈
ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)))) |
25 | | znegcl 9243 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℤ → -𝑡 ∈
ℤ) |
26 | | oveq2 5861 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = -𝑡 → (𝐴 · 𝑥) = (𝐴 · -𝑡)) |
27 | 26 | oveq1d 5868 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -𝑡 → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · -𝑡) + (𝐵 · 𝑦))) |
28 | 27 | eqeq2d 2182 |
. . . . . . . . . . . 12
⊢ (𝑥 = -𝑡 → (𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)))) |
29 | 28 | rexbidv 2471 |
. . . . . . . . . . 11
⊢ (𝑥 = -𝑡 → (∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)))) |
30 | 29 | rspcev 2834 |
. . . . . . . . . 10
⊢ ((-𝑡 ∈ ℤ ∧
∃𝑦 ∈ ℤ
𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) |
31 | 25, 30 | sylan 281 |
. . . . . . . . 9
⊢ ((𝑡 ∈ ℤ ∧
∃𝑦 ∈ ℤ
𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) |
32 | 31 | ex 114 |
. . . . . . . 8
⊢ (𝑡 ∈ ℤ →
(∃𝑦 ∈ ℤ
𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
33 | 32 | adantl 275 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ (∃𝑦 ∈
ℤ 𝑑 = ((𝐴 · -𝑡) + (𝐵 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
34 | 24, 33 | sylbid 149 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℕ0) ∧ -𝐴 ∈ ℕ0) ∧ 𝑑 ∈ ℕ0)
∧ 𝑡 ∈ ℤ)
→ (∃𝑦 ∈
ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
35 | 34 | rexlimdva 2587 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) ∧ 𝑑 ∈ ℕ0) →
(∃𝑡 ∈ ℤ
∃𝑦 ∈ ℤ
𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
36 | 15, 35 | anim12d 333 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) ∧ 𝑑 ∈ ℕ0) →
((∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑡 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦))) → (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))) |
37 | 36 | reximdva 2572 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) → (∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ -𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑡 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((-𝐴 · 𝑡) + (𝐵 · 𝑦))) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))) |
38 | 6, 37 | mpd 13 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
∧ -𝐴 ∈
ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |
39 | | elznn0 9227 |
. . . 4
⊢ (𝐴 ∈ ℤ ↔ (𝐴 ∈ ℝ ∧ (𝐴 ∈ ℕ0 ∨
-𝐴 ∈
ℕ0))) |
40 | 39 | simprbi 273 |
. . 3
⊢ (𝐴 ∈ ℤ → (𝐴 ∈ ℕ0 ∨
-𝐴 ∈
ℕ0)) |
41 | 40 | adantr 274 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
→ (𝐴 ∈
ℕ0 ∨ -𝐴
∈ ℕ0)) |
42 | 3, 38, 41 | mpjaodan 793 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0)
→ ∃𝑑 ∈
ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) |