Proof of Theorem zm1nn
| Step | Hyp | Ref
| Expression |
| 1 | | 0red 11264 |
. . . . . . 7
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ 0 ∈ ℝ) |
| 2 | | simpl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ 𝐽 ∈
ℝ) |
| 3 | | zre 12617 |
. . . . . . . . . 10
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
| 4 | | nn0re 12535 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 5 | | resubcl 11573 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 − 𝑁) ∈ ℝ) |
| 6 | 3, 4, 5 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐿 − 𝑁) ∈
ℝ) |
| 7 | 6 | adantl 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ (𝐿 − 𝑁) ∈
ℝ) |
| 8 | | peano2rem 11576 |
. . . . . . . 8
⊢ ((𝐿 − 𝑁) ∈ ℝ → ((𝐿 − 𝑁) − 1) ∈
ℝ) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ ((𝐿 − 𝑁) − 1) ∈
ℝ) |
| 10 | | lelttr 11351 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 𝐽
∈ ℝ ∧ ((𝐿
− 𝑁) − 1)
∈ ℝ) → ((0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → 0 < ((𝐿 − 𝑁) − 1))) |
| 11 | 1, 2, 9, 10 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ ((0 ≤ 𝐽 ∧
𝐽 < ((𝐿 − 𝑁) − 1)) → 0 < ((𝐿 − 𝑁) − 1))) |
| 12 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ 1 ∈ ℝ) |
| 13 | 12, 6 | posdifd 11850 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (1 < (𝐿 −
𝑁) ↔ 0 < ((𝐿 − 𝑁) − 1))) |
| 14 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ 𝑁 ∈
ℝ) |
| 15 | 3 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ 𝐿 ∈
ℝ) |
| 16 | 12, 14, 15 | ltaddsubd 11863 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ ((1 + 𝑁) < 𝐿 ↔ 1 < (𝐿 − 𝑁))) |
| 17 | | elnn0z 12626 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
| 18 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 0 ∈
ℝ) |
| 19 | | zre 12617 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝑁 ∈
ℝ) |
| 21 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 1 ∈
ℝ) |
| 22 | 18, 20, 21 | leadd2d 11858 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝑁 ↔ (1 + 0) ≤ (1 +
𝑁))) |
| 23 | | 1re 11261 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
| 24 | | 0re 11263 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
| 25 | 23, 24 | readdcli 11276 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 0)
∈ ℝ |
| 26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (1 + 0)
∈ ℝ) |
| 27 | | 1red 11262 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → 1 ∈
ℝ) |
| 28 | 27, 19 | readdcld 11290 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → (1 +
𝑁) ∈
ℝ) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (1 +
𝑁) ∈
ℝ) |
| 30 | 3 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈
ℝ) |
| 31 | | lelttr 11351 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + 0)
∈ ℝ ∧ (1 + 𝑁) ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((1 + 0) ≤ (1 +
𝑁) ∧ (1 + 𝑁) < 𝐿) → (1 + 0) < 𝐿)) |
| 32 | 26, 29, 30, 31 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (((1 +
0) ≤ (1 + 𝑁) ∧ (1 +
𝑁) < 𝐿) → (1 + 0) < 𝐿)) |
| 33 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℤ → (𝐿 − 1) ∈
ℤ) |
| 34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 − 1) ∈
ℤ) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (1 + 0)
< 𝐿) → (𝐿 − 1) ∈
ℤ) |
| 36 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℤ → 1 ∈
ℝ) |
| 37 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℤ → 0 ∈
ℝ) |
| 38 | 36, 37, 3 | ltaddsub2d 11864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ ℤ → ((1 + 0)
< 𝐿 ↔ 0 < (𝐿 − 1))) |
| 39 | 38 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℤ → ((1 + 0)
< 𝐿 → 0 < (𝐿 − 1))) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((1 + 0)
< 𝐿 → 0 < (𝐿 − 1))) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (1 + 0)
< 𝐿) → 0 <
(𝐿 −
1)) |
| 42 | | elnnz 12623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 − 1) ∈ ℕ
↔ ((𝐿 − 1)
∈ ℤ ∧ 0 < (𝐿 − 1))) |
| 43 | 35, 41, 42 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (1 + 0)
< 𝐿) → (𝐿 − 1) ∈
ℕ) |
| 44 | 43 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((1 + 0)
< 𝐿 → (𝐿 − 1) ∈
ℕ)) |
| 45 | 32, 44 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (((1 +
0) ≤ (1 + 𝑁) ∧ (1 +
𝑁) < 𝐿) → (𝐿 − 1) ∈
ℕ)) |
| 46 | 45 | expd 415 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((1 + 0)
≤ (1 + 𝑁) → ((1 +
𝑁) < 𝐿 → (𝐿 − 1) ∈
ℕ))) |
| 47 | 22, 46 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝑁 → ((1 + 𝑁) < 𝐿 → (𝐿 − 1) ∈
ℕ))) |
| 48 | 47 | impancom 451 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 0 ≤
𝑁) → (𝐿 ∈ ℤ → ((1 +
𝑁) < 𝐿 → (𝐿 − 1) ∈
ℕ))) |
| 49 | 17, 48 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ ((1 + 𝑁) < 𝐿 → (𝐿 − 1) ∈
ℕ))) |
| 50 | 49 | imp 406 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ ((1 + 𝑁) < 𝐿 → (𝐿 − 1) ∈
ℕ)) |
| 51 | 16, 50 | sylbird 260 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (1 < (𝐿 −
𝑁) → (𝐿 − 1) ∈
ℕ)) |
| 52 | 13, 51 | sylbird 260 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (0 < ((𝐿 −
𝑁) − 1) → (𝐿 − 1) ∈
ℕ)) |
| 53 | 52 | adantl 481 |
. . . . . 6
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ (0 < ((𝐿 −
𝑁) − 1) → (𝐿 − 1) ∈
ℕ)) |
| 54 | 11, 53 | syld 47 |
. . . . 5
⊢ ((𝐽 ∈ ℝ ∧ (𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ ((0 ≤ 𝐽 ∧
𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈
ℕ)) |
| 55 | 54 | ex 412 |
. . . 4
⊢ (𝐽 ∈ ℝ → ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ ((0 ≤ 𝐽 ∧
𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈
ℕ))) |
| 56 | 55 | com23 86 |
. . 3
⊢ (𝐽 ∈ ℝ → ((0 ≤
𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 − 1) ∈
ℕ))) |
| 57 | 56 | 3impib 1117 |
. 2
⊢ ((𝐽 ∈ ℝ ∧ 0 ≤
𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 − 1) ∈
ℕ)) |
| 58 | 57 | com12 32 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ ((𝐽 ∈ ℝ
∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈
ℕ)) |