Step | Hyp | Ref
| Expression |
1 | | nn0p1nn 12272 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ (𝐴 + 1) ∈
ℕ) |
2 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑎 = 1 → (𝑎 − 1) = (1 − 1)) |
3 | 2 | sbceq1d 3721 |
. . . . . 6
⊢ (𝑎 = 1 → ([(𝑎 − 1) / 𝑥]𝜑 ↔ [(1 − 1) / 𝑥]𝜑)) |
4 | | dfsbcq 3718 |
. . . . . 6
⊢ (𝑎 = 1 → ([𝑎 / 𝑥]𝜑 ↔ [1 / 𝑥]𝜑)) |
5 | 3, 4 | anbi12d 631 |
. . . . 5
⊢ (𝑎 = 1 → (([(𝑎 − 1) / 𝑥]𝜑 ∧ [𝑎 / 𝑥]𝜑) ↔ ([(1 − 1) / 𝑥]𝜑 ∧ [1 / 𝑥]𝜑))) |
6 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑎 = 𝑦 → (𝑎 − 1) = (𝑦 − 1)) |
7 | 6 | sbceq1d 3721 |
. . . . . 6
⊢ (𝑎 = 𝑦 → ([(𝑎 − 1) / 𝑥]𝜑 ↔ [(𝑦 − 1) / 𝑥]𝜑)) |
8 | | dfsbcq 3718 |
. . . . . 6
⊢ (𝑎 = 𝑦 → ([𝑎 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
9 | 7, 8 | anbi12d 631 |
. . . . 5
⊢ (𝑎 = 𝑦 → (([(𝑎 − 1) / 𝑥]𝜑 ∧ [𝑎 / 𝑥]𝜑) ↔ ([(𝑦 − 1) / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑))) |
10 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑎 = (𝑦 + 1) → (𝑎 − 1) = ((𝑦 + 1) − 1)) |
11 | 10 | sbceq1d 3721 |
. . . . . 6
⊢ (𝑎 = (𝑦 + 1) → ([(𝑎 − 1) / 𝑥]𝜑 ↔ [((𝑦 + 1) − 1) / 𝑥]𝜑)) |
12 | | dfsbcq 3718 |
. . . . . 6
⊢ (𝑎 = (𝑦 + 1) → ([𝑎 / 𝑥]𝜑 ↔ [(𝑦 + 1) / 𝑥]𝜑)) |
13 | 11, 12 | anbi12d 631 |
. . . . 5
⊢ (𝑎 = (𝑦 + 1) → (([(𝑎 − 1) / 𝑥]𝜑 ∧ [𝑎 / 𝑥]𝜑) ↔ ([((𝑦 + 1) − 1) / 𝑥]𝜑 ∧ [(𝑦 + 1) / 𝑥]𝜑))) |
14 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑎 = (𝐴 + 1) → (𝑎 − 1) = ((𝐴 + 1) − 1)) |
15 | 14 | sbceq1d 3721 |
. . . . . 6
⊢ (𝑎 = (𝐴 + 1) → ([(𝑎 − 1) / 𝑥]𝜑 ↔ [((𝐴 + 1) − 1) / 𝑥]𝜑)) |
16 | | dfsbcq 3718 |
. . . . . 6
⊢ (𝑎 = (𝐴 + 1) → ([𝑎 / 𝑥]𝜑 ↔ [(𝐴 + 1) / 𝑥]𝜑)) |
17 | 15, 16 | anbi12d 631 |
. . . . 5
⊢ (𝑎 = (𝐴 + 1) → (([(𝑎 − 1) / 𝑥]𝜑 ∧ [𝑎 / 𝑥]𝜑) ↔ ([((𝐴 + 1) − 1) / 𝑥]𝜑 ∧ [(𝐴 + 1) / 𝑥]𝜑))) |
18 | | 2nn0ind.1 |
. . . . . . 7
⊢ 𝜓 |
19 | | ovex 7308 |
. . . . . . . 8
⊢ (1
− 1) ∈ V |
20 | | 1m1e0 12045 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
21 | 20 | eqeq2i 2751 |
. . . . . . . . 9
⊢ (𝑥 = (1 − 1) ↔ 𝑥 = 0) |
22 | | 2nn0ind.4 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) |
23 | 21, 22 | sylbi 216 |
. . . . . . . 8
⊢ (𝑥 = (1 − 1) → (𝜑 ↔ 𝜓)) |
24 | 19, 23 | sbcie 3759 |
. . . . . . 7
⊢
([(1 − 1) / 𝑥]𝜑 ↔ 𝜓) |
25 | 18, 24 | mpbir 230 |
. . . . . 6
⊢
[(1 − 1) / 𝑥]𝜑 |
26 | | 2nn0ind.2 |
. . . . . . 7
⊢ 𝜒 |
27 | | 1ex 10971 |
. . . . . . . 8
⊢ 1 ∈
V |
28 | | 2nn0ind.5 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒)) |
29 | 27, 28 | sbcie 3759 |
. . . . . . 7
⊢
([1 / 𝑥]𝜑 ↔ 𝜒) |
30 | 26, 29 | mpbir 230 |
. . . . . 6
⊢ [1
/ 𝑥]𝜑 |
31 | 25, 30 | pm3.2i 471 |
. . . . 5
⊢
([(1 − 1) / 𝑥]𝜑 ∧ [1 / 𝑥]𝜑) |
32 | | simprr 770 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → [𝑦 / 𝑥]𝜑) |
33 | | nncn 11981 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
34 | | ax-1cn 10929 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
35 | | pncan 11227 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑦 + 1)
− 1) = 𝑦) |
36 | 33, 34, 35 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦) |
37 | 36 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → ((𝑦 + 1) − 1) = 𝑦) |
38 | 37 | sbceq1d 3721 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → ([((𝑦 + 1) − 1) / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
39 | 32, 38 | mpbird 256 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → [((𝑦 + 1) − 1) / 𝑥]𝜑) |
40 | | 2nn0ind.3 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((𝜃 ∧ 𝜏) → 𝜂)) |
41 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝑦 − 1) ∈
V |
42 | | 2nn0ind.6 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 1) → (𝜑 ↔ 𝜃)) |
43 | 41, 42 | sbcie 3759 |
. . . . . . . . . 10
⊢
([(𝑦 −
1) / 𝑥]𝜑 ↔ 𝜃) |
44 | | vex 3436 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
45 | | 2nn0ind.7 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜏)) |
46 | 44, 45 | sbcie 3759 |
. . . . . . . . . 10
⊢
([𝑦 / 𝑥]𝜑 ↔ 𝜏) |
47 | 43, 46 | anbi12i 627 |
. . . . . . . . 9
⊢
(([(𝑦 −
1) / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜃 ∧ 𝜏)) |
48 | | ovex 7308 |
. . . . . . . . . 10
⊢ (𝑦 + 1) ∈ V |
49 | | 2nn0ind.8 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜂)) |
50 | 48, 49 | sbcie 3759 |
. . . . . . . . 9
⊢
([(𝑦 + 1) /
𝑥]𝜑 ↔ 𝜂) |
51 | 40, 47, 50 | 3imtr4g 296 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → [(𝑦 + 1) / 𝑥]𝜑)) |
52 | 51 | imp 407 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → [(𝑦 + 1) / 𝑥]𝜑) |
53 | 39, 52 | jca 512 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧
([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑)) → ([((𝑦 + 1) − 1) / 𝑥]𝜑 ∧ [(𝑦 + 1) / 𝑥]𝜑)) |
54 | 53 | ex 413 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
(([(𝑦 − 1) /
𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜑) → ([((𝑦 + 1) − 1) / 𝑥]𝜑 ∧ [(𝑦 + 1) / 𝑥]𝜑))) |
55 | 5, 9, 13, 17, 31, 54 | nnind 11991 |
. . . 4
⊢ ((𝐴 + 1) ∈ ℕ →
([((𝐴 + 1) −
1) / 𝑥]𝜑 ∧ [(𝐴 + 1) / 𝑥]𝜑)) |
56 | 1, 55 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℕ0
→ ([((𝐴 + 1)
− 1) / 𝑥]𝜑 ∧ [(𝐴 + 1) / 𝑥]𝜑)) |
57 | | nn0cn 12243 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
58 | | pncan 11227 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
59 | 57, 34, 58 | sylancl 586 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0
→ ((𝐴 + 1) − 1)
= 𝐴) |
60 | 59 | sbceq1d 3721 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ ([((𝐴 + 1)
− 1) / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
61 | 60 | biimpa 477 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ [((𝐴 + 1)
− 1) / 𝑥]𝜑) → [𝐴 / 𝑥]𝜑) |
62 | 61 | adantrr 714 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ ([((𝐴 + 1)
− 1) / 𝑥]𝜑 ∧ [(𝐴 + 1) / 𝑥]𝜑)) → [𝐴 / 𝑥]𝜑) |
63 | 56, 62 | mpdan 684 |
. 2
⊢ (𝐴 ∈ ℕ0
→ [𝐴 / 𝑥]𝜑) |
64 | | 2nn0ind.9 |
. . 3
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜌)) |
65 | 64 | sbcieg 3756 |
. 2
⊢ (𝐴 ∈ ℕ0
→ ([𝐴 / 𝑥]𝜑 ↔ 𝜌)) |
66 | 63, 65 | mpbid 231 |
1
⊢ (𝐴 ∈ ℕ0
→ 𝜌) |