Step | Hyp | Ref
| Expression |
1 | | breq2 5078 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑧 < 𝑥 ↔ 𝑧 < 1)) |
2 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 − 𝑧) = (1 − 𝑧)) |
3 | 2 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑥 − 𝑧) ∈ ℕ ↔ (1 − 𝑧) ∈
ℕ)) |
4 | 1, 3 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 1 → (1 − 𝑧) ∈ ℕ))) |
5 | 4 | ralbidv 3112 |
. . . 4
⊢ (𝑥 = 1 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 1 → (1 − 𝑧) ∈
ℕ))) |
6 | | breq2 5078 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑧 < 𝑥 ↔ 𝑧 < 𝑦)) |
7 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 − 𝑧) = (𝑦 − 𝑧)) |
8 | 7 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑧) ∈ ℕ)) |
9 | 6, 8 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
10 | 9 | ralbidv 3112 |
. . . 4
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ))) |
11 | | breq2 5078 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑧 < 𝑥 ↔ 𝑧 < (𝑦 + 1))) |
12 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 − 𝑧) = ((𝑦 + 1) − 𝑧)) |
13 | 12 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
14 | 11, 13 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
15 | 14 | ralbidv 3112 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
16 | | breq2 5078 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑧 < 𝑥 ↔ 𝑧 < 𝐵)) |
17 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 − 𝑧) = (𝐵 − 𝑧)) |
18 | 17 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝑧) ∈ ℕ)) |
19 | 16, 18 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
20 | 19 | ralbidv 3112 |
. . . 4
⊢ (𝑥 = 𝐵 → (∀𝑧 ∈ ℕ (𝑧 < 𝑥 → (𝑥 − 𝑧) ∈ ℕ) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ))) |
21 | | nnnlt1 12005 |
. . . . . 6
⊢ (𝑧 ∈ ℕ → ¬
𝑧 < 1) |
22 | 21 | pm2.21d 121 |
. . . . 5
⊢ (𝑧 ∈ ℕ → (𝑧 < 1 → (1 − 𝑧) ∈
ℕ)) |
23 | 22 | rgen 3074 |
. . . 4
⊢
∀𝑧 ∈
ℕ (𝑧 < 1 → (1
− 𝑧) ∈
ℕ) |
24 | | breq1 5077 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 < 𝑦 ↔ 𝑥 < 𝑦)) |
25 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑦 − 𝑧) = (𝑦 − 𝑥)) |
26 | 25 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑦 − 𝑧) ∈ ℕ ↔ (𝑦 − 𝑥) ∈ ℕ)) |
27 | 24, 26 | imbi12d 345 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ))) |
28 | 27 | cbvralvw 3383 |
. . . . 5
⊢
(∀𝑧 ∈
ℕ (𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) ↔ ∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ)) |
29 | | nncn 11981 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
30 | 29 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℂ) |
31 | | ax-1cn 10929 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
32 | | pncan 11227 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑦 + 1)
− 1) = 𝑦) |
33 | 30, 31, 32 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) = 𝑦) |
34 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑦 ∈
ℕ) |
35 | 33, 34 | eqeltrd 2839 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 + 1) − 1) ∈
ℕ) |
36 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → ((𝑦 + 1) − 𝑧) = ((𝑦 + 1) − 1)) |
37 | 36 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (((𝑦 + 1) − 𝑧) ∈ ℕ ↔ ((𝑦 + 1) − 1) ∈
ℕ)) |
38 | 35, 37 | syl5ibrcom 246 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
39 | 38 | 2a1dd 51 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 → (∀𝑥 ∈ ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
40 | | breq1 5077 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → (𝑥 < 𝑦 ↔ (𝑧 − 1) < 𝑦)) |
41 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 − 1) → (𝑦 − 𝑥) = (𝑦 − (𝑧 − 1))) |
42 | 41 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 − 1) → ((𝑦 − 𝑥) ∈ ℕ ↔ (𝑦 − (𝑧 − 1)) ∈
ℕ)) |
43 | 40, 42 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 − 1) → ((𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) ↔ ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
44 | 43 | rspcv 3557 |
. . . . . . . 8
⊢ ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈
ℕ))) |
45 | | nnre 11980 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
46 | | nnre 11980 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
47 | | 1re 10975 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
48 | | ltsubadd 11445 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑦 ∈
ℝ) → ((𝑧 −
1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
49 | 47, 48 | mp3an2 1448 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
50 | 45, 46, 49 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) < 𝑦 ↔ 𝑧 < (𝑦 + 1))) |
51 | | nncn 11981 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℂ) |
52 | | subsub3 11253 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑦 −
(𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
53 | 31, 52 | mp3an3 1449 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
54 | 29, 51, 53 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑦 − (𝑧 − 1)) = ((𝑦 + 1) − 𝑧)) |
55 | 54 | eleq1d 2823 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑦 − (𝑧 − 1)) ∈ ℕ ↔ ((𝑦 + 1) − 𝑧) ∈ ℕ)) |
56 | 50, 55 | imbi12d 345 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) ↔ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
57 | 56 | biimpd 228 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (((𝑧 − 1) < 𝑦 → (𝑦 − (𝑧 − 1)) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
58 | 44, 57 | syl9r 78 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 − 1) ∈ ℕ
→ (∀𝑥 ∈
ℕ (𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ)))) |
59 | | nn1m1nn 11994 |
. . . . . . . 8
⊢ (𝑧 ∈ ℕ → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
60 | 59 | adantl 482 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 = 1 ∨ (𝑧 − 1) ∈ ℕ)) |
61 | 39, 58, 60 | mpjaod 857 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
62 | 61 | ralrimdva 3106 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
(∀𝑥 ∈ ℕ
(𝑥 < 𝑦 → (𝑦 − 𝑥) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
63 | 28, 62 | syl5bi 241 |
. . . 4
⊢ (𝑦 ∈ ℕ →
(∀𝑧 ∈ ℕ
(𝑧 < 𝑦 → (𝑦 − 𝑧) ∈ ℕ) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ((𝑦 + 1) − 𝑧) ∈ ℕ))) |
64 | 5, 10, 15, 20, 23, 63 | nnind 11991 |
. . 3
⊢ (𝐵 ∈ ℕ →
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) |
65 | | breq1 5077 |
. . . . 5
⊢ (𝑧 = 𝐴 → (𝑧 < 𝐵 ↔ 𝐴 < 𝐵)) |
66 | | oveq2 7283 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝐵 − 𝑧) = (𝐵 − 𝐴)) |
67 | 66 | eleq1d 2823 |
. . . . 5
⊢ (𝑧 = 𝐴 → ((𝐵 − 𝑧) ∈ ℕ ↔ (𝐵 − 𝐴) ∈ ℕ)) |
68 | 65, 67 | imbi12d 345 |
. . . 4
⊢ (𝑧 = 𝐴 → ((𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ) ↔ (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ))) |
69 | 68 | rspcva 3559 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧
∀𝑧 ∈ ℕ
(𝑧 < 𝐵 → (𝐵 − 𝑧) ∈ ℕ)) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
70 | 64, 69 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 → (𝐵 − 𝐴) ∈ ℕ)) |
71 | | nngt0 12004 |
. . 3
⊢ ((𝐵 − 𝐴) ∈ ℕ → 0 < (𝐵 − 𝐴)) |
72 | | nnre 11980 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
73 | | nnre 11980 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
74 | | posdif 11468 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
75 | 72, 73, 74 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
76 | 71, 75 | syl5ibr 245 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵 − 𝐴) ∈ ℕ → 𝐴 < 𝐵)) |
77 | 70, 76 | impbid 211 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) |