Metamath Proof Explorer


Theorem peano5uzi

Description: Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 3-May-2014)

Ref Expression
Hypothesis peano5uzi.1 𝑁 ∈ ℤ
Assertion peano5uzi ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁𝑘 } ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 peano5uzi.1 𝑁 ∈ ℤ
2 breq2 ( 𝑘 = 𝑛 → ( 𝑁𝑘𝑁𝑛 ) )
3 2 elrab ( 𝑛 ∈ { 𝑘 ∈ ℤ ∣ 𝑁𝑘 } ↔ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) )
4 zcn ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
5 4 ad2antrl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → 𝑛 ∈ ℂ )
6 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7 1 6 ax-mp 𝑁 ∈ ℂ
8 ax-1cn 1 ∈ ℂ
9 7 8 subcli ( 𝑁 − 1 ) ∈ ℂ
10 npcan ( ( 𝑛 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℂ ) → ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) = 𝑛 )
11 5 9 10 sylancl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) = 𝑛 )
12 subsub ( ( 𝑛 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑛 − ( 𝑁 − 1 ) ) = ( ( 𝑛𝑁 ) + 1 ) )
13 7 8 12 mp3an23 ( 𝑛 ∈ ℂ → ( 𝑛 − ( 𝑁 − 1 ) ) = ( ( 𝑛𝑁 ) + 1 ) )
14 5 13 syl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( 𝑛 − ( 𝑁 − 1 ) ) = ( ( 𝑛𝑁 ) + 1 ) )
15 znn0sub ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑁𝑛 ↔ ( 𝑛𝑁 ) ∈ ℕ0 ) )
16 1 15 mpan ( 𝑛 ∈ ℤ → ( 𝑁𝑛 ↔ ( 𝑛𝑁 ) ∈ ℕ0 ) )
17 16 biimpa ( ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) → ( 𝑛𝑁 ) ∈ ℕ0 )
18 17 adantl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( 𝑛𝑁 ) ∈ ℕ0 )
19 nn0p1nn ( ( 𝑛𝑁 ) ∈ ℕ0 → ( ( 𝑛𝑁 ) + 1 ) ∈ ℕ )
20 18 19 syl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( ( 𝑛𝑁 ) + 1 ) ∈ ℕ )
21 14 20 eqeltrd ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( 𝑛 − ( 𝑁 − 1 ) ) ∈ ℕ )
22 simpl ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) )
23 oveq1 ( 𝑘 = 1 → ( 𝑘 + ( 𝑁 − 1 ) ) = ( 1 + ( 𝑁 − 1 ) ) )
24 23 eleq1d ( 𝑘 = 1 → ( ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ↔ ( 1 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
25 24 imbi2d ( 𝑘 = 1 → ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ↔ ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 1 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
26 oveq1 ( 𝑘 = 𝑛 → ( 𝑘 + ( 𝑁 − 1 ) ) = ( 𝑛 + ( 𝑁 − 1 ) ) )
27 26 eleq1d ( 𝑘 = 𝑛 → ( ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ↔ ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
28 27 imbi2d ( 𝑘 = 𝑛 → ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ↔ ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
29 oveq1 ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑘 + ( 𝑁 − 1 ) ) = ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) )
30 29 eleq1d ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ↔ ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
31 30 imbi2d ( 𝑘 = ( 𝑛 + 1 ) → ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ↔ ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
32 oveq1 ( 𝑘 = ( 𝑛 − ( 𝑁 − 1 ) ) → ( 𝑘 + ( 𝑁 − 1 ) ) = ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) )
33 32 eleq1d ( 𝑘 = ( 𝑛 − ( 𝑁 − 1 ) ) → ( ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ↔ ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
34 33 imbi2d ( 𝑘 = ( 𝑛 − ( 𝑁 − 1 ) ) → ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑘 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ↔ ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
35 8 7 pncan3i ( 1 + ( 𝑁 − 1 ) ) = 𝑁
36 simpl ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → 𝑁𝐴 )
37 35 36 eqeltrid ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 1 + ( 𝑁 − 1 ) ) ∈ 𝐴 )
38 oveq1 ( 𝑥 = ( 𝑛 + ( 𝑁 − 1 ) ) → ( 𝑥 + 1 ) = ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) )
39 38 eleq1d ( 𝑥 = ( 𝑛 + ( 𝑁 − 1 ) ) → ( ( 𝑥 + 1 ) ∈ 𝐴 ↔ ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) ∈ 𝐴 ) )
40 39 rspccv ( ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 → ( ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 → ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) ∈ 𝐴 ) )
41 40 ad2antll ( ( 𝑛 ∈ ℕ ∧ ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) → ( ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 → ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) ∈ 𝐴 ) )
42 nncn ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
43 42 adantr ( ( 𝑛 ∈ ℕ ∧ ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) → 𝑛 ∈ ℂ )
44 add32 ( ( 𝑛 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) = ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) )
45 9 8 44 mp3an23 ( 𝑛 ∈ ℂ → ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) = ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) )
46 43 45 syl ( ( 𝑛 ∈ ℕ ∧ ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) → ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) = ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) )
47 46 eleq1d ( ( 𝑛 ∈ ℕ ∧ ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) → ( ( ( 𝑛 + ( 𝑁 − 1 ) ) + 1 ) ∈ 𝐴 ↔ ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
48 41 47 sylibd ( ( 𝑛 ∈ ℕ ∧ ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) → ( ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 → ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
49 48 ex ( 𝑛 ∈ ℕ → ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 → ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
50 49 a2d ( 𝑛 ∈ ℕ → ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑛 + ( 𝑁 − 1 ) ) ∈ 𝐴 ) → ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 + 1 ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) ) )
51 25 28 31 34 37 50 nnind ( ( 𝑛 − ( 𝑁 − 1 ) ) ∈ ℕ → ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) ∈ 𝐴 ) )
52 21 22 51 sylc ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → ( ( 𝑛 − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) ∈ 𝐴 )
53 11 52 eqeltrrd ( ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) ) → 𝑛𝐴 )
54 53 ex ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( 𝑛 ∈ ℤ ∧ 𝑁𝑛 ) → 𝑛𝐴 ) )
55 3 54 syl5bi ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑛 ∈ { 𝑘 ∈ ℤ ∣ 𝑁𝑘 } → 𝑛𝐴 ) )
56 55 ssrdv ( ( 𝑁𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁𝑘 } ⊆ 𝐴 )