![]() |
Mathbox for Stefan O'Rear |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > frmy | Structured version Visualization version GIF version |
Description: The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
Ref | Expression |
---|---|
frmy | ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmxyelxp 39015 | . . . 4 ⊢ ((𝑎 ∈ (ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏)) ∈ (ℕ0 × ℤ)) | |
2 | xp2nd 7585 | . . . 4 ⊢ ((◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏)) ∈ (ℕ0 × ℤ) → (2nd ‘(◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏))) ∈ ℤ) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ ((𝑎 ∈ (ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (2nd ‘(◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏))) ∈ ℤ) |
4 | 3 | rgen2 3172 | . 2 ⊢ ∀𝑎 ∈ (ℤ≥‘2)∀𝑏 ∈ ℤ (2nd ‘(◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏))) ∈ ℤ |
5 | df-rmy 39006 | . . 3 ⊢ Yrm = (𝑎 ∈ (ℤ≥‘2), 𝑏 ∈ ℤ ↦ (2nd ‘(◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏)))) | |
6 | 5 | fmpo 7629 | . 2 ⊢ (∀𝑎 ∈ (ℤ≥‘2)∀𝑏 ∈ ℤ (2nd ‘(◡(𝑐 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑐) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑐))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑏))) ∈ ℤ ↔ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ) |
7 | 4, 6 | mpbi 231 | 1 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2083 ∀wral 3107 ↦ cmpt 5047 × cxp 5448 ◡ccnv 5449 ⟶wf 6228 ‘cfv 6232 (class class class)co 7023 1st c1st 7550 2nd c2nd 7551 1c1 10391 + caddc 10393 · cmul 10395 − cmin 10723 2c2 11546 ℕ0cn0 11751 ℤcz 11835 ℤ≥cuz 12097 ↑cexp 13283 √csqrt 14430 Yrm crmy 39004 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-inf2 8957 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 ax-pre-sup 10468 ax-addf 10469 ax-mulf 10470 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-fal 1538 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-iin 4834 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-se 5410 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-isom 6241 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-of 7274 df-om 7444 df-1st 7552 df-2nd 7553 df-supp 7689 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-1o 7960 df-2o 7961 df-oadd 7964 df-omul 7965 df-er 8146 df-map 8265 df-pm 8266 df-ixp 8318 df-en 8365 df-dom 8366 df-sdom 8367 df-fin 8368 df-fsupp 8687 df-fi 8728 df-sup 8759 df-inf 8760 df-oi 8827 df-card 9221 df-acn 9224 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-div 11152 df-nn 11493 df-2 11554 df-3 11555 df-4 11556 df-5 11557 df-6 11558 df-7 11559 df-8 11560 df-9 11561 df-n0 11752 df-xnn0 11822 df-z 11836 df-dec 11953 df-uz 12098 df-q 12202 df-rp 12244 df-xneg 12361 df-xadd 12362 df-xmul 12363 df-ioo 12596 df-ioc 12597 df-ico 12598 df-icc 12599 df-fz 12747 df-fzo 12888 df-fl 13016 df-mod 13092 df-seq 13224 df-exp 13284 df-fac 13488 df-bc 13517 df-hash 13545 df-shft 14264 df-cj 14296 df-re 14297 df-im 14298 df-sqrt 14432 df-abs 14433 df-limsup 14666 df-clim 14683 df-rlim 14684 df-sum 14881 df-ef 15258 df-sin 15260 df-cos 15261 df-pi 15263 df-dvds 15445 df-gcd 15681 df-numer 15908 df-denom 15909 df-struct 16318 df-ndx 16319 df-slot 16320 df-base 16322 df-sets 16323 df-ress 16324 df-plusg 16411 df-mulr 16412 df-starv 16413 df-sca 16414 df-vsca 16415 df-ip 16416 df-tset 16417 df-ple 16418 df-ds 16420 df-unif 16421 df-hom 16422 df-cco 16423 df-rest 16529 df-topn 16530 df-0g 16548 df-gsum 16549 df-topgen 16550 df-pt 16551 df-prds 16554 df-xrs 16608 df-qtop 16613 df-imas 16614 df-xps 16616 df-mre 16690 df-mrc 16691 df-acs 16693 df-mgm 17685 df-sgrp 17727 df-mnd 17738 df-submnd 17779 df-mulg 17986 df-cntz 18192 df-cmn 18639 df-psmet 20223 df-xmet 20224 df-met 20225 df-bl 20226 df-mopn 20227 df-fbas 20228 df-fg 20229 df-cnfld 20232 df-top 21190 df-topon 21207 df-topsp 21229 df-bases 21242 df-cld 21315 df-ntr 21316 df-cls 21317 df-nei 21394 df-lp 21432 df-perf 21433 df-cn 21523 df-cnp 21524 df-haus 21611 df-tx 21858 df-hmeo 22051 df-fil 22142 df-fm 22234 df-flim 22235 df-flf 22236 df-xms 22617 df-ms 22618 df-tms 22619 df-cncf 23173 df-limc 24151 df-dv 24152 df-log 24825 df-squarenn 38944 df-pell1qr 38945 df-pell14qr 38946 df-pell1234qr 38947 df-pellfund 38948 df-rmy 39006 |
This theorem is referenced by: rmxycomplete 39020 rmxynorm 39021 rmxyneg 39023 rmxyadd 39024 rmxy1 39025 rmxy0 39026 rmxp1 39035 rmxm1 39037 rmym1 39038 rmxluc 39039 rmyluc 39040 rmyluc2 39041 rmxdbl 39042 rmydbl 39043 rmxypos 39050 ltrmynn0 39051 ltrmxnn0 39052 ltrmy 39055 rmyeq0 39056 rmyeq 39057 lermy 39058 rmynn 39059 rmynn0 39060 rmyabs 39061 jm2.24nn 39062 jm2.17a 39063 jm2.17b 39064 jm2.17c 39065 jm2.24 39066 rmygeid 39067 jm2.18 39091 jm2.19lem1 39092 jm2.19lem2 39093 jm2.19 39096 jm2.22 39098 jm2.23 39099 jm2.20nn 39100 jm2.25 39102 jm2.26a 39103 jm2.26lem3 39104 jm2.26 39105 jm2.15nn0 39106 jm2.16nn0 39107 jm2.27a 39108 jm2.27c 39110 rmydioph 39117 jm3.1lem1 39120 jm3.1 39123 expdiophlem1 39124 |
Copyright terms: Public domain | W3C validator |