This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0ennn

Description: The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004)

Ref Expression
Assertion nn0ennn ℕ0 ≈ ℕ

Proof

Step Hyp Ref Expression
1 nn0ex ⊢ ℕ0 ∈ V
2 nnex ⊢ ℕ ∈ V
3 nn0p1nn ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 1 ) ∈ ℕ )
4 nnm1nn0 ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 − 1 ) ∈ ℕ0 )
5 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
6 nn0cn ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 subadd ⊢ ( ( 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑥 ↔ ( 1 + 𝑥 ) = 𝑦 ) )
9 7 8 mp3an2 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑥 ↔ ( 1 + 𝑥 ) = 𝑦 ) )
10 eqcom ⊢ ( 𝑥 = ( 𝑦 − 1 ) ↔ ( 𝑦 − 1 ) = 𝑥 )
11 eqcom ⊢ ( 𝑦 = ( 1 + 𝑥 ) ↔ ( 1 + 𝑥 ) = 𝑦 )
12 9 10 11 3bitr4g ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 1 + 𝑥 ) ) )
13 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 + 𝑥 ) = ( 𝑥 + 1 ) )
14 7 13 mpan ⊢ ( 𝑥 ∈ ℂ → ( 1 + 𝑥 ) = ( 𝑥 + 1 ) )
15 14 eqeq2d ⊢ ( 𝑥 ∈ ℂ → ( 𝑦 = ( 1 + 𝑥 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
16 15 adantl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 = ( 1 + 𝑥 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
17 12 16 bitrd ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
18 5 6 17 syl2anr ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
19 1 2 3 4 18 en3i ⊢ ℕ0 ≈ ℕ