Metamath Proof Explorer

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 ⇝