Step | Hyp | Ref
| Expression |
1 | | 1zzd 9344 |
. . 3
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → 1 ∈
ℤ) |
2 | | breq1 4032 |
. . . 4
⊢ (𝑛 = 1 → (𝑛 ∥ 𝑋 ↔ 1 ∥ 𝑋)) |
3 | | breq1 4032 |
. . . 4
⊢ (𝑛 = 1 → (𝑛 ∥ 𝑌 ↔ 1 ∥ 𝑌)) |
4 | 2, 3 | anbi12d 473 |
. . 3
⊢ (𝑛 = 1 → ((𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌) ↔ (1 ∥ 𝑋 ∧ 1 ∥ 𝑌))) |
5 | | 1dvds 11948 |
. . . . 5
⊢ (𝑋 ∈ ℤ → 1 ∥
𝑋) |
6 | | 1dvds 11948 |
. . . . 5
⊢ (𝑌 ∈ ℤ → 1 ∥
𝑌) |
7 | 5, 6 | anim12i 338 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (1
∥ 𝑋 ∧ 1 ∥
𝑌)) |
8 | 7 | adantr 276 |
. . 3
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → (1 ∥ 𝑋 ∧ 1 ∥ 𝑌)) |
9 | | elnnuz 9629 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
10 | 9 | biimpri 133 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ ℕ) |
11 | | simpll 527 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝑋 ∈ ℤ) |
12 | | dvdsdc 11941 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ 𝑋 ∈ ℤ) →
DECID 𝑛
∥ 𝑋) |
13 | 10, 11, 12 | syl2an2 594 |
. . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘1)) → DECID 𝑛 ∥ 𝑋) |
14 | | simplr 528 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝑌 ∈ ℤ) |
15 | | dvdsdc 11941 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ 𝑌 ∈ ℤ) →
DECID 𝑛
∥ 𝑌) |
16 | 10, 14, 15 | syl2an2 594 |
. . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘1)) → DECID 𝑛 ∥ 𝑌) |
17 | 13, 16 | dcand 934 |
. . . 4
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘1)) → DECID (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
18 | 17 | adantlr 477 |
. . 3
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ DECID (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
19 | | dvdsbnd 12093 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑋 ≠ 0) → ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋) |
20 | | nnuz 9628 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
21 | 20 | rexeqi 2695 |
. . . . . . 7
⊢
(∃𝑗 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋 ↔ ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋) |
22 | 19, 21 | sylib 122 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑋 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋) |
23 | | id 19 |
. . . . . . . . 9
⊢ (¬
𝑛 ∥ 𝑋 → ¬ 𝑛 ∥ 𝑋) |
24 | 23 | intnanrd 933 |
. . . . . . . 8
⊢ (¬
𝑛 ∥ 𝑋 → ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
25 | 24 | ralimi 2557 |
. . . . . . 7
⊢
(∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋 → ∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
26 | 25 | reximi 2591 |
. . . . . 6
⊢
(∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑋 → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
27 | 22, 26 | syl 14 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑋 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
28 | 27 | ad4ant14 514 |
. . . 4
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) ∧ 𝑋 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
29 | | dvdsbnd 12093 |
. . . . . . 7
⊢ ((𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌) |
30 | 20 | rexeqi 2695 |
. . . . . . 7
⊢
(∃𝑗 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌 ↔ ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌) |
31 | 29, 30 | sylib 122 |
. . . . . 6
⊢ ((𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌) |
32 | | id 19 |
. . . . . . . . 9
⊢ (¬
𝑛 ∥ 𝑌 → ¬ 𝑛 ∥ 𝑌) |
33 | 32 | intnand 932 |
. . . . . . . 8
⊢ (¬
𝑛 ∥ 𝑌 → ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
34 | 33 | ralimi 2557 |
. . . . . . 7
⊢
(∀𝑛 ∈
(ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌 → ∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
35 | 34 | reximi 2591 |
. . . . . 6
⊢
(∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝑛 ∥ 𝑌 → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
36 | 31, 35 | syl 14 |
. . . . 5
⊢ ((𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
37 | 36 | ad4ant24 516 |
. . . 4
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) ∧ 𝑌 ≠ 0) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
38 | | simpr 110 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → ¬ (𝑋 = 0 ∧ 𝑌 = 0)) |
39 | | simpll 527 |
. . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → 𝑋 ∈ ℤ) |
40 | | 0z 9328 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
41 | | zdceq 9392 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 0 ∈
ℤ) → DECID 𝑋 = 0) |
42 | 39, 40, 41 | sylancl 413 |
. . . . . . 7
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) →
DECID 𝑋 =
0) |
43 | | ianordc 900 |
. . . . . . 7
⊢
(DECID 𝑋 = 0 → (¬ (𝑋 = 0 ∧ 𝑌 = 0) ↔ (¬ 𝑋 = 0 ∨ ¬ 𝑌 = 0))) |
44 | 42, 43 | syl 14 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → (¬ (𝑋 = 0 ∧ 𝑌 = 0) ↔ (¬ 𝑋 = 0 ∨ ¬ 𝑌 = 0))) |
45 | 38, 44 | mpbid 147 |
. . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → (¬ 𝑋 = 0 ∨ ¬ 𝑌 = 0)) |
46 | | df-ne 2365 |
. . . . . 6
⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0) |
47 | | df-ne 2365 |
. . . . . 6
⊢ (𝑌 ≠ 0 ↔ ¬ 𝑌 = 0) |
48 | 46, 47 | orbi12i 765 |
. . . . 5
⊢ ((𝑋 ≠ 0 ∨ 𝑌 ≠ 0) ↔ (¬ 𝑋 = 0 ∨ ¬ 𝑌 = 0)) |
49 | 45, 48 | sylibr 134 |
. . . 4
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → (𝑋 ≠ 0 ∨ 𝑌 ≠ 0)) |
50 | 28, 37, 49 | mpjaodan 799 |
. . 3
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑗 ∈
(ℤ≥‘1)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)) |
51 | 1, 4, 8, 18, 50 | zsupcl 12084 |
. 2
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈
(ℤ≥‘1)) |
52 | 51, 20 | eleqtrrdi 2287 |
1
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬
(𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈
ℕ) |