Description: The function F from snmlval is a mapping from positive integers to real numbers in the range [ 0 , 1 ] . (Contributed by Mario Carneiro, 6-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | snmlff.f | |
|
Assertion | snmlff | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snmlff.f | |
|
2 | fzfid | |
|
3 | ssrab2 | |
|
4 | ssfi | |
|
5 | 2 3 4 | sylancl | |
6 | hashcl | |
|
7 | 5 6 | syl | |
8 | 7 | nn0red | |
9 | nndivre | |
|
10 | 8 9 | mpancom | |
11 | 7 | nn0ge0d | |
12 | nnre | |
|
13 | nngt0 | |
|
14 | divge0 | |
|
15 | 8 11 12 13 14 | syl22anc | |
16 | ssdomg | |
|
17 | 2 3 16 | mpisyl | |
18 | hashdom | |
|
19 | 5 2 18 | syl2anc | |
20 | 17 19 | mpbird | |
21 | nnnn0 | |
|
22 | hashfz1 | |
|
23 | 21 22 | syl | |
24 | 20 23 | breqtrd | |
25 | nncn | |
|
26 | 25 | mulridd | |
27 | 24 26 | breqtrrd | |
28 | 1red | |
|
29 | ledivmul | |
|
30 | 8 28 12 13 29 | syl112anc | |
31 | 27 30 | mpbird | |
32 | elicc01 | |
|
33 | 10 15 31 32 | syl3anbrc | |
34 | 1 33 | fmpti | |