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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
	harmonic.2	⊢ 𝐻 = seq 1 ( + , 𝐹 )
Assertion	harmonic	⊢ ¬ 𝐻 ∈ dom ⇝

Proof

Step	Hyp	Ref	Expression
1		harmonic.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
2		harmonic.2	⊢ 𝐻 = seq 1 ( + , 𝐹 )
3		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4		0zd	⊢ ( 𝐻 ∈ dom ⇝ → 0 ∈ ℤ )
5		1ex	⊢ 1 ∈ V
6	5	fvconst2	⊢ ( 𝑘 ∈ ℕ0 → ( ( ℕ0 × { 1 } ) ‘ 𝑘 ) = 1 )
7	6	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 1 } ) ‘ 𝑘 ) = 1 )
8		1red	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℝ )
9	2	eleq1i	⊢ ( 𝐻 ∈ dom ⇝ ↔ seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
10	9	biimpi	⊢ ( 𝐻 ∈ dom ⇝ → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
11		oveq2	⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
12		ovex	⊢ ( 1 / 𝑘 ) ∈ V
13	11 1 12	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = ( 1 / 𝑘 ) )
14		nnrecre	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
15	13 14	eqeltrd	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
16	15	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
17		nnrp	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
18	17	rpreccld	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
19	18	rpge0d	⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 1 / 𝑘 ) )
20	19 13	breqtrrd	⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
21	20	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
22		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
23	22	lep1d	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≤ ( 𝑘 + 1 ) )
24		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
25		peano2re	⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
26	22 25	syl	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℝ )
27		peano2nn	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
28	27	nngt0d	⊢ ( 𝑘 ∈ ℕ → 0 < ( 𝑘 + 1 ) )
29		lerec	⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ∧ ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) ) → ( 𝑘 ≤ ( 𝑘 + 1 ) ↔ ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) ) )
30	22 24 26 28 29	syl22anc	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ≤ ( 𝑘 + 1 ) ↔ ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) ) )
31	23 30	mpbid	⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) )
32		oveq2	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( 𝑘 + 1 ) ) )
33		ovex	⊢ ( 1 / ( 𝑘 + 1 ) ) ∈ V
34	32 1 33	fvmpt	⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 1 / ( 𝑘 + 1 ) ) )
35	27 34	syl	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 1 / ( 𝑘 + 1 ) ) )
36	31 35 13	3brtr4d	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
37	36	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
38		oveq2	⊢ ( 𝑘 = 𝑗 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑗 ) )
39	38	fveq2d	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) = ( 𝐹 ‘ ( 2 ↑ 𝑗 ) ) )
40	38 39	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 2 ↑ 𝑘 ) · ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) ) = ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ 𝑗 ) ) ) )
41		fconstmpt	⊢ ( ℕ0 × { 1 } ) = ( 𝑘 ∈ ℕ0 ↦ 1 )
42		2nn	⊢ 2 ∈ ℕ
43		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
44	42 43	mpan	⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℕ )
45		oveq2	⊢ ( 𝑛 = ( 2 ↑ 𝑘 ) → ( 1 / 𝑛 ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
46		ovex	⊢ ( 1 / ( 2 ↑ 𝑘 ) ) ∈ V
47	45 1 46	fvmpt	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℕ → ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
48	44 47	syl	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
49	48	oveq2d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 ↑ 𝑘 ) · ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) ) = ( ( 2 ↑ 𝑘 ) · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
50		nncn	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℕ → ( 2 ↑ 𝑘 ) ∈ ℂ )
51		nnne0	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℕ → ( 2 ↑ 𝑘 ) ≠ 0 )
52	50 51	recidd	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℕ → ( ( 2 ↑ 𝑘 ) · ( 1 / ( 2 ↑ 𝑘 ) ) ) = 1 )
53	44 52	syl	⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 ↑ 𝑘 ) · ( 1 / ( 2 ↑ 𝑘 ) ) ) = 1 )
54	49 53	eqtrd	⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 ↑ 𝑘 ) · ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) ) = 1 )
55	54	mpteq2ia	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑘 ) · ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ 1 )
56	41 55	eqtr4i	⊢ ( ℕ0 × { 1 } ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑘 ) · ( 𝐹 ‘ ( 2 ↑ 𝑘 ) ) ) )
57		ovex	⊢ ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ 𝑗 ) ) ) ∈ V
58	40 56 57	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( ( ℕ0 × { 1 } ) ‘ 𝑗 ) = ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ 𝑗 ) ) ) )
59	58	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ0 ) → ( ( ℕ0 × { 1 } ) ‘ 𝑗 ) = ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ 𝑗 ) ) ) )
60	16 21 37 59	climcnds	⊢ ( 𝐻 ∈ dom ⇝ → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 0 ( + , ( ℕ0 × { 1 } ) ) ∈ dom ⇝ ) )
61	10 60	mpbid	⊢ ( 𝐻 ∈ dom ⇝ → seq 0 ( + , ( ℕ0 × { 1 } ) ) ∈ dom ⇝ )
62	3 4 7 8 61	isumrecl	⊢ ( 𝐻 ∈ dom ⇝ → Σ 𝑘 ∈ ℕ0 1 ∈ ℝ )
63		arch	⊢ ( Σ 𝑘 ∈ ℕ0 1 ∈ ℝ → ∃ 𝑗 ∈ ℕ Σ 𝑘 ∈ ℕ0 1 < 𝑗 )
64	62 63	syl	⊢ ( 𝐻 ∈ dom ⇝ → ∃ 𝑗 ∈ ℕ Σ 𝑘 ∈ ℕ0 1 < 𝑗 )
65		fzfid	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 1 ... 𝑗 ) ∈ Fin )
66		ax-1cn	⊢ 1 ∈ ℂ
67		fsumconst	⊢ ( ( ( 1 ... 𝑗 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑗 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑗 ) ) · 1 ) )
68	65 66 67	sylancl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑗 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑗 ) ) · 1 ) )
69		nnnn0	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
70	69	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
71		hashfz1	⊢ ( 𝑗 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑗 ) ) = 𝑗 )
72	70 71	syl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... 𝑗 ) ) = 𝑗 )
73	72	oveq1d	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( ( ♯ ‘ ( 1 ... 𝑗 ) ) · 1 ) = ( 𝑗 · 1 ) )
74		nncn	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
75	74	adantl	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
76	75	mulridd	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 · 1 ) = 𝑗 )
77	68 73 76	3eqtrd	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑗 ) 1 = 𝑗 )
78		0zd	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℤ )
79		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝑗 ) → 𝑘 ∈ ℕ )
80		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
81	79 80	syl	⊢ ( 𝑘 ∈ ( 1 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
82	81	ssriv	⊢ ( 1 ... 𝑗 ) ⊆ ℕ0
83	82	a1i	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 1 ... 𝑗 ) ⊆ ℕ0 )
84	6	adantl	⊢ ( ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 1 } ) ‘ 𝑘 ) = 1 )
85		1red	⊢ ( ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℝ )
86		0le1	⊢ 0 ≤ 1
87	86	a1i	⊢ ( ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 1 )
88	61	adantr	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → seq 0 ( + , ( ℕ0 × { 1 } ) ) ∈ dom ⇝ )
89	3 78 65 83 84 85 87 88	isumless	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑗 ) 1 ≤ Σ 𝑘 ∈ ℕ0 1 )
90	77 89	eqbrtrrd	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 𝑗 ≤ Σ 𝑘 ∈ ℕ0 1 )
91		nnre	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
92		lenlt	⊢ ( ( 𝑗 ∈ ℝ ∧ Σ 𝑘 ∈ ℕ0 1 ∈ ℝ ) → ( 𝑗 ≤ Σ 𝑘 ∈ ℕ0 1 ↔ ¬ Σ 𝑘 ∈ ℕ0 1 < 𝑗 ) )
93	91 62 92	syl2anr	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 𝑗 ≤ Σ 𝑘 ∈ ℕ0 1 ↔ ¬ Σ 𝑘 ∈ ℕ0 1 < 𝑗 ) )
94	90 93	mpbid	⊢ ( ( 𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ¬ Σ 𝑘 ∈ ℕ0 1 < 𝑗 )
95	94	nrexdv	⊢ ( 𝐻 ∈ dom ⇝ → ¬ ∃ 𝑗 ∈ ℕ Σ 𝑘 ∈ ℕ0 1 < 𝑗 )
96	64 95	pm2.65i	⊢ ¬ 𝐻 ∈ dom ⇝