Step |
Hyp |
Ref |
Expression |
1 |
|
elfz2 |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) ) |
2 |
|
simpl2 |
⊢ ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) → 𝑀 ∈ ℤ ) |
3 |
|
1red |
⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℝ ) |
4 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
5 |
4
|
3ad2ant3 |
⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ ) |
6 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ ) |
8 |
|
letr |
⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) → 1 ≤ 𝑀 ) ) |
9 |
3 5 7 8
|
syl3anc |
⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) → 1 ≤ 𝑀 ) ) |
10 |
9
|
imp |
⊢ ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) → 1 ≤ 𝑀 ) |
11 |
|
elnnz1 |
⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀 ) ) |
12 |
2 10 11
|
sylanbrc |
⊢ ( ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) → 𝑀 ∈ ℕ ) |
13 |
1 12
|
sylbi |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℕ ) |
14 |
|
elfzel2 |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℤ ) |
15 |
|
fznn |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) |
16 |
15
|
biimpd |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) |
17 |
14 16
|
mpcom |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) |
18 |
|
3anan12 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ↔ ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) |
19 |
13 17 18
|
sylanbrc |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) → ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) |
20 |
|
nnz |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ ) |
21 |
20 15
|
syl |
⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) ) |
22 |
21
|
biimprd |
⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) → 𝑁 ∈ ( 1 ... 𝑀 ) ) ) |
23 |
22
|
expd |
⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝑁 ≤ 𝑀 → 𝑁 ∈ ( 1 ... 𝑀 ) ) ) ) |
24 |
23
|
3imp21 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) → 𝑁 ∈ ( 1 ... 𝑀 ) ) |
25 |
19 24
|
impbii |
⊢ ( 𝑁 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀 ) ) |