Example (16-1)

　今回は次を証明します．

fを整数係数の１変数多項式関数とするとき，任意の非負整数nに対してf(n)が素数ならば，fは定数関数である

　方針は，素数f(0)の任意の正整数倍に対する関数値も素数，従ってf(0)となることより，任意の正整数を根とする多項式を見出すものですが，素数についての性質をはじめ，様々な道具が入用になります．
　目標は，ひとまず

`!d p:num c:num->int.
(!n:num. ?q:num. prime q /\ &q = &p + &n * isum(0..d)(\k. c k * ( &n ) pow k ) )
==> c d = &0`;;

としておきます．まず必要なパッケージをロードしましょう．

needs "Library/isum.ml";;
needs "Library/prime.ml";;
needs "Library/pocklington.ml";;

needs "Library/analysis.ml";;
needs "Library/transc.ml";;
needs "Examples/sos_win.ml";;

　以下，補題を用意しながら進みます．

g`prime(a*b)==>(a=1\/b=1)`;;
e(DISCH_THEN(fun t-> MP_TAC(MATCH_MP PRIME_IMP_NZ t) THEN MP_TAC t));;
e(REWRITE_TAC[prime; CONJ_SYM]);;
e(STRIP_TAC);;
e(FIRST_X_ASSUM MP_TAC);;
e(FIRST_ASSUM(fun t-> MP_TAC(MP(SPEC`a:num`t)(MESON[divides;]`a divides a*b`))));;
e(FIRST_ASSUM(fun t-> MP_TAC(MP(SPEC`b:num`t)(MESON[divides; MULT_SYM; ]`b divides a*b`))));;
e(CONV_TAC NUM_RING);;