Metamath Proof Explorer


Theorem peano5uzti

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

Ref Expression
Assertion peano5uzti N N A x A x + 1 A k | N k A

Proof

Step Hyp Ref Expression
1 eleq1 N = if N N 1 N A if N N 1 A
2 1 anbi1d N = if N N 1 N A x A x + 1 A if N N 1 A x A x + 1 A
3 breq1 N = if N N 1 N k if N N 1 k
4 3 rabbidv N = if N N 1 k | N k = k | if N N 1 k
5 4 sseq1d N = if N N 1 k | N k A k | if N N 1 k A
6 2 5 imbi12d N = if N N 1 N A x A x + 1 A k | N k A if N N 1 A x A x + 1 A k | if N N 1 k A
7 1z 1
8 7 elimel if N N 1
9 8 peano5uzi if N N 1 A x A x + 1 A k | if N N 1 k A
10 6 9 dedth N N A x A x + 1 A k | N k A