environ
vocabularies HIDDEN, NUMBERS, INT_1, COMPLEX1, ORDINAL1, XREAL_0, SUBSET_1, RAT_1, SEQ_1, SEQ_2, FUNCT_1, XXREAL_0, ORDINAL2, CARD_1, NEWTON, REAL_1, ARYTM_3, RELAT_1, NAT_1, ARYTM_1, VALUED_1, XXREAL_2, SEQ_4, SQUARE_1, VALUED_0, INT_2, PREPOWER, TARSKI, FUNCT_7, ASYMPT_1, XCMPLX_0;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, INT_2, INT_1, NAT_1, NAT_D, NEWTON, RELAT_1, FUNCT_1, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SQUARE_1, SEQ_4, RAT_1;
definitions TARSKI, XXREAL_2;
theorems ABSVALUE, NAT_1, SEQ_1, SEQ_2, INT_1, SQUARE_1, SEQ_4, RAT_1, RFUNCT_2, TARSKI, FUNCT_2, NEWTON, XREAL_0, XCMPLX_0, XCMPLX_1, FUNCOP_1, COMPLEX1, XREAL_1, XXREAL_0, INT_2, ORDINAL1, NAT_D, VALUED_1, VALUED_0, RELAT_1, NUMBERS;
schemes NAT_1, SEQ_1, FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, SEQ_1, SEQ_2, XCMPLX_0;
constructors HIDDEN, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3, PARTFUN1, VALUED_1, SEQ_4, NEWTON, XXREAL_2, RELSET_1, BINOP_2, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1, XCMPLX_0, SEQ_1;
expansions TARSKI, XXREAL_2;
Lm1:
for a, b being Real
for n being natural Number st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
theorem
for
a being
Real for
n being
Nat st 1
< a & 2
<= n holds
a < a |^ n
theorem
for
a being
Real for
n being
Nat st
0 < a &
a < 1 & 2
<= n holds
a |^ n < a
reconsider j = 1 as Element of REAL by NUMBERS:19;
Lm2:
for a being Real
for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
Lm3:
for s being Real_Sequence
for a being Real st a >= 1 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
Lm4:
1 " = 1
;
Lm5:
for a being Real
for k being Integer st a >= 0 holds
a #Z k >= 0
Lm6:
for s being Rational_Sequence
for a being Real st s is convergent & a >= 1 holds
a #Q s is convergent
Lm7:
for s1, s2 being Rational_Sequence
for a being Real st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
Lm8:
for a, b being Real st a > 0 holds
a #R b >= 0
Lm9:
for a, b being Real st a > 0 holds
a #R b <> 0
theorem Th83:
for
a,
b,
c being
Real st
a > 1 &
c > b holds
a #R c > a #R b
theorem Th86:
for
a,
b being
Real st
a > 1 &
b > 0 holds
a #R b > 1
theorem
for
a,
b being
Real st
a > 1 &
b < 0 holds
a #R b < 1
Lm10:
for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Nat holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
Lm11:
for a, b being Real
for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
Lm12:
for a being Real
for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)