Step | Hyp | Ref
| Expression |
1 | | geomulcvg.1 |
. . . . . . 7
โข ๐น = (๐ โ โ0 โฆ (๐ ยท (๐ดโ๐))) |
2 | | elnn0 12422 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
3 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ ๐ด = 0) |
4 | 3 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ (๐ดโ๐) = (0โ๐)) |
5 | | 0exp 14010 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(0โ๐) =
0) |
6 | 4, 5 | sylan9eq 2797 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ) โ (๐ดโ๐) = 0) |
7 | 6 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ) โ (๐ ยท (๐ดโ๐)) = (๐ ยท 0)) |
8 | | nncn 12168 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
9 | 8 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ) โ ๐ โ
โ) |
10 | 9 | mul01d 11361 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ) โ (๐ ยท 0) =
0) |
11 | 7, 10 | eqtrd 2777 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ) โ (๐ ยท (๐ดโ๐)) = 0) |
12 | | simpr 486 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ ๐ = 0) |
13 | 12 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ (๐ ยท (๐ดโ๐)) = (0 ยท (๐ดโ๐))) |
14 | | simplll 774 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ ๐ด โ โ) |
15 | | 0nn0 12435 |
. . . . . . . . . . . . . 14
โข 0 โ
โ0 |
16 | 12, 15 | eqeltrdi 2846 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ ๐ โ โ0) |
17 | 14, 16 | expcld 14058 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ (๐ดโ๐) โ โ) |
18 | 17 | mul02d 11360 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ (0 ยท (๐ดโ๐)) = 0) |
19 | 13, 18 | eqtrd 2777 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ = 0) โ (๐ ยท (๐ดโ๐)) = 0) |
20 | 11, 19 | jaodan 957 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง (๐ โ โ โจ ๐ = 0)) โ (๐ ยท (๐ดโ๐)) = 0) |
21 | 2, 20 | sylan2b 595 |
. . . . . . . 8
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โง ๐ โ โ0)
โ (๐ ยท (๐ดโ๐)) = 0) |
22 | 21 | mpteq2dva 5210 |
. . . . . . 7
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ (๐ โ โ0
โฆ (๐ ยท (๐ดโ๐))) = (๐ โ โ0 โฆ
0)) |
23 | 1, 22 | eqtrid 2789 |
. . . . . 6
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ ๐น = (๐ โ โ0 โฆ
0)) |
24 | | fconstmpt 5699 |
. . . . . . 7
โข
(โ0 ร {0}) = (๐ โ โ0 โฆ
0) |
25 | | nn0uz 12812 |
. . . . . . . 8
โข
โ0 = (โคโฅโ0) |
26 | 25 | xpeq1i 5664 |
. . . . . . 7
โข
(โ0 ร {0}) = ((โคโฅโ0)
ร {0}) |
27 | 24, 26 | eqtr3i 2767 |
. . . . . 6
โข (๐ โ โ0
โฆ 0) = ((โคโฅโ0) ร {0}) |
28 | 23, 27 | eqtrdi 2793 |
. . . . 5
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ ๐น =
((โคโฅโ0) ร {0})) |
29 | 28 | seqeq3d 13921 |
. . . 4
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ seq0( + ,
๐น) = seq0( + ,
((โคโฅโ0) ร {0}))) |
30 | | 0z 12517 |
. . . . 5
โข 0 โ
โค |
31 | | serclim0 15466 |
. . . . 5
โข (0 โ
โค โ seq0( + , ((โคโฅโ0) ร {0}))
โ 0) |
32 | 30, 31 | ax-mp 5 |
. . . 4
โข seq0( + ,
((โคโฅโ0) ร {0})) โ 0 |
33 | 29, 32 | eqbrtrdi 5149 |
. . 3
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ seq0( + ,
๐น) โ
0) |
34 | | seqex 13915 |
. . . 4
โข seq0( + ,
๐น) โ
V |
35 | | c0ex 11156 |
. . . 4
โข 0 โ
V |
36 | 34, 35 | breldm 5869 |
. . 3
โข (seq0( +
, ๐น) โ 0 โ seq0(
+ , ๐น) โ dom โ
) |
37 | 33, 36 | syl 17 |
. 2
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด = 0) โ seq0( + ,
๐น) โ dom โ
) |
38 | | 1red 11163 |
. . . 4
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ 1 โ
โ) |
39 | | abscl 15170 |
. . . . . . . . 9
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
40 | 39 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ๐ด) โ
โ) |
41 | | peano2re 11335 |
. . . . . . . 8
โข
((absโ๐ด)
โ โ โ ((absโ๐ด) + 1) โ โ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ ((absโ๐ด) + 1)
โ โ) |
43 | 42 | rehalfcld 12407 |
. . . . . 6
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (((absโ๐ด) + 1)
/ 2) โ โ) |
44 | 43 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
(((absโ๐ด) + 1) / 2)
โ โ) |
45 | | absrpcl 15180 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ
โ+) |
46 | 45 | adantlr 714 |
. . . . 5
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
(absโ๐ด) โ
โ+) |
47 | 44, 46 | rerpdivcld 12995 |
. . . 4
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
((((absโ๐ด) + 1) / 2)
/ (absโ๐ด)) โ
โ) |
48 | 40 | recnd 11190 |
. . . . . . . 8
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ๐ด) โ
โ) |
49 | 48 | mulid2d 11180 |
. . . . . . 7
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (1 ยท (absโ๐ด)) = (absโ๐ด)) |
50 | | simpr 486 |
. . . . . . . 8
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ๐ด) <
1) |
51 | | 1re 11162 |
. . . . . . . . 9
โข 1 โ
โ |
52 | | avglt1 12398 |
. . . . . . . . 9
โข
(((absโ๐ด)
โ โ โง 1 โ โ) โ ((absโ๐ด) < 1 โ (absโ๐ด) < (((absโ๐ด) + 1) / 2))) |
53 | 40, 51, 52 | sylancl 587 |
. . . . . . . 8
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ ((absโ๐ด) <
1 โ (absโ๐ด) <
(((absโ๐ด) + 1) /
2))) |
54 | 50, 53 | mpbid 231 |
. . . . . . 7
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ๐ด) <
(((absโ๐ด) + 1) /
2)) |
55 | 49, 54 | eqbrtrd 5132 |
. . . . . 6
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (1 ยท (absโ๐ด)) < (((absโ๐ด) + 1) / 2)) |
56 | 55 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ (1
ยท (absโ๐ด))
< (((absโ๐ด) + 1) /
2)) |
57 | 38, 44, 46 | ltmuldivd 13011 |
. . . . 5
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ ((1
ยท (absโ๐ด))
< (((absโ๐ด) + 1) /
2) โ 1 < ((((absโ๐ด) + 1) / 2) / (absโ๐ด)))) |
58 | 56, 57 | mpbid 231 |
. . . 4
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ 1 <
((((absโ๐ด) + 1) / 2)
/ (absโ๐ด))) |
59 | | expmulnbnd 14145 |
. . . 4
โข ((1
โ โ โง ((((absโ๐ด) + 1) / 2) / (absโ๐ด)) โ โ โง 1 <
((((absโ๐ด) + 1) / 2)
/ (absโ๐ด))) โ
โ๐ โ
โ0 โ๐ โ (โคโฅโ๐)(1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐)) |
60 | 38, 47, 58, 59 | syl3anc 1372 |
. . 3
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
โ๐ โ
โ0 โ๐ โ (โคโฅโ๐)(1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐)) |
61 | | eluznn0 12849 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
62 | | nn0cn 12430 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
63 | 62 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ๐ โ
โ) |
64 | 63 | mulid2d 11180 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (1 ยท ๐) =
๐) |
65 | 43 | recnd 11190 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (((absโ๐ด) + 1)
/ 2) โ โ) |
66 | 65 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (((absโ๐ด) + 1)
/ 2) โ โ) |
67 | 48 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (absโ๐ด) โ
โ) |
68 | 46 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (absโ๐ด) โ
โ+) |
69 | 68 | rpne0d 12969 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (absโ๐ด) โ
0) |
70 | | simpr 486 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ๐ โ
โ0) |
71 | 66, 67, 69, 70 | expdivd 14072 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (((((absโ๐ด) +
1) / 2) / (absโ๐ด))โ๐) = (((((absโ๐ด) + 1) / 2)โ๐) / ((absโ๐ด)โ๐))) |
72 | 64, 71 | breq12d 5123 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ((1 ยท ๐) <
(((((absโ๐ด) + 1) / 2)
/ (absโ๐ด))โ๐) โ ๐ < (((((absโ๐ด) + 1) / 2)โ๐) / ((absโ๐ด)โ๐)))) |
73 | | nn0re 12429 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
74 | 73 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ๐ โ
โ) |
75 | | reexpcl 13991 |
. . . . . . . . . . 11
โข
(((((absโ๐ด) +
1) / 2) โ โ โง ๐ โ โ0) โ
((((absโ๐ด) + 1) /
2)โ๐) โ
โ) |
76 | 44, 75 | sylan 581 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ((((absโ๐ด) +
1) / 2)โ๐) โ
โ) |
77 | 40 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
(absโ๐ด) โ
โ) |
78 | | reexpcl 13991 |
. . . . . . . . . . 11
โข
(((absโ๐ด)
โ โ โง ๐
โ โ0) โ ((absโ๐ด)โ๐) โ โ) |
79 | 77, 78 | sylan 581 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ((absโ๐ด)โ๐) โ โ) |
80 | 77 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (absโ๐ด) โ
โ) |
81 | | nn0z 12531 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โค) |
82 | 81 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ๐ โ
โค) |
83 | 68 | rpgt0d 12967 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ 0 < (absโ๐ด)) |
84 | | expgt0 14008 |
. . . . . . . . . . 11
โข
(((absโ๐ด)
โ โ โง ๐
โ โค โง 0 < (absโ๐ด)) โ 0 < ((absโ๐ด)โ๐)) |
85 | 80, 82, 83, 84 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ 0 < ((absโ๐ด)โ๐)) |
86 | | ltmuldiv 12035 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((((absโ๐ด) + 1) /
2)โ๐) โ โ
โง (((absโ๐ด)โ๐) โ โ โง 0 <
((absโ๐ด)โ๐))) โ ((๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โ ๐ < (((((absโ๐ด) + 1) / 2)โ๐) / ((absโ๐ด)โ๐)))) |
87 | 74, 76, 79, 85, 86 | syl112anc 1375 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ((๐ ยท
((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โ ๐ < (((((absโ๐ด) + 1) / 2)โ๐) / ((absโ๐ด)โ๐)))) |
88 | 72, 87 | bitr4d 282 |
. . . . . . . 8
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ ((1 ยท ๐) <
(((((absโ๐ด) + 1) / 2)
/ (absโ๐ด))โ๐) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) |
89 | 61, 88 | sylan2 594 |
. . . . . . 7
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง (๐ โ โ0
โง ๐ โ
(โคโฅโ๐))) โ ((1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) |
90 | 89 | anassrs 469 |
. . . . . 6
โข
(((((๐ด โ
โ โง (absโ๐ด)
< 1) โง ๐ด โ 0)
โง ๐ โ
โ0) โง ๐ โ (โคโฅโ๐)) โ ((1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) |
91 | 90 | ralbidva 3173 |
. . . . 5
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (โ๐ โ
(โคโฅโ๐)(1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐) โ โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) |
92 | | simprl 770 |
. . . . . . . 8
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โ ๐ โ โ0) |
93 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((((absโ๐ด) + 1) / 2)โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
94 | | eqid 2737 |
. . . . . . . . . . 11
โข (๐ โ โ0
โฆ ((((absโ๐ด) +
1) / 2)โ๐)) = (๐ โ โ0
โฆ ((((absโ๐ด) +
1) / 2)โ๐)) |
95 | | ovex 7395 |
. . . . . . . . . . 11
โข
((((absโ๐ด) +
1) / 2)โ๐) โ
V |
96 | 93, 94, 95 | fvmpt 6953 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
97 | 96 | adantl 483 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((((absโ๐ด) +
1) / 2)โ๐))โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
98 | 43 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ
(((absโ๐ด) + 1) / 2)
โ โ) |
99 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ ๐ โ
โ0) |
100 | 98, 99 | reexpcld 14075 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ
((((absโ๐ด) + 1) /
2)โ๐) โ
โ) |
101 | 97, 100 | eqeltrd 2838 |
. . . . . . . 8
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((((absโ๐ด) +
1) / 2)โ๐))โ๐) โ โ) |
102 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ = ๐) |
103 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
104 | 102, 103 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ ยท (๐ดโ๐)) = (๐ ยท (๐ดโ๐))) |
105 | | ovex 7395 |
. . . . . . . . . . 11
โข (๐ ยท (๐ดโ๐)) โ V |
106 | 104, 1, 105 | fvmpt 6953 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐นโ๐) = (๐ ยท (๐ดโ๐))) |
107 | 106 | adantl 483 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ (๐นโ๐) = (๐ ยท (๐ดโ๐))) |
108 | | nn0cn 12430 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
109 | 108 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ ๐ โ
โ) |
110 | | expcl 13992 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
111 | 110 | ad4ant14 751 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
112 | 109, 111 | mulcld 11182 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ (๐ ยท (๐ดโ๐)) โ โ) |
113 | 107, 112 | eqeltrd 2838 |
. . . . . . . 8
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ โ0) โ (๐นโ๐) โ โ) |
114 | | 0red 11165 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ 0 โ โ) |
115 | | absge0 15179 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ โ 0 โค
(absโ๐ด)) |
116 | 115 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ 0 โค (absโ๐ด)) |
117 | 114, 40, 43, 116, 54 | lelttrd 11320 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ 0 < (((absโ๐ด) + 1) / 2)) |
118 | 114, 43, 117 | ltled 11310 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ 0 โค (((absโ๐ด) + 1) / 2)) |
119 | 43, 118 | absidd 15314 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ(((absโ๐ด) + 1) / 2)) = (((absโ๐ด) + 1) / 2)) |
120 | | avglt2 12399 |
. . . . . . . . . . . . . 14
โข
(((absโ๐ด)
โ โ โง 1 โ โ) โ ((absโ๐ด) < 1 โ (((absโ๐ด) + 1) / 2) <
1)) |
121 | 40, 51, 120 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ ((absโ๐ด) <
1 โ (((absโ๐ด) +
1) / 2) < 1)) |
122 | 50, 121 | mpbid 231 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (((absโ๐ด) + 1)
/ 2) < 1) |
123 | 119, 122 | eqbrtrd 5132 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ (absโ(((absโ๐ด) + 1) / 2)) < 1) |
124 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((((absโ๐ด) + 1) / 2)โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
125 | | ovex 7395 |
. . . . . . . . . . . . 13
โข
((((absโ๐ด) +
1) / 2)โ๐) โ
V |
126 | 124, 94, 125 | fvmpt 6953 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
127 | 126 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ โ
โ0) โ ((๐ โ โ0 โฆ
((((absโ๐ด) + 1) /
2)โ๐))โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
128 | 65, 123, 127 | geolim 15762 |
. . . . . . . . . 10
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ seq0( + , (๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))) โ (1 / (1 โ
(((absโ๐ด) + 1) /
2)))) |
129 | | seqex 13915 |
. . . . . . . . . . 11
โข seq0( + ,
(๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))) โ V |
130 | | ovex 7395 |
. . . . . . . . . . 11
โข (1 / (1
โ (((absโ๐ด) +
1) / 2))) โ V |
131 | 129, 130 | breldm 5869 |
. . . . . . . . . 10
โข (seq0( +
, (๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))) โ (1 / (1 โ
(((absโ๐ด) + 1) / 2)))
โ seq0( + , (๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))) โ dom โ ) |
132 | 128, 131 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ seq0( + , (๐ โ
โ0 โฆ ((((absโ๐ด) + 1) / 2)โ๐))) โ dom โ ) |
133 | 132 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โ seq0( + , (๐ โ โ0 โฆ
((((absโ๐ด) + 1) /
2)โ๐))) โ dom
โ ) |
134 | | 1red 11163 |
. . . . . . . 8
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โ 1 โ โ) |
135 | | eluznn0 12849 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
136 | 92, 135 | sylan 581 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ0) |
137 | 136 | nn0red 12481 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
138 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ๐ด โ โ) |
139 | 138 | abscld 15328 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ๐ด) โ
โ) |
140 | 139, 136 | reexpcld 14075 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ด)โ๐) โ โ) |
141 | 137, 140 | remulcld 11192 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (๐ ยท ((absโ๐ด)โ๐)) โ โ) |
142 | 136, 100 | syldan 592 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ((((absโ๐ด) + 1) / 2)โ๐) โ
โ) |
143 | | simprr 772 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โ โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐)) |
144 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ๐)) |
145 | 102, 144 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐ ยท ((absโ๐ด)โ๐)) = (๐ ยท ((absโ๐ด)โ๐))) |
146 | 145, 93 | breq12d 5123 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) |
147 | 146 | rspccva 3583 |
. . . . . . . . . . . 12
โข
((โ๐ โ
(โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โง ๐ โ (โคโฅโ๐)) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐)) |
148 | 143, 147 | sylan 581 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐)) |
149 | 141, 142,
148 | ltled 11310 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (๐ ยท ((absโ๐ด)โ๐)) โค ((((absโ๐ด) + 1) / 2)โ๐)) |
150 | 136 | nn0cnd 12482 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
151 | 138, 136 | expcld 14058 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (๐ดโ๐) โ โ) |
152 | 150, 151 | absmuld 15346 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐ ยท (๐ดโ๐))) = ((absโ๐) ยท (absโ(๐ดโ๐)))) |
153 | 136 | nn0ge0d 12483 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ 0 โค ๐) |
154 | 137, 153 | absidd 15314 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ๐) = ๐) |
155 | 138, 136 | absexpd 15344 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
156 | 154, 155 | oveq12d 7380 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐) ยท (absโ(๐ดโ๐))) = (๐ ยท ((absโ๐ด)โ๐))) |
157 | 152, 156 | eqtrd 2777 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐ ยท (๐ดโ๐))) = (๐ ยท ((absโ๐ด)โ๐))) |
158 | 142 | recnd 11190 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ((((absโ๐ด) + 1) / 2)โ๐) โ
โ) |
159 | 158 | mulid2d 11180 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (1 ยท
((((absโ๐ด) + 1) /
2)โ๐)) =
((((absโ๐ด) + 1) /
2)โ๐)) |
160 | 149, 157,
159 | 3brtr4d 5142 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐ ยท (๐ดโ๐))) โค (1 ยท ((((absโ๐ด) + 1) / 2)โ๐))) |
161 | 136, 106 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) = (๐ ยท (๐ดโ๐))) |
162 | 161 | fveq2d 6851 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ๐)) = (absโ(๐ ยท (๐ดโ๐)))) |
163 | 136, 96 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ0 โฆ
((((absโ๐ด) + 1) /
2)โ๐))โ๐) = ((((absโ๐ด) + 1) / 2)โ๐)) |
164 | 163 | oveq2d 7378 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (1 ยท ((๐ โ โ0
โฆ ((((absโ๐ด) +
1) / 2)โ๐))โ๐)) = (1 ยท ((((absโ๐ด) + 1) / 2)โ๐))) |
165 | 160, 162,
164 | 3brtr4d 5142 |
. . . . . . . 8
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โง ๐ โ (โคโฅโ๐)) โ (absโ(๐นโ๐)) โค (1 ยท ((๐ โ โ0 โฆ
((((absโ๐ด) + 1) /
2)โ๐))โ๐))) |
166 | 25, 92, 101, 113, 133, 134, 165 | cvgcmpce 15710 |
. . . . . . 7
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
(๐ โ
โ0 โง โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐))) โ seq0( + , ๐น) โ dom โ ) |
167 | 166 | expr 458 |
. . . . . 6
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ โ
โ0) โ (โ๐ โ (โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โ seq0( + , ๐น) โ dom โ )) |
168 | 167 | adantlr 714 |
. . . . 5
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (โ๐ โ
(โคโฅโ๐)(๐ ยท ((absโ๐ด)โ๐)) < ((((absโ๐ด) + 1) / 2)โ๐) โ seq0( + , ๐น) โ dom โ )) |
169 | 91, 168 | sylbid 239 |
. . . 4
โข ((((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โง ๐ โ โ0)
โ (โ๐ โ
(โคโฅโ๐)(1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐) โ seq0( + , ๐น) โ dom โ )) |
170 | 169 | rexlimdva 3153 |
. . 3
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ
(โ๐ โ
โ0 โ๐ โ (โคโฅโ๐)(1 ยท ๐) < (((((absโ๐ด) + 1) / 2) / (absโ๐ด))โ๐) โ seq0( + , ๐น) โ dom โ )) |
171 | 60, 170 | mpd 15 |
. 2
โข (((๐ด โ โ โง
(absโ๐ด) < 1) โง
๐ด โ 0) โ seq0( + ,
๐น) โ dom โ
) |
172 | 37, 171 | pm2.61dane 3033 |
1
โข ((๐ด โ โ โง
(absโ๐ด) < 1)
โ seq0( + , ๐น) โ
dom โ ) |