MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  logfac2 Structured version   Visualization version   GIF version

Theorem logfac2 25511
Description: Another expression for the logarithm of a factorial, in terms of the von Mangoldt function. Equation 9.2.7 of [Shapiro], p. 329. (Contributed by Mario Carneiro, 15-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Assertion
Ref Expression
logfac2 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))))
Distinct variable group:   𝐴,𝑘

Proof of Theorem logfac2
Dummy variables 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flge0nn0 13004 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
2 logfac 24901 . . 3 ((⌊‘𝐴) ∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
31, 2syl 17 . 2 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
4 fzfid 13155 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (1...(⌊‘𝐴)) ∈ Fin)
5 fzfid 13155 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘𝐴)) ∈ Fin)
6 ssrab2 3941 . . . . 5 {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ⊆ (1...(⌊‘𝐴))
7 ssfi 8532 . . . . 5 (((1...(⌊‘𝐴)) ∈ Fin ∧ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ⊆ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ∈ Fin)
85, 6, 7sylancl 578 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ∈ Fin)
9 flcl 12979 . . . . . . . . 9 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
109adantr 473 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℤ)
11 fznn 12790 . . . . . . . 8 ((⌊‘𝐴) ∈ ℤ → (𝑘 ∈ (1...(⌊‘𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴))))
1210, 11syl 17 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝑘 ∈ (1...(⌊‘𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴))))
1312anbi1d 621 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛))))
14 nnre 11446 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
1514ad2antlr 715 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘 ∈ ℝ)
16 elfznn 12751 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
1716ad2antrl 716 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑛 ∈ ℕ)
1817nnred 11455 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑛 ∈ ℝ)
19 reflcl 12980 . . . . . . . . . . 11 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ)
2019ad3antrrr 718 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → (⌊‘𝐴) ∈ ℝ)
21 simprr 761 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘𝑛)
22 nnz 11816 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
2322ad2antlr 715 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘 ∈ ℤ)
24 dvdsle 15519 . . . . . . . . . . . 12 ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑘𝑛𝑘𝑛))
2523, 17, 24syl2anc 576 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → (𝑘𝑛𝑘𝑛))
2621, 25mpd 15 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘𝑛)
27 elfzle2 12726 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ≤ (⌊‘𝐴))
2827ad2antrl 716 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑛 ≤ (⌊‘𝐴))
2915, 18, 20, 26, 28letrd 10596 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘 ≤ (⌊‘𝐴))
3029expl 450 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) → 𝑘 ≤ (⌊‘𝐴)))
3130pm4.71rd 555 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)))))
32 an12 633 . . . . . . 7 ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘𝑛)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)))
33 an21 632 . . . . . . 7 (((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛))))
3431, 32, 333bitr4g 306 . . . . . 6 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛))))
3513, 34bitr4d 274 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘𝑛))))
36 breq2 4930 . . . . . . 7 (𝑥 = 𝑛 → (𝑘𝑥𝑘𝑛))
3736elrab 3590 . . . . . 6 (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛))
3837anbi2i 614 . . . . 5 ((𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘𝑛)))
39 breq1 4929 . . . . . . 7 (𝑥 = 𝑘 → (𝑥𝑛𝑘𝑛))
4039elrab 3590 . . . . . 6 (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} ↔ (𝑘 ∈ ℕ ∧ 𝑘𝑛))
4140anbi2i 614 . . . . 5 ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘𝑛)))
4235, 38, 413bitr4g 306 . . . 4 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})))
43 elfznn 12751 . . . . . . . 8 (𝑘 ∈ (1...(⌊‘𝐴)) → 𝑘 ∈ ℕ)
4443adantl 474 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝑘 ∈ ℕ)
45 vmacl 25413 . . . . . . 7 (𝑘 ∈ ℕ → (Λ‘𝑘) ∈ ℝ)
4644, 45syl 17 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈ ℝ)
4746recnd 10467 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈ ℂ)
4847adantrr 705 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥})) → (Λ‘𝑘) ∈ ℂ)
494, 4, 8, 42, 48fsumcom2 14988 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} (Λ‘𝑘))
50 fsumconst 15004 . . . . . 6 (({𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} ∈ Fin ∧ (Λ‘𝑘) ∈ ℂ) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) · (Λ‘𝑘)))
518, 47, 50syl2anc 576 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) · (Λ‘𝑘)))
52 fzfid 13155 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑘))) ∈ Fin)
53 simpll 755 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ)
54 eqid 2773 . . . . . . . . 9 (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)) = (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚))
5553, 44, 54dvdsflf1o 25482 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)):(1...(⌊‘(𝐴 / 𝑘)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥})
5652, 55hasheqf1od 13528 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}))
57 simpl 475 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
58 nndivre 11480 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝐴 / 𝑘) ∈ ℝ)
5957, 43, 58syl2an 587 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑘) ∈ ℝ)
60 nngt0 11470 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 < 𝑘)
6114, 60jca 504 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
6243, 61syl 17 . . . . . . . . . 10 (𝑘 ∈ (1...(⌊‘𝐴)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
63 divge0 11309 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝐴 / 𝑘))
6462, 63sylan2 584 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 0 ≤ (𝐴 / 𝑘))
65 flge0nn0 13004 . . . . . . . . 9 (((𝐴 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑘)) → (⌊‘(𝐴 / 𝑘)) ∈ ℕ0)
6659, 64, 65syl2anc 576 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℕ0)
67 hashfz1 13520 . . . . . . . 8 ((⌊‘(𝐴 / 𝑘)) ∈ ℕ0 → (♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘)))
6866, 67syl 17 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘)))
6956, 68eqtr3d 2811 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) = (⌊‘(𝐴 / 𝑘)))
7069oveq1d 6990 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥}) · (Λ‘𝑘)) = ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘)))
7159flcld 12982 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℤ)
7271zcnd 11900 . . . . . 6 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℂ)
7372, 47mulcomd 10460 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘)) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))))
7451, 70, 733eqtrd 2813 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} (Λ‘𝑘) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))))
7574sumeq2dv 14919 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘𝑥} (Λ‘𝑘) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))))
7616adantl 474 . . . . 5 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
77 vmasum 25510 . . . . 5 (𝑛 ∈ ℕ → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} (Λ‘𝑘) = (log‘𝑛))
7876, 77syl 17 . . . 4 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} (Λ‘𝑘) = (log‘𝑛))
7978sumeq2dv 14919 . . 3 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
8049, 75, 793eqtr3d 2817 . 2 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
813, 80eqtr4d 2812 1 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1508  wcel 2051  {crab 3087  wss 3824   class class class wbr 4926  cmpt 5005  cfv 6186  (class class class)co 6975  Fincfn 8305  cc 10332  cr 10333  0cc0 10334  1c1 10335   · cmul 10339   < clt 10473  cle 10474   / cdiv 11097  cn 11438  0cn0 11706  cz 11792  ...cfz 12707  cfl 12974  !cfa 13447  chash 13504  Σcsu 14902  cdvds 15466  logclog 24855  Λcvma 25387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-inf2 8897  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412  ax-addf 10413  ax-mulf 10414
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-of 7226  df-om 7396  df-1st 7500  df-2nd 7501  df-supp 7633  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-2o 7905  df-oadd 7908  df-er 8088  df-map 8207  df-pm 8208  df-ixp 8259  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-fsupp 8628  df-fi 8669  df-sup 8700  df-inf 8701  df-oi 8768  df-dju 9123  df-card 9161  df-cda 9387  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-4 11504  df-5 11505  df-6 11506  df-7 11507  df-8 11508  df-9 11509  df-n0 11707  df-z 11793  df-dec 11911  df-uz 12058  df-q 12162  df-rp 12204  df-xneg 12323  df-xadd 12324  df-xmul 12325  df-ioo 12557  df-ioc 12558  df-ico 12559  df-icc 12560  df-fz 12708  df-fzo 12849  df-fl 12976  df-mod 13052  df-seq 13184  df-exp 13244  df-fac 13448  df-bc 13477  df-hash 13505  df-shft 14286  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-limsup 14688  df-clim 14705  df-rlim 14706  df-sum 14903  df-ef 15280  df-sin 15282  df-cos 15283  df-pi 15285  df-dvds 15467  df-gcd 15703  df-prm 15871  df-pc 16029  df-struct 16340  df-ndx 16341  df-slot 16342  df-base 16344  df-sets 16345  df-ress 16346  df-plusg 16433  df-mulr 16434  df-starv 16435  df-sca 16436  df-vsca 16437  df-ip 16438  df-tset 16439  df-ple 16440  df-ds 16442  df-unif 16443  df-hom 16444  df-cco 16445  df-rest 16551  df-topn 16552  df-0g 16570  df-gsum 16571  df-topgen 16572  df-pt 16573  df-prds 16576  df-xrs 16630  df-qtop 16635  df-imas 16636  df-xps 16638  df-mre 16728  df-mrc 16729  df-acs 16731  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-submnd 17817  df-mulg 18025  df-cntz 18231  df-cmn 18681  df-psmet 20255  df-xmet 20256  df-met 20257  df-bl 20258  df-mopn 20259  df-fbas 20260  df-fg 20261  df-cnfld 20264  df-top 21222  df-topon 21239  df-topsp 21261  df-bases 21274  df-cld 21347  df-ntr 21348  df-cls 21349  df-nei 21426  df-lp 21464  df-perf 21465  df-cn 21555  df-cnp 21556  df-haus 21643  df-tx 21890  df-hmeo 22083  df-fil 22174  df-fm 22266  df-flim 22267  df-flf 22268  df-xms 22649  df-ms 22650  df-tms 22651  df-cncf 23205  df-limc 24183  df-dv 24184  df-log 24857  df-vma 25393
This theorem is referenced by:  vmadivsum  25776
  Copyright terms: Public domain W3C validator