Proof of Theorem nn1suc
Step | Hyp | Ref
| Expression |
1 | | nn1suc.5 |
. . . . 5
⊢ 𝜓 |
2 | | 1ex 7915 |
. . . . . 6
⊢ 1 ∈
V |
3 | | nn1suc.1 |
. . . . . 6
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) |
4 | 2, 3 | sbcie 2989 |
. . . . 5
⊢
([1 / 𝑥]𝜑 ↔ 𝜓) |
5 | 1, 4 | mpbir 145 |
. . . 4
⊢ [1
/ 𝑥]𝜑 |
6 | | 1nn 8889 |
. . . . . . 7
⊢ 1 ∈
ℕ |
7 | | eleq1 2233 |
. . . . . . 7
⊢ (𝐴 = 1 → (𝐴 ∈ ℕ ↔ 1 ∈
ℕ)) |
8 | 6, 7 | mpbiri 167 |
. . . . . 6
⊢ (𝐴 = 1 → 𝐴 ∈ ℕ) |
9 | | nn1suc.4 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜃)) |
10 | 9 | sbcieg 2987 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
([𝐴 / 𝑥]𝜑 ↔ 𝜃)) |
11 | 8, 10 | syl 14 |
. . . . 5
⊢ (𝐴 = 1 → ([𝐴 / 𝑥]𝜑 ↔ 𝜃)) |
12 | | dfsbcq 2957 |
. . . . 5
⊢ (𝐴 = 1 → ([𝐴 / 𝑥]𝜑 ↔ [1 / 𝑥]𝜑)) |
13 | 11, 12 | bitr3d 189 |
. . . 4
⊢ (𝐴 = 1 → (𝜃 ↔ [1 / 𝑥]𝜑)) |
14 | 5, 13 | mpbiri 167 |
. . 3
⊢ (𝐴 = 1 → 𝜃) |
15 | 14 | a1i 9 |
. 2
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 → 𝜃)) |
16 | | elisset 2744 |
. . . 4
⊢ ((𝐴 − 1) ∈ ℕ
→ ∃𝑦 𝑦 = (𝐴 − 1)) |
17 | | eleq1 2233 |
. . . . . 6
⊢ (𝑦 = (𝐴 − 1) → (𝑦 ∈ ℕ ↔ (𝐴 − 1) ∈
ℕ)) |
18 | 17 | pm5.32ri 452 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) ↔ ((𝐴 − 1) ∈ ℕ ∧ 𝑦 = (𝐴 − 1))) |
19 | | nn1suc.6 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝜒) |
20 | 19 | adantr 274 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) → 𝜒) |
21 | | nnre 8885 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
22 | | peano2re 8055 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ) |
23 | | nn1suc.3 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒)) |
24 | 23 | sbcieg 2987 |
. . . . . . . . 9
⊢ ((𝑦 + 1) ∈ ℝ →
([(𝑦 + 1) / 𝑥]𝜑 ↔ 𝜒)) |
25 | 21, 22, 24 | 3syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
([(𝑦 + 1) / 𝑥]𝜑 ↔ 𝜒)) |
26 | 25 | adantr 274 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) → ([(𝑦 + 1) / 𝑥]𝜑 ↔ 𝜒)) |
27 | | oveq1 5860 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 − 1) → (𝑦 + 1) = ((𝐴 − 1) + 1)) |
28 | 27 | sbceq1d 2960 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 − 1) → ([(𝑦 + 1) / 𝑥]𝜑 ↔ [((𝐴 − 1) + 1) / 𝑥]𝜑)) |
29 | 28 | adantl 275 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) → ([(𝑦 + 1) / 𝑥]𝜑 ↔ [((𝐴 − 1) + 1) / 𝑥]𝜑)) |
30 | 26, 29 | bitr3d 189 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) → (𝜒 ↔ [((𝐴 − 1) + 1) / 𝑥]𝜑)) |
31 | 20, 30 | mpbid 146 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝑦 = (𝐴 − 1)) → [((𝐴 − 1) + 1) / 𝑥]𝜑) |
32 | 18, 31 | sylbir 134 |
. . . 4
⊢ (((𝐴 − 1) ∈ ℕ ∧
𝑦 = (𝐴 − 1)) → [((𝐴 − 1) + 1) / 𝑥]𝜑) |
33 | 16, 32 | exlimddv 1891 |
. . 3
⊢ ((𝐴 − 1) ∈ ℕ
→ [((𝐴 −
1) + 1) / 𝑥]𝜑) |
34 | | nncn 8886 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
35 | | ax-1cn 7867 |
. . . . . 6
⊢ 1 ∈
ℂ |
36 | | npcan 8128 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) + 1) = 𝐴) |
37 | 34, 35, 36 | sylancl 411 |
. . . . 5
⊢ (𝐴 ∈ ℕ → ((𝐴 − 1) + 1) = 𝐴) |
38 | 37 | sbceq1d 2960 |
. . . 4
⊢ (𝐴 ∈ ℕ →
([((𝐴 − 1) +
1) / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
39 | 38, 10 | bitrd 187 |
. . 3
⊢ (𝐴 ∈ ℕ →
([((𝐴 − 1) +
1) / 𝑥]𝜑 ↔ 𝜃)) |
40 | 33, 39 | syl5ib 153 |
. 2
⊢ (𝐴 ∈ ℕ → ((𝐴 − 1) ∈ ℕ
→ 𝜃)) |
41 | | nn1m1nn 8896 |
. 2
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈
ℕ)) |
42 | 15, 40, 41 | mpjaod 713 |
1
⊢ (𝐴 ∈ ℕ → 𝜃) |