Example (22.6)

　先の補題を用いて，thm5で分割した第１の和が奇数分の分数と表せることを証明します．

g`!xn k. 1 <= xn /\ 1 <= k /\ k <= 2 EXP xn - 1 ==> ?x y. &2 pow xn / &k = &x / &y /\ EVEN x /\ ODD y`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(
prove(`k <= 2 EXP xn - 1 ==> k < 2 EXP SUC xn /\  ~(k = 2 EXP xn)`,
SIMP_TAC[EXP] THEN MP_TAC(MESON[TWO; ZERO_LESS_EXP]`0 < 2 EXP xn`) THEN CONV_TAC SOS_RULE)
) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC (SPECL[`xn:num`;`k:num`]thm4) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM REAL_MUL; GSYM REAL_OF_NUM_POW; REAL_FIELD`a/(b*c)=(a/b)/c`]);;
e(ASSUME_TAC(ARITH_RULE`~(&2 = &0)`) THEN ASM_SIMP_TAC[REAL_DIV_POW2_ALT; REAL_OF_NUM_POW]);;
e(ASM_MESON_TAC[
MESON[ARITH_RULE`EVEN(2)`; LE_1; EVEN_EXP]`!x. 0 < x ==> EVEN (2 EXP x)`;
ARITH_RULE`a<b <=> 0<b-a`]);;
let thm7_1 = top_thm();;

g`!a b:num->real. !m. (!k. 1 <= k /\ k <= m ==> ?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y) ==> ?x y. sum (1..m) (\k. a k / b k) = &x / &y /\ EVEN x /\ ODD y`;;
e(STRIP_TAC THEN STRIP_TAC);;
e(INDUCT_TAC);;
e(SIMP_TAC[my; ARITH] THEN MESON_TAC[REAL_FIELD`&0 = &0 / &1`; ARITH_RULE`EVEN 0 /\ ODD 1`]);;
let lemma = MESON[ARITH_RULE`k <= m ==> k <= SUC m`; my; LE_REFL]
    `(!k. 1 <= k /\ k <= SUC m
     ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y)) ==>
     (!k. 1 <= k /\ k <= m
     ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y))
     /\ (?x y. a (SUC m) / b (SUC m) = &x / &y /\ EVEN x /\ ODD y)`;;
e(STRIP_TAC THEN MP_TAC lemma THEN ASM_SIMP_TAC[my; ARITH] THEN STRIP_TAC THEN UNDISCH_TAC `(!k. 1 <= k /\ k <= m
      ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y))
 ==> (?x y. sum (1..m) (\k. a k / b k) = &x / &y /\ EVEN x /\ ODD y)` THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(ASM_MESON_TAC[thm6]);;
let thm7_2 = top_thm();;

g`!xn. 1 <= xn ==> ?x y. sum (1..2 EXP xn - 1) (\k. &2 pow xn / &k) = &x / &y /\ EVEN x /\ ODD y`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPECL[`\k:num. &2 pow xn`;`\k. &k`;`2 EXP xn - 1`]thm7_2) THEN BETA_TAC THEN ASM_SIMP_TAC[thm7_1]);;
let thm7 = top_thm();;