Step | Hyp | Ref
| Expression |
1 | | breq2 5057 |
. . . 4
⊢ (𝑘 = 𝑛 → (𝑁 ≤ 𝑘 ↔ 𝑁 ≤ 𝑛)) |
2 | 1 | elrab 3602 |
. . 3
⊢ (𝑛 ∈ {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ↔ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) |
3 | | zcn 12181 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
4 | 3 | ad2antrl 728 |
. . . . . 6
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → 𝑛 ∈ ℂ) |
5 | | peano5uzi.1 |
. . . . . . . 8
⊢ 𝑁 ∈ ℤ |
6 | | zcn 12181 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ 𝑁 ∈ ℂ |
8 | | ax-1cn 10787 |
. . . . . . 7
⊢ 1 ∈
ℂ |
9 | 7, 8 | subcli 11154 |
. . . . . 6
⊢ (𝑁 − 1) ∈
ℂ |
10 | | npcan 11087 |
. . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ)
→ ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) = 𝑛) |
11 | 4, 9, 10 | sylancl 589 |
. . . . 5
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) = 𝑛) |
12 | | subsub 11108 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
(𝑁 − 1)) = ((𝑛 − 𝑁) + 1)) |
13 | 7, 8, 12 | mp3an23 1455 |
. . . . . . . 8
⊢ (𝑛 ∈ ℂ → (𝑛 − (𝑁 − 1)) = ((𝑛 − 𝑁) + 1)) |
14 | 4, 13 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → (𝑛 − (𝑁 − 1)) = ((𝑛 − 𝑁) + 1)) |
15 | | znn0sub 12224 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 ≤ 𝑛 ↔ (𝑛 − 𝑁) ∈
ℕ0)) |
16 | 5, 15 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (𝑁 ≤ 𝑛 ↔ (𝑛 − 𝑁) ∈
ℕ0)) |
17 | 16 | biimpa 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛) → (𝑛 − 𝑁) ∈
ℕ0) |
18 | 17 | adantl 485 |
. . . . . . . 8
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → (𝑛 − 𝑁) ∈
ℕ0) |
19 | | nn0p1nn 12129 |
. . . . . . . 8
⊢ ((𝑛 − 𝑁) ∈ ℕ0 → ((𝑛 − 𝑁) + 1) ∈ ℕ) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → ((𝑛 − 𝑁) + 1) ∈ ℕ) |
21 | 14, 20 | eqeltrd 2838 |
. . . . . 6
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → (𝑛 − (𝑁 − 1)) ∈
ℕ) |
22 | | simpl 486 |
. . . . . 6
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) |
23 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (𝑘 + (𝑁 − 1)) = (1 + (𝑁 − 1))) |
24 | 23 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = 1 → ((𝑘 + (𝑁 − 1)) ∈ 𝐴 ↔ (1 + (𝑁 − 1)) ∈ 𝐴)) |
25 | 24 | imbi2d 344 |
. . . . . . 7
⊢ (𝑘 = 1 → (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑘 + (𝑁 − 1)) ∈ 𝐴) ↔ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (1 + (𝑁 − 1)) ∈ 𝐴))) |
26 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 + (𝑁 − 1)) = (𝑛 + (𝑁 − 1))) |
27 | 26 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝑘 + (𝑁 − 1)) ∈ 𝐴 ↔ (𝑛 + (𝑁 − 1)) ∈ 𝐴)) |
28 | 27 | imbi2d 344 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑘 + (𝑁 − 1)) ∈ 𝐴) ↔ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑛 + (𝑁 − 1)) ∈ 𝐴))) |
29 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑘 = (𝑛 + 1) → (𝑘 + (𝑁 − 1)) = ((𝑛 + 1) + (𝑁 − 1))) |
30 | 29 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = (𝑛 + 1) → ((𝑘 + (𝑁 − 1)) ∈ 𝐴 ↔ ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴)) |
31 | 30 | imbi2d 344 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑘 + (𝑁 − 1)) ∈ 𝐴) ↔ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴))) |
32 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑘 = (𝑛 − (𝑁 − 1)) → (𝑘 + (𝑁 − 1)) = ((𝑛 − (𝑁 − 1)) + (𝑁 − 1))) |
33 | 32 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = (𝑛 − (𝑁 − 1)) → ((𝑘 + (𝑁 − 1)) ∈ 𝐴 ↔ ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) ∈ 𝐴)) |
34 | 33 | imbi2d 344 |
. . . . . . 7
⊢ (𝑘 = (𝑛 − (𝑁 − 1)) → (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑘 + (𝑁 − 1)) ∈ 𝐴) ↔ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) ∈ 𝐴))) |
35 | 8, 7 | pncan3i 11155 |
. . . . . . . 8
⊢ (1 +
(𝑁 − 1)) = 𝑁 |
36 | | simpl 486 |
. . . . . . . 8
⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → 𝑁 ∈ 𝐴) |
37 | 35, 36 | eqeltrid 2842 |
. . . . . . 7
⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (1 + (𝑁 − 1)) ∈ 𝐴) |
38 | | oveq1 7220 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 + (𝑁 − 1)) → (𝑥 + 1) = ((𝑛 + (𝑁 − 1)) + 1)) |
39 | 38 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑛 + (𝑁 − 1)) → ((𝑥 + 1) ∈ 𝐴 ↔ ((𝑛 + (𝑁 − 1)) + 1) ∈ 𝐴)) |
40 | 39 | rspccv 3534 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 + 1) ∈ 𝐴 → ((𝑛 + (𝑁 − 1)) ∈ 𝐴 → ((𝑛 + (𝑁 − 1)) + 1) ∈ 𝐴)) |
41 | 40 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) → ((𝑛 + (𝑁 − 1)) ∈ 𝐴 → ((𝑛 + (𝑁 − 1)) + 1) ∈ 𝐴)) |
42 | | nncn 11838 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
43 | 42 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) → 𝑛 ∈ ℂ) |
44 | | add32 11050 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ ∧
1 ∈ ℂ) → ((𝑛 + (𝑁 − 1)) + 1) = ((𝑛 + 1) + (𝑁 − 1))) |
45 | 9, 8, 44 | mp3an23 1455 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → ((𝑛 + (𝑁 − 1)) + 1) = ((𝑛 + 1) + (𝑁 − 1))) |
46 | 43, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) → ((𝑛 + (𝑁 − 1)) + 1) = ((𝑛 + 1) + (𝑁 − 1))) |
47 | 46 | eleq1d 2822 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) → (((𝑛 + (𝑁 − 1)) + 1) ∈ 𝐴 ↔ ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴)) |
48 | 41, 47 | sylibd 242 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴)) → ((𝑛 + (𝑁 − 1)) ∈ 𝐴 → ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴)) |
49 | 48 | ex 416 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 + (𝑁 − 1)) ∈ 𝐴 → ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴))) |
50 | 49 | a2d 29 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑛 + (𝑁 − 1)) ∈ 𝐴) → ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 + 1) + (𝑁 − 1)) ∈ 𝐴))) |
51 | 25, 28, 31, 34, 37, 50 | nnind 11848 |
. . . . . 6
⊢ ((𝑛 − (𝑁 − 1)) ∈ ℕ → ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) ∈ 𝐴)) |
52 | 21, 22, 51 | sylc 65 |
. . . . 5
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → ((𝑛 − (𝑁 − 1)) + (𝑁 − 1)) ∈ 𝐴) |
53 | 11, 52 | eqeltrrd 2839 |
. . . 4
⊢ (((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛)) → 𝑛 ∈ 𝐴) |
54 | 53 | ex 416 |
. . 3
⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((𝑛 ∈ ℤ ∧ 𝑁 ≤ 𝑛) → 𝑛 ∈ 𝐴)) |
55 | 2, 54 | syl5bi 245 |
. 2
⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑛 ∈ {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} → 𝑛 ∈ 𝐴)) |
56 | 55 | ssrdv 3907 |
1
⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ⊆ 𝐴) |