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

Metamath Proof Explorer

Theorem nn1suc

Description: If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 16-May-2014)

Ref Expression
Hypotheses nn1suc.1 
|- ( x = 1 -> ( ph <-> ps ) )
nn1suc.3 
|- ( x = ( y + 1 ) -> ( ph <-> ch ) )
nn1suc.4 
|- ( x = A -> ( ph <-> th ) )
nn1suc.5 
|- ps
nn1suc.6 
|- ( y e. NN -> ch )
Assertion nn1suc 
|- ( A e. NN -> th )

Proof

Step Hyp Ref Expression
1 nn1suc.1 
 |-  ( x = 1 -> ( ph <-> ps ) )
2 nn1suc.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> ch ) )
3 nn1suc.4 
 |-  ( x = A -> ( ph <-> th ) )
4 nn1suc.5 
 |-  ps
5 nn1suc.6 
 |-  ( y e. NN -> ch )
6 1ex 
 |-  1 e. _V
7 6 1 sbcie 
 |-  ( [. 1 / x ]. ph <-> ps )
8 4 7 mpbir 
 |-  [. 1 / x ]. ph
9 1nn 
 |-  1 e. NN
10 eleq1 
 |-  ( A = 1 -> ( A e. NN <-> 1 e. NN ) )
11 9 10 mpbiri 
 |-  ( A = 1 -> A e. NN )
12 3 sbcieg 
 |-  ( A e. NN -> ( [. A / x ]. ph <-> th ) )
13 11 12 syl 
 |-  ( A = 1 -> ( [. A / x ]. ph <-> th ) )
14 dfsbcq 
 |-  ( A = 1 -> ( [. A / x ]. ph <-> [. 1 / x ]. ph ) )
15 13 14 bitr3d 
 |-  ( A = 1 -> ( th <-> [. 1 / x ]. ph ) )
16 8 15 mpbiri 
 |-  ( A = 1 -> th )
17 16 a1i 
 |-  ( A e. NN -> ( A = 1 -> th ) )
18 ovex 
 |-  ( y + 1 ) e. _V
19 18 2 sbcie 
 |-  ( [. ( y + 1 ) / x ]. ph <-> ch )
20 oveq1 
 |-  ( y = ( A - 1 ) -> ( y + 1 ) = ( ( A - 1 ) + 1 ) )
21 20 sbceq1d 
 |-  ( y = ( A - 1 ) -> ( [. ( y + 1 ) / x ]. ph <-> [. ( ( A - 1 ) + 1 ) / x ]. ph ) )
22 19 21 bitr3id 
 |-  ( y = ( A - 1 ) -> ( ch <-> [. ( ( A - 1 ) + 1 ) / x ]. ph ) )
23 22 5 vtoclga 
 |-  ( ( A - 1 ) e. NN -> [. ( ( A - 1 ) + 1 ) / x ]. ph )
24 nncn 
 |-  ( A e. NN -> A e. CC )
25 ax-1cn 
 |-  1 e. CC
26 npcan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) + 1 ) = A )
27 24 25 26 sylancl 
 |-  ( A e. NN -> ( ( A - 1 ) + 1 ) = A )
28 27 sbceq1d 
 |-  ( A e. NN -> ( [. ( ( A - 1 ) + 1 ) / x ]. ph <-> [. A / x ]. ph ) )
29 28 12 bitrd 
 |-  ( A e. NN -> ( [. ( ( A - 1 ) + 1 ) / x ]. ph <-> th ) )
30 23 29 imbitrid 
 |-  ( A e. NN -> ( ( A - 1 ) e. NN -> th ) )
31 nn1m1nn 
 |-  ( A e. NN -> ( A = 1 \/ ( A - 1 ) e. NN ) )
32 17 30 31 mpjaod 
 |-  ( A e. NN -> th )