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

Theorem rmxluc 35697
 Description: The X sequence is a Lucas (second-order integer recurrence) sequence. Part 3 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014.)
Assertion
Ref Expression
rmxluc Xrm Xrm Xrm

Proof of Theorem rmxluc
StepHypRef Expression
1 peano2zm 10926 . . . . . 6
2 frmx 35674 . . . . . . . 8 Xrm
32fovcl 6354 . . . . . . 7 Xrm
43nn0cnd 10873 . . . . . 6 Xrm
51, 4sylan2 476 . . . . 5 Xrm
6 peano2z 10924 . . . . . 6
72fovcl 6354 . . . . . . 7 Xrm
87nn0cnd 10873 . . . . . 6 Xrm
96, 8sylan2 476 . . . . 5 Xrm
105, 9addcomd 9781 . . . 4 Xrm Xrm Xrm Xrm
11 rmxp1 35693 . . . . 5 Xrm Xrm Yrm
12 rmxm1 35695 . . . . 5 Xrm Xrm Yrm
1311, 12oveq12d 6262 . . . 4 Xrm Xrm Xrm Yrm Xrm Yrm
142fovcl 6354 . . . . . . . 8 Xrm
1514nn0cnd 10873 . . . . . . 7 Xrm
16 eluzelcn 11116 . . . . . . . 8
1716adantr 466 . . . . . . 7
1815, 17mulcld 9609 . . . . . 6 Xrm
19 rmspecnonsq 35668 . . . . . . . . . 10 NN
2019eldifad 3386 . . . . . . . . 9
2120nncnd 10571 . . . . . . . 8
2221adantr 466 . . . . . . 7
23 frmy 35675 . . . . . . . . 9 Yrm
2423fovcl 6354 . . . . . . . 8 Yrm
2524zcnd 10987 . . . . . . 7 Yrm
2622, 25mulcld 9609 . . . . . 6 Yrm
2717, 15mulcld 9609 . . . . . 6 Xrm
2818, 26, 27ppncand 9972 . . . . 5 Xrm Yrm Xrm Yrm Xrm Xrm
2915, 17mulcomd 9610 . . . . . 6 Xrm Xrm
3029oveq1d 6259 . . . . 5 Xrm Xrm Xrm Xrm
31 2cnd 10628 . . . . . . 7
3231, 17, 15mulassd 9612 . . . . . 6 Xrm Xrm
33272timesd 10801 . . . . . 6 Xrm Xrm Xrm
3432, 33eqtr2d 2458 . . . . 5 Xrm Xrm Xrm
3528, 30, 343eqtrd 2461 . . . 4 Xrm Yrm Xrm Yrm Xrm
3610, 13, 353eqtrd 2461 . . 3 Xrm Xrm Xrm
37 2cn 10626 . . . . . 6
38 mulcl 9569 . . . . . 6
3937, 17, 38sylancr 667 . . . . 5
4039, 15mulcld 9609 . . . 4 Xrm
4140, 5, 9subaddd 9950 . . 3 Xrm Xrm Xrm Xrm Xrm Xrm
4236, 41mpbird 235 . 2 Xrm Xrm Xrm
4342eqcomd 2429 1 Xrm Xrm Xrm
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1872  cfv 5539  (class class class)co 6244  cc 9483  c1 9486   caddc 9488   cmul 9490   cmin 9806  cn 10555  c2 10605  cn0 10815  cz 10883  cuz 11105  cexp 12217  ◻NNcsquarenn 35593   Xrm crmx 35661   Yrm crmy 35662 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-addf 9564  ax-mulf 9565 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-of 6484  df-om 6646  df-1st 6746  df-2nd 6747  df-supp 6865  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-omul 7137  df-er 7313  df-map 7424  df-pm 7425  df-ixp 7473  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-fsupp 7832  df-fi 7873  df-sup 7904  df-inf 7905  df-oi 7973  df-card 8320  df-acn 8323  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-q 11211  df-rp 11249  df-xneg 11355  df-xadd 11356  df-xmul 11357  df-ioo 11585  df-ioc 11586  df-ico 11587  df-icc 11588  df-fz 11731  df-fzo 11862  df-fl 11973  df-mod 12042  df-seq 12159  df-exp 12218  df-fac 12405  df-bc 12433  df-hash 12461  df-shft 13069  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-limsup 13464  df-clim 13490  df-rlim 13491  df-sum 13691  df-ef 14059  df-sin 14061  df-cos 14062  df-pi 14064  df-dvds 14244  df-gcd 14407  df-numer 14622  df-denom 14623  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-mulr 15142  df-starv 15143  df-sca 15144  df-vsca 15145  df-ip 15146  df-tset 15147  df-ple 15148  df-ds 15150  df-unif 15151  df-hom 15152  df-cco 15153  df-rest 15259  df-topn 15260  df-0g 15278  df-gsum 15279  df-topgen 15280  df-pt 15281  df-prds 15284  df-xrs 15338  df-qtop 15344  df-imas 15345  df-xps 15348  df-mre 15430  df-mrc 15431  df-acs 15433  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-submnd 16521  df-mulg 16614  df-cntz 16909  df-cmn 17370  df-psmet 18900  df-xmet 18901  df-met 18902  df-bl 18903  df-mopn 18904  df-fbas 18905  df-fg 18906  df-cnfld 18909  df-top 19858  df-bases 19859  df-topon 19860  df-topsp 19861  df-cld 19971  df-ntr 19972  df-cls 19973  df-nei 20051  df-lp 20089  df-perf 20090  df-cn 20180  df-cnp 20181  df-haus 20268  df-tx 20514  df-hmeo 20707  df-fil 20798  df-fm 20890  df-flim 20891  df-flf 20892  df-xms 21272  df-ms 21273  df-tms 21274  df-cncf 21847  df-limc 22758  df-dv 22759  df-log 23443  df-squarenn 35599  df-pell1qr 35600  df-pell14qr 35601  df-pell1234qr 35602  df-pellfund 35603  df-rmx 35663  df-rmy 35664 This theorem is referenced by:  jm2.18  35756
 Copyright terms: Public domain W3C validator