environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, CARD_1, NAT_1, ZFMISC_1, REALSET1, REAL_1, SUBSET_1, INT_1, CATALAN1, XCMPLX_0;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NEWTON, INT_1, NAT_D, ZFMISC_1;
definitions ;
theorems NAT_1, XCMPLX_1, NAT_2, NEWTON, INT_1, XREAL_1, XXREAL_0, NAT_D;
schemes NAT_2, NAT_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, NAT_2, ORDINAL1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, NEWTON, ZFMISC_1, NAT_D, VALUED_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions ;
theorem Th3:
for
n being
Nat st
n > 1 holds
n < (2 * n) -' 1
theorem Th4:
for
n being
Nat st
n > 1 holds
(n -' 2) + 1
= n -' 1
theorem
for
n being
Nat st
n > 1 holds
(((4 * n) * n) - (2 * n)) / (n + 1) > 1
theorem Th6:
for
n being
Nat st
n > 1 holds
((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !
theorem Th7:
for
n being
Nat holds 2
* (2 - (3 / (n + 1))) < 4