logfaclbnd - Metamath Proof Explorer

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

Theorem logfaclbnd 25806

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

**Assertion**
Ref	Expression
logfaclbnd	⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴))))

Proof of Theorem logfaclbnd Dummy variables 𝑑 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpcn 12387	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ)
2	1	times2d 11869	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · 2) = (𝐴 + 𝐴))
3	2	oveq2d 7151	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · (log‘𝐴)) − (𝐴 · 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴)))
4		relogcl 25167	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℝ)
5	4	recnd 10658	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℂ)
6		2cnd 11703	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → 2 ∈ ℂ)
7	1, 5, 6	subdid 11085	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · ((log‘𝐴) − 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 · 2)))
8		rpre 12385	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ)
9	8, 4	remulcld 10660	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · (log‘𝐴)) ∈ ℝ)
10	9	recnd 10658	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · (log‘𝐴)) ∈ ℂ)
11	10, 1, 1	subsub4d 11017	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → (((𝐴 · (log‘𝐴)) − 𝐴) − 𝐴) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴)))
12	3, 7, 11	3eqtr4d 2843	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · ((log‘𝐴) − 2)) = (((𝐴 · (log‘𝐴)) − 𝐴) − 𝐴))
13	9, 8	resubcld 11057	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · (log‘𝐴)) − 𝐴) ∈ ℝ)
14		fzfid 13336	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (1...(⌊‘𝐴)) ∈ Fin)
15		fzfid 13336	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1...𝑛) ∈ Fin)
16		elfznn 12931	. . . . . . . 8 ⊢ (𝑑 ∈ (1...𝑛) → 𝑑 ∈ ℕ)
17	16	adantl 485	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑑 ∈ (1...𝑛)) → 𝑑 ∈ ℕ)
18	17	nnrecred 11676	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈ ℝ)
19	15, 18	fsumrecl 15083	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ)
20	14, 19	fsumrecl 15083	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ)
21		rprege0 12392	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
22		flge0nn0 13185	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ₀)
23	21, 22	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) ∈ ℕ₀)
24	23	faccld 13640	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (!‘(⌊‘𝐴)) ∈ ℕ)
25	24	nnrpd 12417	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (!‘(⌊‘𝐴)) ∈ ℝ⁺)
26	25	relogcld 25214	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → (log‘(!‘(⌊‘𝐴))) ∈ ℝ)
27	26, 8	readdcld 10659	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝐴))) + 𝐴) ∈ ℝ)
28		elfznn 12931	. . . . . . . . . 10 ⊢ (𝑑 ∈ (1...(⌊‘𝐴)) → 𝑑 ∈ ℕ)
29	28	adantl 485	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℕ)
30	29	nnrecred 11676	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1 / 𝑑) ∈ ℝ)
31	14, 30	fsumrecl 15083	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ)
32	8, 31	remulcld 10660	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) ∈ ℝ)
33		reflcl 13161	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ)
34	8, 33	syl 17	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) ∈ ℝ)
35	32, 34	resubcld 11057	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴)) ∈ ℝ)
36		harmoniclbnd 25594	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑))
37		rpregt0 12391	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
38		lemul2 11482	. . . . . . . 8 ⊢ (((log‘𝐴) ∈ ℝ ∧ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑))))
39	4, 31, 37, 38	syl3anc 1368	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → ((log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑))))
40	36, 39	mpbid 235	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))
41		flle 13164	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ 𝐴)
42	8, 41	syl 17	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) ≤ 𝐴)
43	9, 34, 32, 8, 40, 42	le2subd 11249	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · (log‘𝐴)) − 𝐴) ≤ ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴)))
44	28	nnrecred 11676	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝐴)) → (1 / 𝑑) ∈ ℝ)
45		remulcl 10611	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (1 / 𝑑) ∈ ℝ) → (𝐴 · (1 / 𝑑)) ∈ ℝ)
46	8, 44, 45	syl2an 598	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 · (1 / 𝑑)) ∈ ℝ)
47		peano2rem 10942	. . . . . . . 8 ⊢ ((𝐴 · (1 / 𝑑)) ∈ ℝ → ((𝐴 · (1 / 𝑑)) − 1) ∈ ℝ)
48	46, 47	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 · (1 / 𝑑)) − 1) ∈ ℝ)
49		fzfid 13336	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝑑...(⌊‘𝐴)) ∈ Fin)
50	30	adantr 484	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) → (1 / 𝑑) ∈ ℝ)
51	49, 50	fsumrecl 15083	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ)
52	8	adantr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ)
53	52, 33	syl 17	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (⌊‘𝐴) ∈ ℝ)
54		peano2re 10802	. . . . . . . . . . 11 ⊢ ((⌊‘𝐴) ∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ)
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((⌊‘𝐴) + 1) ∈ ℝ)
56	29	nnred 11640	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℝ)
57		fllep1 13166	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1))
58	8, 57	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ≤ ((⌊‘𝐴) + 1))
59	58	adantr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝐴 ≤ ((⌊‘𝐴) + 1))
60	52, 55, 56, 59	lesub1dd 11245	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑))
61	52, 56	resubcld 11057	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 − 𝑑) ∈ ℝ)
62	55, 56	resubcld 11057	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (((⌊‘𝐴) + 1) − 𝑑) ∈ ℝ)
63	29	nnrpd 12417	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℝ⁺)
64	63	rpreccld 12429	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1 / 𝑑) ∈ ℝ⁺)
65	61, 62, 64	lemul1d 12462	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑) ↔ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))))
66	60, 65	mpbid 235	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))
67	1	adantr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℂ)
68	29	nncnd 11641	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℂ)
69	30	recnd 10658	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1 / 𝑑) ∈ ℂ)
70	67, 68, 69	subdird 11086	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 − 𝑑) · (1 / 𝑑)) = ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑))))
71	29	nnne0d 11675	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ≠ 0)
72	68, 71	recidd 11400	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝑑 · (1 / 𝑑)) = 1)
73	72	oveq2d 7151	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑))) = ((𝐴 · (1 / 𝑑)) − 1))
74	70, 73	eqtr2d 2834	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 · (1 / 𝑑)) − 1) = ((𝐴 − 𝑑) · (1 / 𝑑)))
75		fsumconst 15137	. . . . . . . . . 10 ⊢ (((𝑑...(⌊‘𝐴)) ∈ Fin ∧ (1 / 𝑑) ∈ ℂ) → Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)))
76	49, 69, 75	syl2anc 587	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)))
77		elfzuz3 12899	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ (1...(⌊‘𝐴)) → (⌊‘𝐴) ∈ (ℤ_≥‘𝑑))
78	77	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (⌊‘𝐴) ∈ (ℤ_≥‘𝑑))
79		hashfz 13784	. . . . . . . . . . . 12 ⊢ ((⌊‘𝐴) ∈ (ℤ_≥‘𝑑) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1))
80	78, 79	syl 17	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1))
81	34	recnd 10658	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) ∈ ℂ)
82	81	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (⌊‘𝐴) ∈ ℂ)
83		1cnd 10625	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 1 ∈ ℂ)
84	82, 83, 68	addsubd 11007	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (((⌊‘𝐴) + 1) − 𝑑) = (((⌊‘𝐴) − 𝑑) + 1))
85	80, 84	eqtr4d 2836	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) + 1) − 𝑑))
86	85	oveq1d 7150	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))
87	76, 86	eqtrd 2833	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))
88	66, 74, 87	3brtr4d 5062	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑))
89	14, 48, 51, 88	fsumle 15146	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑑 ∈ (1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑))
90	14, 1, 69	fsummulc2 15131	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)))
91		ax-1cn 10584	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
92		fsumconst 15137	. . . . . . . . . 10 ⊢ (((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑑 ∈ (1...(⌊‘𝐴))1 = ((♯‘(1...(⌊‘𝐴))) · 1))
93	14, 91, 92	sylancl 589	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑑 ∈ (1...(⌊‘𝐴))1 = ((♯‘(1...(⌊‘𝐴))) · 1))
94		hashfz1 13702	. . . . . . . . . . 11 ⊢ ((⌊‘𝐴) ∈ ℕ₀ → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴))
95	23, 94	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ⁺ → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴))
96	95	oveq1d 7150	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → ((♯‘(1...(⌊‘𝐴))) · 1) = ((⌊‘𝐴) · 1))
97	81	mulid1d 10647	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → ((⌊‘𝐴) · 1) = (⌊‘𝐴))
98	93, 96, 97	3eqtrrd 2838	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))1)
99	90, 98	oveq12d 7153	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴)) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1))
100	46	recnd 10658	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 · (1 / 𝑑)) ∈ ℂ)
101	14, 100, 83	fsumsub 15135	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑑 ∈ (1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1))
102	99, 101	eqtr4d 2836	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴)) = Σ𝑑 ∈ (1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1))
103		eqid 2798	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) = (ℤ_≥‘1)
104	103	uztrn2 12250	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)) → 𝑛 ∈ (ℤ_≥‘1))
105	104	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → 𝑛 ∈ (ℤ_≥‘1))
106	105	biantrurd 536	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → ((⌊‘𝐴) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
107		uzss 12253	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℤ_≥‘𝑑) → (ℤ_≥‘𝑛) ⊆ (ℤ_≥‘𝑑))
108	107	ad2antll 728	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → (ℤ_≥‘𝑛) ⊆ (ℤ_≥‘𝑑))
109	108	sseld 3914	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → ((⌊‘𝐴) ∈ (ℤ_≥‘𝑛) → (⌊‘𝐴) ∈ (ℤ_≥‘𝑑)))
110	109	pm4.71rd 566	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → ((⌊‘𝐴) ∈ (ℤ_≥‘𝑛) ↔ ((⌊‘𝐴) ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
111	106, 110	bitr3d 284	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) → ((𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)) ↔ ((⌊‘𝐴) ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
112	111	pm5.32da 582	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → (((𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)) ∧ (𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)))))
113		ancom 464	. . . . . . . . 9 ⊢ (((𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)) ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)) ∧ (𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
114		an4 655	. . . . . . . . 9 ⊢ (((𝑑 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑑)) ∧ (𝑛 ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
115	112, 113, 114	3bitr4g 317	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (((𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)) ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑑)) ∧ (𝑛 ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)))))
116		elfzuzb 12896	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)))
117		elfzuzb 12896	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...𝑛) ↔ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑)))
118	116, 117	anbi12i 629	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ (1...𝑛)) ↔ ((𝑛 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)) ∧ (𝑑 ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘𝑑))))
119		elfzuzb 12896	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑑)))
120		elfzuzb 12896	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝑑...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛)))
121	119, 120	anbi12i 629	. . . . . . . 8 ⊢ ((𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) ↔ ((𝑑 ∈ (ℤ_≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑑)) ∧ (𝑛 ∈ (ℤ_≥‘𝑑) ∧ (⌊‘𝐴) ∈ (ℤ_≥‘𝑛))))
122	115, 118, 121	3bitr4g 317	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ (1...𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴)))))
123	18	recnd 10658	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈ ℂ)
124	123	anasss 470	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ (1...𝑛))) → (1 / 𝑑) ∈ ℂ)
125	14, 14, 15, 122, 124	fsumcom2 15121	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑))
126	89, 102, 125	3brtr4d 5062	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑))
127	13, 35, 20, 43, 126	letrd 10786	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · (log‘𝐴)) − 𝐴) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑))
128	26, 34	readdcld 10659	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ∈ ℝ)
129		elfznn 12931	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
130	129	adantl 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
131	130	nnrpd 12417	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ⁺)
132	131	relogcld 25214	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℝ)
133		peano2re 10802	. . . . . . . 8 ⊢ ((log‘𝑛) ∈ ℝ → ((log‘𝑛) + 1) ∈ ℝ)
134	132, 133	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((log‘𝑛) + 1) ∈ ℝ)
135		nnz 11992	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
136		flid 13173	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ → (⌊‘𝑛) = 𝑛)
137	135, 136	syl 17	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (⌊‘𝑛) = 𝑛)
138	137	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (1...(⌊‘𝑛)) = (1...𝑛))
139	138	sumeq1d 15050	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → Σ𝑑 ∈ (1...(⌊‘𝑛))(1 / 𝑑) = Σ𝑑 ∈ (1...𝑛)(1 / 𝑑))
140		nnre 11632	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
141		nnge1 11653	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 1 ≤ 𝑛)
142		harmonicubnd 25595	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℝ ∧ 1 ≤ 𝑛) → Σ𝑑 ∈ (1...(⌊‘𝑛))(1 / 𝑑) ≤ ((log‘𝑛) + 1))
143	140, 141, 142	syl2anc 587	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → Σ𝑑 ∈ (1...(⌊‘𝑛))(1 / 𝑑) ≤ ((log‘𝑛) + 1))
144	139, 143	eqbrtrrd 5054	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1))
145	130, 144	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1))
146	14, 19, 134, 145	fsumle 15146	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1))
147	132	recnd 10658	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℂ)
148		1cnd 10625	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 1 ∈ ℂ)
149	14, 147, 148	fsumadd 15088	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1))
150		logfac 25192	. . . . . . . . 9 ⊢ ((⌊‘𝐴) ∈ ℕ₀ → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
151	23, 150	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
152		fsumconst 15137	. . . . . . . . . 10 ⊢ (((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝐴))1 = ((♯‘(1...(⌊‘𝐴))) · 1))
153	14, 91, 152	sylancl 589	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))1 = ((♯‘(1...(⌊‘𝐴))) · 1))
154	153, 96, 97	3eqtrrd 2838	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → (⌊‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))1)
155	151, 154	oveq12d 7153	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1))
156	149, 155	eqtr4d 2836	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1) = ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)))
157	146, 156	breqtrd 5056	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)))
158	34, 8, 26, 42	leadd2dd 11244	. . . . 5 ⊢ (𝐴 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ≤ ((log‘(!‘(⌊‘𝐴))) + 𝐴))
159	20, 128, 27, 157, 158	letrd 10786	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘(!‘(⌊‘𝐴))) + 𝐴))
160	13, 20, 27, 127, 159	letrd 10786	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → ((𝐴 · (log‘𝐴)) − 𝐴) ≤ ((log‘(!‘(⌊‘𝐴))) + 𝐴))
161	13, 8, 26	lesubaddd 11226	. . 3 ⊢ (𝐴 ∈ ℝ⁺ → ((((𝐴 · (log‘𝐴)) − 𝐴) − 𝐴) ≤ (log‘(!‘(⌊‘𝐴))) ↔ ((𝐴 · (log‘𝐴)) − 𝐴) ≤ ((log‘(!‘(⌊‘𝐴))) + 𝐴)))
162	160, 161	mpbird 260	. 2 ⊢ (𝐴 ∈ ℝ⁺ → (((𝐴 · (log‘𝐴)) − 𝐴) − 𝐴) ≤ (log‘(!‘(⌊‘𝐴))))
163	12, 162	eqbrtrd 5052	1 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 · ((log‘𝐴) − 2)) ≤ (log‘(!‘(⌊‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ⊆ wss 3881 class class class wbr 5030 ‘cfv 6324 (class class class)co 7135 Fincfn 8492 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 < clt 10664 ≤ cle 10665 − cmin 10859 / cdiv 11286 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 ℝ⁺crp 12377 ...cfz 12885 ⌊cfl 13155 !cfa 13629 ♯chash 13686 Σcsu 15034 logclog 25146

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-fi 8859 df-sup 8890 df-inf 8891 df-oi 8958 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-xnn0 11956 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-ioc 12731 df-ico 12732 df-icc 12733 df-fz 12886 df-fzo 13029 df-fl 13157 df-mod 13233 df-seq 13365 df-exp 13426 df-fac 13630 df-bc 13659 df-hash 13687 df-shft 14418 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-limsup 14820 df-clim 14837 df-rlim 14838 df-sum 15035 df-ef 15413 df-e 15414 df-sin 15415 df-cos 15416 df-tan 15417 df-pi 15418 df-dvds 15600 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-fbas 20088 df-fg 20089 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-cls 21626 df-nei 21703 df-lp 21741 df-perf 21742 df-cn 21832 df-cnp 21833 df-haus 21920 df-cmp 21992 df-tx 22167 df-hmeo 22360 df-fil 22451 df-fm 22543 df-flim 22544 df-flf 22545 df-xms 22927 df-ms 22928 df-tms 22929 df-cncf 23483 df-limc 24469 df-dv 24470 df-ulm 24972 df-log 25148 df-atan 25453 df-em 25578

This theorem is referenced by: (None)

W3C validator