Step | Hyp | Ref
| Expression |
1 | | elfz1end 9074 |
. . 3
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) |
2 | 1 | biimpi 118 |
. 2
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴)) |
3 | | oveq2 5540 |
. . . 4
⊢ (𝑛 = 1 → (1...𝑛) = (1...1)) |
4 | 3 | raleqdv 2555 |
. . 3
⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑)) |
5 | | oveq2 5540 |
. . . 4
⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘)) |
6 | 5 | raleqdv 2555 |
. . 3
⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑)) |
7 | | oveq2 5540 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1))) |
8 | 7 | raleqdv 2555 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑)) |
9 | | oveq2 5540 |
. . . 4
⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴)) |
10 | 9 | raleqdv 2555 |
. . 3
⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑)) |
11 | | prmind.6 |
. . . . 5
⊢ 𝜓 |
12 | | elfz1eq 9054 |
. . . . . 6
⊢ (𝑥 ∈ (1...1) → 𝑥 = 1) |
13 | | prmind.1 |
. . . . . 6
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝑥 ∈ (1...1) → (𝜑 ↔ 𝜓)) |
15 | 11, 14 | mpbiri 166 |
. . . 4
⊢ (𝑥 ∈ (1...1) → 𝜑) |
16 | 15 | rgen 2416 |
. . 3
⊢
∀𝑥 ∈
(1...1)𝜑 |
17 | | peano2nn 8051 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
18 | 17 | ad2antrr 471 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ) |
19 | 18 | nncnd 8053 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ) |
20 | | elfzuz 9041 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈
(ℤ≥‘2)) |
21 | 20 | ad2antrl 473 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈
(ℤ≥‘2)) |
22 | | eluz2nn 8657 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℕ) |
23 | 21, 22 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ) |
24 | 23 | nncnd 8053 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ) |
25 | 23 | nnap0d 8084 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 # 0) |
26 | 19, 24, 25 | divcanap2d 7879 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1)) |
27 | | simprr 498 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1)) |
28 | 23 | nnzd 8468 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ) |
29 | 23 | nnne0d 8083 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0) |
30 | 18 | nnzd 8468 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ) |
31 | | dvdsval2 10198 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) →
(𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ)) |
32 | 28, 29, 30, 31 | syl3anc 1169 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ)) |
33 | 27, 32 | mpbid 145 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ) |
34 | 24 | mulid2d 7137 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦) |
35 | | elfzle2 9047 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1)) |
36 | 35 | ad2antrl 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1)) |
37 | | nncn 8047 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
38 | 37 | ad2antrr 471 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ) |
39 | | ax-1cn 7069 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
40 | | pncan 7314 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
41 | 38, 39, 40 | sylancl 404 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘) |
42 | 36, 41 | breqtrd 3809 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘) |
43 | | nnz 8370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
44 | 43 | ad2antrr 471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ) |
45 | | zleltp1 8406 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
46 | 28, 44, 45 | syl2anc 403 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
47 | 42, 46 | mpbid 145 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1)) |
48 | 34, 47 | eqbrtrd 3805 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1)) |
49 | | 1red 7134 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈
ℝ) |
50 | 18 | nnred 8052 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
51 | 23 | nnred 8052 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ) |
52 | 23 | nngt0d 8082 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦) |
53 | | ltmuldiv 7952 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ (𝑘 +
1) ∈ ℝ ∧ (𝑦
∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦))) |
54 | 49, 50, 51, 52, 53 | syl112anc 1173 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦))) |
55 | 48, 54 | mpbid 145 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦)) |
56 | | eluz2b1 8688 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ≥‘2)
↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 <
((𝑘 + 1) / 𝑦))) |
57 | 33, 55, 56 | sylanbrc 408 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈
(ℤ≥‘2)) |
58 | | fznn 9106 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘))) |
59 | 44, 58 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘))) |
60 | 23, 42, 59 | mpbir2and 885 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘)) |
61 | | simplr 496 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑) |
62 | | prmind.2 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
63 | 62 | rspcv 2697 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...𝑘) → (∀𝑥 ∈ (1...𝑘)𝜑 → 𝜒)) |
64 | 60, 61, 63 | sylc 61 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒) |
65 | 18 | nnrpd 8772 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈
ℝ+) |
66 | 23 | nnrpd 8772 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ+) |
67 | 65, 66 | rpdivcld 8791 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈
ℝ+) |
68 | 67 | rpgt0d 8776 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦)) |
69 | | elnnz 8361 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦))) |
70 | 33, 68, 69 | sylanbrc 408 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ) |
71 | 18 | nnap0d 8084 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) # 0) |
72 | 19, 71 | dividapd 7874 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1) |
73 | | eluz2gt1 8689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈
(ℤ≥‘2) → 1 < 𝑦) |
74 | 21, 73 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦) |
75 | 72, 74 | eqbrtrd 3805 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦) |
76 | 18 | nngt0d 8082 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1)) |
77 | | ltdiv23 7970 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 + 1) ∈ ℝ ∧
((𝑘 + 1) ∈ ℝ
∧ 0 < (𝑘 + 1)) ∧
(𝑦 ∈ ℝ ∧ 0
< 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
78 | 50, 50, 76, 51, 52, 77 | syl122anc 1178 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
79 | 75, 78 | mpbid 145 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1)) |
80 | | zleltp1 8406 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
81 | 33, 44, 80 | syl2anc 403 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
82 | 79, 81 | mpbird 165 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘) |
83 | | fznn 9106 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘))) |
84 | 44, 83 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘))) |
85 | 70, 82, 84 | mpbir2and 885 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘)) |
86 | | prmind.3 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃)) |
87 | 86 | cbvralv 2577 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃) |
88 | 61, 87 | sylib 120 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃) |
89 | | vex 2604 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
90 | 89, 86 | sbcie 2848 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]𝜑 ↔ 𝜃) |
91 | | dfsbcq 2817 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
92 | 90, 91 | syl5bbr 192 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
93 | 92 | rspcv 2697 |
. . . . . . . . . . . . 13
⊢ (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) → (∀𝑧 ∈ (1...𝑘)𝜃 → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
94 | 85, 88, 93 | sylc 61 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) |
95 | 64, 94 | jca 300 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
96 | 92 | anbi2d 451 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))) |
97 | | oveq2 5540 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦))) |
98 | 97 | sbceq1d 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)) |
99 | 96, 98 | imbi12d 232 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑) ↔ ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))) |
100 | 99 | imbi2d 228 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) ↔ (𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧
[((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))) |
101 | | prmind2.8 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → 𝜏)) |
102 | 101 | ancoms 264 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → 𝜏)) |
103 | | eluzelz 8628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
104 | 103 | adantl 271 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ 𝑦 ∈
ℤ) |
105 | | eluzelz 8628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
106 | 105 | adantr 270 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℤ) |
107 | 104, 106 | zmulcld 8475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (𝑦 · 𝑧) ∈
ℤ) |
108 | | prmind.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏)) |
109 | 108 | sbcieg 2846 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 · 𝑧) ∈ ℤ → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏)) |
110 | 107, 109 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ([(𝑦 ·
𝑧) / 𝑥]𝜑 ↔ 𝜏)) |
111 | 102, 110 | sylibrd 167 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) |
112 | 111 | ex 113 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
(ℤ≥‘2) → (𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑))) |
113 | 100, 112 | vtoclga 2664 |
. . . . . . . . . . 11
⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ≥‘2)
→ (𝑦 ∈
(ℤ≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))) |
114 | 57, 21, 95, 113 | syl3c 62 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑) |
115 | 26, 114 | sbceq1dd 2821 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑) |
116 | 115 | rexlimdvaa 2478 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
117 | | ralnex 2358 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(2...((𝑘 + 1) − 1))
¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)) |
118 | | simpl 107 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ) |
119 | | elnnuz 8655 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
120 | 118, 119 | sylib 120 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈
(ℤ≥‘1)) |
121 | | eluzp1p1 8644 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘1) → (𝑘 + 1) ∈ (ℤ≥‘(1
+ 1))) |
122 | 120, 121 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ≥‘(1
+ 1))) |
123 | | df-2 8098 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
124 | 123 | fveq2i 5201 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
125 | 122, 124 | syl6eleqr 2172 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈
(ℤ≥‘2)) |
126 | | isprm3 10500 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ ℙ ↔
((𝑘 + 1) ∈
(ℤ≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1))) |
127 | 126 | baibr 862 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈
(ℤ≥‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ)) |
128 | 125, 127 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ)) |
129 | | simpr 108 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑥 ∈ (1...𝑘)𝜑) |
130 | 62 | cbvralv 2577 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒) |
131 | 129, 130 | sylib 120 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒) |
132 | 118 | nncnd 8053 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ) |
133 | 132, 39, 40 | sylancl 404 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘) |
134 | 133 | oveq2d 5548 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘)) |
135 | 134 | raleqdv 2555 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)) |
136 | 131, 135 | mpbird 165 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒) |
137 | | nfcv 2219 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑘 + 1) |
138 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 |
139 | | nfsbc1v 2833 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑 |
140 | 138, 139 | nfim 1504 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑) |
141 | | oveq1 5539 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1)) |
142 | 141 | oveq2d 5548 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1))) |
143 | 142 | raleqdv 2555 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)) |
144 | | sbceq1a 2824 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
145 | 143, 144 | imbi12d 232 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑))) |
146 | | prmind2.7 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℙ ∧
∀𝑦 ∈
(1...(𝑥 − 1))𝜒) → 𝜑) |
147 | 146 | ex 113 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℙ →
(∀𝑦 ∈
(1...(𝑥 − 1))𝜒 → 𝜑)) |
148 | 137, 140,
145, 147 | vtoclgaf 2663 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ ℙ →
(∀𝑦 ∈
(1...((𝑘 + 1) −
1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)) |
149 | 136, 148 | syl5com 29 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑)) |
150 | 128, 149 | sylbid 148 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
151 | 117, 150 | syl5bir 151 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
152 | | 2z 8379 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
153 | 152 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 2 ∈ ℤ) |
154 | 118 | nnzd 8468 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℤ) |
155 | 154 | peano2zd 8472 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ ℤ) |
156 | | 1zzd 8378 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 1 ∈ ℤ) |
157 | 155, 156 | zsubcld 8474 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) ∈
ℤ) |
158 | 20, 22 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈
ℕ) |
159 | | dvdsdc 10203 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ (𝑘 + 1) ∈ ℤ) →
DECID 𝑦
∥ (𝑘 +
1)) |
160 | 158, 155,
159 | syl2anr 284 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ 𝑦 ∈ (2...((𝑘 + 1) − 1))) →
DECID 𝑦
∥ (𝑘 +
1)) |
161 | 153, 157,
160 | exfzdc 9249 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)) |
162 | | exmiddc 777 |
. . . . . . . . 9
⊢
(DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))) |
163 | 161, 162 | syl 14 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))) |
164 | 116, 151,
163 | mpjaod 670 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑) |
165 | 164 | ex 113 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑)) |
166 | | ralsnsg 3430 |
. . . . . . 7
⊢ ((𝑘 + 1) ∈ ℕ →
(∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
167 | 17, 166 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
168 | 165, 167 | sylibrd 167 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑)) |
169 | 168 | ancld 318 |
. . . 4
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))) |
170 | | fzsuc 9086 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
171 | 119, 170 | sylbi 119 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
172 | 171 | raleqdv 2555 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑)) |
173 | | ralunb 3153 |
. . . . 5
⊢
(∀𝑥 ∈
((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)) |
174 | 172, 173 | syl6bb 194 |
. . . 4
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))) |
175 | 169, 174 | sylibrd 167 |
. . 3
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑)) |
176 | 4, 6, 8, 10, 16, 175 | nnind 8055 |
. 2
⊢ (𝐴 ∈ ℕ →
∀𝑥 ∈ (1...𝐴)𝜑) |
177 | | prmind.5 |
. . 3
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂)) |
178 | 177 | rspcv 2697 |
. 2
⊢ (𝐴 ∈ (1...𝐴) → (∀𝑥 ∈ (1...𝐴)𝜑 → 𝜂)) |
179 | 2, 176, 178 | sylc 61 |
1
⊢ (𝐴 ∈ ℕ → 𝜂) |