Step | Hyp | Ref
| Expression |
1 | | fveq2 5517 |
. . . . 5
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
2 | 1 | eleq1d 2246 |
. . . 4
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
3 | | cvgratnn.6 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
4 | 3 | ralrimiva 2550 |
. . . 4
โข (๐ โ โ๐ โ โ (๐นโ๐) โ โ) |
5 | | cvgratnnlemfm.m |
. . . 4
โข (๐ โ ๐ โ โ) |
6 | 2, 4, 5 | rspcdva 2848 |
. . 3
โข (๐ โ (๐นโ๐) โ โ) |
7 | 6 | abscld 11193 |
. 2
โข (๐ โ (absโ(๐นโ๐)) โ โ) |
8 | | cvgratnn.3 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
9 | | cvgratnn.gt0 |
. . . . . . . . . . 11
โข (๐ โ 0 < ๐ด) |
10 | 8, 9 | gt0ap0d 8589 |
. . . . . . . . . 10
โข (๐ โ ๐ด # 0) |
11 | 8, 10 | rerecclapd 8794 |
. . . . . . . . 9
โข (๐ โ (1 / ๐ด) โ โ) |
12 | | 1red 7975 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
13 | 11, 12 | resubcld 8341 |
. . . . . . . 8
โข (๐ โ ((1 / ๐ด) โ 1) โ
โ) |
14 | | cvgratnn.4 |
. . . . . . . . . 10
โข (๐ โ ๐ด < 1) |
15 | 8, 9 | elrpd 9696 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ
โ+) |
16 | 15 | reclt1d 9713 |
. . . . . . . . . 10
โข (๐ โ (๐ด < 1 โ 1 < (1 / ๐ด))) |
17 | 14, 16 | mpbid 147 |
. . . . . . . . 9
โข (๐ โ 1 < (1 / ๐ด)) |
18 | 12, 11 | posdifd 8492 |
. . . . . . . . 9
โข (๐ โ (1 < (1 / ๐ด) โ 0 < ((1 / ๐ด) โ 1))) |
19 | 17, 18 | mpbid 147 |
. . . . . . . 8
โข (๐ โ 0 < ((1 / ๐ด) โ 1)) |
20 | 13, 19 | elrpd 9696 |
. . . . . . 7
โข (๐ โ ((1 / ๐ด) โ 1) โ
โ+) |
21 | 20 | rpreccld 9710 |
. . . . . 6
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ+) |
22 | 21, 15 | rpdivcld 9717 |
. . . . 5
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ+) |
23 | 22 | rpred 9699 |
. . . 4
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ) |
24 | | fveq2 5517 |
. . . . . . 7
โข (๐ = 1 โ (๐นโ๐) = (๐นโ1)) |
25 | 24 | eleq1d 2246 |
. . . . . 6
โข (๐ = 1 โ ((๐นโ๐) โ โ โ (๐นโ1) โ โ)) |
26 | | 1nn 8933 |
. . . . . . 7
โข 1 โ
โ |
27 | 26 | a1i 9 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
28 | 25, 4, 27 | rspcdva 2848 |
. . . . 5
โข (๐ โ (๐นโ1) โ โ) |
29 | 28 | abscld 11193 |
. . . 4
โข (๐ โ (absโ(๐นโ1)) โ
โ) |
30 | 23, 29 | remulcld 7991 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) โ
โ) |
31 | 30, 5 | nndivred 8972 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐) โ โ) |
32 | | peano2re 8096 |
. . . . 5
โข
((absโ(๐นโ1)) โ โ โ
((absโ(๐นโ1)) +
1) โ โ) |
33 | 29, 32 | syl 14 |
. . . 4
โข (๐ โ ((absโ(๐นโ1)) + 1) โ
โ) |
34 | 23, 33 | remulcld 7991 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) โ
โ) |
35 | 34, 5 | nndivred 8972 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐) โ
โ) |
36 | | nnm1nn0 9220 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
37 | 5, 36 | syl 14 |
. . . . 5
โข (๐ โ (๐ โ 1) โ
โ0) |
38 | 8, 37 | reexpcld 10674 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
39 | 29, 38 | remulcld 7991 |
. . 3
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โ
โ) |
40 | | cvgratnn.7 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
41 | 8, 14, 9, 3, 40, 5 | cvgratnnlemnexp 11535 |
. . 3
โข (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1)))) |
42 | 23, 5 | nndivred 8972 |
. . . . 5
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐) โ โ) |
43 | 28 | absge0d 11196 |
. . . . 5
โข (๐ โ 0 โค (absโ(๐นโ1))) |
44 | 8 | recnd 7989 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
45 | 5 | nnzd 9377 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
46 | 44, 10, 45 | expm1apd 10667 |
. . . . . . . 8
โข (๐ โ (๐ดโ(๐ โ 1)) = ((๐ดโ๐) / ๐ด)) |
47 | 5 | nnnn0d 9232 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ0) |
48 | 8, 47 | reexpcld 10674 |
. . . . . . . . 9
โข (๐ โ (๐ดโ๐) โ โ) |
49 | 21 | rpred 9699 |
. . . . . . . . . 10
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ) |
50 | 49, 5 | nndivred 8972 |
. . . . . . . . 9
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐) โ
โ) |
51 | 8, 14, 9, 5 | cvgratnnlembern 11534 |
. . . . . . . . 9
โข (๐ โ (๐ดโ๐) < ((1 / ((1 / ๐ด) โ 1)) / ๐)) |
52 | 48, 50, 15, 51 | ltdiv1dd 9757 |
. . . . . . . 8
โข (๐ โ ((๐ดโ๐) / ๐ด) < (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด)) |
53 | 46, 52 | eqbrtrd 4027 |
. . . . . . 7
โข (๐ โ (๐ดโ(๐ โ 1)) < (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด)) |
54 | 49 | recnd 7989 |
. . . . . . . 8
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ) |
55 | 5 | nncnd 8936 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
56 | 5 | nnap0d 8968 |
. . . . . . . 8
โข (๐ โ ๐ # 0) |
57 | 54, 55, 44, 56, 10 | divdiv32apd 8776 |
. . . . . . 7
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด) = (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
58 | 53, 57 | breqtrd 4031 |
. . . . . 6
โข (๐ โ (๐ดโ(๐ โ 1)) < (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
59 | 38, 42, 58 | ltled 8079 |
. . . . 5
โข (๐ โ (๐ดโ(๐ โ 1)) โค (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
60 | 38, 42, 29, 43, 59 | lemul2ad 8900 |
. . . 4
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โค ((absโ(๐นโ1)) ยท (((1 / ((1 /
๐ด) โ 1)) / ๐ด) / ๐))) |
61 | 29 | recnd 7989 |
. . . . . . 7
โข (๐ โ (absโ(๐นโ1)) โ
โ) |
62 | 23 | recnd 7989 |
. . . . . . 7
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ) |
63 | 61, 62 | mulcomd 7982 |
. . . . . 6
โข (๐ โ ((absโ(๐นโ1)) ยท ((1 / ((1 /
๐ด) โ 1)) / ๐ด)) = (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1)))) |
64 | 63 | oveq1d 5893 |
. . . . 5
โข (๐ โ (((absโ(๐นโ1)) ยท ((1 / ((1 /
๐ด) โ 1)) / ๐ด)) / ๐) = ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
65 | 61, 62, 55, 56 | divassapd 8786 |
. . . . 5
โข (๐ โ (((absโ(๐นโ1)) ยท ((1 / ((1 /
๐ด) โ 1)) / ๐ด)) / ๐) = ((absโ(๐นโ1)) ยท (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐))) |
66 | 64, 65 | eqtr3d 2212 |
. . . 4
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐) = ((absโ(๐นโ1)) ยท (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐))) |
67 | 60, 66 | breqtrrd 4033 |
. . 3
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โค ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
68 | 7, 39, 31, 41, 67 | letrd 8084 |
. 2
โข (๐ โ (absโ(๐นโ๐)) โค ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
69 | 5 | nnrpd 9697 |
. . 3
โข (๐ โ ๐ โ
โ+) |
70 | 29 | ltp1d 8890 |
. . . 4
โข (๐ โ (absโ(๐นโ1)) <
((absโ(๐นโ1)) +
1)) |
71 | 29, 33, 22, 70 | ltmul2dd 9756 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) < (((1 / ((1 /
๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) +
1))) |
72 | 30, 34, 69, 71 | ltdiv1dd 9757 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐) < ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐)) |
73 | 7, 31, 35, 68, 72 | lelttrd 8085 |
1
โข (๐ โ (absโ(๐นโ๐)) < ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐)) |