Step | Hyp | Ref
| Expression |
1 | | prmind.5 |
. 2
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂)) |
2 | | oveq2 5858 |
. . . 4
⊢ (𝑛 = 1 → (1...𝑛) = (1...1)) |
3 | 2 | raleqdv 2671 |
. . 3
⊢ (𝑛 = 1 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...1)𝜑)) |
4 | | oveq2 5858 |
. . . 4
⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘)) |
5 | 4 | raleqdv 2671 |
. . 3
⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝑘)𝜑)) |
6 | | oveq2 5858 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1))) |
7 | 6 | raleqdv 2671 |
. . 3
⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...(𝑘 + 1))𝜑)) |
8 | | oveq2 5858 |
. . . 4
⊢ (𝑛 = 𝐴 → (1...𝑛) = (1...𝐴)) |
9 | 8 | raleqdv 2671 |
. . 3
⊢ (𝑛 = 𝐴 → (∀𝑥 ∈ (1...𝑛)𝜑 ↔ ∀𝑥 ∈ (1...𝐴)𝜑)) |
10 | | prmind.6 |
. . . . 5
⊢ 𝜓 |
11 | | elfz1eq 9978 |
. . . . . 6
⊢ (𝑥 ∈ (1...1) → 𝑥 = 1) |
12 | | prmind.1 |
. . . . . 6
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝑥 ∈ (1...1) → (𝜑 ↔ 𝜓)) |
14 | 10, 13 | mpbiri 167 |
. . . 4
⊢ (𝑥 ∈ (1...1) → 𝜑) |
15 | 14 | rgen 2523 |
. . 3
⊢
∀𝑥 ∈
(1...1)𝜑 |
16 | | peano2nn 8877 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
17 | 16 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℕ) |
18 | 17 | nncnd 8879 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℂ) |
19 | | elfzuz 9964 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈
(ℤ≥‘2)) |
20 | 19 | ad2antrl 487 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈
(ℤ≥‘2)) |
21 | | eluz2nn 9512 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℕ) |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℕ) |
23 | 22 | nncnd 8879 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℂ) |
24 | 22 | nnap0d 8911 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 # 0) |
25 | 18, 23, 24 | divcanap2d 8696 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 · ((𝑘 + 1) / 𝑦)) = (𝑘 + 1)) |
26 | | simprr 527 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∥ (𝑘 + 1)) |
27 | 22 | nnzd 9320 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℤ) |
28 | 22 | nnne0d 8910 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≠ 0) |
29 | 17 | nnzd 9320 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℤ) |
30 | | dvdsval2 11739 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ (𝑘 + 1) ∈ ℤ) →
(𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ)) |
31 | 27, 28, 29, 30 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∥ (𝑘 + 1) ↔ ((𝑘 + 1) / 𝑦) ∈ ℤ)) |
32 | 26, 31 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℤ) |
33 | 23 | mulid2d 7925 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) = 𝑦) |
34 | | elfzle2 9971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ≤ ((𝑘 + 1) − 1)) |
35 | 34 | ad2antrl 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ ((𝑘 + 1) − 1)) |
36 | | nncn 8873 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
37 | 36 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℂ) |
38 | | ax-1cn 7854 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
39 | | pncan 8112 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
40 | 37, 38, 39 | sylancl 411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) − 1) = 𝑘) |
41 | 35, 40 | breqtrd 4013 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ≤ 𝑘) |
42 | | nnz 9218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
43 | 42 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑘 ∈ ℤ) |
44 | | zleltp1 9254 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
45 | 27, 43, 44 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ≤ 𝑘 ↔ 𝑦 < (𝑘 + 1))) |
46 | 41, 45 | mpbid 146 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 < (𝑘 + 1)) |
47 | 33, 46 | eqbrtrd 4009 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (1 · 𝑦) < (𝑘 + 1)) |
48 | | 1red 7922 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 ∈
ℝ) |
49 | 17 | nnred 8878 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
50 | 22 | nnred 8878 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ) |
51 | 22 | nngt0d 8909 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < 𝑦) |
52 | | ltmuldiv 8777 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ (𝑘 +
1) ∈ ℝ ∧ (𝑦
∈ ℝ ∧ 0 < 𝑦)) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦))) |
53 | 48, 49, 50, 51, 52 | syl112anc 1237 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((1 · 𝑦) < (𝑘 + 1) ↔ 1 < ((𝑘 + 1) / 𝑦))) |
54 | 47, 53 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < ((𝑘 + 1) / 𝑦)) |
55 | | eluz2b1 9547 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ≥‘2)
↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 1 <
((𝑘 + 1) / 𝑦))) |
56 | 32, 54, 55 | sylanbrc 415 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈
(ℤ≥‘2)) |
57 | | prmind.2 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
58 | | simplr 525 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑥 ∈ (1...𝑘)𝜑) |
59 | | fznn 10032 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘))) |
60 | 43, 59 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑦 ∈ (1...𝑘) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑘))) |
61 | 22, 41, 60 | mpbir2and 939 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ (1...𝑘)) |
62 | 57, 58, 61 | rspcdva 2839 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝜒) |
63 | | vex 2733 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
64 | | prmind.3 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃)) |
65 | 63, 64 | sbcie 2989 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑥]𝜑 ↔ 𝜃) |
66 | | dfsbcq 2957 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([𝑧 / 𝑥]𝜑 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
67 | 65, 66 | bitr3id 193 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝜃 ↔ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
68 | 64 | cbvralv 2696 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(1...𝑘)𝜑 ↔ ∀𝑧 ∈ (1...𝑘)𝜃) |
69 | 58, 68 | sylib 121 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ∀𝑧 ∈ (1...𝑘)𝜃) |
70 | 17 | nnrpd 9638 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) ∈
ℝ+) |
71 | 22 | nnrpd 9638 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 𝑦 ∈ ℝ+) |
72 | 70, 71 | rpdivcld 9658 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈
ℝ+) |
73 | 72 | rpgt0d 9643 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < ((𝑘 + 1) / 𝑦)) |
74 | | elnnz 9209 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 + 1) / 𝑦) ∈ ℕ ↔ (((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 0 < ((𝑘 + 1) / 𝑦))) |
75 | 32, 73, 74 | sylanbrc 415 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ ℕ) |
76 | 17 | nnap0d 8911 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝑘 + 1) # 0) |
77 | 18, 76 | dividapd 8690 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) = 1) |
78 | | eluz2gt1 9548 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈
(ℤ≥‘2) → 1 < 𝑦) |
79 | 20, 78 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 1 < 𝑦) |
80 | 77, 79 | eqbrtrd 4009 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / (𝑘 + 1)) < 𝑦) |
81 | 17 | nngt0d 8909 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → 0 < (𝑘 + 1)) |
82 | | ltdiv23 8795 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 + 1) ∈ ℝ ∧
((𝑘 + 1) ∈ ℝ
∧ 0 < (𝑘 + 1)) ∧
(𝑦 ∈ ℝ ∧ 0
< 𝑦)) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
83 | 49, 49, 81, 50, 51, 82 | syl122anc 1242 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / (𝑘 + 1)) < 𝑦 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
84 | 80, 83 | mpbid 146 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) < (𝑘 + 1)) |
85 | | zleltp1 9254 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑘 + 1) / 𝑦) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
86 | 32, 43, 85 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ≤ 𝑘 ↔ ((𝑘 + 1) / 𝑦) < (𝑘 + 1))) |
87 | 84, 86 | mpbird 166 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ≤ 𝑘) |
88 | | fznn 10032 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘))) |
89 | 43, 88 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (((𝑘 + 1) / 𝑦) ∈ (1...𝑘) ↔ (((𝑘 + 1) / 𝑦) ∈ ℕ ∧ ((𝑘 + 1) / 𝑦) ≤ 𝑘))) |
90 | 75, 87, 89 | mpbir2and 939 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → ((𝑘 + 1) / 𝑦) ∈ (1...𝑘)) |
91 | 67, 69, 90 | rspcdva 2839 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) |
92 | 62, 91 | jca 304 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑)) |
93 | 67 | anbi2d 461 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑))) |
94 | | oveq2 5858 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (𝑦 · 𝑧) = (𝑦 · ((𝑘 + 1) / 𝑦))) |
95 | 94 | sbceq1d 2960 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)) |
96 | 93, 95 | imbi12d 233 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → (((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑) ↔ ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))) |
97 | 96 | imbi2d 229 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((𝑘 + 1) / 𝑦) → ((𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) ↔ (𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧
[((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑)))) |
98 | | prmind2.8 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → 𝜏)) |
99 | 98 | ancoms 266 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → 𝜏)) |
100 | | eluzelz 9483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
101 | 100 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ 𝑦 ∈
ℤ) |
102 | | eluzelz 9483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
103 | 102 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℤ) |
104 | 101, 103 | zmulcld 9327 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ (𝑦 · 𝑧) ∈
ℤ) |
105 | | prmind.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏)) |
106 | 105 | sbcieg 2987 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 · 𝑧) ∈ ℤ → ([(𝑦 · 𝑧) / 𝑥]𝜑 ↔ 𝜏)) |
107 | 104, 106 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ([(𝑦 ·
𝑧) / 𝑥]𝜑 ↔ 𝜏)) |
108 | 99, 107 | sylibrd 168 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑦 ∈ (ℤ≥‘2))
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑)) |
109 | 108 | ex 114 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
(ℤ≥‘2) → (𝑦 ∈ (ℤ≥‘2)
→ ((𝜒 ∧ 𝜃) → [(𝑦 · 𝑧) / 𝑥]𝜑))) |
110 | 97, 109 | vtoclga 2796 |
. . . . . . . . . . 11
⊢ (((𝑘 + 1) / 𝑦) ∈ (ℤ≥‘2)
→ (𝑦 ∈
(ℤ≥‘2) → ((𝜒 ∧ [((𝑘 + 1) / 𝑦) / 𝑥]𝜑) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑))) |
111 | 56, 20, 92, 110 | syl3c 63 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑦 · ((𝑘 + 1) / 𝑦)) / 𝑥]𝜑) |
112 | 25, 111 | sbceq1dd 2961 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ (𝑦 ∈ (2...((𝑘 + 1) − 1)) ∧ 𝑦 ∥ (𝑘 + 1))) → [(𝑘 + 1) / 𝑥]𝜑) |
113 | 112 | rexlimdvaa 2588 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
114 | | ralnex 2458 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
(2...((𝑘 + 1) − 1))
¬ 𝑦 ∥ (𝑘 + 1) ↔ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)) |
115 | | simpl 108 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℕ) |
116 | | elnnuz 9510 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
117 | 115, 116 | sylib 121 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈
(ℤ≥‘1)) |
118 | | eluzp1p1 9499 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘1) → (𝑘 + 1) ∈ (ℤ≥‘(1
+ 1))) |
119 | 117, 118 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ (ℤ≥‘(1
+ 1))) |
120 | | df-2 8924 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
121 | 120 | fveq2i 5497 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
122 | 119, 121 | eleqtrrdi 2264 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈
(ℤ≥‘2)) |
123 | | isprm3 12059 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ ℙ ↔
((𝑘 + 1) ∈
(ℤ≥‘2) ∧ ∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1))) |
124 | 123 | baibr 915 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈
(ℤ≥‘2) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ)) |
125 | 122, 124 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) ↔ (𝑘 + 1) ∈ ℙ)) |
126 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑥 ∈ (1...𝑘)𝜑) |
127 | 57 | cbvralv 2696 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(1...𝑘)𝜑 ↔ ∀𝑦 ∈ (1...𝑘)𝜒) |
128 | 126, 127 | sylib 121 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...𝑘)𝜒) |
129 | 115 | nncnd 8879 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℂ) |
130 | 129, 38, 39 | sylancl 411 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) = 𝑘) |
131 | 130 | oveq2d 5866 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (1...((𝑘 + 1) − 1)) = (1...𝑘)) |
132 | 131 | raleqdv 2671 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 ↔ ∀𝑦 ∈ (1...𝑘)𝜒)) |
133 | 128, 132 | mpbird 166 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒) |
134 | | nfcv 2312 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑘 + 1) |
135 | | nfv 1521 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 |
136 | | nfsbc1v 2973 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥[(𝑘 + 1) / 𝑥]𝜑 |
137 | 135, 136 | nfim 1565 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑) |
138 | | oveq1 5857 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑘 + 1) → (𝑥 − 1) = ((𝑘 + 1) − 1)) |
139 | 138 | oveq2d 5866 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑘 + 1) → (1...(𝑥 − 1)) = (1...((𝑘 + 1) − 1))) |
140 | 139 | raleqdv 2671 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (∀𝑦 ∈ (1...(𝑥 − 1))𝜒 ↔ ∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒)) |
141 | | sbceq1a 2964 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
142 | 140, 141 | imbi12d 233 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → ((∀𝑦 ∈ (1...(𝑥 − 1))𝜒 → 𝜑) ↔ (∀𝑦 ∈ (1...((𝑘 + 1) − 1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑))) |
143 | | prmind2.7 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℙ ∧
∀𝑦 ∈
(1...(𝑥 − 1))𝜒) → 𝜑) |
144 | 143 | ex 114 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℙ →
(∀𝑦 ∈
(1...(𝑥 − 1))𝜒 → 𝜑)) |
145 | 134, 137,
142, 144 | vtoclgaf 2795 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ ℙ →
(∀𝑦 ∈
(1...((𝑘 + 1) −
1))𝜒 → [(𝑘 + 1) / 𝑥]𝜑)) |
146 | 133, 145 | syl5com 29 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) ∈ ℙ → [(𝑘 + 1) / 𝑥]𝜑)) |
147 | 125, 146 | sylbid 149 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∀𝑦 ∈ (2...((𝑘 + 1) − 1)) ¬ 𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
148 | 114, 147 | syl5bir 152 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → [(𝑘 + 1) / 𝑥]𝜑)) |
149 | | 2z 9227 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
150 | 149 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 2 ∈ ℤ) |
151 | 115 | nnzd 9320 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 𝑘 ∈ ℤ) |
152 | 151 | peano2zd 9324 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (𝑘 + 1) ∈ ℤ) |
153 | | 1zzd 9226 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → 1 ∈ ℤ) |
154 | 152, 153 | zsubcld 9326 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → ((𝑘 + 1) − 1) ∈
ℤ) |
155 | 19, 21 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (2...((𝑘 + 1) − 1)) → 𝑦 ∈
ℕ) |
156 | | dvdsdc 11747 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ (𝑘 + 1) ∈ ℤ) →
DECID 𝑦
∥ (𝑘 +
1)) |
157 | 155, 152,
156 | syl2anr 288 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) ∧ 𝑦 ∈ (2...((𝑘 + 1) − 1))) →
DECID 𝑦
∥ (𝑘 +
1)) |
158 | 150, 154,
157 | exfzdc 10183 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1)) |
159 | | exmiddc 831 |
. . . . . . . . 9
⊢
(DECID ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))) |
160 | 158, 159 | syl 14 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → (∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1) ∨ ¬ ∃𝑦 ∈ (2...((𝑘 + 1) − 1))𝑦 ∥ (𝑘 + 1))) |
161 | 113, 148,
160 | mpjaod 713 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧
∀𝑥 ∈ (1...𝑘)𝜑) → [(𝑘 + 1) / 𝑥]𝜑) |
162 | 161 | ex 114 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → [(𝑘 + 1) / 𝑥]𝜑)) |
163 | | ralsnsg 3618 |
. . . . . . 7
⊢ ((𝑘 + 1) ∈ ℕ →
(∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
164 | 16, 163 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈ {(𝑘 + 1)}𝜑 ↔ [(𝑘 + 1) / 𝑥]𝜑)) |
165 | 162, 164 | sylibrd 168 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → ∀𝑥 ∈ {(𝑘 + 1)}𝜑)) |
166 | 165 | ancld 323 |
. . . 4
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))) |
167 | | fzsuc 10012 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
168 | 116, 167 | sylbi 120 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
169 | 168 | raleqdv 2671 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...(𝑘 + 1))𝜑 ↔ ∀𝑥 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})𝜑)) |
170 | | ralunb 3308 |
. . . . 5
⊢
(∀𝑥 ∈
((1...𝑘) ∪ {(𝑘 + 1)})𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑)) |
171 | 169, 170 | bitrdi 195 |
. . . 4
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...(𝑘 + 1))𝜑 ↔ (∀𝑥 ∈ (1...𝑘)𝜑 ∧ ∀𝑥 ∈ {(𝑘 + 1)}𝜑))) |
172 | 166, 171 | sylibrd 168 |
. . 3
⊢ (𝑘 ∈ ℕ →
(∀𝑥 ∈
(1...𝑘)𝜑 → ∀𝑥 ∈ (1...(𝑘 + 1))𝜑)) |
173 | 3, 5, 7, 9, 15, 172 | nnind 8881 |
. 2
⊢ (𝐴 ∈ ℕ →
∀𝑥 ∈ (1...𝐴)𝜑) |
174 | | elfz1end 9998 |
. . 3
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) |
175 | 174 | biimpi 119 |
. 2
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ (1...𝐴)) |
176 | 1, 173, 175 | rspcdva 2839 |
1
⊢ (𝐴 ∈ ℕ → 𝜂) |