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 = (n \in ℕ ⟼ \frac{1}{n})$
	harmonic.2	$⊢ H = seq 1 (+ F)$
Assertion	harmonic	$⊢ \neg H \in dom ⇝$

Proof

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

Metamath Proof Explorer

Theorem harmonic

Proof