Step | Hyp | Ref
| Expression |
1 | | nnuz 12798 |
. . . . 5
β’ β =
(β€β₯β1) |
2 | | 1zzd 12530 |
. . . . 5
β’ (β€
β 1 β β€) |
3 | | emcl.1 |
. . . . . . . 8
β’ πΉ = (π β β β¦ (Ξ£π β (1...π)(1 / π) β (logβπ))) |
4 | | emcl.2 |
. . . . . . . 8
β’ πΊ = (π β β β¦ (Ξ£π β (1...π)(1 / π) β (logβ(π + 1)))) |
5 | | emcl.3 |
. . . . . . . 8
β’ π» = (π β β β¦ (logβ(1 + (1 /
π)))) |
6 | | emcl.4 |
. . . . . . . 8
β’ π = (π β β β¦ ((1 / π) β (logβ(1 + (1 /
π))))) |
7 | 3, 4, 5, 6 | emcllem6 26334 |
. . . . . . 7
β’ (πΉ β Ξ³ β§ πΊ β
Ξ³) |
8 | 7 | simpri 486 |
. . . . . 6
β’ πΊ β
Ξ³ |
9 | 8 | a1i 11 |
. . . . 5
β’ (β€
β πΊ β
Ξ³) |
10 | 3, 4 | emcllem1 26329 |
. . . . . . . 8
β’ (πΉ:ββΆβ β§
πΊ:ββΆβ) |
11 | 10 | simpri 486 |
. . . . . . 7
β’ πΊ:ββΆβ |
12 | 11 | ffvelcdmi 7030 |
. . . . . 6
β’ (π β β β (πΊβπ) β β) |
13 | 12 | adantl 482 |
. . . . 5
β’
((β€ β§ π
β β) β (πΊβπ) β β) |
14 | 1, 2, 9, 13 | climrecl 15457 |
. . . 4
β’ (β€
β Ξ³ β β) |
15 | | 1nn 12160 |
. . . . 5
β’ 1 β
β |
16 | | simpr 485 |
. . . . . . 7
β’
((β€ β§ π
β β) β π
β β) |
17 | 8 | a1i 11 |
. . . . . . 7
β’
((β€ β§ π
β β) β πΊ
β Ξ³) |
18 | 12 | adantl 482 |
. . . . . . 7
β’
(((β€ β§ π
β β) β§ π
β β) β (πΊβπ) β β) |
19 | 3, 4 | emcllem2 26330 |
. . . . . . . . 9
β’ (π β β β ((πΉβ(π + 1)) β€ (πΉβπ) β§ (πΊβπ) β€ (πΊβ(π + 1)))) |
20 | 19 | simprd 496 |
. . . . . . . 8
β’ (π β β β (πΊβπ) β€ (πΊβ(π + 1))) |
21 | 20 | adantl 482 |
. . . . . . 7
β’
(((β€ β§ π
β β) β§ π
β β) β (πΊβπ) β€ (πΊβ(π + 1))) |
22 | 1, 16, 17, 18, 21 | climub 15538 |
. . . . . 6
β’
((β€ β§ π
β β) β (πΊβπ) β€ Ξ³) |
23 | 22 | ralrimiva 3141 |
. . . . 5
β’ (β€
β βπ β
β (πΊβπ) β€ Ξ³) |
24 | | fveq2 6839 |
. . . . . . . 8
β’ (π = 1 β (πΊβπ) = (πΊβ1)) |
25 | | oveq2 7361 |
. . . . . . . . . . . . 13
β’ (π = 1 β (1...π) = (1...1)) |
26 | 25 | sumeq1d 15578 |
. . . . . . . . . . . 12
β’ (π = 1 β Ξ£π β (1...π)(1 / π) = Ξ£π β (1...1)(1 / π)) |
27 | | 1z 12529 |
. . . . . . . . . . . . 13
β’ 1 β
β€ |
28 | | ax-1cn 11105 |
. . . . . . . . . . . . 13
β’ 1 β
β |
29 | | oveq2 7361 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (1 / π) = (1 / 1)) |
30 | | 1div1e1 11841 |
. . . . . . . . . . . . . . 15
β’ (1 / 1) =
1 |
31 | 29, 30 | eqtrdi 2792 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (1 / π) = 1) |
32 | 31 | fsum1 15624 |
. . . . . . . . . . . . 13
β’ ((1
β β€ β§ 1 β β) β Ξ£π β (1...1)(1 / π) = 1) |
33 | 27, 28, 32 | mp2an 690 |
. . . . . . . . . . . 12
β’
Ξ£π β
(1...1)(1 / π) =
1 |
34 | 26, 33 | eqtrdi 2792 |
. . . . . . . . . . 11
β’ (π = 1 β Ξ£π β (1...π)(1 / π) = 1) |
35 | | oveq1 7360 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π + 1) = (1 + 1)) |
36 | | df-2 12212 |
. . . . . . . . . . . . 13
β’ 2 = (1 +
1) |
37 | 35, 36 | eqtr4di 2794 |
. . . . . . . . . . . 12
β’ (π = 1 β (π + 1) = 2) |
38 | 37 | fveq2d 6843 |
. . . . . . . . . . 11
β’ (π = 1 β (logβ(π + 1)) =
(logβ2)) |
39 | 34, 38 | oveq12d 7371 |
. . . . . . . . . 10
β’ (π = 1 β (Ξ£π β (1...π)(1 / π) β (logβ(π + 1))) = (1 β
(logβ2))) |
40 | | 1re 11151 |
. . . . . . . . . . . 12
β’ 1 β
β |
41 | | 2rp 12912 |
. . . . . . . . . . . . 13
β’ 2 β
β+ |
42 | | relogcl 25915 |
. . . . . . . . . . . . 13
β’ (2 β
β+ β (logβ2) β β) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(logβ2) β β |
44 | 40, 43 | resubcli 11459 |
. . . . . . . . . . 11
β’ (1
β (logβ2)) β β |
45 | 44 | elexi 3462 |
. . . . . . . . . 10
β’ (1
β (logβ2)) β V |
46 | 39, 4, 45 | fvmpt 6945 |
. . . . . . . . 9
β’ (1 β
β β (πΊβ1)
= (1 β (logβ2))) |
47 | 15, 46 | ax-mp 5 |
. . . . . . . 8
β’ (πΊβ1) = (1 β
(logβ2)) |
48 | 24, 47 | eqtrdi 2792 |
. . . . . . 7
β’ (π = 1 β (πΊβπ) = (1 β
(logβ2))) |
49 | 48 | breq1d 5113 |
. . . . . 6
β’ (π = 1 β ((πΊβπ) β€ Ξ³ β (1 β
(logβ2)) β€ Ξ³)) |
50 | 49 | rspcva 3577 |
. . . . 5
β’ ((1
β β β§ βπ β β (πΊβπ) β€ Ξ³) β (1 β
(logβ2)) β€ Ξ³) |
51 | 15, 23, 50 | sylancr 587 |
. . . 4
β’ (β€
β (1 β (logβ2)) β€ Ξ³) |
52 | | fveq2 6839 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
53 | 52 | negeqd 11391 |
. . . . . . . . . . 11
β’ (π₯ = π β -(πΉβπ₯) = -(πΉβπ)) |
54 | | eqid 2736 |
. . . . . . . . . . 11
β’ (π₯ β β β¦ -(πΉβπ₯)) = (π₯ β β β¦ -(πΉβπ₯)) |
55 | | negex 11395 |
. . . . . . . . . . 11
β’ -(πΉβπ) β V |
56 | 53, 54, 55 | fvmpt 6945 |
. . . . . . . . . 10
β’ (π β β β ((π₯ β β β¦ -(πΉβπ₯))βπ) = -(πΉβπ)) |
57 | 56 | adantl 482 |
. . . . . . . . 9
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) = -(πΉβπ)) |
58 | 7 | simpli 484 |
. . . . . . . . . . . . 13
β’ πΉ β
Ξ³ |
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β πΉ β
Ξ³) |
60 | | 0cnd 11144 |
. . . . . . . . . . . 12
β’ (β€
β 0 β β) |
61 | | nnex 12155 |
. . . . . . . . . . . . . 14
β’ β
β V |
62 | 61 | mptex 7169 |
. . . . . . . . . . . . 13
β’ (π₯ β β β¦ -(πΉβπ₯)) β V |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β (π₯ β β
β¦ -(πΉβπ₯)) β V) |
64 | 10 | simpli 484 |
. . . . . . . . . . . . . . 15
β’ πΉ:ββΆβ |
65 | 64 | ffvelcdmi 7030 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΉβπ) β β) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
67 | 66 | recnd 11179 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
68 | | fveq2 6839 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
69 | 68 | negeqd 11391 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β -(πΉβπ₯) = -(πΉβπ)) |
70 | | negex 11395 |
. . . . . . . . . . . . . . 15
β’ -(πΉβπ) β V |
71 | 69, 54, 70 | fvmpt 6945 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π₯ β β β¦ -(πΉβπ₯))βπ) = -(πΉβπ)) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) = -(πΉβπ)) |
73 | | df-neg 11384 |
. . . . . . . . . . . . 13
β’ -(πΉβπ) = (0 β (πΉβπ)) |
74 | 72, 73 | eqtrdi 2792 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) = (0 β (πΉβπ))) |
75 | 1, 2, 59, 60, 63, 67, 74 | climsubc2 15513 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β β
β¦ -(πΉβπ₯)) β (0 β
Ξ³)) |
76 | 75 | adantr 481 |
. . . . . . . . . 10
β’
((β€ β§ π
β β) β (π₯
β β β¦ -(πΉβπ₯)) β (0 β
Ξ³)) |
77 | 66 | renegcld 11578 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β -(πΉβπ) β β) |
78 | 72, 77 | eqeltrd 2838 |
. . . . . . . . . . 11
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) β β) |
79 | 78 | adantlr 713 |
. . . . . . . . . 10
β’
(((β€ β§ π
β β) β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) β β) |
80 | 19 | simpld 495 |
. . . . . . . . . . . . . 14
β’ (π β β β (πΉβ(π + 1)) β€ (πΉβπ)) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β (πΉβ(π + 1)) β€ (πΉβπ)) |
82 | | peano2nn 12161 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π
β β) β (π +
1) β β) |
84 | 64 | ffvelcdmi 7030 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β β β
(πΉβ(π + 1)) β
β) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π
β β) β (πΉβ(π + 1)) β β) |
86 | 85, 66 | lenegd 11730 |
. . . . . . . . . . . . 13
β’
((β€ β§ π
β β) β ((πΉβ(π + 1)) β€ (πΉβπ) β -(πΉβπ) β€ -(πΉβ(π + 1)))) |
87 | 81, 86 | mpbid 231 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β -(πΉβπ) β€ -(πΉβ(π + 1))) |
88 | | fveq2 6839 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + 1) β (πΉβπ₯) = (πΉβ(π + 1))) |
89 | 88 | negeqd 11391 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + 1) β -(πΉβπ₯) = -(πΉβ(π + 1))) |
90 | | negex 11395 |
. . . . . . . . . . . . . 14
β’ -(πΉβ(π + 1)) β V |
91 | 89, 54, 90 | fvmpt 6945 |
. . . . . . . . . . . . 13
β’ ((π + 1) β β β
((π₯ β β β¦
-(πΉβπ₯))β(π + 1)) = -(πΉβ(π + 1))) |
92 | 83, 91 | syl 17 |
. . . . . . . . . . . 12
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))β(π + 1)) = -(πΉβ(π + 1))) |
93 | 87, 72, 92 | 3brtr4d 5135 |
. . . . . . . . . . 11
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) β€ ((π₯ β β β¦ -(πΉβπ₯))β(π + 1))) |
94 | 93 | adantlr 713 |
. . . . . . . . . 10
β’
(((β€ β§ π
β β) β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) β€ ((π₯ β β β¦ -(πΉβπ₯))β(π + 1))) |
95 | 1, 16, 76, 79, 94 | climub 15538 |
. . . . . . . . 9
β’
((β€ β§ π
β β) β ((π₯
β β β¦ -(πΉβπ₯))βπ) β€ (0 β Ξ³)) |
96 | 57, 95 | eqbrtrrd 5127 |
. . . . . . . 8
β’
((β€ β§ π
β β) β -(πΉβπ) β€ (0 β Ξ³)) |
97 | | df-neg 11384 |
. . . . . . . 8
β’ -Ξ³
= (0 β Ξ³) |
98 | 96, 97 | breqtrrdi 5145 |
. . . . . . 7
β’
((β€ β§ π
β β) β -(πΉβπ) β€ -Ξ³) |
99 | 14 | mptru 1548 |
. . . . . . . 8
β’ Ξ³
β β |
100 | 64 | ffvelcdmi 7030 |
. . . . . . . . 9
β’ (π β β β (πΉβπ) β β) |
101 | 100 | adantl 482 |
. . . . . . . 8
β’
((β€ β§ π
β β) β (πΉβπ) β β) |
102 | | leneg 11654 |
. . . . . . . 8
β’ ((Ξ³
β β β§ (πΉβπ) β β) β (Ξ³ β€ (πΉβπ) β -(πΉβπ) β€ -Ξ³)) |
103 | 99, 101, 102 | sylancr 587 |
. . . . . . 7
β’
((β€ β§ π
β β) β (Ξ³ β€ (πΉβπ) β -(πΉβπ) β€ -Ξ³)) |
104 | 98, 103 | mpbird 256 |
. . . . . 6
β’
((β€ β§ π
β β) β Ξ³ β€ (πΉβπ)) |
105 | 104 | ralrimiva 3141 |
. . . . 5
β’ (β€
β βπ β
β Ξ³ β€ (πΉβπ)) |
106 | | fveq2 6839 |
. . . . . . . 8
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
107 | | fveq2 6839 |
. . . . . . . . . . . . 13
β’ (π = 1 β (logβπ) =
(logβ1)) |
108 | | log1 25925 |
. . . . . . . . . . . . 13
β’
(logβ1) = 0 |
109 | 107, 108 | eqtrdi 2792 |
. . . . . . . . . . . 12
β’ (π = 1 β (logβπ) = 0) |
110 | 34, 109 | oveq12d 7371 |
. . . . . . . . . . 11
β’ (π = 1 β (Ξ£π β (1...π)(1 / π) β (logβπ)) = (1 β 0)) |
111 | | 1m0e1 12270 |
. . . . . . . . . . 11
β’ (1
β 0) = 1 |
112 | 110, 111 | eqtrdi 2792 |
. . . . . . . . . 10
β’ (π = 1 β (Ξ£π β (1...π)(1 / π) β (logβπ)) = 1) |
113 | 40 | elexi 3462 |
. . . . . . . . . 10
β’ 1 β
V |
114 | 112, 3, 113 | fvmpt 6945 |
. . . . . . . . 9
β’ (1 β
β β (πΉβ1)
= 1) |
115 | 15, 114 | ax-mp 5 |
. . . . . . . 8
β’ (πΉβ1) = 1 |
116 | 106, 115 | eqtrdi 2792 |
. . . . . . 7
β’ (π = 1 β (πΉβπ) = 1) |
117 | 116 | breq2d 5115 |
. . . . . 6
β’ (π = 1 β (Ξ³ β€ (πΉβπ) β Ξ³ β€ 1)) |
118 | 117 | rspcva 3577 |
. . . . 5
β’ ((1
β β β§ βπ β β Ξ³ β€ (πΉβπ)) β Ξ³ β€ 1) |
119 | 15, 105, 118 | sylancr 587 |
. . . 4
β’ (β€
β Ξ³ β€ 1) |
120 | 44, 40 | elicc2i 13322 |
. . . 4
β’ (Ξ³
β ((1 β (logβ2))[,]1) β (Ξ³ β β β§ (1
β (logβ2)) β€ Ξ³ β§ Ξ³ β€ 1)) |
121 | 14, 51, 119, 120 | syl3anbrc 1343 |
. . 3
β’ (β€
β Ξ³ β ((1 β (logβ2))[,]1)) |
122 | | ffn 6665 |
. . . . 5
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
123 | 64, 122 | mp1i 13 |
. . . 4
β’ (β€
β πΉ Fn
β) |
124 | 16, 1 | eleqtrdi 2848 |
. . . . . . . 8
β’
((β€ β§ π
β β) β π
β (β€β₯β1)) |
125 | | elfznn 13462 |
. . . . . . . . . 10
β’ (π β (1...π) β π β β) |
126 | 125 | adantl 482 |
. . . . . . . . 9
β’
(((β€ β§ π
β β) β§ π
β (1...π)) β
π β
β) |
127 | 126, 65 | syl 17 |
. . . . . . . 8
β’
(((β€ β§ π
β β) β§ π
β (1...π)) β
(πΉβπ) β β) |
128 | | elfznn 13462 |
. . . . . . . . . 10
β’ (π β (1...(π β 1)) β π β β) |
129 | 128 | adantl 482 |
. . . . . . . . 9
β’
(((β€ β§ π
β β) β§ π
β (1...(π β 1)))
β π β
β) |
130 | 129, 80 | syl 17 |
. . . . . . . 8
β’
(((β€ β§ π
β β) β§ π
β (1...(π β 1)))
β (πΉβ(π + 1)) β€ (πΉβπ)) |
131 | 124, 127,
130 | monoord2 13931 |
. . . . . . 7
β’
((β€ β§ π
β β) β (πΉβπ) β€ (πΉβ1)) |
132 | 131, 115 | breqtrdi 5144 |
. . . . . 6
β’
((β€ β§ π
β β) β (πΉβπ) β€ 1) |
133 | 99, 40 | elicc2i 13322 |
. . . . . 6
β’ ((πΉβπ) β (Ξ³[,]1) β ((πΉβπ) β β β§ Ξ³ β€ (πΉβπ) β§ (πΉβπ) β€ 1)) |
134 | 101, 104,
132, 133 | syl3anbrc 1343 |
. . . . 5
β’
((β€ β§ π
β β) β (πΉβπ) β (Ξ³[,]1)) |
135 | 134 | ralrimiva 3141 |
. . . 4
β’ (β€
β βπ β
β (πΉβπ) β
(Ξ³[,]1)) |
136 | | ffnfv 7062 |
. . . 4
β’ (πΉ:ββΆ(Ξ³[,]1)
β (πΉ Fn β β§
βπ β β
(πΉβπ) β (Ξ³[,]1))) |
137 | 123, 135,
136 | sylanbrc 583 |
. . 3
β’ (β€
β πΉ:ββΆ(Ξ³[,]1)) |
138 | | ffn 6665 |
. . . . 5
β’ (πΊ:ββΆβ β
πΊ Fn
β) |
139 | 11, 138 | mp1i 13 |
. . . 4
β’ (β€
β πΊ Fn
β) |
140 | 11 | ffvelcdmi 7030 |
. . . . . . 7
β’ (π β β β (πΊβπ) β β) |
141 | 140 | adantl 482 |
. . . . . 6
β’
((β€ β§ π
β β) β (πΊβπ) β β) |
142 | 126, 12 | syl 17 |
. . . . . . . 8
β’
(((β€ β§ π
β β) β§ π
β (1...π)) β
(πΊβπ) β β) |
143 | 129, 20 | syl 17 |
. . . . . . . 8
β’
(((β€ β§ π
β β) β§ π
β (1...(π β 1)))
β (πΊβπ) β€ (πΊβ(π + 1))) |
144 | 124, 142,
143 | monoord 13930 |
. . . . . . 7
β’
((β€ β§ π
β β) β (πΊβ1) β€ (πΊβπ)) |
145 | 47, 144 | eqbrtrrid 5139 |
. . . . . 6
β’
((β€ β§ π
β β) β (1 β (logβ2)) β€ (πΊβπ)) |
146 | 44, 99 | elicc2i 13322 |
. . . . . 6
β’ ((πΊβπ) β ((1 β
(logβ2))[,]Ξ³) β ((πΊβπ) β β β§ (1 β
(logβ2)) β€ (πΊβπ) β§ (πΊβπ) β€ Ξ³)) |
147 | 141, 145,
22, 146 | syl3anbrc 1343 |
. . . . 5
β’
((β€ β§ π
β β) β (πΊβπ) β ((1 β
(logβ2))[,]Ξ³)) |
148 | 147 | ralrimiva 3141 |
. . . 4
β’ (β€
β βπ β
β (πΊβπ) β ((1 β
(logβ2))[,]Ξ³)) |
149 | | ffnfv 7062 |
. . . 4
β’ (πΊ:ββΆ((1 β
(logβ2))[,]Ξ³) β (πΊ Fn β β§ βπ β β (πΊβπ) β ((1 β
(logβ2))[,]Ξ³))) |
150 | 139, 148,
149 | sylanbrc 583 |
. . 3
β’ (β€
β πΊ:ββΆ((1
β (logβ2))[,]Ξ³)) |
151 | 121, 137,
150 | 3jca 1128 |
. 2
β’ (β€
β (Ξ³ β ((1 β (logβ2))[,]1) β§ πΉ:ββΆ(Ξ³[,]1) β§ πΊ:ββΆ((1 β
(logβ2))[,]Ξ³))) |
152 | 151 | mptru 1548 |
1
β’ (Ξ³
β ((1 β (logβ2))[,]1) β§ πΉ:ββΆ(Ξ³[,]1) β§ πΊ:ββΆ((1 β
(logβ2))[,]Ξ³)) |