Example (17)

　今回は
http://as305.dyndns.org/aps/problem/view/50
すなわち
[tex:\forall n:num.\, 3\le n \to (n+1)^n

g`!a b c d. &0 < a /\ &0 < b ==> ( a*c<b*d <=> c/b<d/a )`;;
e(REPEAT STRIP_TAC);;
e(ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`; ]);;
e(ASM_SIMP_TAC[RAT_LEMMA3]);;
e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a*b* inv(x)< &0 <=> a*b< &0)`]);;
e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a* inv(x)< &0 <=> a< &0)`] THEN REAL_ARITH_TAC);;
let lemma1=top_thm();;

let lemma2=MESON[
REAL_FIELD`&0< &n ==> (!x. &n <= x /\ x <= &n + &1 ==> &0<x /\ ~(x= &0))`;
DIFF_CONV`(\x. ln x / x)`;
]`&0< &n ==> (!x. &n <= x /\ x <= &n + &1
     ==> ((\x. ln x / x) diffl ((inv x * &1) * x - &1 * ln x) / x pow 2) x)`;;

let lemma3=REAL_SOSFIELD`&0<z ==>(((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2 < &0<=> &1 < ln z)`;;

let lemma4=MESON
[
REAL_FIELD`inv (&2) <= ln (&2)<=> &1<= &2*ln(&2)`;
MP (GSYM(SPECL[`2`;`&2`]LN_POW)) (REAL_FIELD`&0< &2`);
REAL_FIELD`&2 pow 2 = &4`;
]`inv (&2) <= ln (&2)<=> &1<=ln(&4)`;;

　以下証明です．

g`!n. 3<=n ==> (&n + &1) pow n < &n pow (n + 1)`;;
e(REPEAT STRIP_TAC);;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`3<=n==>(n=3 \/ 4<=n)`)));;
e(ASM_SIMP_TAC[ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`4<=n==>(n=4 \/ 5<=n)`)));;
e(ASM_SIMP_TAC[ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;


e(MP_TAC (ARITH_RULE`&3<= &n==> &3<= &n /\ &0< &n + &1 /\ &0< &n /\ &n < &n + &1`) THEN ASM_SIMP_TAC[REAL_LE] THEN REPEAT STRIP_TAC);;
e(MP_TAC (MESON[REAL_POW_LT]`&0< &n + &1 /\ &0< &n ==> &0 < (&n + &1) pow n /\ &0 < &n pow (n + 1)`) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM LN_MONO_LT; LN_POW; GSYM REAL_ADD; lemma1]);;
e(ASM_SIMP_TAC[lemma1]);;
e(MP_TAC (SPECL[`\x. ln x /x`;`\x. ((inv x * &1) * x - &1 * ln x) / x pow 2`;`&n:real`;`&n+ &1`]MVT_ALT) THEN BETA_TAC THEN ASM_SIMP_TAC[]);;
e(ASSUME_TAC(UNDISCH lemma2) THEN ASM_SIMP_TAC[] THEN FIRST_X_ASSUM(fun t->ALL_TAC) THEN REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`] THEN ASM_SIMP_TAC[]);;
e(MP_TAC (REAL_ARITH`&0< &n /\ &n<z ==> &0<z`) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[UNDISCH lemma3]);;
e(MP_TAC (SPEC`inv(&2)`REAL_EXP_BOUND_LEMMA) THEN SIMP_TAC[REAL_ARITH`&0 <= inv (&2) /\ inv (&2) <= inv (&2) /\ &1 + &2 * inv (&2) = &2`] );;

e(REWRITE_TAC[MESON[REAL_ARITH`&0< &2`; EXP_LN; ]`x<= &2<=>x<=exp(ln(&2))`; REAL_EXP_MONO_LE; lemma4]);;

let lemma5=MESON[REAL_ARITH`&0< &4 /\ &0< &5 /\ &4< &5`; LN_MONO_LT]`ln(&4)<ln(&5)`;;

e(ASSUME_TAC lemma5);;

e(ASSUME_TAC (REAL_ARITH`&0< &5`) THEN MP_TAC (MESON[
GSYM REAL_LE;
REAL_LET_TRANS;
LN_MONO_LT]
`5 <= n /\ &n<z /\ &0< &5 /\ &0<z ==> ln(&5)<ln(z)`) THEN ASM_SIMP_TAC[] THEN ASM_REAL_ARITH_TAC);;