let k be Nat; :: thesis: for p being Prime holds
( p < primenumber k iff primeindex p < k )
let p be Prime; :: thesis: ( p < primenumber k iff primeindex p < k )
primenumber (primeindex p) = p by NUMBER10:def 4;
hence ( p < primenumber k iff primeindex p < k ) by MOEBIUS2:21; :: thesis: verum