Step |
Hyp |
Ref |
Expression |
1 |
|
neeq1 |
⊢ ( 𝑦 = 1 → ( 𝑦 ≠ 1 ↔ 1 ≠ 1 ) ) |
2 |
|
eqeq2 |
⊢ ( 𝑦 = 1 → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( 𝑥 + 1 ) = 1 ) ) |
3 |
2
|
rexbidv |
⊢ ( 𝑦 = 1 → ( ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 1 ) ) |
4 |
1 3
|
imbi12d |
⊢ ( 𝑦 = 1 → ( ( 𝑦 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ) ↔ ( 1 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 1 ) ) ) |
5 |
|
neeq1 |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≠ 1 ↔ 𝑧 ≠ 1 ) ) |
6 |
|
eqeq2 |
⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( 𝑥 + 1 ) = 𝑧 ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑧 ) ) |
8 |
5 7
|
imbi12d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ) ↔ ( 𝑧 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑧 ) ) ) |
9 |
|
neeq1 |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( 𝑦 ≠ 1 ↔ ( 𝑧 + 1 ) ≠ 1 ) ) |
10 |
|
eqeq2 |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) ) |
11 |
10
|
rexbidv |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) ) |
12 |
9 11
|
imbi12d |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( ( 𝑦 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ) ↔ ( ( 𝑧 + 1 ) ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) ) ) |
13 |
|
neeq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≠ 1 ↔ 𝐴 ≠ 1 ) ) |
14 |
|
eqeq2 |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( 𝑥 + 1 ) = 𝐴 ) ) |
15 |
14
|
rexbidv |
⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝐴 ) ) |
16 |
13 15
|
imbi12d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑦 ) ↔ ( 𝐴 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝐴 ) ) ) |
17 |
|
df-ne |
⊢ ( 1 ≠ 1 ↔ ¬ 1 = 1 ) |
18 |
|
eqid |
⊢ 1 = 1 |
19 |
18
|
pm2.24i |
⊢ ( ¬ 1 = 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 1 ) |
20 |
17 19
|
sylbi |
⊢ ( 1 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 1 ) |
21 |
|
id |
⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ ) |
22 |
|
oveq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) |
23 |
22
|
eqeq1d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ↔ ( 𝑧 + 1 ) = ( 𝑧 + 1 ) ) ) |
24 |
23
|
adantl |
⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑥 = 𝑧 ) → ( ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ↔ ( 𝑧 + 1 ) = ( 𝑧 + 1 ) ) ) |
25 |
|
eqidd |
⊢ ( 𝑧 ∈ ℕ → ( 𝑧 + 1 ) = ( 𝑧 + 1 ) ) |
26 |
21 24 25
|
rspcedvd |
⊢ ( 𝑧 ∈ ℕ → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) |
27 |
26
|
2a1d |
⊢ ( 𝑧 ∈ ℕ → ( ( 𝑧 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝑧 ) → ( ( 𝑧 + 1 ) ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = ( 𝑧 + 1 ) ) ) ) |
28 |
4 8 12 16 20 27
|
nnind |
⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ≠ 1 → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝐴 ) ) |
29 |
28
|
imp |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐴 ≠ 1 ) → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝐴 ) |