Step | Hyp | Ref
| Expression |
1 | | df-uz 9481 |
. . . . 5
⊢
ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) |
2 | | zex 9214 |
. . . . . 6
⊢ ℤ
∈ V |
3 | 2 | mptex 5720 |
. . . . 5
⊢ (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) ∈ V |
4 | 1, 3 | eqeltri 2243 |
. . . 4
⊢
ℤ≥ ∈ V |
5 | | fvexg 5513 |
. . . 4
⊢
((ℤ≥ ∈ V ∧ 𝑀 ∈ ℤ) →
(ℤ≥‘𝑀) ∈ V) |
6 | 4, 5 | mpan 422 |
. . 3
⊢ (𝑀 ∈ ℤ →
(ℤ≥‘𝑀) ∈ V) |
7 | | nn0ex 9134 |
. . . 4
⊢
ℕ0 ∈ V |
8 | 7 | a1i 9 |
. . 3
⊢ (𝑀 ∈ ℤ →
ℕ0 ∈ V) |
9 | | eluzelz 9489 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → 𝑥 ∈ ℤ) |
10 | 9 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 𝑥 ∈ ℤ) |
11 | | simpl 108 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 𝑀 ∈ ℤ) |
12 | 10, 11 | zsubcld 9332 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → (𝑥 − 𝑀) ∈ ℤ) |
13 | | eluzle 9492 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑥) |
14 | 13 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 𝑀 ≤ 𝑥) |
15 | 10 | zred 9327 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 𝑥 ∈ ℝ) |
16 | 11 | zred 9327 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
17 | 15, 16 | subge0d 8447 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥)) |
18 | 14, 17 | mpbird 166 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → 0 ≤ (𝑥 − 𝑀)) |
19 | | elnn0z 9218 |
. . . . 5
⊢ ((𝑥 − 𝑀) ∈ ℕ0 ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀))) |
20 | 12, 18, 19 | sylanbrc 415 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → (𝑥 − 𝑀) ∈
ℕ0) |
21 | 20 | ex 114 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝑥 ∈
(ℤ≥‘𝑀) → (𝑥 − 𝑀) ∈
ℕ0)) |
22 | | simpl 108 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 𝑀 ∈
ℤ) |
23 | | nn0z 9225 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
24 | 23 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℤ) |
25 | 24, 22 | zaddcld 9331 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (𝑦 + 𝑀) ∈
ℤ) |
26 | | nn0ge0 9153 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ 0 ≤ 𝑦) |
27 | 26 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 0 ≤ 𝑦) |
28 | 22 | zred 9327 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 𝑀 ∈
ℝ) |
29 | 24 | zred 9327 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℝ) |
30 | 28, 29 | addge02d 8446 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (0 ≤ 𝑦 ↔
𝑀 ≤ (𝑦 + 𝑀))) |
31 | 27, 30 | mpbid 146 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ 𝑀 ≤ (𝑦 + 𝑀)) |
32 | | eluz2 9486 |
. . . . 5
⊢ ((𝑦 + 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑦 + 𝑀) ∈ ℤ ∧ 𝑀 ≤ (𝑦 + 𝑀))) |
33 | 22, 25, 31, 32 | syl3anbrc 1176 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (𝑦 + 𝑀) ∈
(ℤ≥‘𝑀)) |
34 | 33 | ex 114 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝑦 ∈ ℕ0
→ (𝑦 + 𝑀) ∈
(ℤ≥‘𝑀))) |
35 | 9 | ad2antrl 487 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑥 ∈
ℤ) |
36 | 35 | zcnd 9328 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑥 ∈
ℂ) |
37 | | simpl 108 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑀 ∈
ℤ) |
38 | 37 | zcnd 9328 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑀 ∈
ℂ) |
39 | | simprr 527 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑦 ∈
ℕ0) |
40 | 39 | nn0cnd 9183 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → 𝑦 ∈
ℂ) |
41 | 36, 38, 40 | subadd2d 8242 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → ((𝑥 − 𝑀) = 𝑦 ↔ (𝑦 + 𝑀) = 𝑥)) |
42 | | bicom 139 |
. . . . . 6
⊢ (((𝑥 − 𝑀) = 𝑦 ↔ (𝑦 + 𝑀) = 𝑥) ↔ ((𝑦 + 𝑀) = 𝑥 ↔ (𝑥 − 𝑀) = 𝑦)) |
43 | | eqcom 2172 |
. . . . . . 7
⊢ ((𝑦 + 𝑀) = 𝑥 ↔ 𝑥 = (𝑦 + 𝑀)) |
44 | | eqcom 2172 |
. . . . . . 7
⊢ ((𝑥 − 𝑀) = 𝑦 ↔ 𝑦 = (𝑥 − 𝑀)) |
45 | 43, 44 | bibi12i 228 |
. . . . . 6
⊢ (((𝑦 + 𝑀) = 𝑥 ↔ (𝑥 − 𝑀) = 𝑦) ↔ (𝑥 = (𝑦 + 𝑀) ↔ 𝑦 = (𝑥 − 𝑀))) |
46 | 42, 45 | bitri 183 |
. . . . 5
⊢ (((𝑥 − 𝑀) = 𝑦 ↔ (𝑦 + 𝑀) = 𝑥) ↔ (𝑥 = (𝑦 + 𝑀) ↔ 𝑦 = (𝑥 − 𝑀))) |
47 | 41, 46 | sylib 121 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0)) → (𝑥 = (𝑦 + 𝑀) ↔ 𝑦 = (𝑥 − 𝑀))) |
48 | 47 | ex 114 |
. . 3
⊢ (𝑀 ∈ ℤ → ((𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ ℕ0) → (𝑥 = (𝑦 + 𝑀) ↔ 𝑦 = (𝑥 − 𝑀)))) |
49 | 6, 8, 21, 34, 48 | en3d 6745 |
. 2
⊢ (𝑀 ∈ ℤ →
(ℤ≥‘𝑀) ≈
ℕ0) |
50 | | nn0ennn 10382 |
. 2
⊢
ℕ0 ≈ ℕ |
51 | | entr 6760 |
. 2
⊢
(((ℤ≥‘𝑀) ≈ ℕ0 ∧
ℕ0 ≈ ℕ) → (ℤ≥‘𝑀) ≈
ℕ) |
52 | 49, 50, 51 | sylancl 411 |
1
⊢ (𝑀 ∈ ℤ →
(ℤ≥‘𝑀) ≈ ℕ) |