let n be Nat; :: thesis: for p being Prime st n > 0 holds
p < primenumber (n + (primeindex p))
let p be Prime; :: thesis: ( n > 0 implies p < primenumber (n + (primeindex p)) )
assume A1: n > 0 ; :: thesis: p < primenumber (n + (primeindex p))
A2: p = primenumber (primeindex p) by Def4;
assume p >= primenumber (n + (primeindex p)) ; :: thesis: contradiction
then 0 + (primeindex p) >= n + (primeindex p) by A2, MOEBIUS2:21;
hence contradiction by A1, XREAL_1:6; :: thesis: verum