logfaclbnd

Description: A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016)

		Ref	Expression
	Assertion	logfaclbnd	$⊢ A \in ℝ^{+} \to A (\log A - 2) \leq \log ⌊A⌋!$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
2	1	times2d	$⊢ A \in ℝ^{+} \to A \cdot 2 = A + A$
3	2	oveq2d	$⊢ A \in ℝ^{+} \to A \log A - A \cdot 2 = A \log A - (A + A)$
4		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
5	4	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
6		2cnd	$⊢ A \in ℝ^{+} \to 2 \in ℂ$
7	1 5 6	subdid	$⊢ A \in ℝ^{+} \to A (\log A - 2) = A \log A - A \cdot 2$
8		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
9	8 4	remulcld	$⊢ A \in ℝ^{+} \to A \log A \in ℝ$
10	9	recnd	$⊢ A \in ℝ^{+} \to A \log A \in ℂ$
11	10 1 1	subsub4d	$⊢ A \in ℝ^{+} \to A \log A - A - A = A \log A - (A + A)$
12	3 7 11	3eqtr4d	$⊢ A \in ℝ^{+} \to A (\log A - 2) = A \log A - A - A$
13	9 8	resubcld	$⊢ A \in ℝ^{+} \to A \log A - A \in ℝ$
14		fzfid	$⊢ A \in ℝ^{+} \to (1 \dots ⌊A⌋) \in Fin$
15		fzfid	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to (1 \dots n) \in Fin$
16		elfznn	$⊢ d \in (1 \dots n) \to d \in ℕ$
17	16	adantl	$⊢ ((A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \land d \in (1 \dots n)) \to d \in ℕ$
18	17	nnrecred	$⊢ ((A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \land d \in (1 \dots n)) \to \frac{1}{d} \in ℝ$
19	15 18	fsumrecl	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to \sum_{d = 1}^{n} (\frac{1}{d}) \in ℝ$
20	14 19	fsumrecl	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d}) \in ℝ$
21		rprege0	$⊢ A \in ℝ^{+} \to (A \in ℝ \land 0 \leq A)$
22		flge0nn0	$⊢ (A \in ℝ \land 0 \leq A) \to ⌊A⌋ \in ℕ_{0}$
23	21 22	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℕ_{0}$
24	23	faccld	$⊢ A \in ℝ^{+} \to ⌊A⌋! \in ℕ$
25	24	nnrpd	$⊢ A \in ℝ^{+} \to ⌊A⌋! \in ℝ^{+}$
26	25	relogcld	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! \in ℝ$
27	26 8	readdcld	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! + A \in ℝ$
28		elfznn	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℕ$
29	28	adantl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d \in ℕ$
30	29	nnrecred	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \frac{1}{d} \in ℝ$
31	14 30	fsumrecl	$⊢ A \in ℝ^{+} \to \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) \in ℝ$
32	8 31	remulcld	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) \in ℝ$
33		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
34	8 33	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℝ$
35	32 34	resubcld	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) - ⌊A⌋ \in ℝ$
36		harmoniclbnd	$⊢ A \in ℝ^{+} \to \log A \leq \sum_{d = 1}^{⌊A⌋} (\frac{1}{d})$
37		rpregt0	$⊢ A \in ℝ^{+} \to (A \in ℝ \land 0 < A)$
38		lemul2	$⊢ (\log A \in ℝ \land \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) \in ℝ \land (A \in ℝ \land 0 < A)) \to (\log A \leq \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) \leftrightarrow A \log A \leq A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}))$
39	4 31 37 38	syl3anc	$⊢ A \in ℝ^{+} \to (\log A \leq \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) \leftrightarrow A \log A \leq A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}))$
40	36 39	mpbid	$⊢ A \in ℝ^{+} \to A \log A \leq A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d})$
41		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
42	8 41	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \leq A$
43	9 34 32 8 40 42	le2subd	$⊢ A \in ℝ^{+} \to A \log A - A \leq A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) - ⌊A⌋$
44	28	nnrecred	$⊢ d \in (1 \dots ⌊A⌋) \to \frac{1}{d} \in ℝ$
45		remulcl	$⊢ (A \in ℝ \land \frac{1}{d} \in ℝ) \to A (\frac{1}{d}) \in ℝ$
46	8 44 45	syl2an	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) \in ℝ$
47		peano2rem	$⊢ A (\frac{1}{d}) \in ℝ \to A (\frac{1}{d}) - 1 \in ℝ$
48	46 47	syl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) - 1 \in ℝ$
49		fzfid	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to (d \dots ⌊A⌋) \in Fin$
50	30	adantr	$⊢ ((A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \land n \in (d \dots ⌊A⌋)) \to \frac{1}{d} \in ℝ$
51	49 50	fsumrecl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \sum_{n = d}^{⌊A⌋} (\frac{1}{d}) \in ℝ$
52	8	adantr	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A \in ℝ$
53	52 33	syl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ \in ℝ$
54		peano2re	$⊢ ⌊A⌋ \in ℝ \to ⌊A⌋ + 1 \in ℝ$
55	53 54	syl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ + 1 \in ℝ$
56	29	nnred	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d \in ℝ$
57		fllep1	$⊢ A \in ℝ \to A \leq ⌊A⌋ + 1$
58	8 57	syl	$⊢ A \in ℝ^{+} \to A \leq ⌊A⌋ + 1$
59	58	adantr	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A \leq ⌊A⌋ + 1$
60	52 55 56 59	lesub1dd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A - d \leq ⌊A⌋ + 1 - d$
61	52 56	resubcld	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A - d \in ℝ$
62	55 56	resubcld	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ + 1 - d \in ℝ$
63	29	nnrpd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d \in ℝ^{+}$
64	63	rpreccld	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \frac{1}{d} \in ℝ^{+}$
65	61 62 64	lemul1d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to (A - d \leq ⌊A⌋ + 1 - d \leftrightarrow (A - d) (\frac{1}{d}) \leq (⌊A⌋ + 1 - d) (\frac{1}{d}))$
66	60 65	mpbid	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to (A - d) (\frac{1}{d}) \leq (⌊A⌋ + 1 - d) (\frac{1}{d})$
67	1	adantr	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A \in ℂ$
68	29	nncnd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d \in ℂ$
69	30	recnd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \frac{1}{d} \in ℂ$
70	67 68 69	subdird	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to (A - d) (\frac{1}{d}) = A (\frac{1}{d}) - d (\frac{1}{d})$
71	29	nnne0d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d \neq 0$
72	68 71	recidd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to d (\frac{1}{d}) = 1$
73	72	oveq2d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) - d (\frac{1}{d}) = A (\frac{1}{d}) - 1$
74	70 73	eqtr2d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) - 1 = (A - d) (\frac{1}{d})$
75		fsumconst	$⊢ ((d \dots ⌊A⌋) \in Fin \land \frac{1}{d} \in ℂ) \to \sum_{n = d}^{⌊A⌋} (\frac{1}{d}) = \|(d \dots ⌊A⌋)\| (\frac{1}{d})$
76	49 69 75	syl2anc	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \sum_{n = d}^{⌊A⌋} (\frac{1}{d}) = \|(d \dots ⌊A⌋)\| (\frac{1}{d})$
77		elfzuz3	$⊢ d \in (1 \dots ⌊A⌋) \to ⌊A⌋ \in ℤ_{\geq d}$
78	77	adantl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ \in ℤ_{\geq d}$
79		hashfz	$⊢ ⌊A⌋ \in ℤ_{\geq d} \to \|(d \dots ⌊A⌋)\| = ⌊A⌋ - d + 1$
80	78 79	syl	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \|(d \dots ⌊A⌋)\| = ⌊A⌋ - d + 1$
81	34	recnd	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℂ$
82	81	adantr	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ \in ℂ$
83		1cnd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to 1 \in ℂ$
84	82 83 68	addsubd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to ⌊A⌋ + 1 - d = ⌊A⌋ - d + 1$
85	80 84	eqtr4d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \|(d \dots ⌊A⌋)\| = ⌊A⌋ + 1 - d$
86	85	oveq1d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \|(d \dots ⌊A⌋)\| (\frac{1}{d}) = (⌊A⌋ + 1 - d) (\frac{1}{d})$
87	76 86	eqtrd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to \sum_{n = d}^{⌊A⌋} (\frac{1}{d}) = (⌊A⌋ + 1 - d) (\frac{1}{d})$
88	66 74 87	3brtr4d	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) - 1 \leq \sum_{n = d}^{⌊A⌋} (\frac{1}{d})$
89	14 48 51 88	fsumle	$⊢ A \in ℝ^{+} \to \sum_{d = 1}^{⌊A⌋} (A (\frac{1}{d}) - 1) \leq \sum_{d = 1}^{⌊A⌋} \sum_{n = d}^{⌊A⌋} (\frac{1}{d})$
90	14 1 69	fsummulc2	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) = \sum_{d = 1}^{⌊A⌋} A (\frac{1}{d})$
91		ax-1cn	$⊢ 1 \in ℂ$
92		fsumconst	$⊢ ((1 \dots ⌊A⌋) \in Fin \land 1 \in ℂ) \to \sum_{d = 1}^{⌊A⌋} 1 = \|(1 \dots ⌊A⌋)\| \cdot 1$
93	14 91 92	sylancl	$⊢ A \in ℝ^{+} \to \sum_{d = 1}^{⌊A⌋} 1 = \|(1 \dots ⌊A⌋)\| \cdot 1$
94		hashfz1	$⊢ ⌊A⌋ \in ℕ_{0} \to \|(1 \dots ⌊A⌋)\| = ⌊A⌋$
95	23 94	syl	$⊢ A \in ℝ^{+} \to \|(1 \dots ⌊A⌋)\| = ⌊A⌋$
96	95	oveq1d	$⊢ A \in ℝ^{+} \to \|(1 \dots ⌊A⌋)\| \cdot 1 = ⌊A⌋ \cdot 1$
97	81	mulridd	$⊢ A \in ℝ^{+} \to ⌊A⌋ \cdot 1 = ⌊A⌋$
98	93 96 97	3eqtrrd	$⊢ A \in ℝ^{+} \to ⌊A⌋ = \sum_{d = 1}^{⌊A⌋} 1$
99	90 98	oveq12d	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) - ⌊A⌋ = \sum_{d = 1}^{⌊A⌋} A (\frac{1}{d}) - \sum_{d = 1}^{⌊A⌋} 1$
100	46	recnd	$⊢ (A \in ℝ^{+} \land d \in (1 \dots ⌊A⌋)) \to A (\frac{1}{d}) \in ℂ$
101	14 100 83	fsumsub	$⊢ A \in ℝ^{+} \to \sum_{d = 1}^{⌊A⌋} (A (\frac{1}{d}) - 1) = \sum_{d = 1}^{⌊A⌋} A (\frac{1}{d}) - \sum_{d = 1}^{⌊A⌋} 1$
102	99 101	eqtr4d	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) - ⌊A⌋ = \sum_{d = 1}^{⌊A⌋} (A (\frac{1}{d}) - 1)$
103		eqid	$⊢ ℤ_{\geq 1} = ℤ_{\geq 1}$
104	103	uztrn2	$⊢ (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}) \to n \in ℤ_{\geq 1}$
105	104	adantl	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to n \in ℤ_{\geq 1}$
106	105	biantrurd	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to (⌊A⌋ \in ℤ_{\geq n} \leftrightarrow (n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}))$
107		uzss	$⊢ n \in ℤ_{\geq d} \to ℤ_{\geq n} \subseteq ℤ_{\geq d}$
108	107	ad2antll	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to ℤ_{\geq n} \subseteq ℤ_{\geq d}$
109	108	sseld	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to (⌊A⌋ \in ℤ_{\geq n} \to ⌊A⌋ \in ℤ_{\geq d})$
110	109	pm4.71rd	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to (⌊A⌋ \in ℤ_{\geq n} \leftrightarrow (⌊A⌋ \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n}))$
111	106 110	bitr3d	$⊢ (A \in ℝ^{+} \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \to ((n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}) \leftrightarrow (⌊A⌋ \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n}))$
112	111	pm5.32da	$⊢ A \in ℝ^{+} \to (((d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}) \land (n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n})) \leftrightarrow ((d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}) \land (⌊A⌋ \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n})))$
113		ancom	$⊢ ((n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}) \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \leftrightarrow ((d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}) \land (n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}))$
114		an4	$⊢ ((d \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq d}) \land (n \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n})) \leftrightarrow ((d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}) \land (⌊A⌋ \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n}))$
115	112 113 114	3bitr4g	$⊢ A \in ℝ^{+} \to (((n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}) \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})) \leftrightarrow ((d \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq d}) \land (n \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n})))$
116		elfzuzb	$⊢ n \in (1 \dots ⌊A⌋) \leftrightarrow (n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n})$
117		elfzuzb	$⊢ d \in (1 \dots n) \leftrightarrow (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d})$
118	116 117	anbi12i	$⊢ (n \in (1 \dots ⌊A⌋) \land d \in (1 \dots n)) \leftrightarrow ((n \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq n}) \land (d \in ℤ_{\geq 1} \land n \in ℤ_{\geq d}))$
119		elfzuzb	$⊢ d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq d})$
120		elfzuzb	$⊢ n \in (d \dots ⌊A⌋) \leftrightarrow (n \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n})$
121	119 120	anbi12i	$⊢ (d \in (1 \dots ⌊A⌋) \land n \in (d \dots ⌊A⌋)) \leftrightarrow ((d \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ_{\geq d}) \land (n \in ℤ_{\geq d} \land ⌊A⌋ \in ℤ_{\geq n}))$
122	115 118 121	3bitr4g	$⊢ A \in ℝ^{+} \to ((n \in (1 \dots ⌊A⌋) \land d \in (1 \dots n)) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land n \in (d \dots ⌊A⌋)))$
123	18	recnd	$⊢ ((A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \land d \in (1 \dots n)) \to \frac{1}{d} \in ℂ$
124	123	anasss	$⊢ (A \in ℝ^{+} \land (n \in (1 \dots ⌊A⌋) \land d \in (1 \dots n))) \to \frac{1}{d} \in ℂ$
125	14 14 15 122 124	fsumcom2	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d}) = \sum_{d = 1}^{⌊A⌋} \sum_{n = d}^{⌊A⌋} (\frac{1}{d})$
126	89 102 125	3brtr4d	$⊢ A \in ℝ^{+} \to A \sum_{d = 1}^{⌊A⌋} (\frac{1}{d}) - ⌊A⌋ \leq \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d})$
127	13 35 20 43 126	letrd	$⊢ A \in ℝ^{+} \to A \log A - A \leq \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d})$
128	26 34	readdcld	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! + ⌊A⌋ \in ℝ$
129		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
130	129	adantl	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
131	130	nnrpd	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to n \in ℝ^{+}$
132	131	relogcld	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to \log n \in ℝ$
133		peano2re	$⊢ \log n \in ℝ \to \log n + 1 \in ℝ$
134	132 133	syl	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to \log n + 1 \in ℝ$
135		nnz	$⊢ n \in ℕ \to n \in ℤ$
136		flid	$⊢ n \in ℤ \to ⌊n⌋ = n$
137	135 136	syl	$⊢ n \in ℕ \to ⌊n⌋ = n$
138	137	oveq2d	$⊢ n \in ℕ \to (1 \dots ⌊n⌋) = (1 \dots n)$
139	138	sumeq1d	$⊢ n \in ℕ \to \sum_{d = 1}^{⌊n⌋} (\frac{1}{d}) = \sum_{d = 1}^{n} (\frac{1}{d})$
140		nnre	$⊢ n \in ℕ \to n \in ℝ$
141		nnge1	$⊢ n \in ℕ \to 1 \leq n$
142		harmonicubnd	$⊢ (n \in ℝ \land 1 \leq n) \to \sum_{d = 1}^{⌊n⌋} (\frac{1}{d}) \leq \log n + 1$
143	140 141 142	syl2anc	$⊢ n \in ℕ \to \sum_{d = 1}^{⌊n⌋} (\frac{1}{d}) \leq \log n + 1$
144	139 143	eqbrtrrd	$⊢ n \in ℕ \to \sum_{d = 1}^{n} (\frac{1}{d}) \leq \log n + 1$
145	130 144	syl	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to \sum_{d = 1}^{n} (\frac{1}{d}) \leq \log n + 1$
146	14 19 134 145	fsumle	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d}) \leq \sum_{n = 1}^{⌊A⌋} (\log n + 1)$
147	132	recnd	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to \log n \in ℂ$
148		1cnd	$⊢ (A \in ℝ^{+} \land n \in (1 \dots ⌊A⌋)) \to 1 \in ℂ$
149	14 147 148	fsumadd	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} (\log n + 1) = \sum_{n = 1}^{⌊A⌋} \log n + \sum_{n = 1}^{⌊A⌋} 1$
150		logfac	$⊢ ⌊A⌋ \in ℕ_{0} \to \log ⌊A⌋! = \sum_{n = 1}^{⌊A⌋} \log n$
151	23 150	syl	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! = \sum_{n = 1}^{⌊A⌋} \log n$
152		fsumconst	$⊢ ((1 \dots ⌊A⌋) \in Fin \land 1 \in ℂ) \to \sum_{n = 1}^{⌊A⌋} 1 = \|(1 \dots ⌊A⌋)\| \cdot 1$
153	14 91 152	sylancl	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} 1 = \|(1 \dots ⌊A⌋)\| \cdot 1$
154	153 96 97	3eqtrrd	$⊢ A \in ℝ^{+} \to ⌊A⌋ = \sum_{n = 1}^{⌊A⌋} 1$
155	151 154	oveq12d	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! + ⌊A⌋ = \sum_{n = 1}^{⌊A⌋} \log n + \sum_{n = 1}^{⌊A⌋} 1$
156	149 155	eqtr4d	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} (\log n + 1) = \log ⌊A⌋! + ⌊A⌋$
157	146 156	breqtrd	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d}) \leq \log ⌊A⌋! + ⌊A⌋$
158	34 8 26 42	leadd2dd	$⊢ A \in ℝ^{+} \to \log ⌊A⌋! + ⌊A⌋ \leq \log ⌊A⌋! + A$
159	20 128 27 157 158	letrd	$⊢ A \in ℝ^{+} \to \sum_{n = 1}^{⌊A⌋} \sum_{d = 1}^{n} (\frac{1}{d}) \leq \log ⌊A⌋! + A$
160	13 20 27 127 159	letrd	$⊢ A \in ℝ^{+} \to A \log A - A \leq \log ⌊A⌋! + A$
161	13 8 26	lesubaddd	$⊢ A \in ℝ^{+} \to (A \log A - A - A \leq \log ⌊A⌋! \leftrightarrow A \log A - A \leq \log ⌊A⌋! + A)$
162	160 161	mpbird	$⊢ A \in ℝ^{+} \to A \log A - A - A \leq \log ⌊A⌋!$
163	12 162	eqbrtrd	$⊢ A \in ℝ^{+} \to A (\log A - 2) \leq \log ⌊A⌋!$

Metamath Proof Explorer

Theorem logfaclbnd

Proof