Proof of Theorem dfgcd3
Step | Hyp | Ref
| Expression |
1 | | gcdcl 16209 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
2 | | simplr 766 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 ∈ ℕ0) |
3 | 2 | nn0zd 12421 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 ∈ ℤ) |
4 | | iddvds 15975 |
. . . . . . . 8
⊢ (𝑑 ∈ ℤ → 𝑑 ∥ 𝑑) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 ∥ 𝑑) |
6 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
7 | | breq1 5082 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑑 → (𝑧 ∥ 𝑑 ↔ 𝑑 ∥ 𝑑)) |
8 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑑 → (𝑧 ∥ 𝑀 ↔ 𝑑 ∥ 𝑀)) |
9 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑑 → (𝑧 ∥ 𝑁 ↔ 𝑑 ∥ 𝑁)) |
10 | 8, 9 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑑 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁))) |
11 | 7, 10 | bibi12d 346 |
. . . . . . . . 9
⊢ (𝑧 = 𝑑 → ((𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ (𝑑 ∥ 𝑑 ↔ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁)))) |
12 | 11 | rspcv 3556 |
. . . . . . . 8
⊢ (𝑑 ∈ ℤ →
(∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → (𝑑 ∥ 𝑑 ↔ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁)))) |
13 | 3, 6, 12 | sylc 65 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (𝑑 ∥ 𝑑 ↔ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁))) |
14 | 5, 13 | mpbid 231 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁)) |
15 | | biimpr 219 |
. . . . . . . 8
⊢ ((𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)) |
16 | 15 | ralimi 3089 |
. . . . . . 7
⊢
(∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)) |
17 | 6, 16 | syl 17 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)) |
18 | | dfgcd2 16250 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑑 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝑑 ∧ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)))) |
19 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (𝑑 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝑑 ∧ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)))) |
20 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ 𝑑 ∈
ℕ0) |
21 | 20 | nn0ge0d 12294 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ 0 ≤ 𝑑) |
22 | 21 | 3biant1d 1477 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (((𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)) ↔ (0 ≤ 𝑑 ∧ (𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)))) |
23 | 19, 22 | bitr4d 281 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (𝑑 = (𝑀 gcd 𝑁) ↔ ((𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)))) |
24 | 23 | adantr 481 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (𝑑 = (𝑀 gcd 𝑁) ↔ ((𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁) ∧ ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) → 𝑧 ∥ 𝑑)))) |
25 | 14, 17, 24 | mpbir2and 710 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 = (𝑀 gcd 𝑁)) |
26 | 25 | ex 413 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → 𝑑 = (𝑀 gcd 𝑁))) |
27 | | dvdsgcdb 16249 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ 𝑧 ∥ (𝑀 gcd 𝑁))) |
28 | 27 | bicomd 222 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑧 ∥ (𝑀 gcd 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
29 | 28 | 3coml 1126 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ (𝑀 gcd 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
30 | 29 | ad4ant124 1172 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 = (𝑀 gcd 𝑁)) ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ (𝑀 gcd 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
31 | | breq2 5083 |
. . . . . . . . . 10
⊢ (𝑑 = (𝑀 gcd 𝑁) → (𝑧 ∥ 𝑑 ↔ 𝑧 ∥ (𝑀 gcd 𝑁))) |
32 | 31 | bibi1d 344 |
. . . . . . . . 9
⊢ (𝑑 = (𝑀 gcd 𝑁) → ((𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ (𝑧 ∥ (𝑀 gcd 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
33 | 32 | ad2antlr 724 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 = (𝑀 gcd 𝑁)) ∧ 𝑧 ∈ ℤ) → ((𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ (𝑧 ∥ (𝑀 gcd 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
34 | 30, 33 | mpbird 256 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 = (𝑀 gcd 𝑁)) ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
35 | 34 | ralrimiva 3110 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 = (𝑀 gcd 𝑁)) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
36 | 35 | ex 413 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑑 = (𝑀 gcd 𝑁) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
37 | 36 | adantr 481 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (𝑑 = (𝑀 gcd 𝑁) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
38 | 26, 37 | impbid 211 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑑 ∈ ℕ0)
→ (∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ 𝑑 = (𝑀 gcd 𝑁))) |
39 | 1, 38 | riota5 7256 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(℩𝑑 ∈
ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) = (𝑀 gcd 𝑁)) |
40 | 39 | eqcomd 2746 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |