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