Theorem harmonic

Description: The harmonic series H diverges. This fact follows from the stronger emcl , which establishes that the harmonic series grows as log n + gamma +o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014)

	Ref	Expression
Hypotheses	harmonic.1	$$⊢F=\left(n\in \mathbb{N}⟼\frac{1}{n}\right)$$
	harmonic.2	$$⊢H=seq1\left(+,F\right)$$
Assertion	harmonic	$$⊢\neg H\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		harmonic.1	$$⊢F=\left(n\in \mathbb{N}⟼\frac{1}{n}\right)$$
2		harmonic.2	$$⊢H=seq1\left(+,F\right)$$
3		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
4		0zd	$$⊢H\in \mathrm{dom}⇝\to 0\in \mathbb{Z}$$
5		1ex	$$⊢1\in \mathrm{V}$$
6	5	fvconst2	$$⊢k\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)\left(k\right)=1$$
7	6	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge k\in {\mathbb{N}}_0\right)\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)\left(k\right)=1$$
8		1red	$$⊢\left(H\in \mathrm{dom}⇝\wedge k\in {\mathbb{N}}_0\right)\to 1\in ℝ$$
9	2	eleq1i	$$⊢H\in \mathrm{dom}⇝\leftrightarrow seq1\left(+,F\right)\in \mathrm{dom}⇝$$
10	9	biimpi	$$⊢H\in \mathrm{dom}⇝\to seq1\left(+,F\right)\in \mathrm{dom}⇝$$
11		oveq2	$$⊢n=k\to \frac{1}{n}=\frac{1}{k}$$
12		ovex	$$⊢\frac{1}{k}\in \mathrm{V}$$
13	11 1 12	fvmpt	$$⊢k\in \mathbb{N}\to F\left(k\right)=\frac{1}{k}$$
14		nnrecre	$$⊢k\in \mathbb{N}\to \frac{1}{k}\in ℝ$$
15	13 14	eqeltrd	$$⊢k\in \mathbb{N}\to F\left(k\right)\in ℝ$$
16	15	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge k\in \mathbb{N}\right)\to F\left(k\right)\in ℝ$$
17		nnrp	$$⊢k\in \mathbb{N}\to k\in {ℝ}^{+}$$
18	17	rpreccld	$$⊢k\in \mathbb{N}\to \frac{1}{k}\in {ℝ}^{+}$$
19	18	rpge0d	$$⊢k\in \mathbb{N}\to 0\le \frac{1}{k}$$
20	19 13	breqtrrd	$$⊢k\in \mathbb{N}\to 0\le F\left(k\right)$$
21	20	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge k\in \mathbb{N}\right)\to 0\le F\left(k\right)$$
22		nnre	$$⊢k\in \mathbb{N}\to k\in ℝ$$
23	22	lep1d	$$⊢k\in \mathbb{N}\to k\le k+1$$
24		nngt0	$$⊢k\in \mathbb{N}\to 0<k$$
25		peano2re	$$⊢k\in ℝ\to k+1\in ℝ$$
26	22 25	syl	$$⊢k\in \mathbb{N}\to k+1\in ℝ$$
27		peano2nn	$$⊢k\in \mathbb{N}\to k+1\in \mathbb{N}$$
28	27	nngt0d	$$⊢k\in \mathbb{N}\to 0<k+1$$
29		lerec	$$⊢\left(\left(k\in ℝ\wedge 0<k\right)\wedge \left(k+1\in ℝ\wedge 0<k+1\right)\right)\to \left(k\le k+1\leftrightarrow \frac{1}{k+1}\le \frac{1}{k}\right)$$
30	22 24 26 28 29	syl22anc	$$⊢k\in \mathbb{N}\to \left(k\le k+1\leftrightarrow \frac{1}{k+1}\le \frac{1}{k}\right)$$
31	23 30	mpbid	$$⊢k\in \mathbb{N}\to \frac{1}{k+1}\le \frac{1}{k}$$
32		oveq2	$$⊢n=k+1\to \frac{1}{n}=\frac{1}{k+1}$$
33		ovex	$$⊢\frac{1}{k+1}\in \mathrm{V}$$
34	32 1 33	fvmpt	$$⊢k+1\in \mathbb{N}\to F\left(k+1\right)=\frac{1}{k+1}$$
35	27 34	syl	$$⊢k\in \mathbb{N}\to F\left(k+1\right)=\frac{1}{k+1}$$
36	31 35 13	3brtr4d	$$⊢k\in \mathbb{N}\to F\left(k+1\right)\le F\left(k\right)$$
37	36	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge k\in \mathbb{N}\right)\to F\left(k+1\right)\le F\left(k\right)$$
38		oveq2	$$⊢k=j\to 2^k=2^j$$
39	38	fveq2d	$$⊢k=j\to F\left(2^k\right)=F\left(2^j\right)$$
40	38 39	oveq12d	$$⊢k=j\to 2^{k}F\left(2^k\right)=2^{j}F\left(2^j\right)$$
41		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{1\right\}=\left(k\in {\mathbb{N}}_0⟼1\right)$$
42		2nn	$$⊢2\in \mathbb{N}$$
43		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge k\in {\mathbb{N}}_0\right)\to 2^k\in \mathbb{N}$$
44	42 43	mpan	$$⊢k\in {\mathbb{N}}_0\to 2^k\in \mathbb{N}$$
45		oveq2	$$⊢n=2^k\to \frac{1}{n}=\frac{1}{2^k}$$
46		ovex	$$⊢\frac{1}{2^k}\in \mathrm{V}$$
47	45 1 46	fvmpt	$$⊢2^k\in \mathbb{N}\to F\left(2^k\right)=\frac{1}{2^k}$$
48	44 47	syl	$$⊢k\in {\mathbb{N}}_0\to F\left(2^k\right)=\frac{1}{2^k}$$
49	48	oveq2d	$$⊢k\in {\mathbb{N}}_0\to 2^{k}F\left(2^k\right)=2^k\left(\frac{1}{2^k}\right)$$
50		nncn	$$⊢2^k\in \mathbb{N}\to 2^k\in ℂ$$
51		nnne0	$$⊢2^k\in \mathbb{N}\to 2^k\ne 0$$
52	50 51	recidd	$$⊢2^k\in \mathbb{N}\to 2^k\left(\frac{1}{2^k}\right)=1$$
53	44 52	syl	$$⊢k\in {\mathbb{N}}_0\to 2^k\left(\frac{1}{2^k}\right)=1$$
54	49 53	eqtrd	$$⊢k\in {\mathbb{N}}_0\to 2^{k}F\left(2^k\right)=1$$
55	54	mpteq2ia	$$⊢\left(k\in {\mathbb{N}}_0⟼2^{k}F\left(2^k\right)\right)=\left(k\in {\mathbb{N}}_0⟼1\right)$$
56	41 55	eqtr4i	$$⊢{\mathbb{N}}_0\times \left\{1\right\}=\left(k\in {\mathbb{N}}_0⟼2^{k}F\left(2^k\right)\right)$$
57		ovex	$$⊢2^{j}F\left(2^j\right)\in \mathrm{V}$$
58	40 56 57	fvmpt	$$⊢j\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)\left(j\right)=2^{j}F\left(2^j\right)$$
59	58	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in {\mathbb{N}}_0\right)\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)\left(j\right)=2^{j}F\left(2^j\right)$$
60	16 21 37 59	climcnds	$$⊢H\in \mathrm{dom}⇝\to \left(seq1\left(+,F\right)\in \mathrm{dom}⇝\leftrightarrow seq0\left(+,\left({\mathbb{N}}_0\times \left\{1\right\}\right)\right)\in \mathrm{dom}⇝\right)$$
61	10 60	mpbid	$$⊢H\in \mathrm{dom}⇝\to seq0\left(+,\left({\mathbb{N}}_0\times \left\{1\right\}\right)\right)\in \mathrm{dom}⇝$$
62	3 4 7 8 61	isumrecl	$$⊢H\in \mathrm{dom}⇝\to \sum _{k\in {\mathbb{N}}_0}1\in ℝ$$
63		arch	$$⊢\sum _{k\in {\mathbb{N}}_0}1\in ℝ\to \exists j\in \mathbb{N}\sum _{k\in {\mathbb{N}}_0}1<j$$
64	62 63	syl	$$⊢H\in \mathrm{dom}⇝\to \exists j\in \mathbb{N}\sum _{k\in {\mathbb{N}}_0}1<j$$
65		fzfid	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \left(1\dots j\right)\in \mathrm{Fin}$$
66		ax-1cn	$$⊢1\in ℂ$$
67		fsumconst	$$⊢\left(\left(1\dots j\right)\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k=1}^{j}1=\left|\left(1\dots j\right)\right|\cdot 1$$
68	65 66 67	sylancl	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \sum _{k=1}^{j}1=\left|\left(1\dots j\right)\right|\cdot 1$$
69		nnnn0	$$⊢j\in \mathbb{N}\to j\in {\mathbb{N}}_0$$
70	69	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to j\in {\mathbb{N}}_0$$
71		hashfz1	$$⊢j\in {\mathbb{N}}_0\to \left|\left(1\dots j\right)\right|=j$$
72	70 71	syl	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \left|\left(1\dots j\right)\right|=j$$
73	72	oveq1d	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \left|\left(1\dots j\right)\right|\cdot 1=j\cdot 1$$
74		nncn	$$⊢j\in \mathbb{N}\to j\in ℂ$$
75	74	adantl	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to j\in ℂ$$
76	75	mulridd	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to j\cdot 1=j$$
77	68 73 76	3eqtrd	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \sum _{k=1}^{j}1=j$$
78		0zd	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to 0\in \mathbb{Z}$$
79		elfznn	$$⊢k\in \left(1\dots j\right)\to k\in \mathbb{N}$$
80		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
81	79 80	syl	$$⊢k\in \left(1\dots j\right)\to k\in {\mathbb{N}}_0$$
82	81	ssriv	$$⊢\left(1\dots j\right)\subseteq {\mathbb{N}}_0$$
83	82	a1i	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \left(1\dots j\right)\subseteq {\mathbb{N}}_0$$
84	6	adantl	$$⊢\left(\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\wedge k\in {\mathbb{N}}_0\right)\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)\left(k\right)=1$$
85		1red	$$⊢\left(\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\wedge k\in {\mathbb{N}}_0\right)\to 1\in ℝ$$
86		0le1	$$⊢0\le 1$$
87	86	a1i	$$⊢\left(\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\wedge k\in {\mathbb{N}}_0\right)\to 0\le 1$$
88	61	adantr	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to seq0\left(+,\left({\mathbb{N}}_0\times \left\{1\right\}\right)\right)\in \mathrm{dom}⇝$$
89	3 78 65 83 84 85 87 88	isumless	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \sum _{k=1}^{j}1\le \sum _{k\in {\mathbb{N}}_0}1$$
90	77 89	eqbrtrrd	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to j\le \sum _{k\in {\mathbb{N}}_0}1$$
91		nnre	$$⊢j\in \mathbb{N}\to j\in ℝ$$
92		lenlt	$$⊢\left(j\in ℝ\wedge \sum _{k\in {\mathbb{N}}_0}1\in ℝ\right)\to \left(j\le \sum _{k\in {\mathbb{N}}_0}1\leftrightarrow \neg \sum _{k\in {\mathbb{N}}_0}1<j\right)$$
93	91 62 92	syl2anr	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \left(j\le \sum _{k\in {\mathbb{N}}_0}1\leftrightarrow \neg \sum _{k\in {\mathbb{N}}_0}1<j\right)$$
94	90 93	mpbid	$$⊢\left(H\in \mathrm{dom}⇝\wedge j\in \mathbb{N}\right)\to \neg \sum _{k\in {\mathbb{N}}_0}1<j$$
95	94	nrexdv	$$⊢H\in \mathrm{dom}⇝\to \neg \exists j\in \mathbb{N}\sum _{k\in {\mathbb{N}}_0}1<j$$
96	64 95	pm2.65i	$$⊢\neg H\in \mathrm{dom}⇝$$