Step | Hyp | Ref
| Expression |
1 | | lgamgulm.r |
. . . . . . 7
β’ (π β π
β β) |
2 | | lgamgulm.u |
. . . . . . 7
β’ π = {π₯ β β β£ ((absβπ₯) β€ π
β§ βπ β β0 (1 / π
) β€ (absβ(π₯ + π)))} |
3 | 1, 2 | lgamgulmlem1 26394 |
. . . . . 6
β’ (π β π β (β β (β€ β
β))) |
4 | 3 | sselda 3945 |
. . . . 5
β’ ((π β§ π§ β π) β π§ β (β β (β€ β
β))) |
5 | | ovex 7391 |
. . . . 5
β’
(Ξ£π β
β ((π§ Β·
(logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§)) β V |
6 | | df-lgam 26384 |
. . . . . 6
β’ log
Ξ = (π§ β
(β β (β€ β β)) β¦ (Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§))) |
7 | 6 | fvmpt2 6960 |
. . . . 5
β’ ((π§ β (β β
(β€ β β)) β§ (Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§)) β V) β (log
Ξβπ§) =
(Ξ£π β β
((π§ Β·
(logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§))) |
8 | 4, 5, 7 | sylancl 587 |
. . . 4
β’ ((π β§ π§ β π) β (log Ξβπ§) = (Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§))) |
9 | | nnuz 12811 |
. . . . . . 7
β’ β =
(β€β₯β1) |
10 | | 1zzd 12539 |
. . . . . . 7
β’ ((π β§ π§ β π) β 1 β β€) |
11 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π = π β (π + 1) = (π + 1)) |
12 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
13 | 11, 12 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = π β ((π + 1) / π) = ((π + 1) / π)) |
14 | 13 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π = π β (logβ((π + 1) / π)) = (logβ((π + 1) / π))) |
15 | 14 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π = π β (π§ Β· (logβ((π + 1) / π))) = (π§ Β· (logβ((π + 1) / π)))) |
16 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = π β (π§ / π) = (π§ / π)) |
17 | 16 | fvoveq1d 7380 |
. . . . . . . . . 10
β’ (π = π β (logβ((π§ / π) + 1)) = (logβ((π§ / π) + 1))) |
18 | 15, 17 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) = ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
19 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) = (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
20 | | ovex 7391 |
. . . . . . . . 9
β’ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β V |
21 | 18, 19, 20 | fvmpt 6949 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))βπ) = ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
22 | 21 | adantl 483 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ π β β) β ((π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))βπ) = ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
23 | 4 | eldifad 3923 |
. . . . . . . . . 10
β’ ((π β§ π§ β π) β π§ β β) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β π§ β β) |
25 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ π β β) β π β β) |
26 | 25 | peano2nnd 12175 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ π β β) β (π + 1) β β) |
27 | 26 | nnrpd 12960 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ π β β) β (π + 1) β
β+) |
28 | 25 | nnrpd 12960 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ π β β) β π β β+) |
29 | 27, 28 | rpdivcld 12979 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ π β β) β ((π + 1) / π) β
β+) |
30 | 29 | relogcld 25994 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β (logβ((π + 1) / π)) β β) |
31 | 30 | recnd 11188 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β (logβ((π + 1) / π)) β β) |
32 | 24, 31 | mulcld 11180 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ π β β) β (π§ Β· (logβ((π + 1) / π))) β β) |
33 | 25 | nncnd 12174 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ π β β) β π β β) |
34 | 25 | nnne0d 12208 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ π β β) β π β 0) |
35 | 24, 33, 34 | divcld 11936 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β (π§ / π) β β) |
36 | | 1cnd 11155 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β 1 β
β) |
37 | 35, 36 | addcld 11179 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β ((π§ / π) + 1) β β) |
38 | 4 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β π§ β (β β (β€ β
β))) |
39 | 38, 25 | dmgmdivn0 26393 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β ((π§ / π) + 1) β 0) |
40 | 37, 39 | logcld 25942 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ π β β) β (logβ((π§ / π) + 1)) β β) |
41 | 32, 40 | subcld 11517 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ π β β) β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β β) |
42 | | 1z 12538 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
43 | | seqfn 13924 |
. . . . . . . . . . . 12
β’ (1 β
β€ β seq1( βf + , πΊ) Fn
(β€β₯β1)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . 11
β’ seq1(
βf + , πΊ)
Fn (β€β₯β1) |
45 | 9 | fneq2i 6601 |
. . . . . . . . . . 11
β’ (seq1(
βf + , πΊ)
Fn β β seq1( βf + , πΊ) Fn
(β€β₯β1)) |
46 | 44, 45 | mpbir 230 |
. . . . . . . . . 10
β’ seq1(
βf + , πΊ)
Fn β |
47 | | lgamgulm.g |
. . . . . . . . . . . 12
β’ πΊ = (π β β β¦ (π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))) |
48 | 1, 2, 47 | lgamgulm 26400 |
. . . . . . . . . . 11
β’ (π β seq1( βf
+ , πΊ) β dom
(βπ’βπ)) |
49 | | ulmdm 25768 |
. . . . . . . . . . 11
β’ (seq1(
βf + , πΊ)
β dom (βπ’βπ) β seq1( βf + , πΊ)(βπ’βπ)((βπ’βπ)βseq1(
βf + , πΊ))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . . 10
β’ (π β seq1( βf
+ , πΊ)(βπ’βπ)((βπ’βπ)βseq1(
βf + , πΊ))) |
51 | | ulmf2 25759 |
. . . . . . . . . 10
β’ ((seq1(
βf + , πΊ)
Fn β β§ seq1( βf + , πΊ)(βπ’βπ)((βπ’βπ)βseq1(
βf + , πΊ))) β seq1( βf + ,
πΊ):ββΆ(β
βm π)) |
52 | 46, 50, 51 | sylancr 588 |
. . . . . . . . 9
β’ (π β seq1( βf
+ , πΊ):ββΆ(β βm
π)) |
53 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π§ β π) β seq1( βf + , πΊ):ββΆ(β
βm π)) |
54 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π§ β π) β π§ β π) |
55 | | seqex 13914 |
. . . . . . . . 9
β’ seq1( + ,
(π β β β¦
((π§ Β·
(logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))) β V |
56 | 55 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π§ β π) β seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))) β V) |
57 | 47 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ π β β) β πΊ = (π β β β¦ (π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))) |
58 | 57 | seqeq3d 13920 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ π β β) β seq1(
βf + , πΊ)
= seq1( βf + , (π β β β¦ (π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))))) |
59 | 58 | fveq1d 6845 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ π β β) β (seq1(
βf + , πΊ)βπ) = (seq1( βf + , (π β β β¦ (π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))))βπ)) |
60 | | cnex 11137 |
. . . . . . . . . . . . . . 15
β’ β
β V |
61 | 2, 60 | rabex2 5292 |
. . . . . . . . . . . . . 14
β’ π β V |
62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β V) |
63 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
64 | 63, 9 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
65 | | fz1ssnn 13478 |
. . . . . . . . . . . . . 14
β’
(1...π) β
β |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (1...π) β
β) |
67 | | ovexd 7393 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β β β§ π§ β π)) β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β V) |
68 | 62, 64, 66, 67 | seqof2 13972 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1(
βf + , (π
β β β¦ (π§
β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))))βπ) = (π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))) |
69 | 68 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ π β β) β (seq1(
βf + , (π
β β β¦ (π§
β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))))βπ) = (π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))) |
70 | 59, 69 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β (seq1(
βf + , πΊ)βπ) = (π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))) |
71 | 70 | fveq1d 6845 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β ((seq1(
βf + , πΊ)βπ)βπ§) = ((π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))βπ§)) |
72 | 54 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ π β β) β π§ β π) |
73 | | fvex 6856 |
. . . . . . . . . 10
β’ (seq1( +
, (π β β β¦
((π§ Β·
(logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ) β V |
74 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ)) = (π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ)) |
75 | 74 | fvmpt2 6960 |
. . . . . . . . . 10
β’ ((π§ β π β§ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ) β V) β ((π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))βπ§) = (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ)) |
76 | 72, 73, 75 | sylancl 587 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ π β β) β ((π§ β π β¦ (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ))βπ§) = (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ)) |
77 | 71, 76 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ π β β) β ((seq1(
βf + , πΊ)βπ)βπ§) = (seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))))βπ)) |
78 | 50 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π§ β π) β seq1( βf + , πΊ)(βπ’βπ)((βπ’βπ)βseq1(
βf + , πΊ))) |
79 | 9, 10, 53, 54, 56, 77, 78 | ulmclm 25762 |
. . . . . . 7
β’ ((π β§ π§ β π) β seq1( + , (π β β β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))) β
(((βπ’βπ)βseq1( βf + , πΊ))βπ§)) |
80 | 9, 10, 22, 41, 79 | isumclim 15647 |
. . . . . 6
β’ ((π β§ π§ β π) β Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) =
(((βπ’βπ)βseq1( βf + , πΊ))βπ§)) |
81 | | ulmcl 25756 |
. . . . . . . 8
β’ (seq1(
βf + , πΊ)(βπ’βπ)((βπ’βπ)βseq1(
βf + , πΊ))
β ((βπ’βπ)βseq1( βf + , πΊ)):πβΆβ) |
82 | 50, 81 | syl 17 |
. . . . . . 7
β’ (π β
((βπ’βπ)βseq1( βf + , πΊ)):πβΆβ) |
83 | 82 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π§ β π) β
(((βπ’βπ)βseq1( βf + , πΊ))βπ§) β β) |
84 | 80, 83 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π§ β π) β Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β β) |
85 | 4 | dmgmn0 26391 |
. . . . . 6
β’ ((π β§ π§ β π) β π§ β 0) |
86 | 23, 85 | logcld 25942 |
. . . . 5
β’ ((π β§ π§ β π) β (logβπ§) β β) |
87 | 84, 86 | subcld 11517 |
. . . 4
β’ ((π β§ π§ β π) β (Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§)) β
β) |
88 | 8, 87 | eqeltrd 2834 |
. . 3
β’ ((π β§ π§ β π) β (log Ξβπ§) β
β) |
89 | 88 | ralrimiva 3140 |
. 2
β’ (π β βπ§ β π (log Ξβπ§) β β) |
90 | | ffn 6669 |
. . . . . 6
β’
(((βπ’βπ)βseq1( βf + , πΊ)):πβΆβ β
((βπ’βπ)βseq1( βf + , πΊ)) Fn π) |
91 | 50, 81, 90 | 3syl 18 |
. . . . 5
β’ (π β
((βπ’βπ)βseq1( βf + , πΊ)) Fn π) |
92 | | nfcv 2904 |
. . . . . . 7
β’
β²π§(βπ’βπ) |
93 | | nfcv 2904 |
. . . . . . . 8
β’
β²π§1 |
94 | | nfcv 2904 |
. . . . . . . 8
β’
β²π§
βf + |
95 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π§β |
96 | | nfmpt1 5214 |
. . . . . . . . . 10
β’
β²π§(π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
97 | 95, 96 | nfmpt 5213 |
. . . . . . . . 9
β’
β²π§(π β β β¦ (π§ β π β¦ ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))))) |
98 | 47, 97 | nfcxfr 2902 |
. . . . . . . 8
β’
β²π§πΊ |
99 | 93, 94, 98 | nfseq 13922 |
. . . . . . 7
β’
β²π§seq1(
βf + , πΊ) |
100 | 92, 99 | nffv 6853 |
. . . . . 6
β’
β²π§((βπ’βπ)βseq1(
βf + , πΊ)) |
101 | 100 | dffn5f 6914 |
. . . . 5
β’
(((βπ’βπ)βseq1( βf + , πΊ)) Fn π β
((βπ’βπ)βseq1( βf + , πΊ)) = (π§ β π β¦
(((βπ’βπ)βseq1( βf + , πΊ))βπ§))) |
102 | 91, 101 | sylib 217 |
. . . 4
β’ (π β
((βπ’βπ)βseq1( βf + , πΊ)) = (π§ β π β¦
(((βπ’βπ)βseq1( βf + , πΊ))βπ§))) |
103 | 8 | oveq1d 7373 |
. . . . . 6
β’ ((π β§ π§ β π) β ((log Ξβπ§) + (logβπ§)) = ((Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§)) + (logβπ§))) |
104 | 84, 86 | npcand 11521 |
. . . . . 6
β’ ((π β§ π§ β π) β ((Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1))) β (logβπ§)) + (logβπ§)) = Ξ£π β β ((π§ Β· (logβ((π + 1) / π))) β (logβ((π§ / π) + 1)))) |
105 | 103, 104,
80 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ π§ β π) β
(((βπ’βπ)βseq1( βf + , πΊ))βπ§) = ((log Ξβπ§) + (logβπ§))) |
106 | 105 | mpteq2dva 5206 |
. . . 4
β’ (π β (π§ β π β¦
(((βπ’βπ)βseq1( βf + , πΊ))βπ§)) = (π§ β π β¦ ((log Ξβπ§) + (logβπ§)))) |
107 | 102, 106 | eqtrd 2773 |
. . 3
β’ (π β
((βπ’βπ)βseq1( βf + , πΊ)) = (π§ β π β¦ ((log Ξβπ§) + (logβπ§)))) |
108 | 50, 107 | breqtrd 5132 |
. 2
β’ (π β seq1( βf
+ , πΊ)(βπ’βπ)(π§ β π β¦ ((log Ξβπ§) + (logβπ§)))) |
109 | 89, 108 | jca 513 |
1
β’ (π β (βπ§ β π (log Ξβπ§) β β β§ seq1(
βf + , πΊ)(βπ’βπ)(π§ β π β¦ ((log Ξβπ§) + (logβπ§))))) |