Step | Hyp | Ref
| Expression |
1 | | fveq2 5516 |
. . . . 5
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
2 | 1 | eleq1d 2246 |
. . . 4
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
3 | | cvgratnn.6 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
4 | 3 | ralrimiva 2550 |
. . . 4
โข (๐ โ โ๐ โ โ (๐นโ๐) โ โ) |
5 | | cvgratnnlemfm.m |
. . . 4
โข (๐ โ ๐ โ โ) |
6 | 2, 4, 5 | rspcdva 2847 |
. . 3
โข (๐ โ (๐นโ๐) โ โ) |
7 | 6 | abscld 11190 |
. 2
โข (๐ โ (absโ(๐นโ๐)) โ โ) |
8 | | cvgratnn.3 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
9 | | cvgratnn.gt0 |
. . . . . . . . . . 11
โข (๐ โ 0 < ๐ด) |
10 | 8, 9 | gt0ap0d 8586 |
. . . . . . . . . 10
โข (๐ โ ๐ด # 0) |
11 | 8, 10 | rerecclapd 8791 |
. . . . . . . . 9
โข (๐ โ (1 / ๐ด) โ โ) |
12 | | 1red 7972 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
13 | 11, 12 | resubcld 8338 |
. . . . . . . 8
โข (๐ โ ((1 / ๐ด) โ 1) โ
โ) |
14 | | cvgratnn.4 |
. . . . . . . . . 10
โข (๐ โ ๐ด < 1) |
15 | 8, 9 | elrpd 9693 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ
โ+) |
16 | 15 | reclt1d 9710 |
. . . . . . . . . 10
โข (๐ โ (๐ด < 1 โ 1 < (1 / ๐ด))) |
17 | 14, 16 | mpbid 147 |
. . . . . . . . 9
โข (๐ โ 1 < (1 / ๐ด)) |
18 | 12, 11 | posdifd 8489 |
. . . . . . . . 9
โข (๐ โ (1 < (1 / ๐ด) โ 0 < ((1 / ๐ด) โ 1))) |
19 | 17, 18 | mpbid 147 |
. . . . . . . 8
โข (๐ โ 0 < ((1 / ๐ด) โ 1)) |
20 | 13, 19 | elrpd 9693 |
. . . . . . 7
โข (๐ โ ((1 / ๐ด) โ 1) โ
โ+) |
21 | 20 | rpreccld 9707 |
. . . . . 6
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ+) |
22 | 21, 15 | rpdivcld 9714 |
. . . . 5
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ+) |
23 | 22 | rpred 9696 |
. . . 4
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ) |
24 | | fveq2 5516 |
. . . . . . 7
โข (๐ = 1 โ (๐นโ๐) = (๐นโ1)) |
25 | 24 | eleq1d 2246 |
. . . . . 6
โข (๐ = 1 โ ((๐นโ๐) โ โ โ (๐นโ1) โ โ)) |
26 | | 1nn 8930 |
. . . . . . 7
โข 1 โ
โ |
27 | 26 | a1i 9 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
28 | 25, 4, 27 | rspcdva 2847 |
. . . . 5
โข (๐ โ (๐นโ1) โ โ) |
29 | 28 | abscld 11190 |
. . . 4
โข (๐ โ (absโ(๐นโ1)) โ
โ) |
30 | 23, 29 | remulcld 7988 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) โ
โ) |
31 | 30, 5 | nndivred 8969 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐) โ โ) |
32 | | peano2re 8093 |
. . . . 5
โข
((absโ(๐นโ1)) โ โ โ
((absโ(๐นโ1)) +
1) โ โ) |
33 | 29, 32 | syl 14 |
. . . 4
โข (๐ โ ((absโ(๐นโ1)) + 1) โ
โ) |
34 | 23, 33 | remulcld 7988 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) โ
โ) |
35 | 34, 5 | nndivred 8969 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐) โ
โ) |
36 | | nnm1nn0 9217 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
37 | 5, 36 | syl 14 |
. . . . 5
โข (๐ โ (๐ โ 1) โ
โ0) |
38 | 8, 37 | reexpcld 10671 |
. . . 4
โข (๐ โ (๐ดโ(๐ โ 1)) โ
โ) |
39 | 29, 38 | remulcld 7988 |
. . 3
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โ
โ) |
40 | | cvgratnn.7 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
41 | 8, 14, 9, 3, 40, 5 | cvgratnnlemnexp 11532 |
. . 3
โข (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1)))) |
42 | 23, 5 | nndivred 8969 |
. . . . 5
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐) โ โ) |
43 | 28 | absge0d 11193 |
. . . . 5
โข (๐ โ 0 โค (absโ(๐นโ1))) |
44 | 8 | recnd 7986 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
45 | 5 | nnzd 9374 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
46 | 44, 10, 45 | expm1apd 10664 |
. . . . . . . 8
โข (๐ โ (๐ดโ(๐ โ 1)) = ((๐ดโ๐) / ๐ด)) |
47 | 5 | nnnn0d 9229 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ0) |
48 | 8, 47 | reexpcld 10671 |
. . . . . . . . 9
โข (๐ โ (๐ดโ๐) โ โ) |
49 | 21 | rpred 9696 |
. . . . . . . . . 10
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ) |
50 | 49, 5 | nndivred 8969 |
. . . . . . . . 9
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐) โ
โ) |
51 | 8, 14, 9, 5 | cvgratnnlembern 11531 |
. . . . . . . . 9
โข (๐ โ (๐ดโ๐) < ((1 / ((1 / ๐ด) โ 1)) / ๐)) |
52 | 48, 50, 15, 51 | ltdiv1dd 9754 |
. . . . . . . 8
โข (๐ โ ((๐ดโ๐) / ๐ด) < (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด)) |
53 | 46, 52 | eqbrtrd 4026 |
. . . . . . 7
โข (๐ โ (๐ดโ(๐ โ 1)) < (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด)) |
54 | 49 | recnd 7986 |
. . . . . . . 8
โข (๐ โ (1 / ((1 / ๐ด) โ 1)) โ
โ) |
55 | 5 | nncnd 8933 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
56 | 5 | nnap0d 8965 |
. . . . . . . 8
โข (๐ โ ๐ # 0) |
57 | 54, 55, 44, 56, 10 | divdiv32apd 8773 |
. . . . . . 7
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐) / ๐ด) = (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
58 | 53, 57 | breqtrd 4030 |
. . . . . 6
โข (๐ โ (๐ดโ(๐ โ 1)) < (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
59 | 38, 42, 58 | ltled 8076 |
. . . . 5
โข (๐ โ (๐ดโ(๐ โ 1)) โค (((1 / ((1 / ๐ด) โ 1)) / ๐ด) / ๐)) |
60 | 38, 42, 29, 43, 59 | lemul2ad 8897 |
. . . 4
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โค ((absโ(๐นโ1)) ยท (((1 / ((1 /
๐ด) โ 1)) / ๐ด) / ๐))) |
61 | 29 | recnd 7986 |
. . . . . . 7
โข (๐ โ (absโ(๐นโ1)) โ
โ) |
62 | 23 | recnd 7986 |
. . . . . . 7
โข (๐ โ ((1 / ((1 / ๐ด) โ 1)) / ๐ด) โ
โ) |
63 | 61, 62 | mulcomd 7979 |
. . . . . 6
โข (๐ โ ((absโ(๐นโ1)) ยท ((1 / ((1 /
๐ด) โ 1)) / ๐ด)) = (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1)))) |
64 | 63 | oveq1d 5890 |
. . . . 5
โข (๐ โ (((absโ(๐นโ1)) ยท ((1 / ((1 /
๐ด) โ 1)) / ๐ด)) / ๐) = ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
65 | 61, 62, 55, 56 | divassapd 8783 |
. . . . 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 4032 |
. . 3
โข (๐ โ ((absโ(๐นโ1)) ยท (๐ดโ(๐ โ 1))) โค ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
68 | 7, 39, 31, 41, 67 | letrd 8081 |
. 2
โข (๐ โ (absโ(๐นโ๐)) โค ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐)) |
69 | 5 | nnrpd 9694 |
. . 3
โข (๐ โ ๐ โ
โ+) |
70 | 29 | ltp1d 8887 |
. . . 4
โข (๐ โ (absโ(๐นโ1)) <
((absโ(๐นโ1)) +
1)) |
71 | 29, 33, 22, 70 | ltmul2dd 9753 |
. . 3
โข (๐ โ (((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) < (((1 / ((1 /
๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) +
1))) |
72 | 30, 34, 69, 71 | ltdiv1dd 9754 |
. 2
โข (๐ โ ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท (absโ(๐นโ1))) / ๐) < ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐)) |
73 | 7, 31, 35, 68, 72 | lelttrd 8082 |
1
โข (๐ โ (absโ(๐นโ๐)) < ((((1 / ((1 / ๐ด) โ 1)) / ๐ด) ยท ((absโ(๐นโ1)) + 1)) / ๐)) |