Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
โข (๐ โ โ0
โ (0...(๐ โ 1))
โ Fin) |
2 | | elfznn0 13541 |
. . . . 5
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
3 | | 2re 12234 |
. . . . . . 7
โข 2 โ
โ |
4 | | 3nn 12239 |
. . . . . . . . 9
โข 3 โ
โ |
5 | | 2nn0 12437 |
. . . . . . . . . . 11
โข 2 โ
โ0 |
6 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ0) |
7 | | nn0mulcl 12456 |
. . . . . . . . . . 11
โข ((2
โ โ0 โง ๐ โ โ0) โ (2
ยท ๐) โ
โ0) |
8 | 5, 6, 7 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (2 ยท ๐) โ
โ0) |
9 | | nn0p1nn 12459 |
. . . . . . . . . 10
โข ((2
ยท ๐) โ
โ0 โ ((2 ยท ๐) + 1) โ โ) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((2 ยท ๐) + 1) โ โ) |
11 | | nnmulcl 12184 |
. . . . . . . . 9
โข ((3
โ โ โง ((2 ยท ๐) + 1) โ โ) โ (3 ยท ((2
ยท ๐) + 1)) โ
โ) |
12 | 4, 10, 11 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (3 ยท ((2 ยท ๐) + 1)) โ โ) |
13 | | 9nn 12258 |
. . . . . . . . 9
โข 9 โ
โ |
14 | | nnexpcl 13987 |
. . . . . . . . 9
โข ((9
โ โ โง ๐
โ โ0) โ (9โ๐) โ โ) |
15 | 13, 6, 14 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (9โ๐) โ โ) |
16 | 12, 15 | nnmulcld 12213 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) |
17 | | nndivre 12201 |
. . . . . . 7
โข ((2
โ โ โง ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) โ (2 / ((3 ยท
((2 ยท ๐) + 1))
ยท (9โ๐)))
โ โ) |
18 | 3, 16, 17 | sylancr 588 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ) |
19 | 18 | recnd 11190 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ) |
20 | 2, 19 | sylan2 594 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ (0...(๐ โ 1))) โ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))
โ โ) |
21 | 1, 20 | fsumcl 15625 |
. . 3
โข (๐ โ โ0
โ ฮฃ๐ โ
(0...(๐ โ 1))(2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))
โ โ) |
22 | | eqid 2737 |
. . . . 5
โข
(โคโฅโ๐) = (โคโฅโ๐) |
23 | | nn0z 12531 |
. . . . 5
โข (๐ โ โ0
โ ๐ โ
โค) |
24 | | eluznn0 12849 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
25 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
26 | 25 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
27 | 26 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = ๐ โ (3 ยท ((2 ยท ๐) + 1)) = (3 ยท ((2
ยท ๐) +
1))) |
28 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = ๐ โ (9โ๐) = (9โ๐)) |
29 | 27, 28 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐ โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) = ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) |
30 | 29 | oveq2d 7378 |
. . . . . . 7
โข (๐ = ๐ โ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = (2 / ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
31 | | eqid 2737 |
. . . . . . 7
โข (๐ โ โ0
โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) = (๐ โ โ0 โฆ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))) |
32 | | ovex 7395 |
. . . . . . 7
โข (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))
โ V |
33 | 30, 31, 32 | fvmpt 6953 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))โ๐) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
34 | 24, 33 | syl 17 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))โ๐) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
35 | 24, 18 | syldan 592 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) โ
โ) |
36 | 31 | log2cnv 26310 |
. . . . . . 7
โข seq0( + ,
(๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ (logโ2) |
37 | | seqex 13915 |
. . . . . . . 8
โข seq0( + ,
(๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ V |
38 | | fvex 6860 |
. . . . . . . 8
โข
(logโ2) โ V |
39 | 37, 38 | breldm 5869 |
. . . . . . 7
โข (seq0( +
, (๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ (logโ2) โ seq0( + ,
(๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ dom โ ) |
40 | 36, 39 | mp1i 13 |
. . . . . 6
โข (๐ โ โ0
โ seq0( + , (๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ dom โ ) |
41 | | nn0uz 12812 |
. . . . . . 7
โข
โ0 = (โคโฅโ0) |
42 | | id 22 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ0) |
43 | 33 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ โ โ0 โฆ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))โ๐) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
44 | 43, 19 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ โ โ0 โฆ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))โ๐) โ โ) |
45 | 41, 42, 44 | iserex 15548 |
. . . . . 6
โข (๐ โ โ0
โ (seq0( + , (๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ dom โ โ seq๐( + , (๐ โ โ0 โฆ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))))
โ dom โ )) |
46 | 40, 45 | mpbid 231 |
. . . . 5
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ dom โ ) |
47 | 22, 23, 34, 35, 46 | isumrecl 15657 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ
โ) |
48 | 47 | recnd 11190 |
. . 3
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ
โ) |
49 | | 0zd 12518 |
. . . . 5
โข (๐ โ โ0
โ 0 โ โค) |
50 | 36 | a1i 11 |
. . . . 5
โข (๐ โ โ0
โ seq0( + , (๐ โ
โ0 โฆ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) โ (logโ2)) |
51 | 41, 49, 43, 19, 50 | isumclim 15649 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
โ0 (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = (logโ2)) |
52 | 41, 22, 42, 43, 19, 40 | isumsplit 15732 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
โ0 (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = (ฮฃ๐ โ (0...(๐ โ 1))(2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) + ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) |
53 | 51, 52 | eqtr3d 2779 |
. . 3
โข (๐ โ โ0
โ (logโ2) = (ฮฃ๐ โ (0...(๐ โ 1))(2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) + ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) |
54 | 21, 48, 53 | mvrladdd 11575 |
. 2
โข (๐ โ โ0
โ ((logโ2) โ ฮฃ๐ โ (0...(๐ โ 1))(2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐)))) =
ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
55 | 3 | a1i 11 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 2 โ โ) |
56 | | 0le2 12262 |
. . . . . . 7
โข 0 โค
2 |
57 | 56 | a1i 11 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค 2) |
58 | 16 | nnred 12175 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) |
59 | 16 | nngt0d 12209 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 < ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) |
60 | | divge0 12031 |
. . . . . 6
โข (((2
โ โ โง 0 โค 2) โง (((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ โง 0 <
((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) โ 0 โค (2 / ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
61 | 55, 57, 58, 59, 60 | syl22anc 838 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
62 | 24, 61 | syldan 592 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 โค (2 / ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
63 | 22, 23, 34, 35, 46, 62 | isumge0 15658 |
. . 3
โข (๐ โ โ0
โ 0 โค ฮฃ๐
โ (โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
64 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((1 / 9)โ๐) = ((1 / 9)โ๐)) |
65 | 64 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = ๐ โ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 /
9)โ๐)) = ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐))) |
66 | | eqid 2737 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐))) = (๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐))) |
67 | | ovex 7395 |
. . . . . . . . 9
โข ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)) โ V |
68 | 65, 66, 67 | fvmpt 6953 |
. . . . . . . 8
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)))โ๐) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 /
9)โ๐))) |
69 | 68 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))โ๐) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 /
9)โ๐))) |
70 | | 9cn 12260 |
. . . . . . . . . . 11
โข 9 โ
โ |
71 | 70 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 9 โ โ) |
72 | 13 | nnne0i 12200 |
. . . . . . . . . . 11
โข 9 โ
0 |
73 | 72 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 9 โ 0) |
74 | | nn0z 12531 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โค) |
75 | 74 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โค) |
76 | 71, 73, 75 | exprecd 14066 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((1 / 9)โ๐) = (1 / (9โ๐))) |
77 | 76 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)) = ((2 / (3 ยท ((2
ยท ๐) + 1))) ยท
(1 / (9โ๐)))) |
78 | | nn0mulcl 12456 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ0 โง ๐ โ โ0) โ (2
ยท ๐) โ
โ0) |
79 | 5, 78 | mpan 689 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ0) |
80 | | nn0p1nn 12459 |
. . . . . . . . . . . . . 14
โข ((2
ยท ๐) โ
โ0 โ ((2 ยท ๐) + 1) โ โ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โ) |
82 | | nnmulcl 12184 |
. . . . . . . . . . . . 13
โข ((3
โ โ โง ((2 ยท ๐) + 1) โ โ) โ (3 ยท
((2 ยท ๐) + 1))
โ โ) |
83 | 4, 81, 82 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (3 ยท ((2 ยท ๐) + 1)) โ โ) |
84 | | nndivre 12201 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (3 ยท ((2 ยท ๐) + 1)) โ โ) โ (2 / (3
ยท ((2 ยท ๐) +
1))) โ โ) |
85 | 3, 83, 84 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (2 / (3 ยท ((2 ยท ๐) + 1))) โ โ) |
86 | 85 | recnd 11190 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (2 / (3 ยท ((2 ยท ๐) + 1))) โ โ) |
87 | 86 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (2 / (3 ยท ((2 ยท ๐) + 1))) โ โ) |
88 | 15 | nncnd 12176 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (9โ๐) โ โ) |
89 | 15 | nnne0d 12210 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (9โ๐) โ 0) |
90 | 87, 88, 89 | divrecd 11941 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((2 / (3 ยท ((2 ยท ๐) + 1))) / (9โ๐)) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท (1 /
(9โ๐)))) |
91 | | 2cnd 12238 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 2 โ โ) |
92 | 83 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (3 ยท ((2 ยท ๐) + 1)) โ โ) |
93 | 92 | nncnd 12176 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (3 ยท ((2 ยท ๐) + 1)) โ โ) |
94 | 92 | nnne0d 12210 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (3 ยท ((2 ยท ๐) + 1)) โ 0) |
95 | 91, 93, 88, 94, 89 | divdiv1d 11969 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((2 / (3 ยท ((2 ยท ๐) + 1))) / (9โ๐)) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
96 | 77, 90, 95 | 3eqtr2d 2783 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)) = (2 / ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
97 | 69, 96 | eqtrd 2777 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))โ๐) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
98 | 24, 97 | syldan 592 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))โ๐) = (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
99 | 92, 15 | nnmulcld 12213 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) |
100 | | nndivre 12201 |
. . . . . . 7
โข ((2
โ โ โง ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) โ (2 / ((3 ยท
((2 ยท ๐) + 1))
ยท (9โ๐)))
โ โ) |
101 | 3, 99, 100 | sylancr 588 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ) |
102 | 24, 101 | syldan 592 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) โ
โ) |
103 | 79 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ
โ0) |
104 | 103 | nn0red 12481 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ โ) |
105 | 5, 24, 7 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ
โ0) |
106 | 105 | nn0red 12481 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 ยท ๐) โ โ) |
107 | | 1red 11163 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 1 โ โ) |
108 | | eluzle 12783 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
109 | 108 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โค ๐) |
110 | | nn0re 12429 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
111 | 110 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
112 | 24 | nn0red 12481 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
113 | 3 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 2 โ โ) |
114 | | 2pos 12263 |
. . . . . . . . . . . 12
โข 0 <
2 |
115 | 114 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 < 2) |
116 | | lemul2 12015 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ โง (2 โ
โ โง 0 < 2)) โ (๐ โค ๐ โ (2 ยท ๐) โค (2 ยท ๐))) |
117 | 111, 112,
113, 115, 116 | syl112anc 1375 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (๐ โค ๐ โ (2 ยท ๐) โค (2 ยท ๐))) |
118 | 109, 117 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 ยท ๐) โค (2 ยท ๐)) |
119 | 104, 106,
107, 118 | leadd1dd 11776 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 ยท ๐) + 1) โค ((2 ยท ๐) + 1)) |
120 | 81 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 ยท ๐) + 1) โ โ) |
121 | 120 | nnred 12175 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 ยท ๐) + 1) โ โ) |
122 | 24, 10 | syldan 592 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 ยท ๐) + 1) โ โ) |
123 | 122 | nnred 12175 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 ยท ๐) + 1) โ โ) |
124 | | 3re 12240 |
. . . . . . . . . 10
โข 3 โ
โ |
125 | 124 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 3 โ โ) |
126 | | 3pos 12265 |
. . . . . . . . . 10
โข 0 <
3 |
127 | 126 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 < 3) |
128 | | lemul2 12015 |
. . . . . . . . 9
โข ((((2
ยท ๐) + 1) โ
โ โง ((2 ยท ๐) + 1) โ โ โง (3 โ โ
โง 0 < 3)) โ (((2 ยท ๐) + 1) โค ((2 ยท ๐) + 1) โ (3 ยท ((2 ยท ๐) + 1)) โค (3 ยท ((2
ยท ๐) +
1)))) |
129 | 121, 123,
125, 127, 128 | syl112anc 1375 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (((2 ยท ๐) + 1) โค ((2 ยท ๐) + 1) โ (3 ยท ((2 ยท ๐) + 1)) โค (3 ยท ((2
ยท ๐) +
1)))) |
130 | 119, 129 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (3 ยท ((2 ยท ๐) + 1)) โค (3 ยท ((2
ยท ๐) +
1))) |
131 | 83 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (3 ยท ((2 ยท ๐) + 1)) โ
โ) |
132 | 131 | nnred 12175 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (3 ยท ((2 ยท ๐) + 1)) โ
โ) |
133 | 24, 12 | syldan 592 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (3 ยท ((2 ยท ๐) + 1)) โ
โ) |
134 | 133 | nnred 12175 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (3 ยท ((2 ยท ๐) + 1)) โ
โ) |
135 | 13, 24, 14 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (9โ๐) โ โ) |
136 | 135 | nnred 12175 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (9โ๐) โ โ) |
137 | 135 | nngt0d 12209 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 < (9โ๐)) |
138 | | lemul1 12014 |
. . . . . . . 8
โข (((3
ยท ((2 ยท ๐) +
1)) โ โ โง (3 ยท ((2 ยท ๐) + 1)) โ โ โง ((9โ๐) โ โ โง 0 <
(9โ๐))) โ ((3
ยท ((2 ยท ๐) +
1)) โค (3 ยท ((2 ยท ๐) + 1)) โ ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐)) โค ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))) |
139 | 132, 134,
136, 137, 138 | syl112anc 1375 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((3 ยท ((2 ยท ๐) + 1)) โค (3 ยท ((2
ยท ๐) + 1)) โ
((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โค ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
140 | 130, 139 | mpbid 231 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โค ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐))) |
141 | 24, 99 | syldan 592 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ
โ) |
142 | 141 | nnred 12175 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ
โ) |
143 | 141 | nngt0d 12209 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 < ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) |
144 | 24, 58 | syldan 592 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ
โ) |
145 | 24, 59 | syldan 592 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ 0 < ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) |
146 | | lediv2 12052 |
. . . . . . 7
โข (((((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))
โ โ โง 0 < ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โง (((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ โง 0 <
((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โง (2 โ โ โง 0 < 2))
โ (((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โค ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ (2 / ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐))) โค (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))) |
147 | 142, 143,
144, 145, 113, 115, 146 | syl222anc 1387 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โค ((3 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)) โ (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))
โค (2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) |
148 | 140, 147 | mpbid 231 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) โค (2 / ((3
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))) |
149 | | 9re 12259 |
. . . . . . . . . . . 12
โข 9 โ
โ |
150 | 149, 72 | rereccli 11927 |
. . . . . . . . . . 11
โข (1 / 9)
โ โ |
151 | 150 | recni 11176 |
. . . . . . . . . 10
โข (1 / 9)
โ โ |
152 | 151 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ (1 / 9) โ โ) |
153 | | 0re 11164 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
154 | | 9pos 12273 |
. . . . . . . . . . . . . 14
โข 0 <
9 |
155 | 149, 154 | recgt0ii 12068 |
. . . . . . . . . . . . 13
โข 0 < (1
/ 9) |
156 | 153, 150,
155 | ltleii 11285 |
. . . . . . . . . . . 12
โข 0 โค (1
/ 9) |
157 | | absid 15188 |
. . . . . . . . . . . 12
โข (((1 / 9)
โ โ โง 0 โค (1 / 9)) โ (absโ(1 / 9)) = (1 /
9)) |
158 | 150, 156,
157 | mp2an 691 |
. . . . . . . . . . 11
โข
(absโ(1 / 9)) = (1 / 9) |
159 | | 1lt9 12366 |
. . . . . . . . . . . . 13
โข 1 <
9 |
160 | | recgt1i 12059 |
. . . . . . . . . . . . 13
โข ((9
โ โ โง 1 < 9) โ (0 < (1 / 9) โง (1 / 9) <
1)) |
161 | 149, 159,
160 | mp2an 691 |
. . . . . . . . . . . 12
โข (0 <
(1 / 9) โง (1 / 9) < 1) |
162 | 161 | simpri 487 |
. . . . . . . . . . 11
โข (1 / 9)
< 1 |
163 | 158, 162 | eqbrtri 5131 |
. . . . . . . . . 10
โข
(absโ(1 / 9)) < 1 |
164 | 163 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ (absโ(1 / 9)) < 1) |
165 | | eqid 2737 |
. . . . . . . . . . 11
โข (๐ โ โ0
โฆ ((1 / 9)โ๐)) =
(๐ โ
โ0 โฆ ((1 / 9)โ๐)) |
166 | | ovex 7395 |
. . . . . . . . . . 11
โข ((1 /
9)โ๐) โ
V |
167 | 64, 165, 166 | fvmpt 6953 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / 9)โ๐))โ๐) = ((1 / 9)โ๐)) |
168 | 24, 167 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ ((1 /
9)โ๐))โ๐) = ((1 / 9)โ๐)) |
169 | 152, 164,
42, 168 | geolim2 15763 |
. . . . . . . 8
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ ((1 / 9)โ๐)))
โ (((1 / 9)โ๐) /
(1 โ (1 / 9)))) |
170 | 70 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ 9 โ โ) |
171 | 72 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ 9 โ 0) |
172 | 170, 171,
23 | exprecd 14066 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((1 / 9)โ๐) =
(1 / (9โ๐))) |
173 | 70, 72 | dividi 11895 |
. . . . . . . . . . . . 13
โข (9 / 9) =
1 |
174 | 173 | oveq1i 7372 |
. . . . . . . . . . . 12
โข ((9 / 9)
โ (1 / 9)) = (1 โ (1 / 9)) |
175 | | ax-1cn 11116 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
176 | 70, 72 | pm3.2i 472 |
. . . . . . . . . . . . . 14
โข (9 โ
โ โง 9 โ 0) |
177 | | divsubdir 11856 |
. . . . . . . . . . . . . 14
โข ((9
โ โ โง 1 โ โ โง (9 โ โ โง 9 โ 0))
โ ((9 โ 1) / 9) = ((9 / 9) โ (1 / 9))) |
178 | 70, 175, 176, 177 | mp3an 1462 |
. . . . . . . . . . . . 13
โข ((9
โ 1) / 9) = ((9 / 9) โ (1 / 9)) |
179 | | 9m1e8 12294 |
. . . . . . . . . . . . . 14
โข (9
โ 1) = 8 |
180 | 179 | oveq1i 7372 |
. . . . . . . . . . . . 13
โข ((9
โ 1) / 9) = (8 / 9) |
181 | 178, 180 | eqtr3i 2767 |
. . . . . . . . . . . 12
โข ((9 / 9)
โ (1 / 9)) = (8 / 9) |
182 | 174, 181 | eqtr3i 2767 |
. . . . . . . . . . 11
โข (1
โ (1 / 9)) = (8 / 9) |
183 | 182 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (1 โ (1 / 9)) = (8 / 9)) |
184 | 172, 183 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((1 / 9)โ๐) /
(1 โ (1 / 9))) = ((1 / (9โ๐)) / (8 / 9))) |
185 | 175 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 1 โ โ) |
186 | | nnexpcl 13987 |
. . . . . . . . . . . 12
โข ((9
โ โ โง ๐
โ โ0) โ (9โ๐) โ โ) |
187 | 13, 186 | mpan 689 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (9โ๐) โ
โ) |
188 | 187 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (9โ๐) โ
โ) |
189 | | 8cn 12257 |
. . . . . . . . . . . 12
โข 8 โ
โ |
190 | 189, 70, 72 | divcli 11904 |
. . . . . . . . . . 11
โข (8 / 9)
โ โ |
191 | 190 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (8 / 9) โ โ) |
192 | 187 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (9โ๐) โ
0) |
193 | | 8nn 12255 |
. . . . . . . . . . . . 13
โข 8 โ
โ |
194 | 193 | nnne0i 12200 |
. . . . . . . . . . . 12
โข 8 โ
0 |
195 | 189, 70, 194, 72 | divne0i 11910 |
. . . . . . . . . . 11
โข (8 / 9)
โ 0 |
196 | 195 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (8 / 9) โ 0) |
197 | 185, 188,
191, 192, 196 | divdiv32d 11963 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((1 / (9โ๐)) /
(8 / 9)) = ((1 / (8 / 9)) / (9โ๐))) |
198 | | recdiv 11868 |
. . . . . . . . . . . 12
โข (((8
โ โ โง 8 โ 0) โง (9 โ โ โง 9 โ 0)) โ
(1 / (8 / 9)) = (9 / 8)) |
199 | 189, 194,
70, 72, 198 | mp4an 692 |
. . . . . . . . . . 11
โข (1 / (8 /
9)) = (9 / 8) |
200 | 199 | oveq1i 7372 |
. . . . . . . . . 10
โข ((1 / (8
/ 9)) / (9โ๐)) = ((9 /
8) / (9โ๐)) |
201 | 189 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ 8 โ โ) |
202 | 194 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ 8 โ 0) |
203 | 170, 201,
188, 202, 192 | divdiv1d 11969 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((9 / 8) / (9โ๐)) = (9 / (8 ยท (9โ๐)))) |
204 | 200, 203 | eqtrid 2789 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((1 / (8 / 9)) / (9โ๐)) = (9 / (8 ยท (9โ๐)))) |
205 | 184, 197,
204 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ โ0
โ (((1 / 9)โ๐) /
(1 โ (1 / 9))) = (9 / (8 ยท (9โ๐)))) |
206 | 169, 205 | breqtrd 5136 |
. . . . . . 7
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ ((1 / 9)โ๐)))
โ (9 / (8 ยท (9โ๐)))) |
207 | | expcl 13992 |
. . . . . . . . 9
โข (((1 / 9)
โ โ โง ๐
โ โ0) โ ((1 / 9)โ๐) โ โ) |
208 | 151, 24, 207 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((1 / 9)โ๐) โ โ) |
209 | 168, 208 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ ((1 /
9)โ๐))โ๐) โ
โ) |
210 | 24, 68 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))โ๐) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 /
9)โ๐))) |
211 | 168 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((2 / (3 ยท ((2 ยท
๐) + 1))) ยท ((๐ โ โ0
โฆ ((1 / 9)โ๐))โ๐)) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 /
9)โ๐))) |
212 | 210, 211 | eqtr4d 2780 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ((๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))โ๐) = ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((๐ โ โ0
โฆ ((1 / 9)โ๐))โ๐))) |
213 | 22, 23, 86, 206, 209, 212 | isermulc2 15549 |
. . . . . 6
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)))) โ ((2 / (3 ยท
((2 ยท ๐) + 1)))
ยท (9 / (8 ยท (9โ๐))))) |
214 | | seqex 13915 |
. . . . . . 7
โข seq๐( + , (๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))) โ V |
215 | | ovex 7395 |
. . . . . . 7
โข ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท (9 / (8 ยท (9โ๐)))) โ V |
216 | 214, 215 | breldm 5869 |
. . . . . 6
โข (seq๐( + , (๐ โ โ0 โฆ ((2 / (3
ยท ((2 ยท ๐) +
1))) ยท ((1 / 9)โ๐)))) โ ((2 / (3 ยท ((2 ยท
๐) + 1))) ยท (9 / (8
ยท (9โ๐))))
โ seq๐( + , (๐ โ โ0
โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)))) โ dom โ
) |
217 | 213, 216 | syl 17 |
. . . . 5
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)))) โ dom โ
) |
218 | 22, 23, 34, 35, 98, 102, 148, 46, 217 | isumle 15736 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โค ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)))) |
219 | 102 | recnd 11190 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ (2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐))) โ
โ) |
220 | | 3cn 12241 |
. . . . . . . . . . . 12
โข 3 โ
โ |
221 | | 4cn 12245 |
. . . . . . . . . . . 12
โข 4 โ
โ |
222 | | 2cn 12235 |
. . . . . . . . . . . 12
โข 2 โ
โ |
223 | | 4ne0 12268 |
. . . . . . . . . . . 12
โข 4 โ
0 |
224 | | 3ne0 12266 |
. . . . . . . . . . . 12
โข 3 โ
0 |
225 | | 2ne0 12264 |
. . . . . . . . . . . 12
โข 2 โ
0 |
226 | 220, 221,
222, 220, 223, 224, 225 | divdivdivi 11925 |
. . . . . . . . . . 11
โข ((3 / 4)
/ (2 / 3)) = ((3 ยท 3) / (4 ยท 2)) |
227 | | 3t3e9 12327 |
. . . . . . . . . . . 12
โข (3
ยท 3) = 9 |
228 | | 4t2e8 12328 |
. . . . . . . . . . . 12
โข (4
ยท 2) = 8 |
229 | 227, 228 | oveq12i 7374 |
. . . . . . . . . . 11
โข ((3
ยท 3) / (4 ยท 2)) = (9 / 8) |
230 | 226, 229 | eqtri 2765 |
. . . . . . . . . 10
โข ((3 / 4)
/ (2 / 3)) = (9 / 8) |
231 | 230 | oveq2i 7373 |
. . . . . . . . 9
โข ((2 / 3)
ยท ((3 / 4) / (2 / 3))) = ((2 / 3) ยท (9 / 8)) |
232 | 220, 221,
223 | divcli 11904 |
. . . . . . . . . 10
โข (3 / 4)
โ โ |
233 | 222, 220,
224 | divcli 11904 |
. . . . . . . . . 10
โข (2 / 3)
โ โ |
234 | 222, 220,
225, 224 | divne0i 11910 |
. . . . . . . . . 10
โข (2 / 3)
โ 0 |
235 | 232, 233,
234 | divcan2i 11905 |
. . . . . . . . 9
โข ((2 / 3)
ยท ((3 / 4) / (2 / 3))) = (3 / 4) |
236 | 231, 235 | eqtr3i 2767 |
. . . . . . . 8
โข ((2 / 3)
ยท (9 / 8)) = (3 / 4) |
237 | 236 | oveq1i 7372 |
. . . . . . 7
โข (((2 / 3)
ยท (9 / 8)) / (((2 ยท ๐) + 1) ยท (9โ๐))) = ((3 / 4) / (((2 ยท ๐) + 1) ยท (9โ๐))) |
238 | | 2cnd 12238 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 2 โ โ) |
239 | 220 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 3 โ โ) |
240 | 81 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โ) |
241 | 224 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 3 โ 0) |
242 | 81 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ 0) |
243 | 238, 239,
240, 241, 242 | divdiv1d 11969 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((2 / 3) / ((2 ยท ๐) + 1)) = (2 / (3 ยท ((2 ยท
๐) + 1)))) |
244 | 243, 203 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ โ0
โ (((2 / 3) / ((2 ยท ๐) + 1)) ยท ((9 / 8) / (9โ๐))) = ((2 / (3 ยท ((2
ยท ๐) + 1))) ยท
(9 / (8 ยท (9โ๐))))) |
245 | 233 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ (2 / 3) โ โ) |
246 | 70, 189, 194 | divcli 11904 |
. . . . . . . . . 10
โข (9 / 8)
โ โ |
247 | 246 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ (9 / 8) โ โ) |
248 | 245, 240,
247, 188, 242, 192 | divmuldivd 11979 |
. . . . . . . 8
โข (๐ โ โ0
โ (((2 / 3) / ((2 ยท ๐) + 1)) ยท ((9 / 8) / (9โ๐))) = (((2 / 3) ยท (9 /
8)) / (((2 ยท ๐) + 1)
ยท (9โ๐)))) |
249 | 244, 248 | eqtr3d 2779 |
. . . . . . 7
โข (๐ โ โ0
โ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท (9 / (8 ยท
(9โ๐)))) = (((2 / 3)
ยท (9 / 8)) / (((2 ยท ๐) + 1) ยท (9โ๐)))) |
250 | 221 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 4 โ โ) |
251 | 250, 240,
188 | mulassd 11185 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) = (4 ยท (((2 ยท ๐) + 1) ยท (9โ๐)))) |
252 | 251 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ โ0
โ (3 / ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = (3 / (4 ยท (((2 ยท ๐) + 1) ยท (9โ๐))))) |
253 | 81, 187 | nnmulcld 12213 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) ยท (9โ๐))
โ โ) |
254 | 253 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) ยท (9โ๐))
โ โ) |
255 | 223 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ0
โ 4 โ 0) |
256 | 253 | nnne0d 12210 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) ยท (9โ๐))
โ 0) |
257 | 239, 250,
254, 255, 256 | divdiv1d 11969 |
. . . . . . . 8
โข (๐ โ โ0
โ ((3 / 4) / (((2 ยท ๐) + 1) ยท (9โ๐))) = (3 / (4 ยท (((2 ยท ๐) + 1) ยท (9โ๐))))) |
258 | 252, 257 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ โ0
โ (3 / ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = ((3 / 4) / (((2 ยท ๐) + 1) ยท (9โ๐)))) |
259 | 237, 249,
258 | 3eqtr4a 2803 |
. . . . . 6
โข (๐ โ โ0
โ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท (9 / (8 ยท
(9โ๐)))) = (3 / ((4
ยท ((2 ยท ๐) +
1)) ยท (9โ๐)))) |
260 | 213, 259 | breqtrd 5136 |
. . . . 5
โข (๐ โ โ0
โ seq๐( + , (๐ โ โ0
โฆ ((2 / (3 ยท ((2 ยท ๐) + 1))) ยท ((1 / 9)โ๐)))) โ (3 / ((4 ยท
((2 ยท ๐) + 1))
ยท (9โ๐)))) |
261 | 22, 23, 98, 219, 260 | isumclim 15649 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) = (3 / ((4 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
262 | 218, 261 | breqtrd 5136 |
. . 3
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โค (3 / ((4 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))) |
263 | | 4nn 12243 |
. . . . . . 7
โข 4 โ
โ |
264 | | nnmulcl 12184 |
. . . . . . 7
โข ((4
โ โ โง ((2 ยท ๐) + 1) โ โ) โ (4 ยท
((2 ยท ๐) + 1))
โ โ) |
265 | 263, 81, 264 | sylancr 588 |
. . . . . 6
โข (๐ โ โ0
โ (4 ยท ((2 ยท ๐) + 1)) โ โ) |
266 | 265, 187 | nnmulcld 12213 |
. . . . 5
โข (๐ โ โ0
โ ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) |
267 | | nndivre 12201 |
. . . . 5
โข ((3
โ โ โง ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐)) โ โ) โ (3 / ((4 ยท
((2 ยท ๐) + 1))
ยท (9โ๐)))
โ โ) |
268 | 124, 266,
267 | sylancr 588 |
. . . 4
โข (๐ โ โ0
โ (3 / ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ) |
269 | | elicc2 13336 |
. . . 4
โข ((0
โ โ โง (3 / ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ) โ (ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ (0[,](3 / ((4
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))
โ (ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ โง 0 โค
ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โง ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โค (3 / ((4 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))))) |
270 | 153, 268,
269 | sylancr 588 |
. . 3
โข (๐ โ โ0
โ (ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ (0[,](3 / ((4
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))
โ (ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ โ โง 0 โค
ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โง ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โค (3 / ((4 ยท ((2
ยท ๐) + 1)) ยท
(9โ๐)))))) |
271 | 47, 63, 262, 270 | mpbir3and 1343 |
. 2
โข (๐ โ โ0
โ ฮฃ๐ โ
(โคโฅโ๐)(2 / ((3 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))) โ (0[,](3 / ((4
ยท ((2 ยท ๐) +
1)) ยท (9โ๐))))) |
272 | 54, 271 | eqeltrd 2838 |
1
โข (๐ โ โ0
โ ((logโ2) โ ฮฃ๐ โ (0...(๐ โ 1))(2 / ((3 ยท ((2 ยท
๐) + 1)) ยท
(9โ๐)))) โ
(0[,](3 / ((4 ยท ((2 ยท ๐) + 1)) ยท (9โ๐))))) |