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 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 )