Metamath Proof Explorer

Theorem 2nn0ind

Description: Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 2nn0ind.1 
 |-  ps
2 2nn0ind.2 
 |-  ch
3 2nn0ind.3 
 |-  ( y e. NN -> ( ( th /\ ta ) -> et ) )
4 2nn0ind.4 
 |-  ( x = 0 -> ( ph <-> ps ) )
5 2nn0ind.5 
 |-  ( x = 1 -> ( ph <-> ch ) )
6 2nn0ind.6 
 |-  ( x = ( y - 1 ) -> ( ph <-> th ) )
7 2nn0ind.7 
 |-  ( x = y -> ( ph <-> ta ) )
8 2nn0ind.8 
 |-  ( x = ( y + 1 ) -> ( ph <-> et ) )
9 2nn0ind.9 
 |-  ( x = A -> ( ph <-> rh ) )
10 nn0p1nn 
 |-  ( A e. NN0 -> ( A + 1 ) e. NN )
11 oveq1 
 |-  ( a = 1 -> ( a - 1 ) = ( 1 - 1 ) )
12 11 sbceq1d 
 |-  ( a = 1 -> ( [. ( a - 1 ) / x ]. ph <-> [. ( 1 - 1 ) / x ]. ph ) )
13 dfsbcq 
 |-  ( a = 1 -> ( [. a / x ]. ph <-> [. 1 / x ]. ph ) )
14 12 13 anbi12d 
 |-  ( a = 1 -> ( ( [. ( a - 1 ) / x ]. ph /\ [. a / x ]. ph ) <-> ( [. ( 1 - 1 ) / x ]. ph /\ [. 1 / x ]. ph ) ) )
15 oveq1 
 |-  ( a = y -> ( a - 1 ) = ( y - 1 ) )
16 15 sbceq1d 
 |-  ( a = y -> ( [. ( a - 1 ) / x ]. ph <-> [. ( y - 1 ) / x ]. ph ) )
17 dfsbcq 
 |-  ( a = y -> ( [. a / x ]. ph <-> [. y / x ]. ph ) )
18 16 17 anbi12d 
 |-  ( a = y -> ( ( [. ( a - 1 ) / x ]. ph /\ [. a / x ]. ph ) <-> ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) )
19 oveq1 
 |-  ( a = ( y + 1 ) -> ( a - 1 ) = ( ( y + 1 ) - 1 ) )
20 19 sbceq1d 
 |-  ( a = ( y + 1 ) -> ( [. ( a - 1 ) / x ]. ph <-> [. ( ( y + 1 ) - 1 ) / x ]. ph ) )
21 dfsbcq 
 |-  ( a = ( y + 1 ) -> ( [. a / x ]. ph <-> [. ( y + 1 ) / x ]. ph ) )
22 20 21 anbi12d 
 |-  ( a = ( y + 1 ) -> ( ( [. ( a - 1 ) / x ]. ph /\ [. a / x ]. ph ) <-> ( [. ( ( y + 1 ) - 1 ) / x ]. ph /\ [. ( y + 1 ) / x ]. ph ) ) )
23 oveq1 
 |-  ( a = ( A + 1 ) -> ( a - 1 ) = ( ( A + 1 ) - 1 ) )
24 23 sbceq1d 
 |-  ( a = ( A + 1 ) -> ( [. ( a - 1 ) / x ]. ph <-> [. ( ( A + 1 ) - 1 ) / x ]. ph ) )
25 dfsbcq 
 |-  ( a = ( A + 1 ) -> ( [. a / x ]. ph <-> [. ( A + 1 ) / x ]. ph ) )
26 24 25 anbi12d 
 |-  ( a = ( A + 1 ) -> ( ( [. ( a - 1 ) / x ]. ph /\ [. a / x ]. ph ) <-> ( [. ( ( A + 1 ) - 1 ) / x ]. ph /\ [. ( A + 1 ) / x ]. ph ) ) )
27 ovex 
 |-  ( 1 - 1 ) e. _V
28 1m1e0 
 |-  ( 1 - 1 ) = 0
29 28 eqeq2i 
 |-  ( x = ( 1 - 1 ) <-> x = 0 )
30 29 4 sylbi 
 |-  ( x = ( 1 - 1 ) -> ( ph <-> ps ) )
31 27 30 sbcie 
 |-  ( [. ( 1 - 1 ) / x ]. ph <-> ps )
32 1 31 mpbir 
 |-  [. ( 1 - 1 ) / x ]. ph
33 1ex 
 |-  1 e. _V
34 33 5 sbcie 
 |-  ( [. 1 / x ]. ph <-> ch )
35 2 34 mpbir 
 |-  [. 1 / x ]. ph
36 32 35 pm3.2i 
 |-  ( [. ( 1 - 1 ) / x ]. ph /\ [. 1 / x ]. ph )
37 simprr 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> [. y / x ]. ph )
38 nncn 
 |-  ( y e. NN -> y e. CC )
39 ax-1cn 
 |-  1 e. CC
40 pncan 
 |-  ( ( y e. CC /\ 1 e. CC ) -> ( ( y + 1 ) - 1 ) = y )
41 38 39 40 sylancl 
 |-  ( y e. NN -> ( ( y + 1 ) - 1 ) = y )
42 41 adantr 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> ( ( y + 1 ) - 1 ) = y )
43 42 sbceq1d 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> ( [. ( ( y + 1 ) - 1 ) / x ]. ph <-> [. y / x ]. ph ) )
44 37 43 mpbird 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> [. ( ( y + 1 ) - 1 ) / x ]. ph )
45 ovex 
 |-  ( y - 1 ) e. _V
46 45 6 sbcie 
 |-  ( [. ( y - 1 ) / x ]. ph <-> th )
47 vex 
 |-  y e. _V
48 47 7 sbcie 
 |-  ( [. y / x ]. ph <-> ta )
49 46 48 anbi12i 
 |-  ( ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) <-> ( th /\ ta ) )
50 ovex 
 |-  ( y + 1 ) e. _V
51 50 8 sbcie 
 |-  ( [. ( y + 1 ) / x ]. ph <-> et )
52 3 49 51 3imtr4g 
 |-  ( y e. NN -> ( ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) -> [. ( y + 1 ) / x ]. ph ) )
53 52 imp 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> [. ( y + 1 ) / x ]. ph )
54 44 53 jca 
 |-  ( ( y e. NN /\ ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) ) -> ( [. ( ( y + 1 ) - 1 ) / x ]. ph /\ [. ( y + 1 ) / x ]. ph ) )
55 54 ex 
 |-  ( y e. NN -> ( ( [. ( y - 1 ) / x ]. ph /\ [. y / x ]. ph ) -> ( [. ( ( y + 1 ) - 1 ) / x ]. ph /\ [. ( y + 1 ) / x ]. ph ) ) )
56 14 18 22 26 36 55 nnind 
 |-  ( ( A + 1 ) e. NN -> ( [. ( ( A + 1 ) - 1 ) / x ]. ph /\ [. ( A + 1 ) / x ]. ph ) )
57 10 56 syl 
 |-  ( A e. NN0 -> ( [. ( ( A + 1 ) - 1 ) / x ]. ph /\ [. ( A + 1 ) / x ]. ph ) )
58 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
59 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
60 58 39 59 sylancl 
 |-  ( A e. NN0 -> ( ( A + 1 ) - 1 ) = A )
61 60 sbceq1d 
 |-  ( A e. NN0 -> ( [. ( ( A + 1 ) - 1 ) / x ]. ph <-> [. A / x ]. ph ) )
62 61 biimpa 
 |-  ( ( A e. NN0 /\ [. ( ( A + 1 ) - 1 ) / x ]. ph ) -> [. A / x ]. ph )
63 62 adantrr 
 |-  ( ( A e. NN0 /\ ( [. ( ( A + 1 ) - 1 ) / x ]. ph /\ [. ( A + 1 ) / x ]. ph ) ) -> [. A / x ]. ph )
64 57 63 mpdan 
 |-  ( A e. NN0 -> [. A / x ]. ph )
65 9 sbcieg 
 |-  ( A e. NN0 -> ( [. A / x ]. ph <-> rh ) )
66 64 65 mpbid 
 |-  ( A e. NN0 -> rh )