Theorem vmacl 25787

Description: Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)

Assertion

Ref	Expression
vmacl	⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ)

Proof of Theorem vmacl

Dummy variables 𝑘 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2838	. 2 ⊢ ((Λ‘𝐴) = 0 → ((Λ‘𝐴) ∈ ℝ ↔ 0 ∈ ℝ))
2		isppw2 25784	. . . 4 ⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)))
3		vmappw 25785	. . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝))
4		prmnn 16055	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
5	4	nnrpd 12455	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ+)
6	5	relogcld 25298	. . . . . . . 8 ⊢ (𝑝 ∈ ℙ → (log‘𝑝) ∈ ℝ)
7	6	adantr 485	. . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℝ)
8	3, 7	eqeltrd 2851	. . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) ∈ ℝ)
9		fveq2 6651	. . . . . . 7 ⊢ (𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) = (Λ‘(𝑝↑𝑘)))
10	9	eleq1d 2835	. . . . . 6 ⊢ (𝐴 = (𝑝↑𝑘) → ((Λ‘𝐴) ∈ ℝ ↔ (Λ‘(𝑝↑𝑘)) ∈ ℝ))
11	8, 10	syl5ibrcom 250	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) ∈ ℝ))
12	11	rexlimivv 3214	. . . 4 ⊢ (∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘) → (Λ‘𝐴) ∈ ℝ)
13	2, 12	syl6bi 256	. . 3 ⊢ (𝐴 ∈ ℕ → ((Λ‘𝐴) ≠ 0 → (Λ‘𝐴) ∈ ℝ))
14	13	imp 411	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (Λ‘𝐴) ≠ 0) → (Λ‘𝐴) ∈ ℝ)
15		0red 10667	. 2 ⊢ (𝐴 ∈ ℕ → 0 ∈ ℝ)
16	1, 14, 15	pm2.61ne 3034	1 ⊢ (𝐴 ∈ ℕ → (Λ‘𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∃wrex 3069  ‘cfv 6328  (class class class)co 7143  ℝcr 10559  0cc0 10560  ℕcn 11659  ↑cexp 13464  ℙcprime 16052  logclog 25230  Λcvma 25761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-inf2 9122  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-pre-sup 10638  ax-addf 10639  ax-mulf 10640

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8473  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-fi 8893  df-sup 8924  df-inf 8925  df-oi 8992  df-dju 9348  df-card 9386  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-div 11321  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-z 12006  df-dec 12123  df-uz 12268  df-q 12374  df-rp 12416  df-xneg 12533  df-xadd 12534  df-xmul 12535  df-ioo 12768  df-ioc 12769  df-ico 12770  df-icc 12771  df-fz 12925  df-fzo 13068  df-fl 13196  df-mod 13272  df-seq 13404  df-exp 13465  df-fac 13669  df-bc 13698  df-hash 13726  df-shft 14459  df-cj 14491  df-re 14492  df-im 14493  df-sqrt 14627  df-abs 14628  df-limsup 14861  df-clim 14878  df-rlim 14879  df-sum 15076  df-ef 15454  df-sin 15456  df-cos 15457  df-pi 15459  df-dvds 15641  df-gcd 15879  df-prm 16053  df-pc 16214  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-starv 16623  df-sca 16624  df-vsca 16625  df-ip 16626  df-tset 16627  df-ple 16628  df-ds 16630  df-unif 16631  df-hom 16632  df-cco 16633  df-rest 16739  df-topn 16740  df-0g 16758  df-gsum 16759  df-topgen 16760  df-pt 16761  df-prds 16764  df-xrs 16818  df-qtop 16823  df-imas 16824  df-xps 16826  df-mre 16900  df-mrc 16901  df-acs 16903  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-submnd 18008  df-mulg 18277  df-cntz 18499  df-cmn 18960  df-psmet 20143  df-xmet 20144  df-met 20145  df-bl 20146  df-mopn 20147  df-fbas 20148  df-fg 20149  df-cnfld 20152  df-top 21579  df-topon 21596  df-topsp 21618  df-bases 21631  df-cld 21704  df-ntr 21705  df-cls 21706  df-nei 21783  df-lp 21821  df-perf 21822  df-cn 21912  df-cnp 21913  df-haus 22000  df-tx 22247  df-hmeo 22440  df-fil 22531  df-fm 22623  df-flim 22624  df-flf 22625  df-xms 23007  df-ms 23008  df-tms 23009  df-cncf 23564  df-limc 24550  df-dv 24551  df-log 25232  df-vma 25767

This theorem is referenced by:  vmaf  25788  vmage0  25790  chpf  25792  efchpcl  25794  chpp1  25824  chpwordi  25826  chtlepsi  25874  vmasum  25884  logfac2  25885  chpval2  25886  vmadivsum  26150  vmadivsumb  26151  rplogsumlem2  26153  rpvmasumlem  26155  dchrvmasum2if  26165  dchrvmasumiflem2  26170  rpvmasum2  26180  dchrisum0re  26181  dchrvmasumlem  26191  rplogsum  26195  vmalogdivsum2  26206  vmalogdivsum  26207  2vmadivsumlem  26208  logsqvma  26210  logsqvma2  26211  selberg  26216  selbergb  26217  selberg2lem  26218  selberg2  26219  selberg2b  26220  chpdifbndlem1  26221  selberg3lem1  26225  selberg3lem2  26226  selberg3  26227  selberg4lem1  26228  selberg4  26229  pntrsumo1  26233  selbergr  26236  selberg3r  26237  selberg4r  26238  selberg34r  26239  pntsf  26241  pntsval2  26244  pntrlog2bndlem1  26245  pntpbnd1a  26253