environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, ZFMISC_1, CARD_1, XBOOLE_0, ARYTM_1, TARSKI, ARYTM_2, ARYTM_3, ARYTM_0, REAL_1, XXREAL_0, NAT_1, RELAT_1, INT_1, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, AXIOMS, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1, ZFMISC_1, XBOOLE_0, NUMBERS, ARYTM_0, ARYTM_2, ARYTM_1, XREAL_1, XXREAL_0, ORDINAL1, XTUPLE_0, SUBSET_1;
schemes NAT_1, XBOOLE_0, SUBSET_1;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1;
constructors HIDDEN, FUNCT_4, ARYTM_1, ARYTM_0, XXREAL_0, REAL_1, NAT_1, FINSET_1, CARD_1, XREAL_0, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0;
expansions TARSKI;
Lm1:
for z being object st z in [:{0},NAT:] \ {[0,0]} holds
ex k being Nat st z = - k
Lm2:
for x being object
for k being Nat st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}
theorem Th6:
for
k being
Nat for
i1,
i2 being
Integer st
i1 + k = i2 holds
i1 <= i2
Lm3:
for j being Element of NAT st j < 1 holds
j = 0
Lm4:
for i1 being Integer st 0 < i1 holds
1 <= i1
theorem Th9:
for
i1,
i2 being
Integer holds
(
i1 * i2 = 1 iff ( (
i1 = 1 &
i2 = 1 ) or (
i1 = - 1 &
i2 = - 1 ) ) )
theorem
for
i1,
i2 being
Integer holds
(
i1 * i2 = - 1 iff ( (
i1 = - 1 &
i2 = 1 ) or (
i1 = 1 &
i2 = - 1 ) ) )
Lm5:
for i0, i1 being Integer st i0 <= i1 holds
ex k being Nat st i0 + k = i1
Lm6:
for i0, i1 being Integer st i0 <= i1 holds
ex k being Nat st i1 - k = i0
scheme
IntIndFull{
F1()
-> Integer,
P1[
Integer] } :
provided
A1:
P1[
F1()]
and A2:
for
i2 being
Integer st
P1[
i2] holds
(
P1[
i2 - 1] &
P1[
i2 + 1] )
theorem Th23:
for
r being
Real for
i1,
i2 being
Integer st
i1 <= r &
r - 1
< i1 &
i2 <= r &
r - 1
< i2 holds
i1 = i2
theorem Th24:
for
r being
Real for
i1,
i2 being
Integer st
r <= i1 &
i1 < r + 1 &
r <= i2 &
i2 < r + 1 holds
i1 = i2
Lm7:
for r being Real ex n being Nat st r < n