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 
|- F = ( n e. NN |-> ( 1 / n ) )
harmonic.2 
|- H = seq 1 ( + , F )
Assertion harmonic 
|- -. H e. dom ~~>

Proof

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