| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑧 < 𝑥 ↔ 𝑧 < 1)) |
| 2 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 − 𝑧) = (1 − 𝑧)) |
| 3 | 2 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 − 𝑧) ∈ ℕ ↔ (1 − 𝑧) ∈
ℕ)) |
| 4 | 1, 3 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 1 → (1 − 𝑧) ∈ ℕ))) |
| 5 | 4 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = 1 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 1 → (1 − 𝑧) ∈
ℕ))) |
| 6 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑧 < 𝑥 ↔ 𝑧 < 𝑦)) |
| 7 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 − 𝑧) = (𝑦 − 𝑧)) |
| 8 | 7 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑧) ∈ ℕ)) |
| 9 | 6, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
| 10 | 9 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
| 11 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑧 < 𝑥 ↔ 𝑧 < (𝑦 + 1))) |
| 12 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 − 𝑧) = ((𝑦 + 1) − 𝑧)) |
| 13 | 12 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
| 14 | 11, 13 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 15 | 14 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 16 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑧 < 𝑥 ↔ 𝑧 < 𝐵)) |
| 17 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 − 𝑧) = (𝐵 − 𝑧)) |
| 18 | 17 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝑧) ∈ ℕ)) |
| 19 | 16, 18 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
| 20 | 19 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = 𝐵 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
| 21 | | nnnlt1 12298 |
. . . . . 6
⊢ (𝑧 ∈ ℕ → ¬
𝑧 < 1) |
| 22 | 21 | pm2.21d 121 |
. . . . 5
⊢ (𝑧 ∈ ℕ → (𝑧 < 1 → (1 − 𝑧) ∈
ℕ)) |
| 23 | 22 | rgen 3063 |
. . . 4
⊢
∀𝑧 ∈
ℕ (𝑧 < 1 → (1
− 𝑧) ∈
ℕ) |
| 24 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 < 𝑦 ↔ 𝑥 < 𝑦)) |
| 25 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑦 − 𝑧) = (𝑦 − 𝑥)) |
| 26 | 25 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑦 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑥) ∈ ℕ)) |
| 27 | 24, 26 | imbi12d 344 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ))) |
| 28 | 27 | cbvralvw 3237 |
. . . . 5
⊢
(∀𝑧 ∈
ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ ∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ)) |
| 29 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℂ) |
| 31 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 32 | | pncan 11514 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑦 + 1)
− 1) = 𝑦) |
| 33 | 30, 31, 32 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) = 𝑦) |
| 34 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℕ) |
| 35 | 33, 34 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) ∈
ℕ) |
| 36 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → ((𝑦 + 1) − 𝑧) = ((𝑦 + 1) − 1)) |
| 37 | 36 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (((𝑦 + 1) − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 1) ∈
ℕ)) |
| 38 | 35, 37 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
| 39 | 38 | 2a1dd 51 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → (∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
| 40 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → (𝑥 < 𝑦 ↔ (𝑧 − 1) < 𝑦)) |
| 41 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 − 1) → (𝑦 − 𝑥) = (𝑦 − (𝑧 − 1))) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → ((𝑦 − 𝑥) ∈ ℕ ↔ (𝑦 − (𝑧 − 1)) ∈
ℕ)) |
| 43 | 40, 42 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 − 1) → ((𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) ↔ ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
| 44 | 43 | rspcv 3618 |
. . . . . . . 8
⊢ ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
| 45 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
| 46 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 47 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 48 | | ltsubadd 11733 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑦 ∈
ℝ) → ((𝑧 −
1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
| 49 | 47, 48 | mp3an2 1451 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
| 50 | 45, 46, 49 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
| 51 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℂ) |
| 52 | | subsub3 11541 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑦 −
(𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
| 53 | 31, 52 | mp3an3 1452 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
| 54 | 29, 51, 53 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
| 55 | 54 | eleq1d 2826 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 − (𝑧 − 1)) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
| 56 | 50, 55 | imbi12d 344 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 57 | 56 | biimpd 229 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 58 | 44, 57 | syl9r 78 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
| 59 | | nn1m1nn 12287 |
. . . . . . . 8
⊢ (𝑧 ∈ ℕ → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
| 60 | 59 | adantl 481 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
| 61 | 39, 58, 60 | mpjaod 861 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 62 | 61 | ralrimdva 3154 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 63 | 28, 62 | biimtrid 242 |
. . . 4
⊢ (𝑦 ∈ ℕ →
(∀𝑧 ∈ ℕ
(𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
| 64 | 5, 10, 15, 20, 23, 63 | nnind 12284 |
. . 3
⊢ (𝐵 ∈ ℕ →
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) |
| 65 | | breq1 5146 |
. . . . 5
⊢ (𝑧 = 𝐴 → (𝑧 < 𝐵 ↔ 𝐴 < 𝐵)) |
| 66 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝐵 − 𝑧) = (𝐵 − 𝐴)) |
| 67 | 66 | eleq1d 2826 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((𝐵 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝐴) ∈ ℕ)) |
| 68 | 65, 67 | imbi12d 344 |
. . . 4
⊢ (𝑧 = 𝐴 → ((𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ) ↔ (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ))) |
| 69 | 68 | rspcva 3620 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
| 70 | 64, 69 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
| 71 | | nngt0 12297 |
. . 3
⊢ ((𝐵 − 𝐴) ∈ ℕ → 0 < (𝐵 − 𝐴)) |
| 72 | | nnre 12273 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 73 | | nnre 12273 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 74 | | posdif 11756 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
| 75 | 72, 73, 74 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
| 76 | 71, 75 | imbitrrid 246 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵 − 𝐴) ∈ ℕ → 𝐴 < 𝐵)) |
| 77 | 70, 76 | impbid 212 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) |