logfac2

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)

		Ref	Expression
	Assertion	logfac2	$⊢ (A \in ℝ \land 0 \leq A) \to \log ⌊A⌋! = \sum_{k = 1}^{⌊A⌋} Λ (k) ⌊\frac{A}{k}⌋$

Proof

Step	Hyp	Ref	Expression
1		flge0nn0	$⊢ (A \in ℝ \land 0 \leq A) \to ⌊A⌋ \in ℕ_{0}$
2		logfac	$⊢ ⌊A⌋ \in ℕ_{0} \to \log ⌊A⌋! = \sum_{n = 1}^{⌊A⌋} \log n$
3	1 2	syl	$⊢ (A \in ℝ \land 0 \leq A) \to \log ⌊A⌋! = \sum_{n = 1}^{⌊A⌋} \log n$
4		fzfid	$⊢ (A \in ℝ \land 0 \leq A) \to (1 \dots ⌊A⌋) \in Fin$
5		fzfid	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊A⌋) \in Fin$
6		ssrab2	$⊢ \{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \subseteq (1 \dots ⌊A⌋)$
7		ssfi	$⊢ ((1 \dots ⌊A⌋) \in Fin \land \{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \subseteq (1 \dots ⌊A⌋)) \to \{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \in Fin$
8	5 6 7	sylancl	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \in Fin$
9		flcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℤ$
10	9	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to ⌊A⌋ \in ℤ$
11		fznn	$⊢ ⌊A⌋ \in ℤ \to (k \in (1 \dots ⌊A⌋) \leftrightarrow (k \in ℕ \land k \leq ⌊A⌋))$
12	10 11	syl	$⊢ (A \in ℝ \land 0 \leq A) \to (k \in (1 \dots ⌊A⌋) \leftrightarrow (k \in ℕ \land k \leq ⌊A⌋))$
13	12	anbi1d	$⊢ (A \in ℝ \land 0 \leq A) \to ((k \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \leftrightarrow ((k \in ℕ \land k \leq ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)))$
14		nnre	$⊢ k \in ℕ \to k \in ℝ$
15	14	ad2antlr	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k \in ℝ$
16		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
17	16	ad2antrl	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to n \in ℕ$
18	17	nnred	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to n \in ℝ$
19		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
20	19	ad3antrrr	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to ⌊A⌋ \in ℝ$
21		simprr	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k ∥ n$
22		nnz	$⊢ k \in ℕ \to k \in ℤ$
23	22	ad2antlr	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k \in ℤ$
24		dvdsle	$⊢ (k \in ℤ \land n \in ℕ) \to (k ∥ n \to k \leq n)$
25	23 17 24	syl2anc	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to (k ∥ n \to k \leq n)$
26	21 25	mpd	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k \leq n$
27		elfzle2	$⊢ n \in (1 \dots ⌊A⌋) \to n \leq ⌊A⌋$
28	27	ad2antrl	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to n \leq ⌊A⌋$
29	15 18 20 26 28	letrd	$⊢ (((A \in ℝ \land 0 \leq A) \land k \in ℕ) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k \leq ⌊A⌋$
30	29	expl	$⊢ (A \in ℝ \land 0 \leq A) \to ((k \in ℕ \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \to k \leq ⌊A⌋)$
31	30	pm4.71rd	$⊢ (A \in ℝ \land 0 \leq A) \to ((k \in ℕ \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \leftrightarrow (k \leq ⌊A⌋ \land (k \in ℕ \land (n \in (1 \dots ⌊A⌋) \land k ∥ n))))$
32		an12	$⊢ (n \in (1 \dots ⌊A⌋) \land (k \in ℕ \land k ∥ n)) \leftrightarrow (k \in ℕ \land (n \in (1 \dots ⌊A⌋) \land k ∥ n))$
33		an21	$⊢ ((k \in ℕ \land k \leq ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \leftrightarrow (k \leq ⌊A⌋ \land (k \in ℕ \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)))$
34	31 32 33	3bitr4g	$⊢ (A \in ℝ \land 0 \leq A) \to ((n \in (1 \dots ⌊A⌋) \land (k \in ℕ \land k ∥ n)) \leftrightarrow ((k \in ℕ \land k \leq ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)))$
35	13 34	bitr4d	$⊢ (A \in ℝ \land 0 \leq A) \to ((k \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n)) \leftrightarrow (n \in (1 \dots ⌊A⌋) \land (k \in ℕ \land k ∥ n)))$
36		breq2	$⊢ x = n \to (k ∥ x \leftrightarrow k ∥ n)$
37	36	elrab	$⊢ n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \leftrightarrow (n \in (1 \dots ⌊A⌋) \land k ∥ n)$
38	37	anbi2i	$⊢ (k \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}) \leftrightarrow (k \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land k ∥ n))$
39		breq1	$⊢ x = k \to (x ∥ n \leftrightarrow k ∥ n)$
40	39	elrab	$⊢ k \in \{x \in ℕ \| x ∥ n\} \leftrightarrow (k \in ℕ \land k ∥ n)$
41	40	anbi2i	$⊢ (n \in (1 \dots ⌊A⌋) \land k \in \{x \in ℕ \| x ∥ n\}) \leftrightarrow (n \in (1 \dots ⌊A⌋) \land (k \in ℕ \land k ∥ n))$
42	35 38 41	3bitr4g	$⊢ (A \in ℝ \land 0 \leq A) \to ((k \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}) \leftrightarrow (n \in (1 \dots ⌊A⌋) \land k \in \{x \in ℕ \| x ∥ n\}))$
43		elfznn	$⊢ k \in (1 \dots ⌊A⌋) \to k \in ℕ$
44	43	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to k \in ℕ$
45		vmacl	$⊢ k \in ℕ \to Λ (k) \in ℝ$
46	44 45	syl	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to Λ (k) \in ℝ$
47	46	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to Λ (k) \in ℂ$
48	47	adantrr	$⊢ ((A \in ℝ \land 0 \leq A) \land (k \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\})) \to Λ (k) \in ℂ$
49	4 4 8 42 48	fsumcom2	$⊢ (A \in ℝ \land 0 \leq A) \to \sum_{k = 1}^{⌊A⌋} \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}} Λ (k) = \sum_{n = 1}^{⌊A⌋} \sum_{k \in \{x \in ℕ \| x ∥ n\}} Λ (k)$
50		fsumconst	$⊢ (\{x \in (1 \dots ⌊A⌋) \| k ∥ x\} \in Fin \land Λ (k) \in ℂ) \to \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}} Λ (k) = \|\{x \in (1 \dots ⌊A⌋) \| k ∥ x\}\| Λ (k)$
51	8 47 50	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}} Λ (k) = \|\{x \in (1 \dots ⌊A⌋) \| k ∥ x\}\| Λ (k)$
52		fzfid	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{k}⌋) \in Fin$
53		simpll	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to A \in ℝ$
54		eqid	$⊢ (m \in (1 \dots ⌊\frac{A}{k}⌋) ⟼ k m) = (m \in (1 \dots ⌊\frac{A}{k}⌋) ⟼ k m)$
55	53 44 54	dvdsflf1o	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to (m \in (1 \dots ⌊\frac{A}{k}⌋) ⟼ k m) : (1 \dots ⌊\frac{A}{k}⌋) \underset{1-1 onto}{⟶} \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}$
56	52 55	hasheqf1od	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \|(1 \dots ⌊\frac{A}{k}⌋)\| = \|\{x \in (1 \dots ⌊A⌋) \| k ∥ x\}\|$
57		simpl	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℝ$
58		nndivre	$⊢ (A \in ℝ \land k \in ℕ) \to \frac{A}{k} \in ℝ$
59	57 43 58	syl2an	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \frac{A}{k} \in ℝ$
60		nngt0	$⊢ k \in ℕ \to 0 < k$
61	14 60	jca	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
62	43 61	syl	$⊢ k \in (1 \dots ⌊A⌋) \to (k \in ℝ \land 0 < k)$
63		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{A}{k}$
64	62 63	sylan2	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to 0 \leq \frac{A}{k}$
65		flge0nn0	$⊢ (\frac{A}{k} \in ℝ \land 0 \leq \frac{A}{k}) \to ⌊\frac{A}{k}⌋ \in ℕ_{0}$
66	59 64 65	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to ⌊\frac{A}{k}⌋ \in ℕ_{0}$
67		hashfz1	$⊢ ⌊\frac{A}{k}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{A}{k}⌋)\| = ⌊\frac{A}{k}⌋$
68	66 67	syl	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \|(1 \dots ⌊\frac{A}{k}⌋)\| = ⌊\frac{A}{k}⌋$
69	56 68	eqtr3d	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \|\{x \in (1 \dots ⌊A⌋) \| k ∥ x\}\| = ⌊\frac{A}{k}⌋$
70	69	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \|\{x \in (1 \dots ⌊A⌋) \| k ∥ x\}\| Λ (k) = ⌊\frac{A}{k}⌋ Λ (k)$
71	59	flcld	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to ⌊\frac{A}{k}⌋ \in ℤ$
72	71	zcnd	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to ⌊\frac{A}{k}⌋ \in ℂ$
73	72 47	mulcomd	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to ⌊\frac{A}{k}⌋ Λ (k) = Λ (k) ⌊\frac{A}{k}⌋$
74	51 70 73	3eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land k \in (1 \dots ⌊A⌋)) \to \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}} Λ (k) = Λ (k) ⌊\frac{A}{k}⌋$
75	74	sumeq2dv	$⊢ (A \in ℝ \land 0 \leq A) \to \sum_{k = 1}^{⌊A⌋} \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| k ∥ x\}} Λ (k) = \sum_{k = 1}^{⌊A⌋} Λ (k) ⌊\frac{A}{k}⌋$
76	16	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
77		vmasum	$⊢ n \in ℕ \to \sum_{k \in \{x \in ℕ \| x ∥ n\}} Λ (k) = \log n$
78	76 77	syl	$⊢ ((A \in ℝ \land 0 \leq A) \land n \in (1 \dots ⌊A⌋)) \to \sum_{k \in \{x \in ℕ \| x ∥ n\}} Λ (k) = \log n$
79	78	sumeq2dv	$⊢ (A \in ℝ \land 0 \leq A) \to \sum_{n = 1}^{⌊A⌋} \sum_{k \in \{x \in ℕ \| x ∥ n\}} Λ (k) = \sum_{n = 1}^{⌊A⌋} \log n$
80	49 75 79	3eqtr3d	$⊢ (A \in ℝ \land 0 \leq A) \to \sum_{k = 1}^{⌊A⌋} Λ (k) ⌊\frac{A}{k}⌋ = \sum_{n = 1}^{⌊A⌋} \log n$
81	3 80	eqtr4d	$⊢ (A \in ℝ \land 0 \leq A) \to \log ⌊A⌋! = \sum_{k = 1}^{⌊A⌋} Λ (k) ⌊\frac{A}{k}⌋$

Metamath Proof Explorer

Theorem logfac2

Proof