environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, PARTFUN1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_1, INT_1, RELAT_1, ARYTM_1, POWER, ABIAN, ZFMISC_1, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, INT_1, NAT_1, NAT_D, POWER, ABIAN, FUNCT_1, PARTFUN1, FINSEQ_1, XXREAL_0;
definitions NAT_D;
theorems AXIOMS, INT_1, NAT_1, ABIAN, POWER, FINSEQ_1, FINSEQ_4, XREAL_1, TARSKI, XCMPLX_1, ORDINAL1, NAT_D, XXREAL_0, XREAL_0, ZFMISC_1, CARD_1;
schemes NAT_1, RECDEF_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, ABIAN, SERIES_1, XBOOLE_0, ZFMISC_1, ORDINAL1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, SERIES_1, BINARITH, ABIAN;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1;
expansions ;
theorem
for
i,
j,
k,
l being
Nat st
i <= j &
k <= j &
i = (j -' k) + l holds
k = (j -' i) + l
theorem
for
i,
j being
Nat st
j < i holds
(i -' (j + 1)) + 1
= i -' j
theorem Th8:
for
i,
j being
Nat st
i >= j holds
j -' i = 0
theorem
for
k,
n being
Nat st
n <= k &
k < n + n holds
k div n = 1
scheme
Indfrom2{
P1[
set ] } :
provided
A1:
P1[2]
and A2:
for
k being non
trivial Nat st
P1[
k] holds
P1[
k + 1]
theorem
for
i,
j,
k being
Nat holds
(i -' j) -' k = i -' (j + k)