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 e. ZZ
Assertion peano5uzi
|- ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A )

Proof

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