Step | Hyp | Ref
| Expression |
1 | | cvgratnn.n |
. 2
โข (๐ โ ๐ โ (โคโฅโ๐)) |
2 | | 2fveq3 5521 |
. . . . 5
โข (๐ค = ๐ โ (absโ(๐นโ๐ค)) = (absโ(๐นโ๐))) |
3 | | oveq1 5882 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ค โ ๐) = (๐ โ ๐)) |
4 | 3 | oveq2d 5891 |
. . . . . 6
โข (๐ค = ๐ โ (๐ดโ(๐ค โ ๐)) = (๐ดโ(๐ โ ๐))) |
5 | 4 | oveq2d 5891 |
. . . . 5
โข (๐ค = ๐ โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) = ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) |
6 | 2, 5 | breq12d 4017 |
. . . 4
โข (๐ค = ๐ โ ((absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
7 | 6 | imbi2d 230 |
. . 3
โข (๐ค = ๐ โ ((๐ โ (absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐)))) โ (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))))) |
8 | | 2fveq3 5521 |
. . . . 5
โข (๐ค = ๐ โ (absโ(๐นโ๐ค)) = (absโ(๐นโ๐))) |
9 | | oveq1 5882 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ค โ ๐) = (๐ โ ๐)) |
10 | 9 | oveq2d 5891 |
. . . . . 6
โข (๐ค = ๐ โ (๐ดโ(๐ค โ ๐)) = (๐ดโ(๐ โ ๐))) |
11 | 10 | oveq2d 5891 |
. . . . 5
โข (๐ค = ๐ โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) = ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) |
12 | 8, 11 | breq12d 4017 |
. . . 4
โข (๐ค = ๐ โ ((absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
13 | 12 | imbi2d 230 |
. . 3
โข (๐ค = ๐ โ ((๐ โ (absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐)))) โ (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))))) |
14 | | 2fveq3 5521 |
. . . . 5
โข (๐ค = (๐ + 1) โ (absโ(๐นโ๐ค)) = (absโ(๐นโ(๐ + 1)))) |
15 | | oveq1 5882 |
. . . . . . 7
โข (๐ค = (๐ + 1) โ (๐ค โ ๐) = ((๐ + 1) โ ๐)) |
16 | 15 | oveq2d 5891 |
. . . . . 6
โข (๐ค = (๐ + 1) โ (๐ดโ(๐ค โ ๐)) = (๐ดโ((๐ + 1) โ ๐))) |
17 | 16 | oveq2d 5891 |
. . . . 5
โข (๐ค = (๐ + 1) โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) = ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))) |
18 | 14, 17 | breq12d 4017 |
. . . 4
โข (๐ค = (๐ + 1) โ ((absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
19 | 18 | imbi2d 230 |
. . 3
โข (๐ค = (๐ + 1) โ ((๐ โ (absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐)))) โ (๐ โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))))) |
20 | | 2fveq3 5521 |
. . . . 5
โข (๐ค = ๐ โ (absโ(๐นโ๐ค)) = (absโ(๐นโ๐))) |
21 | | oveq1 5882 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ค โ ๐) = (๐ โ ๐)) |
22 | 21 | oveq2d 5891 |
. . . . . 6
โข (๐ค = ๐ โ (๐ดโ(๐ค โ ๐)) = (๐ดโ(๐ โ ๐))) |
23 | 22 | oveq2d 5891 |
. . . . 5
โข (๐ค = ๐ โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) = ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) |
24 | 20, 23 | breq12d 4017 |
. . . 4
โข (๐ค = ๐ โ ((absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐))) โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
25 | 24 | imbi2d 230 |
. . 3
โข (๐ค = ๐ โ ((๐ โ (absโ(๐นโ๐ค)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ค โ ๐)))) โ (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))))) |
26 | | fveq2 5516 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
27 | 26 | eleq1d 2246 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
28 | | cvgratnn.6 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
29 | 28 | ralrimiva 2550 |
. . . . . . . 8
โข (๐ โ โ๐ โ โ (๐นโ๐) โ โ) |
30 | | cvgratnn.m |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
31 | 27, 29, 30 | rspcdva 2847 |
. . . . . . 7
โข (๐ โ (๐นโ๐) โ โ) |
32 | 31 | abscld 11190 |
. . . . . 6
โข (๐ โ (absโ(๐นโ๐)) โ โ) |
33 | 32 | leidd 8471 |
. . . . 5
โข (๐ โ (absโ(๐นโ๐)) โค (absโ(๐นโ๐))) |
34 | 30 | nncnd 8933 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
35 | 34 | subidd 8256 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐) = 0) |
36 | 35 | oveq2d 5891 |
. . . . . . . 8
โข (๐ โ (๐ดโ(๐ โ ๐)) = (๐ดโ0)) |
37 | | cvgratnn.3 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
38 | 37 | recnd 7986 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
39 | 38 | exp0d 10648 |
. . . . . . . 8
โข (๐ โ (๐ดโ0) = 1) |
40 | 36, 39 | eqtrd 2210 |
. . . . . . 7
โข (๐ โ (๐ดโ(๐ โ ๐)) = 1) |
41 | 40 | oveq2d 5891 |
. . . . . 6
โข (๐ โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) = ((absโ(๐นโ๐)) ยท 1)) |
42 | 32 | recnd 7986 |
. . . . . . 7
โข (๐ โ (absโ(๐นโ๐)) โ โ) |
43 | 42 | mulridd 7974 |
. . . . . 6
โข (๐ โ ((absโ(๐นโ๐)) ยท 1) = (absโ(๐นโ๐))) |
44 | 41, 43 | eqtrd 2210 |
. . . . 5
โข (๐ โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) = (absโ(๐นโ๐))) |
45 | 33, 44 | breqtrrd 4032 |
. . . 4
โข (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) |
46 | 45 | a1i 9 |
. . 3
โข (๐ โ โค โ (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
47 | | eluznn 9600 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
48 | 30, 47 | sylan 283 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
49 | 48, 28 | syldan 282 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
50 | 49 | abscld 11190 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ๐)) โ โ) |
51 | 32 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ๐)) โ โ) |
52 | 37 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ด โ โ) |
53 | | uznn0sub 9559 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ โ ๐) โ
โ0) |
54 | 53 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ โ ๐) โ
โ0) |
55 | 52, 54 | reexpcld 10671 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ดโ(๐ โ ๐)) โ โ) |
56 | 51, 55 | remulcld 7988 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ โ) |
57 | | 0red 7958 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ 0 โ
โ) |
58 | | cvgratnn.gt0 |
. . . . . . . . . 10
โข (๐ โ 0 < ๐ด) |
59 | 58 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ 0 < ๐ด) |
60 | 57, 52, 59 | ltled 8076 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ 0 โค ๐ด) |
61 | | lemul2a 8816 |
. . . . . . . . 9
โข
((((absโ(๐นโ๐)) โ โ โง ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ โ โง (๐ด โ โ โง 0 โค ๐ด)) โง (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) โ (๐ด ยท (absโ(๐นโ๐))) โค (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
62 | 61 | ex 115 |
. . . . . . . 8
โข
(((absโ(๐นโ๐)) โ โ โง ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ โ โง (๐ด โ โ โง 0 โค ๐ด)) โ ((absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ (๐ด ยท (absโ(๐นโ๐))) โค (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))))) |
63 | 50, 56, 52, 60, 62 | syl112anc 1242 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ (๐ด ยท (absโ(๐นโ๐))) โค (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))))) |
64 | 38 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ด โ โ) |
65 | 42 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ๐)) โ โ) |
66 | 55 | recnd 7986 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ดโ(๐ โ ๐)) โ โ) |
67 | 64, 65, 66 | mul12d 8109 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) = ((absโ(๐นโ๐)) ยท (๐ด ยท (๐ดโ(๐ โ ๐))))) |
68 | 64, 54 | expp1d 10655 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ดโ((๐ โ ๐) + 1)) = ((๐ดโ(๐ โ ๐)) ยท ๐ด)) |
69 | 48 | nncnd 8933 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
70 | | 1cnd 7973 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ 1 โ
โ) |
71 | | eluzel2 9533 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
72 | 71 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
73 | 72 | zcnd 9376 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
74 | 69, 70, 73 | addsubd 8289 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐ + 1) โ ๐) = ((๐ โ ๐) + 1)) |
75 | 74 | oveq2d 5891 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ดโ((๐ + 1) โ ๐)) = (๐ดโ((๐ โ ๐) + 1))) |
76 | 64, 66 | mulcomd 7979 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ด ยท (๐ดโ(๐ โ ๐))) = ((๐ดโ(๐ โ ๐)) ยท ๐ด)) |
77 | 68, 75, 76 | 3eqtr4rd 2221 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ด ยท (๐ดโ(๐ โ ๐))) = (๐ดโ((๐ + 1) โ ๐))) |
78 | 77 | oveq2d 5891 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) ยท (๐ด ยท (๐ดโ(๐ โ ๐)))) = ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))) |
79 | 67, 78 | eqtrd 2210 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) = ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))) |
80 | 79 | breq2d 4016 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐ด ยท (absโ(๐นโ๐))) โค (๐ด ยท ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) โ (๐ด ยท (absโ(๐นโ๐))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
81 | 63, 80 | sylibd 149 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ (๐ด ยท (absโ(๐นโ๐))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
82 | | cvgratnn.7 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
83 | 48, 82 | syldan 282 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) |
84 | | fveq2 5516 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐นโ๐) = (๐นโ(๐ + 1))) |
85 | 84 | eleq1d 2246 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ ((๐นโ๐) โ โ โ (๐นโ(๐ + 1)) โ โ)) |
86 | | fveq2 5516 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
87 | 86 | eleq1d 2246 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐นโ๐) โ โ โ (๐นโ๐) โ โ)) |
88 | 87 | cbvralv 2704 |
. . . . . . . . . . . 12
โข
(โ๐ โ
โ (๐นโ๐) โ โ โ
โ๐ โ โ
(๐นโ๐) โ โ) |
89 | 29, 88 | sylib 122 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ โ (๐นโ๐) โ โ) |
90 | 89 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ โ (๐นโ๐) โ โ) |
91 | 48 | peano2nnd 8934 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ + 1) โ โ) |
92 | 85, 90, 91 | rspcdva 2847 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ(๐ + 1)) โ โ) |
93 | 92 | abscld 11190 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ(๐ + 1))) โ โ) |
94 | 52, 50 | remulcld 7988 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ด ยท (absโ(๐นโ๐))) โ โ) |
95 | | peano2uz 9583 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
96 | 95 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ + 1) โ
(โคโฅโ๐)) |
97 | | uznn0sub 9559 |
. . . . . . . . . . 11
โข ((๐ + 1) โ
(โคโฅโ๐) โ ((๐ + 1) โ ๐) โ
โ0) |
98 | 96, 97 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐ + 1) โ ๐) โ
โ0) |
99 | 52, 98 | reexpcld 10671 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐ดโ((๐ + 1) โ ๐)) โ โ) |
100 | 51, 99 | remulcld 7988 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))) โ โ) |
101 | | letr 8040 |
. . . . . . . 8
โข
(((absโ(๐นโ(๐ + 1))) โ โ โง (๐ด ยท (absโ(๐นโ๐))) โ โ โง ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))) โ โ) โ
(((absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐))) โง (๐ด ยท (absโ(๐นโ๐))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
102 | 93, 94, 100, 101 | syl3anc 1238 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (((absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐))) โง (๐ด ยท (absโ(๐นโ๐))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
103 | 83, 102 | mpand 429 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐ด ยท (absโ(๐นโ๐))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
104 | 81, 103 | syld 45 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐))))) |
105 | 104 | expcom 116 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (๐ โ ((absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))) โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))))) |
106 | 105 | a2d 26 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ((๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) โ (๐ โ (absโ(๐นโ(๐ + 1))) โค ((absโ(๐นโ๐)) ยท (๐ดโ((๐ + 1) โ ๐)))))) |
107 | 7, 13, 19, 25, 46, 106 | uzind4 9588 |
. 2
โข (๐ โ
(โคโฅโ๐) โ (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐))))) |
108 | 1, 107 | mpcom 36 |
1
โข (๐ โ (absโ(๐นโ๐)) โค ((absโ(๐นโ๐)) ยท (๐ดโ(๐ โ ๐)))) |