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 biimtrid 
 |-  ( ( 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 )