This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0indd

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Hypotheses nn0indd.1 
|- ( x = 0 -> ( ps <-> ch ) )
nn0indd.2 
|- ( x = y -> ( ps <-> th ) )
nn0indd.3 
|- ( x = ( y + 1 ) -> ( ps <-> ta ) )
nn0indd.4 
|- ( x = A -> ( ps <-> et ) )
nn0indd.5 
|- ( ph -> ch )
nn0indd.6 
|- ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta )
Assertion nn0indd 
|- ( ( ph /\ A e. NN0 ) -> et )

Proof

Step Hyp Ref Expression
1 nn0indd.1 
 |-  ( x = 0 -> ( ps <-> ch ) )
2 nn0indd.2 
 |-  ( x = y -> ( ps <-> th ) )
3 nn0indd.3 
 |-  ( x = ( y + 1 ) -> ( ps <-> ta ) )
4 nn0indd.4 
 |-  ( x = A -> ( ps <-> et ) )
5 nn0indd.5 
 |-  ( ph -> ch )
6 nn0indd.6 
 |-  ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta )
7 1 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
8 2 imbi2d 
 |-  ( x = y -> ( ( ph -> ps ) <-> ( ph -> th ) ) )
9 3 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ph -> ps ) <-> ( ph -> ta ) ) )
10 4 imbi2d 
 |-  ( x = A -> ( ( ph -> ps ) <-> ( ph -> et ) ) )
11 6 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( th -> ta ) )
12 11 expcom 
 |-  ( y e. NN0 -> ( ph -> ( th -> ta ) ) )
13 12 a2d 
 |-  ( y e. NN0 -> ( ( ph -> th ) -> ( ph -> ta ) ) )
14 7 8 9 10 5 13 nn0ind 
 |-  ( A e. NN0 -> ( ph -> et ) )
15 14 impcom 
 |-  ( ( ph /\ A e. NN0 ) -> et )