Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.2 |
. . . . . . . . . 10
โข (๐ โ ๐น:โโถ(0[,)+โ)) |
2 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
3 | | ffvelcdm 7036 |
. . . . . . . . . 10
โข ((๐น:โโถ(0[,)+โ)
โง ๐ฆ โ โ)
โ (๐นโ๐ฆ) โ
(0[,)+โ)) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ (๐นโ๐ฆ) โ (0[,)+โ)) |
5 | | elrege0 13380 |
. . . . . . . . 9
โข ((๐นโ๐ฆ) โ (0[,)+โ) โ ((๐นโ๐ฆ) โ โ โง 0 โค (๐นโ๐ฆ))) |
6 | 4, 5 | sylib 217 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ ((๐นโ๐ฆ) โ โ โง 0 โค (๐นโ๐ฆ))) |
7 | 6 | simpld 496 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ (๐นโ๐ฆ) โ โ) |
8 | | 2nn 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
9 | | nnnn0 12428 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
10 | | nnexpcl 13989 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ โ โ
(2โ๐) โ
โ) |
12 | 11 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ (2โ๐) โ
โ) |
13 | 12 | nnred 12176 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ (2โ๐) โ
โ) |
14 | 7, 13 | remulcld 11193 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ ((๐นโ๐ฆ) ยท (2โ๐)) โ โ) |
15 | | reflcl 13710 |
. . . . . 6
โข (((๐นโ๐ฆ) ยท (2โ๐)) โ โ โ
(โโ((๐นโ๐ฆ) ยท (2โ๐))) โ โ) |
16 | 14, 15 | syl 17 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ
(โโ((๐นโ๐ฆ) ยท (2โ๐))) โ โ) |
17 | 16, 12 | nndivred 12215 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ โ) |
18 | 12 | nnnn0d 12481 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ (2โ๐) โ
โ0) |
19 | 18 | nn0ge0d 12484 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ 0 โค (2โ๐)) |
20 | | mulge0 11681 |
. . . . . . . 8
โข ((((๐นโ๐ฆ) โ โ โง 0 โค (๐นโ๐ฆ)) โง ((2โ๐) โ โ โง 0 โค (2โ๐))) โ 0 โค ((๐นโ๐ฆ) ยท (2โ๐))) |
21 | 6, 13, 19, 20 | syl12anc 836 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ 0 โค ((๐นโ๐ฆ) ยท (2โ๐))) |
22 | | flge0nn0 13734 |
. . . . . . 7
โข ((((๐นโ๐ฆ) ยท (2โ๐)) โ โ โง 0 โค ((๐นโ๐ฆ) ยท (2โ๐))) โ (โโ((๐นโ๐ฆ) ยท (2โ๐))) โ
โ0) |
23 | 14, 21, 22 | syl2anc 585 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ
(โโ((๐นโ๐ฆ) ยท (2โ๐))) โ
โ0) |
24 | 23 | nn0ge0d 12484 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ 0 โค
(โโ((๐นโ๐ฆ) ยท (2โ๐)))) |
25 | 12 | nngt0d 12210 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ 0 < (2โ๐)) |
26 | | divge0 12032 |
. . . . 5
โข
((((โโ((๐นโ๐ฆ) ยท (2โ๐))) โ โ โง 0 โค
(โโ((๐นโ๐ฆ) ยท (2โ๐)))) โง ((2โ๐) โ โ โง 0 < (2โ๐))) โ 0 โค
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
27 | 16, 24, 13, 25, 26 | syl22anc 838 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ 0 โค
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
28 | | elrege0 13380 |
. . . 4
โข
(((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ (0[,)+โ) โ
(((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ โ โง 0 โค
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)))) |
29 | 17, 27, 28 | sylanbrc 584 |
. . 3
โข ((๐ โง (๐ โ โ โง ๐ฆ โ โ)) โ
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ (0[,)+โ)) |
30 | 29 | ralrimivva 3194 |
. 2
โข (๐ โ โ๐ โ โ โ๐ฆ โ โ ((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ (0[,)+โ)) |
31 | | mbfi1fseq.3 |
. . 3
โข ๐ฝ = (๐ โ โ, ๐ฆ โ โ โฆ
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
32 | 31 | fmpo 8004 |
. 2
โข
(โ๐ โ
โ โ๐ฆ โ
โ ((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) โ (0[,)+โ) โ ๐ฝ:(โ ร
โ)โถ(0[,)+โ)) |
33 | 30, 32 | sylib 217 |
1
โข (๐ โ ๐ฝ:(โ ร
โ)โถ(0[,)+โ)) |