Metamath Proof Explorer


Theorem snmlff

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 F=nk1n|ARkmodR=Bn
Assertion snmlff F:01

Proof

Step Hyp Ref Expression
1 snmlff.f F=nk1n|ARkmodR=Bn
2 fzfid n1nFin
3 ssrab2 k1n|ARkmodR=B1n
4 ssfi 1nFink1n|ARkmodR=B1nk1n|ARkmodR=BFin
5 2 3 4 sylancl nk1n|ARkmodR=BFin
6 hashcl k1n|ARkmodR=BFink1n|ARkmodR=B0
7 5 6 syl nk1n|ARkmodR=B0
8 7 nn0red nk1n|ARkmodR=B
9 nndivre k1n|ARkmodR=Bnk1n|ARkmodR=Bn
10 8 9 mpancom nk1n|ARkmodR=Bn
11 7 nn0ge0d n0k1n|ARkmodR=B
12 nnre nn
13 nngt0 n0<n
14 divge0 k1n|ARkmodR=B0k1n|ARkmodR=Bn0<n0k1n|ARkmodR=Bn
15 8 11 12 13 14 syl22anc n0k1n|ARkmodR=Bn
16 ssdomg 1nFink1n|ARkmodR=B1nk1n|ARkmodR=B1n
17 2 3 16 mpisyl nk1n|ARkmodR=B1n
18 hashdom k1n|ARkmodR=BFin1nFink1n|ARkmodR=B1nk1n|ARkmodR=B1n
19 5 2 18 syl2anc nk1n|ARkmodR=B1nk1n|ARkmodR=B1n
20 17 19 mpbird nk1n|ARkmodR=B1n
21 nnnn0 nn0
22 hashfz1 n01n=n
23 21 22 syl n1n=n
24 20 23 breqtrd nk1n|ARkmodR=Bn
25 nncn nn
26 25 mulridd nn1=n
27 24 26 breqtrrd nk1n|ARkmodR=Bn1
28 1red n1
29 ledivmul k1n|ARkmodR=B1n0<nk1n|ARkmodR=Bn1k1n|ARkmodR=Bn1
30 8 28 12 13 29 syl112anc nk1n|ARkmodR=Bn1k1n|ARkmodR=Bn1
31 27 30 mpbird nk1n|ARkmodR=Bn1
32 elicc01 k1n|ARkmodR=Bn01k1n|ARkmodR=Bn0k1n|ARkmodR=Bnk1n|ARkmodR=Bn1
33 10 15 31 32 syl3anbrc nk1n|ARkmodR=Bn01
34 1 33 fmpti F:01