Step | Hyp | Ref
| Expression |
1 | | nnuz 12813 |
. . . . 5
β’ β =
(β€β₯β1) |
2 | | 1zzd 12541 |
. . . . 5
β’ (β€
β 1 β β€) |
3 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (1 / π) = (1 / π)) |
4 | 3 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (1 + (1 / π)) = (1 + (1 / π))) |
5 | 4 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (logβ(1 + (1 / π))) = (logβ(1 + (1 / π)))) |
6 | 3, 5 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((1 / π) β (logβ(1 + (1 / π)))) = ((1 / π) β (logβ(1 + (1 / π))))) |
7 | | emcl.4 |
. . . . . . . . 9
β’ π = (π β β β¦ ((1 / π) β (logβ(1 + (1 /
π))))) |
8 | | ovex 7395 |
. . . . . . . . 9
β’ ((1 /
π) β (logβ(1 +
(1 / π)))) β
V |
9 | 6, 7, 8 | fvmpt 6953 |
. . . . . . . 8
β’ (π β β β (πβπ) = ((1 / π) β (logβ(1 + (1 / π))))) |
10 | 9 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π
β β) β (πβπ) = ((1 / π) β (logβ(1 + (1 / π))))) |
11 | | nnrecre 12202 |
. . . . . . . . . 10
β’ (π β β β (1 /
π) β
β) |
12 | 11 | adantl 483 |
. . . . . . . . 9
β’
((β€ β§ π
β β) β (1 / π) β β) |
13 | | 1rp 12926 |
. . . . . . . . . . 11
β’ 1 β
β+ |
14 | | nnrp 12933 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β+) |
15 | 14 | rpreccld 12974 |
. . . . . . . . . . . 12
β’ (π β β β (1 /
π) β
β+) |
16 | 15 | adantl 483 |
. . . . . . . . . . 11
β’
((β€ β§ π
β β) β (1 / π) β
β+) |
17 | | rpaddcl 12944 |
. . . . . . . . . . 11
β’ ((1
β β+ β§ (1 / π) β β+) β (1 + (1
/ π)) β
β+) |
18 | 13, 16, 17 | sylancr 588 |
. . . . . . . . . 10
β’
((β€ β§ π
β β) β (1 + (1 / π)) β
β+) |
19 | 18 | relogcld 25994 |
. . . . . . . . 9
β’
((β€ β§ π
β β) β (logβ(1 + (1 / π))) β β) |
20 | 12, 19 | resubcld 11590 |
. . . . . . . 8
β’
((β€ β§ π
β β) β ((1 / π) β (logβ(1 + (1 / π)))) β
β) |
21 | 20 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π
β β) β ((1 / π) β (logβ(1 + (1 / π)))) β
β) |
22 | | emcl.1 |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ (Ξ£π β (1...π)(1 / π) β (logβπ))) |
23 | | emcl.2 |
. . . . . . . . . 10
β’ πΊ = (π β β β¦ (Ξ£π β (1...π)(1 / π) β (logβ(π + 1)))) |
24 | | emcl.3 |
. . . . . . . . . 10
β’ π» = (π β β β¦ (logβ(1 + (1 /
π)))) |
25 | 22, 23, 24, 7 | emcllem5 26365 |
. . . . . . . . 9
β’ πΊ = seq1( + , π) |
26 | 22, 23 | emcllem1 26361 |
. . . . . . . . . . . 12
β’ (πΉ:ββΆβ β§
πΊ:ββΆβ) |
27 | 26 | simpri 487 |
. . . . . . . . . . 11
β’ πΊ:ββΆβ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β πΊ:ββΆβ) |
29 | 22, 23 | emcllem2 26362 |
. . . . . . . . . . . 12
β’ (π β β β ((πΉβ(π + 1)) β€ (πΉβπ) β§ (πΊβπ) β€ (πΊβ(π + 1)))) |
30 | 29 | simprd 497 |
. . . . . . . . . . 11
β’ (π β β β (πΊβπ) β€ (πΊβ(π + 1))) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
β’
((β€ β§ π
β β) β (πΊβπ) β€ (πΊβ(π + 1))) |
32 | | 1nn 12171 |
. . . . . . . . . . . 12
β’ 1 β
β |
33 | 26 | simpli 485 |
. . . . . . . . . . . . 13
β’ πΉ:ββΆβ |
34 | 33 | ffvelcdmi 7039 |
. . . . . . . . . . . 12
β’ (1 β
β β (πΉβ1)
β β) |
35 | 32, 34 | ax-mp 5 |
. . . . . . . . . . 11
β’ (πΉβ1) β
β |
36 | 27 | ffvelcdmi 7039 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΊβπ) β β) |
37 | 36 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΊβπ) β β) |
38 | 33 | ffvelcdmi 7039 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΉβπ) β β) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
40 | 35 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΉβ1) β β) |
41 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . 19
β’
(logβ(1 + (1 / π))) β V |
42 | 5, 24, 41 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π»βπ) = (logβ(1 + (1 / π)))) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π
β β) β (π»βπ) = (logβ(1 + (1 / π)))) |
44 | 22, 23, 24 | emcllem3 26363 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π»βπ) = ((πΉβπ) β (πΊβπ))) |
45 | 44 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π
β β) β (π»βπ) = ((πΉβπ) β (πΊβπ))) |
46 | 43, 45 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π
β β) β (logβ(1 + (1 / π))) = ((πΉβπ) β (πΊβπ))) |
47 | | 1re 11162 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β |
48 | | readdcl 11141 |
. . . . . . . . . . . . . . . . . 18
β’ ((1
β β β§ (1 / π) β β) β (1 + (1 / π)) β
β) |
49 | 47, 12, 48 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π
β β) β (1 + (1 / π)) β β) |
50 | | ltaddrp 12959 |
. . . . . . . . . . . . . . . . . 18
β’ ((1
β β β§ (1 / π) β β+) β 1 <
(1 + (1 / π))) |
51 | 47, 16, 50 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π
β β) β 1 < (1 + (1 / π))) |
52 | 49, 51 | rplogcld 26000 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π
β β) β (logβ(1 + (1 / π))) β
β+) |
53 | 46, 52 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π
β β) β ((πΉβπ) β (πΊβπ)) β
β+) |
54 | 53 | rpge0d 12968 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π
β β) β 0 β€ ((πΉβπ) β (πΊβπ))) |
55 | 39, 37 | subge0d 11752 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π
β β) β (0 β€ ((πΉβπ) β (πΊβπ)) β (πΊβπ) β€ (πΉβπ))) |
56 | 54, 55 | mpbid 231 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΊβπ) β€ (πΉβπ)) |
57 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = 1 β (πΉβπ₯) = (πΉβ1)) |
58 | 57 | breq1d 5120 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 1 β ((πΉβπ₯) β€ (πΉβ1) β (πΉβ1) β€ (πΉβ1))) |
59 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
60 | 59 | breq1d 5120 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((πΉβπ₯) β€ (πΉβ1) β (πΉβπ) β€ (πΉβ1))) |
61 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π + 1) β (πΉβπ₯) = (πΉβ(π + 1))) |
62 | 61 | breq1d 5120 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + 1) β ((πΉβπ₯) β€ (πΉβ1) β (πΉβ(π + 1)) β€ (πΉβ1))) |
63 | 35 | leidi 11696 |
. . . . . . . . . . . . . . 15
β’ (πΉβ1) β€ (πΉβ1) |
64 | 29 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (πΉβ(π + 1)) β€ (πΉβπ)) |
65 | | peano2nn 12172 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π + 1) β
β) |
66 | 33 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β β β
(πΉβ(π + 1)) β
β) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (πΉβ(π + 1)) β β) |
68 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (πΉβ1) β
β) |
69 | | letr 11256 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβ(π + 1)) β β β§ (πΉβπ) β β β§ (πΉβ1) β β) β (((πΉβ(π + 1)) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβ1)) β (πΉβ(π + 1)) β€ (πΉβ1))) |
70 | 67, 38, 68, 69 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (((πΉβ(π + 1)) β€ (πΉβπ) β§ (πΉβπ) β€ (πΉβ1)) β (πΉβ(π + 1)) β€ (πΉβ1))) |
71 | 64, 70 | mpand 694 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((πΉβπ) β€ (πΉβ1) β (πΉβ(π + 1)) β€ (πΉβ1))) |
72 | 58, 60, 62, 60, 63, 71 | nnind 12178 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΉβπ) β€ (πΉβ1)) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΉβπ) β€ (πΉβ1)) |
74 | 37, 39, 40, 56, 73 | letrd 11319 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β (πΊβπ) β€ (πΉβ1)) |
75 | 74 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (β€
β βπ β
β (πΊβπ) β€ (πΉβ1)) |
76 | | brralrspcev 5170 |
. . . . . . . . . . 11
β’ (((πΉβ1) β β β§
βπ β β
(πΊβπ) β€ (πΉβ1)) β βπ₯ β β βπ β β (πΊβπ) β€ π₯) |
77 | 35, 75, 76 | sylancr 588 |
. . . . . . . . . 10
β’ (β€
β βπ₯ β
β βπ β
β (πΊβπ) β€ π₯) |
78 | 1, 2, 28, 31, 77 | climsup 15561 |
. . . . . . . . 9
β’ (β€
β πΊ β sup(ran
πΊ, β, <
)) |
79 | 25, 78 | eqbrtrrid 5146 |
. . . . . . . 8
β’ (β€
β seq1( + , π) β
sup(ran πΊ, β, <
)) |
80 | | climrel 15381 |
. . . . . . . . 9
β’ Rel
β |
81 | 80 | releldmi 5908 |
. . . . . . . 8
β’ (seq1( +
, π) β sup(ran πΊ, β, < ) β seq1( +
, π) β dom β
) |
82 | 79, 81 | syl 17 |
. . . . . . 7
β’ (β€
β seq1( + , π) β
dom β ) |
83 | 1, 2, 10, 21, 82 | isumclim2 15650 |
. . . . . 6
β’ (β€
β seq1( + , π) β
Ξ£π β β ((1
/ π) β (logβ(1
+ (1 / π))))) |
84 | | df-em 26358 |
. . . . . 6
β’ Ξ³ =
Ξ£π β β ((1
/ π) β (logβ(1
+ (1 / π)))) |
85 | 83, 25, 84 | 3brtr4g 5144 |
. . . . 5
β’ (β€
β πΊ β
Ξ³) |
86 | | nnex 12166 |
. . . . . . . 8
β’ β
β V |
87 | 86 | mptex 7178 |
. . . . . . 7
β’ (π β β β¦
(Ξ£π β (1...π)(1 / π) β (logβπ))) β V |
88 | 22, 87 | eqeltri 2834 |
. . . . . 6
β’ πΉ β V |
89 | 88 | a1i 11 |
. . . . 5
β’ (β€
β πΉ β
V) |
90 | 22, 23, 24 | emcllem4 26364 |
. . . . . 6
β’ π» β 0 |
91 | 90 | a1i 11 |
. . . . 5
β’ (β€
β π» β
0) |
92 | 37 | recnd 11190 |
. . . . 5
β’
((β€ β§ π
β β) β (πΊβπ) β β) |
93 | 39, 37 | resubcld 11590 |
. . . . . . 7
β’
((β€ β§ π
β β) β ((πΉβπ) β (πΊβπ)) β β) |
94 | 45, 93 | eqeltrd 2838 |
. . . . . 6
β’
((β€ β§ π
β β) β (π»βπ) β β) |
95 | 94 | recnd 11190 |
. . . . 5
β’
((β€ β§ π
β β) β (π»βπ) β β) |
96 | 45 | oveq2d 7378 |
. . . . . 6
β’
((β€ β§ π
β β) β ((πΊβπ) + (π»βπ)) = ((πΊβπ) + ((πΉβπ) β (πΊβπ)))) |
97 | 39 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
98 | 92, 97 | pncan3d 11522 |
. . . . . 6
β’
((β€ β§ π
β β) β ((πΊβπ) + ((πΉβπ) β (πΊβπ))) = (πΉβπ)) |
99 | 96, 98 | eqtr2d 2778 |
. . . . 5
β’
((β€ β§ π
β β) β (πΉβπ) = ((πΊβπ) + (π»βπ))) |
100 | 1, 2, 85, 89, 91, 92, 95, 99 | climadd 15521 |
. . . 4
β’ (β€
β πΉ β (Ξ³ +
0)) |
101 | 85 | mptru 1549 |
. . . . . 6
β’ πΊ β
Ξ³ |
102 | | climcl 15388 |
. . . . . 6
β’ (πΊ β Ξ³ β Ξ³
β β) |
103 | 101, 102 | ax-mp 5 |
. . . . 5
β’ Ξ³
β β |
104 | 103 | addid1i 11349 |
. . . 4
β’ (Ξ³
+ 0) = Ξ³ |
105 | 100, 104 | breqtrdi 5151 |
. . 3
β’ (β€
β πΉ β
Ξ³) |
106 | 105 | mptru 1549 |
. 2
β’ πΉ β
Ξ³ |
107 | 106, 101 | pm3.2i 472 |
1
β’ (πΉ β Ξ³ β§ πΊ β
Ξ³) |