![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vmacl | Structured version Visualization version GIF version |
Description: Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.) |
Ref | Expression |
---|---|
vmacl | ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2825 | . 2 ⊢ ((Λ‘𝐴) = 0 → ((Λ‘𝐴) ∈ ℝ ↔ 0 ∈ ℝ)) | |
2 | isppw2 26410 | . . . 4 ⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | |
3 | vmappw 26411 | . . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) | |
4 | prmnn 16504 | . . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ) | |
5 | 4 | nnrpd 12909 | . . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ+) |
6 | 5 | relogcld 25924 | . . . . . . . 8 ⊢ (𝑝 ∈ ℙ → (log‘𝑝) ∈ ℝ) |
7 | 6 | adantr 481 | . . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℝ) |
8 | 3, 7 | eqeltrd 2838 | . . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) ∈ ℝ) |
9 | fveq2 6839 | . . . . . . 7 ⊢ (𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) = (Λ‘(𝑝↑𝑘))) | |
10 | 9 | eleq1d 2822 | . . . . . 6 ⊢ (𝐴 = (𝑝↑𝑘) → ((Λ‘𝐴) ∈ ℝ ↔ (Λ‘(𝑝↑𝑘)) ∈ ℝ)) |
11 | 8, 10 | syl5ibrcom 246 | . . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) ∈ ℝ)) |
12 | 11 | rexlimivv 3194 | . . . 4 ⊢ (∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) ∈ ℝ) |
13 | 2, 12 | syl6bi 252 | . . 3 ⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 → (Λ‘𝐴) ∈ ℝ)) |
14 | 13 | imp 407 | . 2 ⊢ ((𝐴 ∈ ℕ ∧ (Λ‘𝐴) ≠ 0) → (Λ‘𝐴) ∈ ℝ) |
15 | 0red 11116 | . 2 ⊢ (𝐴 ∈ ℕ → 0 ∈ ℝ) | |
16 | 1, 14, 15 | pm2.61ne 3028 | 1 ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∃wrex 3071 ‘cfv 6493 (class class class)co 7351 ℝcr 11008 0cc0 11009 ℕcn 12111 ↑cexp 13921 ℙcprime 16501 logclog 25856 Λcvma 26387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5240 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7664 ax-inf2 9535 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088 ax-mulf 11089 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4864 df-int 4906 df-iun 4954 df-iin 4955 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-se 5587 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6251 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7307 df-ov 7354 df-oprab 7355 df-mpo 7356 df-of 7609 df-om 7795 df-1st 7913 df-2nd 7914 df-supp 8085 df-frecs 8204 df-wrecs 8235 df-recs 8309 df-rdg 8348 df-1o 8404 df-2o 8405 df-oadd 8408 df-er 8606 df-map 8725 df-pm 8726 df-ixp 8794 df-en 8842 df-dom 8843 df-sdom 8844 df-fin 8845 df-fsupp 9264 df-fi 9305 df-sup 9336 df-inf 9337 df-oi 9404 df-dju 9795 df-card 9833 df-pnf 11149 df-mnf 11150 df-xr 11151 df-ltxr 11152 df-le 11153 df-sub 11345 df-neg 11346 df-div 11771 df-nn 12112 df-2 12174 df-3 12175 df-4 12176 df-5 12177 df-6 12178 df-7 12179 df-8 12180 df-9 12181 df-n0 12372 df-z 12458 df-dec 12577 df-uz 12722 df-q 12828 df-rp 12870 df-xneg 12987 df-xadd 12988 df-xmul 12989 df-ioo 13222 df-ioc 13223 df-ico 13224 df-icc 13225 df-fz 13379 df-fzo 13522 df-fl 13651 df-mod 13729 df-seq 13861 df-exp 13922 df-fac 14128 df-bc 14157 df-hash 14185 df-shft 14906 df-cj 14938 df-re 14939 df-im 14940 df-sqrt 15074 df-abs 15075 df-limsup 15307 df-clim 15324 df-rlim 15325 df-sum 15525 df-ef 15904 df-sin 15906 df-cos 15907 df-pi 15909 df-dvds 16091 df-gcd 16329 df-prm 16502 df-pc 16663 df-struct 16973 df-sets 16990 df-slot 17008 df-ndx 17020 df-base 17038 df-ress 17067 df-plusg 17100 df-mulr 17101 df-starv 17102 df-sca 17103 df-vsca 17104 df-ip 17105 df-tset 17106 df-ple 17107 df-ds 17109 df-unif 17110 df-hom 17111 df-cco 17112 df-rest 17258 df-topn 17259 df-0g 17277 df-gsum 17278 df-topgen 17279 df-pt 17280 df-prds 17283 df-xrs 17338 df-qtop 17343 df-imas 17344 df-xps 17346 df-mre 17420 df-mrc 17421 df-acs 17423 df-mgm 18451 df-sgrp 18500 df-mnd 18511 df-submnd 18556 df-mulg 18826 df-cntz 19050 df-cmn 19517 df-psmet 20735 df-xmet 20736 df-met 20737 df-bl 20738 df-mopn 20739 df-fbas 20740 df-fg 20741 df-cnfld 20744 df-top 22189 df-topon 22206 df-topsp 22228 df-bases 22242 df-cld 22316 df-ntr 22317 df-cls 22318 df-nei 22395 df-lp 22433 df-perf 22434 df-cn 22524 df-cnp 22525 df-haus 22612 df-tx 22859 df-hmeo 23052 df-fil 23143 df-fm 23235 df-flim 23236 df-flf 23237 df-xms 23619 df-ms 23620 df-tms 23621 df-cncf 24187 df-limc 25176 df-dv 25177 df-log 25858 df-vma 26393 |
This theorem is referenced by: vmaf 26414 vmage0 26416 chpf 26418 efchpcl 26420 chpp1 26450 chpwordi 26452 chtlepsi 26500 vmasum 26510 logfac2 26511 chpval2 26512 vmadivsum 26776 vmadivsumb 26777 rplogsumlem2 26779 rpvmasumlem 26781 dchrvmasum2if 26791 dchrvmasumiflem2 26796 rpvmasum2 26806 dchrisum0re 26807 dchrvmasumlem 26817 rplogsum 26821 vmalogdivsum2 26832 vmalogdivsum 26833 2vmadivsumlem 26834 logsqvma 26836 logsqvma2 26837 selberg 26842 selbergb 26843 selberg2lem 26844 selberg2 26845 selberg2b 26846 chpdifbndlem1 26847 selberg3lem1 26851 selberg3lem2 26852 selberg3 26853 selberg4lem1 26854 selberg4 26855 pntrsumo1 26859 selbergr 26862 selberg3r 26863 selberg4r 26864 selberg34r 26865 pntsf 26867 pntsval2 26870 pntrlog2bndlem1 26871 pntpbnd1a 26879 |
Copyright terms: Public domain | W3C validator |