environ
vocabularies HIDDEN, NUMBERS, NAT_1, XREAL_0, ORDINAL1, FINSEQ_1, RELAT_1, FUNCT_1, XXREAL_0, XBOOLE_0, SUBSET_1, ARYTM_3, TARSKI, FINSEQ_2, XCMPLX_0, CARD_3, REAL_1, CARD_1, ORDINAL4, REALSET1, ARYTM_1, PARTFUN1, INT_2, INT_1, FINSET_1, SQUARE_1, FUNCOP_1, NEWTON, VALUED_0, FUNCT_7, MEMBERED;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, PARTFUN1, FUNCT_2, MEMBERED, VALUED_0, FINSET_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, INT_1, INT_2, NAT_1, NAT_D, RVSUM_1, SQUARE_1, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, RVSUM_1, FINSEQ_1, FINSEQ_2, FUNCT_1, INT_1, XREAL_0, XBOOLE_0, XCMPLX_1, INT_2, CARD_2, CARD_1, XBOOLE_1, XREAL_1, XCMPLX_0, XXREAL_0, FINSOP_1, ORDINAL1, NAT_D, PARTFUN1, VALUED_1, FUNCOP_1, ZFMISC_1;
schemes NAT_1, FINSEQ_1, SUBSET_1, NAT_D;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0, CARD_1;
constructors HIDDEN, PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2, FINSOP_1, RVSUM_1, FUNCOP_1, RELSET_1, FINSEQOP;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, FINSEQ_1, SQUARE_1, FINSEQ_2, RVSUM_1;
expansions TARSKI, XBOOLE_0;
theorem Th33:
for
k,
l being
Nat st
l >= 1 holds
k * l >= k
theorem Th34:
for
k,
n,
l being
Nat st
l >= 1 &
n >= k * l holds
n >= k
theorem
for
n being
Nat st
n <> 0 holds
(n + 1) / n > 1
theorem Th37:
for
k being
Nat holds
k / (k + 1) < 1
theorem Th38:
for
l being
Nat holds
l ! >= l
Lm1:
SetPrimenumber 2 = {}
Lm2:
for n being Nat holds SetPrimenumber n = { k where k is Element of NAT : ( k < n & k is prime ) }
defpred S1[ Nat] means for i being Nat st 2 <= i holds
i |^ $1 >= $1 + 1;
Lm3:
S1[ 0 ]
by RVSUM_1:94;
Lm4:
for n being Nat st S1[n] holds
S1[n + 1]
theorem Th85:
for
n,
i being
Nat st 2
<= i holds
i |^ n >= n + 1
theorem
for
n,
i being
Nat st 2
<= i holds
i |^ n > n
Lm5:
for n1, n2, m1, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
theorem
for
n1,
n2,
m1,
m2 being
Nat st
(2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
(
n1 = n2 &
m1 = m2 )