Step | Hyp | Ref
| Expression |
1 | | gcdcl 15228 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
2 | 1 | nn0ge0d 11354 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ≤
(𝑀 gcd 𝑁)) |
3 | | gcddvds 15225 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
4 | | 3anass 1042 |
. . . . . . . 8
⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ))) |
5 | | ancom 466 |
. . . . . . . 8
⊢ ((𝑒 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈
ℤ)) |
6 | 4, 5 | bitri 264 |
. . . . . . 7
⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈
ℤ)) |
7 | | dvdsgcd 15261 |
. . . . . . 7
⊢ ((𝑒 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))) |
8 | 6, 7 | sylbir 225 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑒 ∈ ℤ) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))) |
9 | 8 | ralrimiva 2966 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∀𝑒 ∈ ℤ
((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))) |
10 | 2, 3, 9 | 3jca 1242 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤
(𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))) |
11 | 10 | adantr 481 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))) |
12 | | breq2 4657 |
. . . . 5
⊢ (𝐷 = (𝑀 gcd 𝑁) → (0 ≤ 𝐷 ↔ 0 ≤ (𝑀 gcd 𝑁))) |
13 | | breq1 4656 |
. . . . . 6
⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀)) |
14 | | breq1 4656 |
. . . . . 6
⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝐷 ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁)) |
15 | 13, 14 | anbi12d 747 |
. . . . 5
⊢ (𝐷 = (𝑀 gcd 𝑁) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))) |
16 | | breq2 4657 |
. . . . . . 7
⊢ (𝐷 = (𝑀 gcd 𝑁) → (𝑒 ∥ 𝐷 ↔ 𝑒 ∥ (𝑀 gcd 𝑁))) |
17 | 16 | imbi2d 330 |
. . . . . 6
⊢ (𝐷 = (𝑀 gcd 𝑁) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))) |
18 | 17 | ralbidv 2986 |
. . . . 5
⊢ (𝐷 = (𝑀 gcd 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁)))) |
19 | 12, 15, 18 | 3anbi123d 1399 |
. . . 4
⊢ (𝐷 = (𝑀 gcd 𝑁) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))) |
20 | 19 | adantl 482 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ (𝑀 gcd 𝑁) ∧ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ (𝑀 gcd 𝑁))))) |
21 | 11, 20 | mpbird 247 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐷 = (𝑀 gcd 𝑁)) → (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) |
22 | | gcdval 15218 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))) |
23 | 22 | adantr 481 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))) |
24 | | iftrue 4092 |
. . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0) |
25 | 24 | adantr 481 |
. . . . 5
⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 0) |
26 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐷 ∥ 𝑀 ↔ 𝐷 ∥ 0)) |
27 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (𝐷 ∥ 𝑁 ↔ 𝐷 ∥ 0)) |
28 | 26, 27 | bi2anan9 917 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0))) |
29 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝑒 ∥ 𝑀 ↔ 𝑒 ∥ 0)) |
30 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑒 ∥ 𝑁 ↔ 𝑒 ∥ 0)) |
31 | 29, 30 | bi2anan9 917 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑒 ∥ 0 ∧ 𝑒 ∥ 0))) |
32 | 31 | imbi1d 331 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))) |
33 | 32 | ralbidv 2986 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷))) |
34 | 28, 33 | 3anbi23d 1402 |
. . . . . . . 8
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)))) |
35 | | dvdszrcl 14988 |
. . . . . . . . . . . 12
⊢ (𝐷 ∥ 0 → (𝐷 ∈ ℤ ∧ 0 ∈
ℤ)) |
36 | | dvds0 14997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ ℤ → 𝑒 ∥ 0) |
37 | 36, 36 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ ℤ → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ ℤ ∧ 0 ≤
𝐷) ∧ 𝑒 ∈ ℤ) → (𝑒 ∥ 0 ∧ 𝑒 ∥ 0)) |
39 | | pm5.5 351 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ ℤ ∧ 0 ≤
𝐷) ∧ 𝑒 ∈ ℤ) → (((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ 𝑒 ∥ 𝐷)) |
41 | 40 | ralbidva 2985 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℤ ∧ 0 ≤
𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) ↔ ∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷)) |
42 | | 0z 11388 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ |
43 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 0 → (𝑒 ∥ 𝐷 ↔ 0 ∥ 𝐷)) |
44 | 43 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℤ → (∀𝑒
∈ ℤ 𝑒 ∥
𝐷 → 0 ∥ 𝐷)) |
45 | 42, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑒 ∈
ℤ 𝑒 ∥ 𝐷 → 0 ∥ 𝐷) |
46 | | 0dvds 15002 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ ℤ → (0
∥ 𝐷 ↔ 𝐷 = 0)) |
47 | 46 | biimpd 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ ℤ → (0
∥ 𝐷 → 𝐷 = 0)) |
48 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 =
𝐷 ↔ 𝐷 = 0) |
49 | 47, 48 | syl6ibr 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ ℤ → (0
∥ 𝐷 → 0 = 𝐷)) |
50 | 45, 49 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ ℤ →
(∀𝑒 ∈ ℤ
𝑒 ∥ 𝐷 → 0 = 𝐷)) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℤ ∧ 0 ≤
𝐷) → (∀𝑒 ∈ ℤ 𝑒 ∥ 𝐷 → 0 = 𝐷)) |
52 | 41, 51 | sylbid 230 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ ℤ ∧ 0 ≤
𝐷) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷)) |
53 | 52 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ ℤ → (0 ≤
𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))) |
54 | 53 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ ℤ ∧ 0 ∈
ℤ) → (0 ≤ 𝐷
→ (∀𝑒 ∈
ℤ ((𝑒 ∥ 0 ∧
𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))) |
55 | 35, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐷 ∥ 0 → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))) |
56 | 55 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) → (0 ≤ 𝐷 → (∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))) |
57 | 56 | com12 32 |
. . . . . . . . 9
⊢ (0 ≤
𝐷 → ((𝐷 ∥ 0 ∧ 𝐷 ∥ 0) →
(∀𝑒 ∈ ℤ
((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷) → 0 = 𝐷))) |
58 | 57 | 3imp 1256 |
. . . . . . . 8
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 0 ∧ 𝐷 ∥ 0) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 0 ∧ 𝑒 ∥ 0) → 𝑒 ∥ 𝐷)) → 0 = 𝐷) |
59 | 34, 58 | syl6bi 243 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 0 = 𝐷)) |
60 | 59 | adantld 483 |
. . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 0 = 𝐷)) |
61 | 60 | imp 445 |
. . . . 5
⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 0 = 𝐷) |
62 | 25, 61 | eqtrd 2656 |
. . . 4
⊢ (((𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷) |
63 | | iffalse 4095 |
. . . . . 6
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
64 | 63 | adantr 481 |
. . . . 5
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
65 | | ltso 10118 |
. . . . . . 7
⊢ < Or
ℝ |
66 | 65 | a1i 11 |
. . . . . 6
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → < Or
ℝ) |
67 | | dvdszrcl 14988 |
. . . . . . . . . . 11
⊢ (𝐷 ∥ 𝑀 → (𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ)) |
68 | 67 | simpld 475 |
. . . . . . . . . 10
⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℤ) |
69 | 68 | zred 11482 |
. . . . . . . . 9
⊢ (𝐷 ∥ 𝑀 → 𝐷 ∈ ℝ) |
70 | 69 | adantr 481 |
. . . . . . . 8
⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℝ) |
71 | 70 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → 𝐷 ∈ ℝ) |
72 | 71 | ad2antll 765 |
. . . . . 6
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → 𝐷 ∈ ℝ) |
73 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀)) |
74 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (𝑛 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁)) |
75 | 73, 74 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑛 = 𝑦 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁))) |
76 | 75 | elrab 3363 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁))) |
77 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑀 ↔ 𝑦 ∥ 𝑀)) |
78 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁)) |
79 | 77, 78 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑦 → ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) ↔ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁))) |
80 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑦 → (𝑒 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷)) |
81 | 79, 80 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑦 → (((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) ↔ ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷))) |
82 | 81 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℤ →
(∀𝑒 ∈ ℤ
((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → 𝑦 ∥ 𝐷))) |
83 | 82 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℤ → ((𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷))) |
84 | 83 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)) |
85 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → 𝑦 ∥ 𝐷)) |
86 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ∈ ℕ0
↔ (𝐷 ∈ ℤ
∧ 0 ≤ 𝐷)) |
87 | 86 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈ ℤ → (0 ≤
𝐷 → 𝐷 ∈
ℕ0)) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 ≤
𝐷 → 𝐷 ∈
ℕ0)) |
89 | 67, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∥ 𝑀 → (0 ≤ 𝐷 → 𝐷 ∈
ℕ0)) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (0 ≤ 𝐷 → 𝐷 ∈
ℕ0)) |
91 | 90 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈
ℕ0) |
92 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑦 ∈
ℤ ∧ (𝑦 ∥
𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝑦 ∈ ℤ) |
93 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐷 ∈ ℕ0
↔ (𝐷 ∈ ℕ
∨ 𝐷 =
0)) |
94 | | 2a1 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐷 ∈ ℕ → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))) |
95 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐷 = 0 → (𝐷 ∥ 𝑀 ↔ 0 ∥ 𝑀)) |
96 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐷 = 0 → (𝐷 ∥ 𝑁 ↔ 0 ∥ 𝑁)) |
97 | 95, 96 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐷 = 0 → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))) |
98 | 97 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐷 = 0 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ↔ (0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))) |
100 | | ianor 509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∨ ¬ 𝑁 = 0)) |
101 | | dvdszrcl 14988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (0
∥ 𝑀 → (0 ∈
ℤ ∧ 𝑀 ∈
ℤ)) |
102 | | 0dvds 15002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑀 ∈ ℤ → (0
∥ 𝑀 ↔ 𝑀 = 0)) |
103 | | pm2.24 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑀 = 0 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)) |
104 | 102, 103 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑀 ∈ ℤ → (0
∥ 𝑀 → (¬
𝑀 = 0 → 𝐷 ∈
ℕ))) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((0
∈ ℤ ∧ 𝑀
∈ ℤ) → (0 ∥ 𝑀 → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ))) |
106 | 101, 105 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (0
∥ 𝑀 → (¬
𝑀 = 0 → 𝐷 ∈
ℕ)) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((0
∥ 𝑀 ∧ 0 ∥
𝑁) → (¬ 𝑀 = 0 → 𝐷 ∈ ℕ)) |
108 | 107 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (¬
𝑀 = 0 → ((0 ∥
𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ)) |
109 | | dvdszrcl 14988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (0
∥ 𝑁 → (0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) |
110 | | 0dvds 15002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) |
111 | | pm2.24 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑁 = 0 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)) |
112 | 110, 111 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 → (¬
𝑁 = 0 → 𝐷 ∈
ℕ))) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 ∥ 𝑁 → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ))) |
114 | 109, 113 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (0
∥ 𝑁 → (¬
𝑁 = 0 → 𝐷 ∈
ℕ)) |
115 | 114 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((0
∥ 𝑀 ∧ 0 ∥
𝑁) → (¬ 𝑁 = 0 → 𝐷 ∈ ℕ)) |
116 | 115 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (¬
𝑁 = 0 → ((0 ∥
𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ)) |
117 | 108, 116 | jaoi 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((¬
𝑀 = 0 ∨ ¬ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ)) |
118 | 100, 117 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → ((0 ∥ 𝑀 ∧ 0 ∥ 𝑁) → 𝐷 ∈ ℕ)) |
119 | 118 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ)) |
120 | 119 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) → 𝐷 ∈ ℕ)) |
121 | 99, 120 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐷 = 0 ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)) |
122 | 121 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐷 = 0 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))) |
123 | 94, 122 | jaoi 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐷 ∈ ℕ ∨ 𝐷 = 0) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))) |
124 | 93, 123 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐷 ∈ ℕ0
→ (((𝑦 ∈ ℤ
∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ))) |
125 | 124 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) → ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → 𝐷 ∈ ℕ)) |
126 | 125 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑦 ∈
ℤ ∧ (𝑦 ∥
𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → 𝐷 ∈ ℕ) |
127 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷)) |
128 | 92, 126, 127 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑦 ∈
ℤ ∧ (𝑦 ∥
𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝐷 ∈ ℕ0) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷)) |
129 | 128 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝐷 ∈ ℕ0 → ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷)))) |
130 | 129 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∥ 𝐷 → (𝐷 ∈ ℕ0 → ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷)))) |
131 | 130 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0) → ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷))) |
132 | 131 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0)) →
(((𝑦 ∈ ℤ ∧
(𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ≤ 𝐷)) |
133 | 132 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((0
≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → 𝑦 ≤ 𝐷) |
134 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
135 | 134 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑦 ∈ ℝ) |
136 | 70 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0)) → 𝐷 ∈
ℝ) |
137 | | lenlt 10116 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦)) |
138 | 135, 136,
137 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((0
≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → (𝑦 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑦)) |
139 | 133, 138 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((0
≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) ∧ (𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0)) ∧ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) → ¬ 𝐷 < 𝑦) |
140 | 139 | exp31 630 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ((𝑦 ∥ 𝐷 ∧ 𝐷 ∈ ℕ0) → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦))) |
141 | 91, 140 | mpan2d 710 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (𝑦 ∥ 𝐷 → (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ¬ 𝐷 < 𝑦))) |
142 | 141 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦))) |
143 | 142 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑦 ∥ 𝐷 → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦))) |
144 | 85, 143 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → ¬ 𝐷 < 𝑦))) |
145 | 144 | com13 88 |
. . . . . . . . . . . . 13
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁)) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦))) |
146 | 145 | ex 450 |
. . . . . . . . . . . 12
⊢ (0 ≤
𝐷 → ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)))) |
147 | 146 | 3imp 1256 |
. . . . . . . . . . 11
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ¬ 𝐷 < 𝑦)) |
148 | 147 | com12 32 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → ¬ 𝐷 < 𝑦)) |
149 | 148 | expimpd 629 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → ¬ 𝐷 < 𝑦)) |
150 | 149 | expimpd 629 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℤ ∧ (𝑦 ∥ 𝑀 ∧ 𝑦 ∥ 𝑁)) → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦)) |
151 | 76, 150 | sylbi 207 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ((¬ (𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → ¬ 𝐷 < 𝑦)) |
152 | 151 | impcom 446 |
. . . . . 6
⊢ (((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) → ¬ 𝐷 < 𝑦) |
153 | 68 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → 𝐷 ∈ ℤ) |
154 | 153 | ancri 575 |
. . . . . . . . . . 11
⊢ ((𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
155 | 154 | 3ad2ant2 1083 |
. . . . . . . . . 10
⊢ ((0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
156 | 155 | ad2antll 765 |
. . . . . . . . 9
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
157 | 156 | adantr 481 |
. . . . . . . 8
⊢ (((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
158 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑀 ↔ 𝐷 ∥ 𝑀)) |
159 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐷 → (𝑛 ∥ 𝑁 ↔ 𝐷 ∥ 𝑁)) |
160 | 158, 159 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑛 = 𝐷 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
161 | 160 | elrab 3363 |
. . . . . . . 8
⊢ (𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐷 ∈ ℤ ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁))) |
162 | 157, 161 | sylibr 224 |
. . . . . . 7
⊢ (((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝐷 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) |
163 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑧 = 𝐷 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷)) |
164 | 163 | adantl 482 |
. . . . . . 7
⊢ ((((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) ∧ 𝑧 = 𝐷) → (𝑦 < 𝑧 ↔ 𝑦 < 𝐷)) |
165 | | simprr 796 |
. . . . . . 7
⊢ (((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → 𝑦 < 𝐷) |
166 | 162, 164,
165 | rspcedvd 3317 |
. . . . . 6
⊢ (((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) ∧ (𝑦 ∈ ℝ ∧ 𝑦 < 𝐷)) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧) |
167 | 66, 72, 152, 166 | eqsupd 8363 |
. . . . 5
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) = 𝐷) |
168 | 64, 167 | eqtrd 2656 |
. . . 4
⊢ ((¬
(𝑀 = 0 ∧ 𝑁 = 0) ∧ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷) |
169 | 62, 168 | pm2.61ian 831 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) = 𝐷) |
170 | 23, 169 | eqtr2d 2657 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ≤
𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))) → 𝐷 = (𝑀 gcd 𝑁)) |
171 | 21, 170 | impbida 877 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) |