Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2nn0ind Structured version   Visualization version   Unicode version

Theorem 2nn0ind 35864
 Description: Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.)
Hypotheses
Ref Expression
2nn0ind.1
2nn0ind.2
2nn0ind.3
2nn0ind.4
2nn0ind.5
2nn0ind.6
2nn0ind.7
2nn0ind.8
2nn0ind.9
Assertion
Ref Expression
2nn0ind
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem 2nn0ind
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nn0p1nn 10933 . . . 4
2 oveq1 6315 . . . . . . 7
32sbceq1d 3260 . . . . . 6
4 dfsbcq 3257 . . . . . 6
53, 4anbi12d 725 . . . . 5
6 oveq1 6315 . . . . . . 7
76sbceq1d 3260 . . . . . 6
8 dfsbcq 3257 . . . . . 6
97, 8anbi12d 725 . . . . 5
10 oveq1 6315 . . . . . . 7
1110sbceq1d 3260 . . . . . 6
12 dfsbcq 3257 . . . . . 6
1311, 12anbi12d 725 . . . . 5
14 oveq1 6315 . . . . . . 7
1514sbceq1d 3260 . . . . . 6
16 dfsbcq 3257 . . . . . 6
1715, 16anbi12d 725 . . . . 5
18 2nn0ind.1 . . . . . . 7
19 ovex 6336 . . . . . . . 8
20 1m1e0 10700 . . . . . . . . . 10
2120eqeq2i 2483 . . . . . . . . 9
22 2nn0ind.4 . . . . . . . . 9
2321, 22sylbi 200 . . . . . . . 8
2419, 23sbcie 3290 . . . . . . 7
2518, 24mpbir 214 . . . . . 6
26 2nn0ind.2 . . . . . . 7
27 1ex 9656 . . . . . . . 8
28 2nn0ind.5 . . . . . . . 8
2927, 28sbcie 3290 . . . . . . 7
3026, 29mpbir 214 . . . . . 6
3125, 30pm3.2i 462 . . . . 5
32 simprr 774 . . . . . . . 8
33 nncn 10639 . . . . . . . . . . 11
34 ax-1cn 9615 . . . . . . . . . . 11
35 pncan 9901 . . . . . . . . . . 11
3633, 34, 35sylancl 675 . . . . . . . . . 10
3736adantr 472 . . . . . . . . 9
3837sbceq1d 3260 . . . . . . . 8
3932, 38mpbird 240 . . . . . . 7
40 2nn0ind.3 . . . . . . . . 9
41 ovex 6336 . . . . . . . . . . 11
42 2nn0ind.6 . . . . . . . . . . 11
4341, 42sbcie 3290 . . . . . . . . . 10
44 vex 3034 . . . . . . . . . . 11
45 2nn0ind.7 . . . . . . . . . . 11
4644, 45sbcie 3290 . . . . . . . . . 10
4743, 46anbi12i 711 . . . . . . . . 9
48 ovex 6336 . . . . . . . . . 10
49 2nn0ind.8 . . . . . . . . . 10
5048, 49sbcie 3290 . . . . . . . . 9
5140, 47, 503imtr4g 278 . . . . . . . 8
5251imp 436 . . . . . . 7
5339, 52jca 541 . . . . . 6
5453ex 441 . . . . 5
555, 9, 13, 17, 31, 54nnind 10649 . . . 4
561, 55syl 17 . . 3
57 nn0cn 10903 . . . . . . 7
58 pncan 9901 . . . . . . 7
5957, 34, 58sylancl 675 . . . . . 6
6059sbceq1d 3260 . . . . 5
6160biimpa 492 . . . 4