先の補題を用いて，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 …

今回は，奇数分の偶数と表せる有理数が加法について閉じていることの証明です． let lemma01 = MESON[ODD_EXISTS; LT_0; REAL_LT]`!x. ODD x ==> &0 < &x`;; g`!a b c d. EVEN a /\ EVEN c /\ ODD b /\ ODD d ==> ?x y. &a / &b + &c / &d = &x / &y /\ EVEN…

今回は，先の和にを掛けてになる項と残りの和に分割する補題です． let lemma01 = MP (SPECL[`\k. &2 pow xn / &k`;`1`;`2 EXP xn`;`n - 2 EXP xn`]SUM_ADD_SPLIT) (prove(`1 <= 2 EXP xn + 1`,MP_TAC(MESON[TWO; ZERO_LESS_EXP]`0 < 2 EXP n`) THEN ARITH_T…

今回は，先の和の各項の分母の中での指数がに等しいものは唯一つであり，その他のの指数はより小さいことの証明です． g`!x y n. ODD y /\ 2 EXP x * y < 2 EXP (SUC n) ==> x <= n`;; e(REPEAT STRIP_TAC);; e(ASSUME_TAC(UNDISCH(MESON[ODD_EXISTS; LT_0; …