Step | Hyp | Ref
| Expression |
1 | | breq2 5114 |
. . 3
โข ((๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) โ ((absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))))) |
2 | | breq2 5114 |
. . 3
โข (((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) โ ((absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))))) |
3 | | lgamgulm.r |
. . . . . 6
โข (๐ โ ๐
โ โ) |
4 | 3 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐
โ โ) |
5 | 4 | adantr 482 |
. . . 4
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง (2 ยท ๐
) โค ๐) โ ๐
โ โ) |
6 | | lgamgulm.u |
. . . . 5
โข ๐ = {๐ฅ โ โ โฃ ((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐)))} |
7 | | fveq2 6847 |
. . . . . . . 8
โข (๐ฅ = ๐ก โ (absโ๐ฅ) = (absโ๐ก)) |
8 | 7 | breq1d 5120 |
. . . . . . 7
โข (๐ฅ = ๐ก โ ((absโ๐ฅ) โค ๐
โ (absโ๐ก) โค ๐
)) |
9 | | fvoveq1 7385 |
. . . . . . . . 9
โข (๐ฅ = ๐ก โ (absโ(๐ฅ + ๐)) = (absโ(๐ก + ๐))) |
10 | 9 | breq2d 5122 |
. . . . . . . 8
โข (๐ฅ = ๐ก โ ((1 / ๐
) โค (absโ(๐ฅ + ๐)) โ (1 / ๐
) โค (absโ(๐ก + ๐)))) |
11 | 10 | ralbidv 3175 |
. . . . . . 7
โข (๐ฅ = ๐ก โ (โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐)) โ โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ก + ๐)))) |
12 | 8, 11 | anbi12d 632 |
. . . . . 6
โข (๐ฅ = ๐ก โ (((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐))) โ ((absโ๐ก) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ก + ๐))))) |
13 | 12 | cbvrabv 3420 |
. . . . 5
โข {๐ฅ โ โ โฃ
((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 /
๐
) โค (absโ(๐ฅ + ๐)))} = {๐ก โ โ โฃ ((absโ๐ก) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ก + ๐)))} |
14 | 6, 13 | eqtri 2765 |
. . . 4
โข ๐ = {๐ก โ โ โฃ ((absโ๐ก) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ก + ๐)))} |
15 | | simplrl 776 |
. . . 4
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง (2 ยท ๐
) โค ๐) โ ๐ โ โ) |
16 | | simprr 772 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ฆ โ ๐) |
17 | 16 | adantr 482 |
. . . 4
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง (2 ยท ๐
) โค ๐) โ ๐ฆ โ ๐) |
18 | | simpr 486 |
. . . 4
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง (2 ยท ๐
) โค ๐) โ (2 ยท ๐
) โค ๐) |
19 | 5, 14, 15, 17, 18 | lgamgulmlem3 26396 |
. . 3
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง (2 ยท ๐
) โค ๐) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
20 | 3, 6 | lgamgulmlem1 26394 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (โ โ (โค โ
โ))) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ (โ โ (โค โ
โ))) |
22 | 21, 16 | sseldd 3950 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ฆ โ (โ โ (โค โ
โ))) |
23 | 22 | eldifad 3927 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ฆ โ โ) |
24 | | simprl 770 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ โ) |
25 | 24 | peano2nnd 12177 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ + 1) โ โ) |
26 | 25 | nnrpd 12962 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ + 1) โ
โ+) |
27 | 24 | nnrpd 12962 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ โ+) |
28 | 26, 27 | rpdivcld 12981 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ + 1) / ๐) โ
โ+) |
29 | 28 | relogcld 25994 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ((๐ + 1) / ๐)) โ โ) |
30 | 29 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ((๐ + 1) / ๐)) โ โ) |
31 | 23, 30 | mulcld 11182 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ฆ ยท (logโ((๐ + 1) / ๐))) โ โ) |
32 | 24 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ โ) |
33 | 24 | nnne0d 12210 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ 0) |
34 | 23, 32, 33 | divcld 11938 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ฆ / ๐) โ โ) |
35 | | 1cnd 11157 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 1 โ โ) |
36 | 34, 35 | addcld 11181 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ / ๐) + 1) โ โ) |
37 | 22, 24 | dmgmdivn0 26393 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ / ๐) + 1) โ 0) |
38 | 36, 37 | logcld 25942 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ((๐ฆ / ๐) + 1)) โ โ) |
39 | 31, 38 | subcld 11519 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1))) โ โ) |
40 | 39 | abscld 15328 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โ โ) |
41 | 31 | abscld 15328 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) โ โ) |
42 | 38 | abscld 15328 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(logโ((๐ฆ / ๐) + 1))) โ โ) |
43 | 41, 42 | readdcld 11191 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) + (absโ(logโ((๐ฆ / ๐) + 1)))) โ โ) |
44 | 4 | nnred 12175 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐
โ โ) |
45 | 44, 29 | remulcld 11192 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
ยท (logโ((๐ + 1) / ๐))) โ โ) |
46 | 4 | peano2nnd 12177 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โ โ) |
47 | 46 | nnrpd 12962 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โ
โ+) |
48 | 47, 27 | rpmulcld 12980 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐
+ 1) ยท ๐) โ
โ+) |
49 | 48 | relogcld 25994 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ((๐
+ 1) ยท ๐)) โ โ) |
50 | | pire 25831 |
. . . . . . . 8
โข ฯ
โ โ |
51 | 50 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ฯ โ
โ) |
52 | 49, 51 | readdcld 11191 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((logโ((๐
+ 1) ยท ๐)) + ฯ) โ โ) |
53 | 45, 52 | readdcld 11191 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) โ โ) |
54 | 31, 38 | abs2dif2d 15350 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค ((absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) + (absโ(logโ((๐ฆ / ๐) + 1))))) |
55 | 23, 30 | absmuld 15346 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) = ((absโ๐ฆ) ยท (absโ(logโ((๐ + 1) / ๐))))) |
56 | 28 | rpred 12964 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ + 1) / ๐) โ โ) |
57 | 32 | mulid2d 11180 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 ยท ๐) = ๐) |
58 | 24 | nnred 12175 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ โ) |
59 | 58 | lep1d 12093 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โค (๐ + 1)) |
60 | 57, 59 | eqbrtrd 5132 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 ยท ๐) โค (๐ + 1)) |
61 | | 1red 11163 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 1 โ โ) |
62 | 58, 61 | readdcld 11191 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ + 1) โ โ) |
63 | 61, 62, 27 | lemuldivd 13013 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((1 ยท ๐) โค (๐ + 1) โ 1 โค ((๐ + 1) / ๐))) |
64 | 60, 63 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 1 โค ((๐ + 1) / ๐)) |
65 | 56, 64 | logge0d 26001 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 0 โค (logโ((๐ + 1) / ๐))) |
66 | 29, 65 | absidd 15314 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(logโ((๐ + 1) / ๐))) = (logโ((๐ + 1) / ๐))) |
67 | 66 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) ยท (absโ(logโ((๐ + 1) / ๐)))) = ((absโ๐ฆ) ยท (logโ((๐ + 1) / ๐)))) |
68 | 55, 67 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) = ((absโ๐ฆ) ยท (logโ((๐ + 1) / ๐)))) |
69 | 23 | abscld 15328 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ๐ฆ) โ โ) |
70 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ (absโ๐ฅ) = (absโ๐ฆ)) |
71 | 70 | breq1d 5120 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ ((absโ๐ฅ) โค ๐
โ (absโ๐ฆ) โค ๐
)) |
72 | | fvoveq1 7385 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ฆ โ (absโ(๐ฅ + ๐)) = (absโ(๐ฆ + ๐))) |
73 | 72 | breq2d 5122 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ ((1 / ๐
) โค (absโ(๐ฅ + ๐)) โ (1 / ๐
) โค (absโ(๐ฆ + ๐)))) |
74 | 73 | ralbidv 3175 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐)) โ โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐)))) |
75 | 71, 74 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ฆ โ (((absโ๐ฅ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฅ + ๐))) โ ((absโ๐ฆ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐))))) |
76 | 75, 6 | elrab2 3653 |
. . . . . . . . . . 11
โข (๐ฆ โ ๐ โ (๐ฆ โ โ โง ((absโ๐ฆ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐))))) |
77 | 76 | simprbi 498 |
. . . . . . . . . 10
โข (๐ฆ โ ๐ โ ((absโ๐ฆ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐)))) |
78 | 77 | ad2antll 728 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) โค ๐
โง โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐)))) |
79 | 78 | simpld 496 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ๐ฆ) โค ๐
) |
80 | 69, 44, 29, 65, 79 | lemul1ad 12101 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) ยท (logโ((๐ + 1) / ๐))) โค (๐
ยท (logโ((๐ + 1) / ๐)))) |
81 | 68, 80 | eqbrtrd 5132 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) โค (๐
ยท (logโ((๐ + 1) / ๐)))) |
82 | 36, 37 | absrpcld 15340 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โ
โ+) |
83 | 82 | relogcld 25994 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ(absโ((๐ฆ / ๐) + 1))) โ โ) |
84 | 83 | recnd 11190 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ(absโ((๐ฆ / ๐) + 1))) โ โ) |
85 | 84 | abscld 15328 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ
(absโ(logโ(absโ((๐ฆ / ๐) + 1)))) โ โ) |
86 | 85, 51 | readdcld 11191 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ
((absโ(logโ(absโ((๐ฆ / ๐) + 1)))) + ฯ) โ
โ) |
87 | | abslogle 25989 |
. . . . . . . 8
โข ((((๐ฆ / ๐) + 1) โ โ โง ((๐ฆ / ๐) + 1) โ 0) โ
(absโ(logโ((๐ฆ /
๐) + 1))) โค
((absโ(logโ(absโ((๐ฆ / ๐) + 1)))) + ฯ)) |
88 | 36, 37, 87 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(logโ((๐ฆ / ๐) + 1))) โค
((absโ(logโ(absโ((๐ฆ / ๐) + 1)))) + ฯ)) |
89 | | 1rp 12926 |
. . . . . . . . . . . 12
โข 1 โ
โ+ |
90 | | relogdiv 25964 |
. . . . . . . . . . . 12
โข ((1
โ โ+ โง ((๐
+ 1) ยท ๐) โ โ+) โ
(logโ(1 / ((๐
+ 1)
ยท ๐))) =
((logโ1) โ (logโ((๐
+ 1) ยท ๐)))) |
91 | 89, 48, 90 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ(1 / ((๐
+ 1) ยท ๐))) = ((logโ1) โ
(logโ((๐
+ 1)
ยท ๐)))) |
92 | | log1 25957 |
. . . . . . . . . . . . 13
โข
(logโ1) = 0 |
93 | 92 | oveq1i 7372 |
. . . . . . . . . . . 12
โข
((logโ1) โ (logโ((๐
+ 1) ยท ๐))) = (0 โ (logโ((๐
+ 1) ยท ๐))) |
94 | | df-neg 11395 |
. . . . . . . . . . . 12
โข
-(logโ((๐
+ 1)
ยท ๐)) = (0 โ
(logโ((๐
+ 1)
ยท ๐))) |
95 | 93, 94 | eqtr4i 2768 |
. . . . . . . . . . 11
โข
((logโ1) โ (logโ((๐
+ 1) ยท ๐))) = -(logโ((๐
+ 1) ยท ๐)) |
96 | 91, 95 | eqtr2di 2794 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ -(logโ((๐
+ 1) ยท ๐)) = (logโ(1 / ((๐
+ 1) ยท ๐)))) |
97 | 46 | nnrecred 12211 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / (๐
+ 1)) โ โ) |
98 | 23, 32 | addcld 11181 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ฆ + ๐) โ โ) |
99 | 98 | abscld 15328 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ + ๐)) โ โ) |
100 | 4 | nnrecred 12211 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / ๐
) โ โ) |
101 | 4 | nnrpd 12962 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐
โ
โ+) |
102 | | 0le1 11685 |
. . . . . . . . . . . . . . . 16
โข 0 โค
1 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 0 โค 1) |
104 | 44 | lep1d 12093 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐
โค (๐
+ 1)) |
105 | 101, 47, 61, 103, 104 | lediv2ad 12986 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / (๐
+ 1)) โค (1 / ๐
)) |
106 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐ฆ + ๐) = (๐ฆ + ๐)) |
107 | 106 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (absโ(๐ฆ + ๐)) = (absโ(๐ฆ + ๐))) |
108 | 107 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((1 / ๐
) โค (absโ(๐ฆ + ๐)) โ (1 / ๐
) โค (absโ(๐ฆ + ๐)))) |
109 | 78 | simprd 497 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ โ๐ โ โ0 (1 / ๐
) โค (absโ(๐ฆ + ๐))) |
110 | 24 | nnnn0d 12480 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐ โ โ0) |
111 | 108, 109,
110 | rspcdva 3585 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / ๐
) โค (absโ(๐ฆ + ๐))) |
112 | 97, 100, 99, 105, 111 | letrd 11319 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / (๐
+ 1)) โค (absโ(๐ฆ + ๐))) |
113 | 97, 99, 27, 112 | lediv1dd 13022 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((1 / (๐
+ 1)) / ๐) โค ((absโ(๐ฆ + ๐)) / ๐)) |
114 | 46 | nncnd 12176 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โ โ) |
115 | 46 | nnne0d 12210 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โ 0) |
116 | 114, 32, 115, 33 | recdiv2d 11956 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((1 / (๐
+ 1)) / ๐) = (1 / ((๐
+ 1) ยท ๐))) |
117 | 23, 32, 32, 33 | divdird 11976 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ + ๐) / ๐) = ((๐ฆ / ๐) + (๐ / ๐))) |
118 | 32, 33 | dividd 11936 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐ / ๐) = 1) |
119 | 118 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ / ๐) + (๐ / ๐)) = ((๐ฆ / ๐) + 1)) |
120 | 117, 119 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ฆ / ๐) + 1) = ((๐ฆ + ๐) / ๐)) |
121 | 120 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) = (absโ((๐ฆ + ๐) / ๐))) |
122 | 98, 32, 33 | absdivd 15347 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ + ๐) / ๐)) = ((absโ(๐ฆ + ๐)) / (absโ๐))) |
123 | 27 | rpge0d 12968 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 0 โค ๐) |
124 | 58, 123 | absidd 15314 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ๐) = ๐) |
125 | 124 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ + ๐)) / (absโ๐)) = ((absโ(๐ฆ + ๐)) / ๐)) |
126 | 121, 122,
125 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ + ๐)) / ๐) = (absโ((๐ฆ / ๐) + 1))) |
127 | 113, 116,
126 | 3brtr3d 5141 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / ((๐
+ 1) ยท ๐)) โค (absโ((๐ฆ / ๐) + 1))) |
128 | 48 | rpreccld 12974 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (1 / ((๐
+ 1) ยท ๐)) โ
โ+) |
129 | 128, 82 | logled 25998 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((1 / ((๐
+ 1) ยท ๐)) โค (absโ((๐ฆ / ๐) + 1)) โ (logโ(1 / ((๐
+ 1) ยท ๐))) โค
(logโ(absโ((๐ฆ /
๐) +
1))))) |
130 | 127, 129 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ(1 / ((๐
+ 1) ยท ๐))) โค
(logโ(absโ((๐ฆ /
๐) + 1)))) |
131 | 96, 130 | eqbrtrd 5132 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ -(logโ((๐
+ 1) ยท ๐)) โค (logโ(absโ((๐ฆ / ๐) + 1)))) |
132 | 36 | abscld 15328 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โ โ) |
133 | 44, 61 | readdcld 11191 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โ โ) |
134 | 48 | rpred 12964 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐
+ 1) ยท ๐) โ โ) |
135 | 34 | abscld 15328 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ / ๐)) โ โ) |
136 | 135, 61 | readdcld 11191 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ / ๐)) + 1) โ โ) |
137 | 34, 35 | abstrid 15348 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โค ((absโ(๐ฆ / ๐)) + (absโ1))) |
138 | | abs1 15189 |
. . . . . . . . . . . . . 14
โข
(absโ1) = 1 |
139 | 138 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข
((absโ(๐ฆ /
๐)) + (absโ1)) =
((absโ(๐ฆ / ๐)) + 1) |
140 | 137, 139 | breqtrdi 5151 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โค ((absโ(๐ฆ / ๐)) + 1)) |
141 | 89 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 1 โ
โ+) |
142 | 23 | absge0d 15336 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 0 โค (absโ๐ฆ)) |
143 | 24 | nnge1d 12208 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 1 โค ๐) |
144 | 69, 44, 141, 58, 142, 79, 143 | lediv12ad 13023 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) / ๐) โค (๐
/ 1)) |
145 | 23, 32, 33 | absdivd 15347 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ / ๐)) = ((absโ๐ฆ) / (absโ๐))) |
146 | 124 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) / (absโ๐)) = ((absโ๐ฆ) / ๐)) |
147 | 145, 146 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ๐ฆ) / ๐) = (absโ(๐ฆ / ๐))) |
148 | 4 | nncnd 12176 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ๐
โ โ) |
149 | 148 | div1d 11930 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
/ 1) = ๐
) |
150 | 144, 147,
149 | 3brtr3d 5141 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(๐ฆ / ๐)) โค ๐
) |
151 | 135, 44, 61, 150 | leadd1dd 11776 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ / ๐)) + 1) โค (๐
+ 1)) |
152 | 132, 136,
133, 140, 151 | letrd 11319 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โค (๐
+ 1)) |
153 | 47 | rpge0d 12968 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ 0 โค (๐
+ 1)) |
154 | 133, 58, 153, 143 | lemulge11d 12099 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐
+ 1) โค ((๐
+ 1) ยท ๐)) |
155 | 132, 133,
134, 152, 154 | letrd 11319 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ / ๐) + 1)) โค ((๐
+ 1) ยท ๐)) |
156 | 82, 48 | logled 25998 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ((๐ฆ / ๐) + 1)) โค ((๐
+ 1) ยท ๐) โ (logโ(absโ((๐ฆ / ๐) + 1))) โค (logโ((๐
+ 1) ยท ๐)))) |
157 | 155, 156 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (logโ(absโ((๐ฆ / ๐) + 1))) โค (logโ((๐
+ 1) ยท ๐))) |
158 | 83, 49 | absled 15322 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ
((absโ(logโ(absโ((๐ฆ / ๐) + 1)))) โค (logโ((๐
+ 1) ยท ๐)) โ (-(logโ((๐
+ 1) ยท ๐)) โค (logโ(absโ((๐ฆ / ๐) + 1))) โง (logโ(absโ((๐ฆ / ๐) + 1))) โค (logโ((๐
+ 1) ยท ๐))))) |
159 | 131, 157,
158 | mpbir2and 712 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ
(absโ(logโ(absโ((๐ฆ / ๐) + 1)))) โค (logโ((๐
+ 1) ยท ๐))) |
160 | 85, 49, 51, 159 | leadd1dd 11776 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ
((absโ(logโ(absโ((๐ฆ / ๐) + 1)))) + ฯ) โค ((logโ((๐
+ 1) ยท ๐)) + ฯ)) |
161 | 42, 86, 52, 88, 160 | letrd 11319 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ(logโ((๐ฆ / ๐) + 1))) โค ((logโ((๐
+ 1) ยท ๐)) + ฯ)) |
162 | 41, 42, 45, 52, 81, 161 | le2addd 11781 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((absโ(๐ฆ ยท (logโ((๐ + 1) / ๐)))) + (absโ(logโ((๐ฆ / ๐) + 1)))) โค ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) |
163 | 40, 43, 53, 54, 162 | letrd 11319 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) |
164 | 163 | adantr 482 |
. . 3
โข (((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โง ยฌ (2 ยท ๐
) โค ๐) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) |
165 | 1, 2, 19, 164 | ifbothda 4529 |
. 2
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) โค if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
166 | | oveq1 7369 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
167 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ = ๐) |
168 | 166, 167 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ + 1) / ๐) = ((๐ + 1) / ๐)) |
169 | 168 | fveq2d 6851 |
. . . . . . . . . 10
โข (๐ = ๐ โ (logโ((๐ + 1) / ๐)) = (logโ((๐ + 1) / ๐))) |
170 | 169 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ง ยท (logโ((๐ + 1) / ๐))) = (๐ง ยท (logโ((๐ + 1) / ๐)))) |
171 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ง / ๐) = (๐ง / ๐)) |
172 | 171 | fvoveq1d 7384 |
. . . . . . . . 9
โข (๐ = ๐ โ (logโ((๐ง / ๐) + 1)) = (logโ((๐ง / ๐) + 1))) |
173 | 170, 172 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) = ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1)))) |
174 | 173 | mpteq2dv 5212 |
. . . . . . 7
โข (๐ = ๐ โ (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1)))) = (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))) |
175 | | lgamgulm.g |
. . . . . . 7
โข ๐บ = (๐ โ โ โฆ (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))) |
176 | | cnex 11139 |
. . . . . . . . 9
โข โ
โ V |
177 | 6, 176 | rabex2 5296 |
. . . . . . . 8
โข ๐ โ V |
178 | 177 | mptex 7178 |
. . . . . . 7
โข (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1)))) โ V |
179 | 174, 175,
178 | fvmpt 6953 |
. . . . . 6
โข (๐ โ โ โ (๐บโ๐) = (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))) |
180 | 179 | ad2antrl 727 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐บโ๐) = (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))) |
181 | 180 | fveq1d 6849 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐บโ๐)โ๐ฆ) = ((๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))โ๐ฆ)) |
182 | | oveq1 7369 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (๐ง ยท (logโ((๐ + 1) / ๐))) = (๐ฆ ยท (logโ((๐ + 1) / ๐)))) |
183 | | oveq1 7369 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ (๐ง / ๐) = (๐ฆ / ๐)) |
184 | 183 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (logโ((๐ง / ๐) + 1)) = (logโ((๐ฆ / ๐) + 1))) |
185 | 182, 184 | oveq12d 7380 |
. . . . . 6
โข (๐ง = ๐ฆ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) = ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) |
186 | | eqid 2737 |
. . . . . 6
โข (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1)))) = (๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1)))) |
187 | | ovex 7395 |
. . . . . 6
โข ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1))) โ V |
188 | 185, 186,
187 | fvmpt 6953 |
. . . . 5
โข (๐ฆ โ ๐ โ ((๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))โ๐ฆ) = ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) |
189 | 188 | ad2antll 728 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐ง โ ๐ โฆ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))))โ๐ฆ) = ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) |
190 | 181, 189 | eqtrd 2777 |
. . 3
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ ((๐บโ๐)โ๐ฆ) = ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1)))) |
191 | 190 | fveq2d 6851 |
. 2
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐บโ๐)โ๐ฆ)) = (absโ((๐ฆ ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ฆ / ๐) + 1))))) |
192 | | breq2 5114 |
. . . . 5
โข (๐ = ๐ โ ((2 ยท ๐
) โค ๐ โ (2 ยท ๐
) โค ๐)) |
193 | | oveq1 7369 |
. . . . . . 7
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
194 | 193 | oveq2d 7378 |
. . . . . 6
โข (๐ = ๐ โ ((2 ยท (๐
+ 1)) / (๐โ2)) = ((2 ยท (๐
+ 1)) / (๐โ2))) |
195 | 194 | oveq2d 7378 |
. . . . 5
โข (๐ = ๐ โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) = (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
196 | 169 | oveq2d 7378 |
. . . . . 6
โข (๐ = ๐ โ (๐
ยท (logโ((๐ + 1) / ๐))) = (๐
ยท (logโ((๐ + 1) / ๐)))) |
197 | | oveq2 7370 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐
+ 1) ยท ๐) = ((๐
+ 1) ยท ๐)) |
198 | 197 | fveq2d 6851 |
. . . . . . 7
โข (๐ = ๐ โ (logโ((๐
+ 1) ยท ๐)) = (logโ((๐
+ 1) ยท ๐))) |
199 | 198 | oveq1d 7377 |
. . . . . 6
โข (๐ = ๐ โ ((logโ((๐
+ 1) ยท ๐)) + ฯ) = ((logโ((๐
+ 1) ยท ๐)) + ฯ)) |
200 | 196, 199 | oveq12d 7380 |
. . . . 5
โข (๐ = ๐ โ ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) = ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) |
201 | 192, 195,
200 | ifbieq12d 4519 |
. . . 4
โข (๐ = ๐ โ if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
202 | | lgamgulm.t |
. . . 4
โข ๐ = (๐ โ โ โฆ if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
203 | | ovex 7395 |
. . . . 5
โข (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ V |
204 | | ovex 7395 |
. . . . 5
โข ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) โ V |
205 | 203, 204 | ifex 4541 |
. . . 4
โข if((2
ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) โ V |
206 | 201, 202,
205 | fvmpt 6953 |
. . 3
โข (๐ โ โ โ (๐โ๐) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
207 | 206 | ad2antrl 727 |
. 2
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (๐โ๐) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
208 | 165, 191,
207 | 3brtr4d 5142 |
1
โข ((๐ โง (๐ โ โ โง ๐ฆ โ ๐)) โ (absโ((๐บโ๐)โ๐ฆ)) โค (๐โ๐)) |