Step | Hyp | Ref
| Expression |
1 | | breq2 3981 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑧 < 𝑥 ↔ 𝑧 < 1)) |
2 | | oveq1 5844 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 − 𝑧) = (1 − 𝑧)) |
3 | 2 | eleq1d 2233 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 − 𝑧) ∈ ℕ ↔ (1 − 𝑧) ∈
ℕ)) |
4 | 1, 3 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 1 → (1 − 𝑧) ∈ ℕ))) |
5 | 4 | ralbidv 2464 |
. . . 4
⊢ (𝑥 = 1 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 1 → (1 − 𝑧) ∈
ℕ))) |
6 | | breq2 3981 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑧 < 𝑥 ↔ 𝑧 < 𝑦)) |
7 | | oveq1 5844 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 − 𝑧) = (𝑦 − 𝑧)) |
8 | 7 | eleq1d 2233 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑧) ∈ ℕ)) |
9 | 6, 8 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
10 | 9 | ralbidv 2464 |
. . . 4
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
11 | | breq2 3981 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑧 < 𝑥 ↔ 𝑧 < (𝑦 + 1))) |
12 | | oveq1 5844 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 − 𝑧) = ((𝑦 + 1) − 𝑧)) |
13 | 12 | eleq1d 2233 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
14 | 11, 13 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
15 | 14 | ralbidv 2464 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
16 | | breq2 3981 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑧 < 𝑥 ↔ 𝑧 < 𝐵)) |
17 | | oveq1 5844 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 − 𝑧) = (𝐵 − 𝑧)) |
18 | 17 | eleq1d 2233 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝑧) ∈ ℕ)) |
19 | 16, 18 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
20 | 19 | ralbidv 2464 |
. . . 4
⊢ (𝑥 = 𝐵 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
21 | | nnnlt1 8875 |
. . . . . 6
⊢ (𝑧 ∈ ℕ → ¬
𝑧 < 1) |
22 | 21 | pm2.21d 609 |
. . . . 5
⊢ (𝑧 ∈ ℕ → (𝑧 < 1 → (1 − 𝑧) ∈
ℕ)) |
23 | 22 | rgen 2517 |
. . . 4
⊢
∀𝑧 ∈
ℕ (𝑧 < 1 → (1
− 𝑧) ∈
ℕ) |
24 | | breq1 3980 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 < 𝑦 ↔ 𝑥 < 𝑦)) |
25 | | oveq2 5845 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑦 − 𝑧) = (𝑦 − 𝑥)) |
26 | 25 | eleq1d 2233 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑦 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑥) ∈ ℕ)) |
27 | 24, 26 | imbi12d 233 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ))) |
28 | 27 | cbvralv 2690 |
. . . . 5
⊢
(∀𝑧 ∈
ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ ∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ)) |
29 | | nncn 8857 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
30 | 29 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℂ) |
31 | | ax-1cn 7838 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
32 | | pncan 8096 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑦 + 1)
− 1) = 𝑦) |
33 | 30, 31, 32 | sylancl 410 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) = 𝑦) |
34 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℕ) |
35 | 33, 34 | eqeltrd 2241 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) ∈
ℕ) |
36 | | oveq2 5845 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → ((𝑦 + 1) − 𝑧) = ((𝑦 + 1) − 1)) |
37 | 36 | eleq1d 2233 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (((𝑦 + 1) − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 1) ∈
ℕ)) |
38 | 35, 37 | syl5ibrcom 156 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
39 | 38 | a1dd 48 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
40 | 39 | a1dd 48 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → (∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
41 | | breq1 3980 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → (𝑥 < 𝑦 ↔ (𝑧 − 1) < 𝑦)) |
42 | | oveq2 5845 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 − 1) → (𝑦 − 𝑥) = (𝑦 − (𝑧 − 1))) |
43 | 42 | eleq1d 2233 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → ((𝑦 − 𝑥) ∈ ℕ ↔ (𝑦 − (𝑧 − 1)) ∈
ℕ)) |
44 | 41, 43 | imbi12d 233 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 − 1) → ((𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) ↔ ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
45 | 44 | rspcv 2822 |
. . . . . . . 8
⊢ ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
46 | | nnre 8856 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
47 | | nnre 8856 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
48 | | 1re 7890 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
49 | | ltsubadd 8322 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑦 ∈
ℝ) → ((𝑧 −
1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
50 | 48, 49 | mp3an2 1314 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
51 | 46, 47, 50 | syl2anr 288 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
52 | | nncn 8857 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℂ) |
53 | | subsub3 8122 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑦 −
(𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
54 | 31, 53 | mp3an3 1315 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
55 | 29, 52, 54 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
56 | 55 | eleq1d 2233 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 − (𝑧 − 1)) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
57 | 51, 56 | imbi12d 233 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
58 | 57 | biimpd 143 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
59 | 45, 58 | syl9r 73 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
60 | | nn1m1nn 8867 |
. . . . . . . 8
⊢ (𝑧 ∈ ℕ → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
61 | 60 | adantl 275 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
62 | 40, 59, 61 | mpjaod 708 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
63 | 62 | ralrimdva 2544 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
64 | 28, 63 | syl5bi 151 |
. . . 4
⊢ (𝑦 ∈ ℕ →
(∀𝑧 ∈ ℕ
(𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
65 | 5, 10, 15, 20, 23, 64 | nnind 8865 |
. . 3
⊢ (𝐵 ∈ ℕ →
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) |
66 | | breq1 3980 |
. . . . 5
⊢ (𝑧 = 𝐴 → (𝑧 < 𝐵 ↔ 𝐴 < 𝐵)) |
67 | | oveq2 5845 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝐵 − 𝑧) = (𝐵 − 𝐴)) |
68 | 67 | eleq1d 2233 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((𝐵 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝐴) ∈ ℕ)) |
69 | 66, 68 | imbi12d 233 |
. . . 4
⊢ (𝑧 = 𝐴 → ((𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ) ↔ (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ))) |
70 | 69 | rspcva 2824 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
71 | 65, 70 | sylan2 284 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
72 | | nngt0 8874 |
. . 3
⊢ ((𝐵 − 𝐴) ∈ ℕ → 0 < (𝐵 − 𝐴)) |
73 | | nnre 8856 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
74 | | nnre 8856 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
75 | | posdif 8345 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
76 | 73, 74, 75 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
77 | 72, 76 | syl5ibr 155 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵 − 𝐴) ∈ ℕ → 𝐴 < 𝐵)) |
78 | 71, 77 | impbid 128 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) |