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

Theorem 2nn0ind 31120
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  |-  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
Ref Expression
2nn0ind  |-  ( A  e.  NN0  ->  rh )
Distinct variable groups:    x, y    x, A    ps, x    ch, x    th, x    ta, x    et, x    rh, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)    ch( y)    th( y)    ta( y)    et( y)    rh( y)    A( y)

Proof of Theorem 2nn0ind
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 nn0p1nn 10831 . . . 4  |-  ( A  e.  NN0  ->  ( A  +  1 )  e.  NN )
2 oveq1 6277 . . . . . . 7  |-  ( a  =  1  ->  (
a  -  1 )  =  ( 1  -  1 ) )
32sbceq1d 3329 . . . . . 6  |-  ( a  =  1  ->  ( [. ( a  -  1 )  /  x ]. ph  <->  [. ( 1  -  1 )  /  x ]. ph ) )
4 dfsbcq 3326 . . . . . 6  |-  ( a  =  1  ->  ( [. a  /  x ]. ph  <->  [. 1  /  x ]. ph ) )
53, 4anbi12d 708 . . . . 5  |-  ( a  =  1  ->  (
( [. ( a  - 
1 )  /  x ]. ph  /\  [. a  /  x ]. ph )  <->  (
[. ( 1  -  1 )  /  x ]. ph  /\  [. 1  /  x ]. ph )
) )
6 oveq1 6277 . . . . . . 7  |-  ( a  =  y  ->  (
a  -  1 )  =  ( y  - 
1 ) )
76sbceq1d 3329 . . . . . 6  |-  ( a  =  y  ->  ( [. ( a  -  1 )  /  x ]. ph  <->  [. ( y  -  1 )  /  x ]. ph ) )
8 dfsbcq 3326 . . . . . 6  |-  ( a  =  y  ->  ( [. a  /  x ]. ph  <->  [. y  /  x ]. ph ) )
97, 8anbi12d 708 . . . . 5  |-  ( a  =  y  ->  (
( [. ( a  - 
1 )  /  x ]. ph  /\  [. a  /  x ]. ph )  <->  (
[. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
) )
10 oveq1 6277 . . . . . . 7  |-  ( a  =  ( y  +  1 )  ->  (
a  -  1 )  =  ( ( y  +  1 )  - 
1 ) )
1110sbceq1d 3329 . . . . . 6  |-  ( a  =  ( y  +  1 )  ->  ( [. ( a  -  1 )  /  x ]. ph  <->  [. ( ( y  +  1 )  -  1 )  /  x ]. ph ) )
12 dfsbcq 3326 . . . . . 6  |-  ( a  =  ( y  +  1 )  ->  ( [. a  /  x ]. ph  <->  [. ( y  +  1 )  /  x ]. ph ) )
1311, 12anbi12d 708 . . . . 5  |-  ( a  =  ( y  +  1 )  ->  (
( [. ( a  - 
1 )  /  x ]. ph  /\  [. a  /  x ]. ph )  <->  (
[. ( ( y  +  1 )  - 
1 )  /  x ]. ph  /\  [. (
y  +  1 )  /  x ]. ph )
) )
14 oveq1 6277 . . . . . . 7  |-  ( a  =  ( A  + 
1 )  ->  (
a  -  1 )  =  ( ( A  +  1 )  - 
1 ) )
1514sbceq1d 3329 . . . . . 6  |-  ( a  =  ( A  + 
1 )  ->  ( [. ( a  -  1 )  /  x ]. ph  <->  [. ( ( A  + 
1 )  -  1 )  /  x ]. ph ) )
16 dfsbcq 3326 . . . . . 6  |-  ( a  =  ( A  + 
1 )  ->  ( [. a  /  x ]. ph  <->  [. ( A  + 
1 )  /  x ]. ph ) )
1715, 16anbi12d 708 . . . . 5  |-  ( a  =  ( A  + 
1 )  ->  (
( [. ( a  - 
1 )  /  x ]. ph  /\  [. a  /  x ]. ph )  <->  (
[. ( ( A  +  1 )  - 
1 )  /  x ]. ph  /\  [. ( A  +  1 )  /  x ]. ph )
) )
18 2nn0ind.1 . . . . . . 7  |-  ps
19 ovex 6298 . . . . . . . 8  |-  ( 1  -  1 )  e. 
_V
20 1m1e0 10600 . . . . . . . . . 10  |-  ( 1  -  1 )  =  0
2120eqeq2i 2472 . . . . . . . . 9  |-  ( x  =  ( 1  -  1 )  <->  x  = 
0 )
22 2nn0ind.4 . . . . . . . . 9  |-  ( x  =  0  ->  ( ph 
<->  ps ) )
2321, 22sylbi 195 . . . . . . . 8  |-  ( x  =  ( 1  -  1 )  ->  ( ph 
<->  ps ) )
2419, 23sbcie 3359 . . . . . . 7  |-  ( [. ( 1  -  1 )  /  x ]. ph  <->  ps )
2518, 24mpbir 209 . . . . . 6  |-  [. (
1  -  1 )  /  x ]. ph
26 2nn0ind.2 . . . . . . 7  |-  ch
27 1ex 9580 . . . . . . . 8  |-  1  e.  _V
28 2nn0ind.5 . . . . . . . 8  |-  ( x  =  1  ->  ( ph 
<->  ch ) )
2927, 28sbcie 3359 . . . . . . 7  |-  ( [.
1  /  x ]. ph  <->  ch )
3026, 29mpbir 209 . . . . . 6  |-  [. 1  /  x ]. ph
3125, 30pm3.2i 453 . . . . 5  |-  ( [. ( 1  -  1 )  /  x ]. ph 
/\  [. 1  /  x ]. ph )
32 simprr 755 . . . . . . . 8  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  [. y  /  x ]. ph )
33 nncn 10539 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  y  e.  CC )
34 ax-1cn 9539 . . . . . . . . . . 11  |-  1  e.  CC
35 pncan 9817 . . . . . . . . . . 11  |-  ( ( y  e.  CC  /\  1  e.  CC )  ->  ( ( y  +  1 )  -  1 )  =  y )
3633, 34, 35sylancl 660 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( y  +  1 )  -  1 )  =  y )
3736adantr 463 . . . . . . . . 9  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  ( (
y  +  1 )  -  1 )  =  y )
3837sbceq1d 3329 . . . . . . . 8  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  ( [. ( ( y  +  1 )  -  1 )  /  x ]. ph  <->  [. y  /  x ]. ph ) )
3932, 38mpbird 232 . . . . . . 7  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  [. ( ( y  +  1 )  -  1 )  /  x ]. ph )
40 2nn0ind.3 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( th  /\  ta )  ->  et ) )
41 ovex 6298 . . . . . . . . . . 11  |-  ( y  -  1 )  e. 
_V
42 2nn0ind.6 . . . . . . . . . . 11  |-  ( x  =  ( y  - 
1 )  ->  ( ph 
<->  th ) )
4341, 42sbcie 3359 . . . . . . . . . 10  |-  ( [. ( y  -  1 )  /  x ]. ph  <->  th )
44 vex 3109 . . . . . . . . . . 11  |-  y  e. 
_V
45 2nn0ind.7 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( ph 
<->  ta ) )
4644, 45sbcie 3359 . . . . . . . . . 10  |-  ( [. y  /  x ]. ph  <->  ta )
4743, 46anbi12i 695 . . . . . . . . 9  |-  ( (
[. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )  <->  ( th  /\  ta )
)
48 ovex 6298 . . . . . . . . . 10  |-  ( y  +  1 )  e. 
_V
49 2nn0ind.8 . . . . . . . . . 10  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  et ) )
5048, 49sbcie 3359 . . . . . . . . 9  |-  ( [. ( y  +  1 )  /  x ]. ph  <->  et )
5140, 47, 503imtr4g 270 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )  ->  [. ( y  +  1 )  /  x ]. ph ) )
5251imp 427 . . . . . . 7  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  [. ( y  +  1 )  /  x ]. ph )
5339, 52jca 530 . . . . . 6  |-  ( ( y  e.  NN  /\  ( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )
)  ->  ( [. ( ( y  +  1 )  -  1 )  /  x ]. ph 
/\  [. ( y  +  1 )  /  x ]. ph ) )
5453ex 432 . . . . 5  |-  ( y  e.  NN  ->  (
( [. ( y  - 
1 )  /  x ]. ph  /\  [. y  /  x ]. ph )  ->  ( [. ( ( y  +  1 )  -  1 )  /  x ]. ph  /\  [. (
y  +  1 )  /  x ]. ph )
) )
555, 9, 13, 17, 31, 54nnind 10549 . . . 4  |-  ( ( A  +  1 )  e.  NN  ->  ( [. ( ( A  + 
1 )  -  1 )  /  x ]. ph 
/\  [. ( A  + 
1 )  /  x ]. ph ) )
561, 55syl 16 . . 3  |-  ( A  e.  NN0  ->  ( [. ( ( A  + 
1 )  -  1 )  /  x ]. ph 
/\  [. ( A  + 
1 )  /  x ]. ph ) )
57 nn0cn 10801 . . . . . . 7  |-  ( A  e.  NN0  ->  A  e.  CC )
58 pncan 9817 . . . . . . 7  |-  ( ( A  e.  CC  /\  1  e.  CC )  ->  ( ( A  + 
1 )  -  1 )  =  A )
5957, 34, 58sylancl 660 . . . . . 6  |-  ( A  e.  NN0  ->  ( ( A  +  1 )  -  1 )  =  A )
6059sbceq1d 3329 . . . . 5  |-  ( A  e.  NN0  ->  ( [. ( ( A  + 
1 )  -  1 )  /  x ]. ph  <->  [. A  /  x ]. ph ) )
6160biimpa 482 . . . 4  |-  ( ( A  e.  NN0  /\  [. ( ( A  + 
1 )  -  1 )  /  x ]. ph )  ->  [. A  /  x ]. ph )
6261adantrr 714 . . 3  |-  ( ( A  e.  NN0  /\  ( [. ( ( A  +  1 )  - 
1 )  /  x ]. ph  /\  [. ( A  +  1 )  /  x ]. ph )
)  ->  [. A  /  x ]. ph )
6356, 62mpdan 666 . 2  |-  ( A  e.  NN0  ->  [. A  /  x ]. ph )
64 2nn0ind.9 . . 3  |-  ( x  =  A  ->  ( ph 
<->  rh ) )
6564sbcieg 3357 . 2  |-  ( A  e.  NN0  ->  ( [. A  /  x ]. ph  <->  rh )
)
6663, 65mpbid 210 1  |-  ( A  e.  NN0  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823   [.wsbc 3324  (class class class)co 6270   CCcc 9479   0cc0 9481   1c1 9482    + caddc 9484    - cmin 9796   NNcn 10531   NN0cn0 10791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622  df-sub 9798  df-nn 10532  df-n0 10792
This theorem is referenced by:  jm2.18  31169  jm2.15nn0  31184  jm2.16nn0  31185
  Copyright terms: Public domain W3C validator