Metamath Proof Explorer

Theorem nn0ind-raph

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 nn0ind-raph.1 
 |-  ( x = 0 -> ( ph <-> ps ) )
2 nn0ind-raph.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 nn0ind-raph.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> th ) )
4 nn0ind-raph.4 
 |-  ( x = A -> ( ph <-> ta ) )
5 nn0ind-raph.5 
 |-  ps
6 nn0ind-raph.6 
 |-  ( y e. NN0 -> ( ch -> th ) )
7 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
8 dfsbcq2 
 |-  ( z = 1 -> ( [ z / x ] ph <-> [. 1 / x ]. ph ) )
9 nfv 
 |-  F/ x ch
10 9 2 sbhypf 
 |-  ( z = y -> ( [ z / x ] ph <-> ch ) )
11 nfv 
 |-  F/ x th
12 11 3 sbhypf 
 |-  ( z = ( y + 1 ) -> ( [ z / x ] ph <-> th ) )
13 nfv 
 |-  F/ x ta
14 13 4 sbhypf 
 |-  ( z = A -> ( [ z / x ] ph <-> ta ) )
15 nfsbc1v 
 |-  F/ x [. 1 / x ]. ph
16 1ex 
 |-  1 e. _V
17 c0ex 
 |-  0 e. _V
18 0nn0 
 |-  0 e. NN0
19 eleq1a 
 |-  ( 0 e. NN0 -> ( y = 0 -> y e. NN0 ) )
20 18 19 ax-mp 
 |-  ( y = 0 -> y e. NN0 )
21 5 1 mpbiri 
 |-  ( x = 0 -> ph )
22 eqeq2 
 |-  ( y = 0 -> ( x = y <-> x = 0 ) )
23 22 2 biimtrrdi 
 |-  ( y = 0 -> ( x = 0 -> ( ph <-> ch ) ) )
24 23 pm5.74d 
 |-  ( y = 0 -> ( ( x = 0 -> ph ) <-> ( x = 0 -> ch ) ) )
25 21 24 mpbii 
 |-  ( y = 0 -> ( x = 0 -> ch ) )
26 25 com12 
 |-  ( x = 0 -> ( y = 0 -> ch ) )
27 17 26 vtocle 
 |-  ( y = 0 -> ch )
28 20 27 6 sylc 
 |-  ( y = 0 -> th )
29 28 adantr 
 |-  ( ( y = 0 /\ x = 1 ) -> th )
30 oveq1 
 |-  ( y = 0 -> ( y + 1 ) = ( 0 + 1 ) )
31 0p1e1 
 |-  ( 0 + 1 ) = 1
32 30 31 eqtrdi 
 |-  ( y = 0 -> ( y + 1 ) = 1 )
33 32 eqeq2d 
 |-  ( y = 0 -> ( x = ( y + 1 ) <-> x = 1 ) )
34 33 3 biimtrrdi 
 |-  ( y = 0 -> ( x = 1 -> ( ph <-> th ) ) )
35 34 imp 
 |-  ( ( y = 0 /\ x = 1 ) -> ( ph <-> th ) )
36 29 35 mpbird 
 |-  ( ( y = 0 /\ x = 1 ) -> ph )
37 36 ex 
 |-  ( y = 0 -> ( x = 1 -> ph ) )
38 17 37 vtocle 
 |-  ( x = 1 -> ph )
39 sbceq1a 
 |-  ( x = 1 -> ( ph <-> [. 1 / x ]. ph ) )
40 38 39 mpbid 
 |-  ( x = 1 -> [. 1 / x ]. ph )
41 15 16 40 vtoclef 
 |-  [. 1 / x ]. ph
42 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
43 42 6 syl 
 |-  ( y e. NN -> ( ch -> th ) )
44 8 10 12 14 41 43 nnind 
 |-  ( A e. NN -> ta )
45 nfv 
 |-  F/ x ( 0 = A -> ta )
46 eqeq1 
 |-  ( x = 0 -> ( x = A <-> 0 = A ) )
47 1 bicomd 
 |-  ( x = 0 -> ( ps <-> ph ) )
48 47 4 sylan9bb 
 |-  ( ( x = 0 /\ x = A ) -> ( ps <-> ta ) )
49 5 48 mpbii 
 |-  ( ( x = 0 /\ x = A ) -> ta )
50 49 ex 
 |-  ( x = 0 -> ( x = A -> ta ) )
51 46 50 sylbird 
 |-  ( x = 0 -> ( 0 = A -> ta ) )
52 45 17 51 vtoclef 
 |-  ( 0 = A -> ta )
53 52 eqcoms 
 |-  ( A = 0 -> ta )
54 44 53 jaoi 
 |-  ( ( A e. NN \/ A = 0 ) -> ta )
55 7 54 sylbi 
 |-  ( A e. NN0 -> ta )