Step | Hyp | Ref
| Expression |
1 | | rpnnen2.3 |
. . . 4
โข (๐ โ ๐ต โ โ) |
2 | | rpnnen2.2 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
3 | | rpnnen2.4 |
. . . . 5
โข (๐ โ ๐ โ (๐ด โ ๐ต)) |
4 | | eldifi 4091 |
. . . . . 6
โข (๐ โ (๐ด โ ๐ต) โ ๐ โ ๐ด) |
5 | | ssel2 3944 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ ๐ด) โ ๐ โ โ) |
6 | 4, 5 | sylan2 594 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (๐ด โ ๐ต)) โ ๐ โ โ) |
7 | 2, 3, 6 | syl2anc 585 |
. . . 4
โข (๐ โ ๐ โ โ) |
8 | | rpnnen2.1 |
. . . . 5
โข ๐น = (๐ฅ โ ๐ซ โ โฆ (๐ โ โ โฆ if(๐ โ ๐ฅ, ((1 / 3)โ๐), 0))) |
9 | 8 | rpnnen2lem6 16108 |
. . . 4
โข ((๐ต โ โ โง ๐ โ โ) โ
ฮฃ๐ โ
(โคโฅโ๐)((๐นโ๐ต)โ๐) โ โ) |
10 | 1, 7, 9 | syl2anc 585 |
. . 3
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) โ โ) |
11 | | 3nn 12239 |
. . . . . 6
โข 3 โ
โ |
12 | | nnrecre 12202 |
. . . . . 6
โข (3 โ
โ โ (1 / 3) โ โ) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
โข (1 / 3)
โ โ |
14 | 7 | nnnn0d 12480 |
. . . . 5
โข (๐ โ ๐ โ โ0) |
15 | | reexpcl 13991 |
. . . . 5
โข (((1 / 3)
โ โ โง ๐
โ โ0) โ ((1 / 3)โ๐) โ โ) |
16 | 13, 14, 15 | sylancr 588 |
. . . 4
โข (๐ โ ((1 / 3)โ๐) โ
โ) |
17 | 8 | rpnnen2lem6 16108 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ
ฮฃ๐ โ
(โคโฅโ๐)((๐นโ๐ด)โ๐) โ โ) |
18 | 2, 7, 17 | syl2anc 585 |
. . . 4
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐) โ โ) |
19 | | nnrp 12933 |
. . . . . . . . 9
โข (3 โ
โ โ 3 โ โ+) |
20 | | rpreccl 12948 |
. . . . . . . . 9
โข (3 โ
โ+ โ (1 / 3) โ โ+) |
21 | 11, 19, 20 | mp2b 10 |
. . . . . . . 8
โข (1 / 3)
โ โ+ |
22 | 7 | nnzd 12533 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
23 | | rpexpcl 13993 |
. . . . . . . 8
โข (((1 / 3)
โ โ+ โง ๐ โ โค) โ ((1 / 3)โ๐) โ
โ+) |
24 | 21, 22, 23 | sylancr 588 |
. . . . . . 7
โข (๐ โ ((1 / 3)โ๐) โ
โ+) |
25 | 24 | rpred 12964 |
. . . . . 6
โข (๐ โ ((1 / 3)โ๐) โ
โ) |
26 | 25 | rehalfcld 12407 |
. . . . 5
โข (๐ โ (((1 / 3)โ๐) / 2) โ
โ) |
27 | 3 | snssd 4774 |
. . . . . . . . 9
โข (๐ โ {๐} โ (๐ด โ ๐ต)) |
28 | 2 | ssdifd 4105 |
. . . . . . . . 9
โข (๐ โ (๐ด โ ๐ต) โ (โ โ ๐ต)) |
29 | 27, 28 | sstrd 3959 |
. . . . . . . 8
โข (๐ โ {๐} โ (โ โ ๐ต)) |
30 | 7 | snssd 4774 |
. . . . . . . . 9
โข (๐ โ {๐} โ โ) |
31 | | ssconb 4102 |
. . . . . . . . 9
โข ((๐ต โ โ โง {๐} โ โ) โ (๐ต โ (โ โ {๐}) โ {๐} โ (โ โ ๐ต))) |
32 | 1, 30, 31 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (๐ต โ (โ โ {๐}) โ {๐} โ (โ โ ๐ต))) |
33 | 29, 32 | mpbird 257 |
. . . . . . 7
โข (๐ โ ๐ต โ (โ โ {๐})) |
34 | | difssd 4097 |
. . . . . . 7
โข (๐ โ (โ โ {๐}) โ
โ) |
35 | 8 | rpnnen2lem7 16109 |
. . . . . . 7
โข ((๐ต โ (โ โ {๐}) โง (โ โ {๐}) โ โ โง ๐ โ โ) โ
ฮฃ๐ โ
(โคโฅโ๐)((๐นโ๐ต)โ๐) โค ฮฃ๐ โ (โคโฅโ๐)((๐นโ(โ โ {๐}))โ๐)) |
36 | 33, 34, 7, 35 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) โค ฮฃ๐ โ (โคโฅโ๐)((๐นโ(โ โ {๐}))โ๐)) |
37 | 8 | rpnnen2lem9 16111 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ
(โคโฅโ๐)((๐นโ(โ โ {๐}))โ๐) = (0 + (((1 / 3)โ(๐ + 1)) / (1 โ (1 /
3))))) |
38 | 7, 37 | syl 17 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ(โ โ {๐}))โ๐) = (0 + (((1 / 3)โ(๐ + 1)) / (1 โ (1 /
3))))) |
39 | 13 | recni 11176 |
. . . . . . . . . . . 12
โข (1 / 3)
โ โ |
40 | | expp1 13981 |
. . . . . . . . . . . 12
โข (((1 / 3)
โ โ โง ๐
โ โ0) โ ((1 / 3)โ(๐ + 1)) = (((1 / 3)โ๐) ยท (1 / 3))) |
41 | 39, 14, 40 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ ((1 / 3)โ(๐ + 1)) = (((1 / 3)โ๐) ยท (1 /
3))) |
42 | 25 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ โ ((1 / 3)โ๐) โ
โ) |
43 | | 3cn 12241 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
44 | | 3ne0 12266 |
. . . . . . . . . . . . 13
โข 3 โ
0 |
45 | | divrec 11836 |
. . . . . . . . . . . . 13
โข ((((1 /
3)โ๐) โ โ
โง 3 โ โ โง 3 โ 0) โ (((1 / 3)โ๐) / 3) = (((1 / 3)โ๐) ยท (1 / 3))) |
46 | 43, 44, 45 | mp3an23 1454 |
. . . . . . . . . . . 12
โข (((1 /
3)โ๐) โ โ
โ (((1 / 3)โ๐) /
3) = (((1 / 3)โ๐)
ยท (1 / 3))) |
47 | 42, 46 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((1 / 3)โ๐) / 3) = (((1 / 3)โ๐) ยท (1 /
3))) |
48 | 41, 47 | eqtr4d 2780 |
. . . . . . . . . 10
โข (๐ โ ((1 / 3)โ(๐ + 1)) = (((1 / 3)โ๐) / 3)) |
49 | 48 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ (((1 / 3)โ(๐ + 1)) / (1 โ (1 / 3))) =
((((1 / 3)โ๐) / 3) /
(1 โ (1 / 3)))) |
50 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
51 | 43, 44 | pm3.2i 472 |
. . . . . . . . . . . . 13
โข (3 โ
โ โง 3 โ 0) |
52 | | divsubdir 11856 |
. . . . . . . . . . . . 13
โข ((3
โ โ โง 1 โ โ โง (3 โ โ โง 3 โ 0))
โ ((3 โ 1) / 3) = ((3 / 3) โ (1 / 3))) |
53 | 43, 50, 51, 52 | mp3an 1462 |
. . . . . . . . . . . 12
โข ((3
โ 1) / 3) = ((3 / 3) โ (1 / 3)) |
54 | | 3m1e2 12288 |
. . . . . . . . . . . . 13
โข (3
โ 1) = 2 |
55 | 54 | oveq1i 7372 |
. . . . . . . . . . . 12
โข ((3
โ 1) / 3) = (2 / 3) |
56 | 43, 44 | dividi 11895 |
. . . . . . . . . . . . 13
โข (3 / 3) =
1 |
57 | 56 | oveq1i 7372 |
. . . . . . . . . . . 12
โข ((3 / 3)
โ (1 / 3)) = (1 โ (1 / 3)) |
58 | 53, 55, 57 | 3eqtr3ri 2774 |
. . . . . . . . . . 11
โข (1
โ (1 / 3)) = (2 / 3) |
59 | 58 | oveq2i 7373 |
. . . . . . . . . 10
โข ((((1 /
3)โ๐) / 3) / (1
โ (1 / 3))) = ((((1 / 3)โ๐) / 3) / (2 / 3)) |
60 | | 2cnne0 12370 |
. . . . . . . . . . . 12
โข (2 โ
โ โง 2 โ 0) |
61 | | divcan7 11871 |
. . . . . . . . . . . 12
โข ((((1 /
3)โ๐) โ โ
โง (2 โ โ โง 2 โ 0) โง (3 โ โ โง 3 โ
0)) โ ((((1 / 3)โ๐) / 3) / (2 / 3)) = (((1 / 3)โ๐) / 2)) |
62 | 60, 51, 61 | mp3an23 1454 |
. . . . . . . . . . 11
โข (((1 /
3)โ๐) โ โ
โ ((((1 / 3)โ๐) /
3) / (2 / 3)) = (((1 / 3)โ๐) / 2)) |
63 | 42, 62 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((((1 / 3)โ๐) / 3) / (2 / 3)) = (((1 /
3)โ๐) /
2)) |
64 | 59, 63 | eqtrid 2789 |
. . . . . . . . 9
โข (๐ โ ((((1 / 3)โ๐) / 3) / (1 โ (1 / 3))) =
(((1 / 3)โ๐) /
2)) |
65 | 49, 64 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((1 / 3)โ(๐ + 1)) / (1 โ (1 / 3))) =
(((1 / 3)โ๐) /
2)) |
66 | 65 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (0 + (((1 / 3)โ(๐ + 1)) / (1 โ (1 / 3)))) =
(0 + (((1 / 3)โ๐) /
2))) |
67 | 26 | recnd 11190 |
. . . . . . . 8
โข (๐ โ (((1 / 3)โ๐) / 2) โ
โ) |
68 | 67 | addid2d 11363 |
. . . . . . 7
โข (๐ โ (0 + (((1 / 3)โ๐) / 2)) = (((1 / 3)โ๐) / 2)) |
69 | 38, 66, 68 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ(โ โ {๐}))โ๐) = (((1 / 3)โ๐) / 2)) |
70 | 36, 69 | breqtrd 5136 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) โค (((1 / 3)โ๐) / 2)) |
71 | | rphalflt 12951 |
. . . . . 6
โข (((1 /
3)โ๐) โ
โ+ โ (((1 / 3)โ๐) / 2) < ((1 / 3)โ๐)) |
72 | 24, 71 | syl 17 |
. . . . 5
โข (๐ โ (((1 / 3)โ๐) / 2) < ((1 / 3)โ๐)) |
73 | 10, 26, 25, 70, 72 | lelttrd 11320 |
. . . 4
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) < ((1 / 3)โ๐)) |
74 | | eluznn 12850 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
75 | 7, 74 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
76 | 8 | rpnnen2lem1 16103 |
. . . . . . . 8
โข (({๐} โ โ โง ๐ โ โ) โ ((๐นโ{๐})โ๐) = if(๐ โ {๐}, ((1 / 3)โ๐), 0)) |
77 | 30, 75, 76 | syl2an2r 684 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ((๐นโ{๐})โ๐) = if(๐ โ {๐}, ((1 / 3)โ๐), 0)) |
78 | 77 | sumeq2dv 15595 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ{๐})โ๐) = ฮฃ๐ โ (โคโฅโ๐)if(๐ โ {๐}, ((1 / 3)โ๐), 0)) |
79 | | uzid 12785 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
80 | 22, 79 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ (โคโฅโ๐)) |
81 | 80 | snssd 4774 |
. . . . . . 7
โข (๐ โ {๐} โ (โคโฅโ๐)) |
82 | | vex 3452 |
. . . . . . . . 9
โข ๐ โ V |
83 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((1 / 3)โ๐) = ((1 / 3)โ๐)) |
84 | 83 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ = ๐ โ (((1 / 3)โ๐) โ โ โ ((1 / 3)โ๐) โ
โ)) |
85 | 82, 84 | ralsn 4647 |
. . . . . . . 8
โข
(โ๐ โ
{๐} ((1 / 3)โ๐) โ โ โ ((1 /
3)โ๐) โ
โ) |
86 | 42, 85 | sylibr 233 |
. . . . . . 7
โข (๐ โ โ๐ โ {๐} ((1 / 3)โ๐) โ โ) |
87 | | ssidd 3972 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐) โ (โคโฅโ๐)) |
88 | 87 | orcd 872 |
. . . . . . 7
โข (๐ โ
((โคโฅโ๐) โ (โคโฅโ๐) โจ
(โคโฅโ๐) โ Fin)) |
89 | | sumss2 15618 |
. . . . . . 7
โข ((({๐} โ
(โคโฅโ๐) โง โ๐ โ {๐} ((1 / 3)โ๐) โ โ) โง
((โคโฅโ๐) โ (โคโฅโ๐) โจ
(โคโฅโ๐) โ Fin)) โ ฮฃ๐ โ {๐} ((1 / 3)โ๐) = ฮฃ๐ โ (โคโฅโ๐)if(๐ โ {๐}, ((1 / 3)โ๐), 0)) |
90 | 81, 86, 88, 89 | syl21anc 837 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ {๐} ((1 / 3)โ๐) = ฮฃ๐ โ (โคโฅโ๐)if(๐ โ {๐}, ((1 / 3)โ๐), 0)) |
91 | 83 | sumsn 15638 |
. . . . . . 7
โข ((๐ โ โ โง ((1 /
3)โ๐) โ โ)
โ ฮฃ๐ โ
{๐} ((1 / 3)โ๐) = ((1 / 3)โ๐)) |
92 | 7, 42, 91 | syl2anc 585 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ {๐} ((1 / 3)โ๐) = ((1 / 3)โ๐)) |
93 | 78, 90, 92 | 3eqtr2d 2783 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ{๐})โ๐) = ((1 / 3)โ๐)) |
94 | 3, 4 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ด) |
95 | 94 | snssd 4774 |
. . . . . 6
โข (๐ โ {๐} โ ๐ด) |
96 | 8 | rpnnen2lem7 16109 |
. . . . . 6
โข (({๐} โ ๐ด โง ๐ด โ โ โง ๐ โ โ) โ ฮฃ๐ โ
(โคโฅโ๐)((๐นโ{๐})โ๐) โค ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐)) |
97 | 95, 2, 7, 96 | syl3anc 1372 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ{๐})โ๐) โค ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐)) |
98 | 93, 97 | eqbrtrrd 5134 |
. . . 4
โข (๐ โ ((1 / 3)โ๐) โค ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐)) |
99 | 10, 16, 18, 73, 98 | ltletrd 11322 |
. . 3
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) < ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐)) |
100 | 10, 99 | gtned 11297 |
. 2
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐) โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐)) |
101 | | rpnnen2.5 |
. . . . 5
โข (๐ โ โ๐ โ โ (๐ < ๐ โ (๐ โ ๐ด โ ๐ โ ๐ต))) |
102 | | rpnnen2.6 |
. . . . 5
โข (๐ โ ฮฃ๐ โ โ ((๐นโ๐ด)โ๐) = ฮฃ๐ โ โ ((๐นโ๐ต)โ๐)) |
103 | 8, 2, 1, 3, 101, 102 | rpnnen2lem10 16112 |
. . . 4
โข ((๐ โง ๐) โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐) = ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐)) |
104 | 103 | ex 414 |
. . 3
โข (๐ โ (๐ โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐) = ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐))) |
105 | 104 | necon3ad 2957 |
. 2
โข (๐ โ (ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ด)โ๐) โ ฮฃ๐ โ (โคโฅโ๐)((๐นโ๐ต)โ๐) โ ยฌ ๐)) |
106 | 100, 105 | mpd 15 |
1
โข (๐ โ ยฌ ๐) |