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 N
Assertion peano5uzi N A x A x + 1 A k | N k A

Proof

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