:: Integer and Rational Exponents
:: by Konrad Raczkowski
::
:: Received September 21, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
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;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
registration
let i be Integer;
cluster |.i.| -> natural;
end;
reserve x for set;
reserve a, b, c for Real;
reserve m, n, m1, m2 for Nat;
reserve k, l for Integer;
reserve p, q for Rational;
reserve s1, s2 for Real_Sequence;
theorem :: PREPOWER:1
s1 is convergent & (for n holds s1.n>=a) implies lim s1 >= a;
theorem :: PREPOWER:2
s1 is convergent & (for n holds s1.n<=a) implies lim s1 <= a;
definition
let a be Real;
func a GeoSeq -> Real_Sequence means
:: PREPOWER:def 1
for m holds it.m = a|^m;
end;
theorem :: PREPOWER:3
s1 = a GeoSeq iff s1.0 = 1 & for m holds s1.(m+1) = s1.m * a;
theorem :: PREPOWER:4
for a st a <> 0 holds for m holds a GeoSeq.m <> 0;
theorem :: PREPOWER:5
for a being Complex
for n being natural Number holds 0 <> a implies 0 <> a |^ n;
theorem :: PREPOWER:6
for n being natural Number holds 0 < a implies 0 < a |^ n;
theorem :: PREPOWER:7
for a being Complex, n being natural Number holds (1/a) |^ n = 1 / a |^ n;
theorem :: PREPOWER:8
for a,b being Complex
for n being natural Number holds (b/a) |^ n = b |^ n / a |^ n;
theorem :: PREPOWER:9
for n being natural Number st 0 < a & a <= b holds a |^ n <= b |^ n;
theorem :: PREPOWER:10
for n being natural Number st 0 <= a & a < b & 1 <= n holds a |^ n < b |^ n;
theorem :: PREPOWER:11
for n being natural Number holds a>=1 implies a |^ n >= 1;
theorem :: PREPOWER:12
for n being natural Number st 1 <= a & 1 <= n holds a <= a |^ n;
theorem :: PREPOWER:13
for n being Nat st 1 < a & 2 <= n holds a < a |^ n;
theorem :: PREPOWER:14
for n being natural Number st 0 < a & a <= 1 & 1 <= n holds a |^ n <= a;
theorem :: PREPOWER:15
for n being Nat st 0 < a & a < 1 & 2 <= n holds a |^ n < a;
theorem :: PREPOWER:16
for n being natural Number holds -1 < a implies (1 + a) |^ n >= 1 + n * a;
theorem :: PREPOWER:17
for n being natural Number st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + 3 |^ n * a;
theorem :: PREPOWER:18
s1 is convergent & (for n holds s2.n = (s1.n) |^ m) implies s2
is convergent & lim s2 = (lim s1) |^ m;
definition
let n be natural Number;
let a be Real;
assume
1 <= n;
func n -Root a -> Real means
:: PREPOWER:def 2
it |^ n = a & it > 0 if a>0, it = 0 if a=0;
end;
registration
let n;
let a be Real;
cluster n -Root a -> real;
end;
theorem :: PREPOWER:19
for n being Nat st a>=0 & n>=1 holds (n -Root a) |^ n = a & n
-Root (a |^ n) = a;
theorem :: PREPOWER:20
n>=1 implies n -Root 1 = 1;
theorem :: PREPOWER:21
a>=0 implies 1 -Root a = a;
theorem :: PREPOWER:22
a>=0 & b>=0 & n>=1 implies n -Root (a*b) = n -Root a * n -Root b;
theorem :: PREPOWER:23
a>0 & n>=1 implies n -Root (1/a) = 1/(n -Root a);
theorem :: PREPOWER:24
a>=0 & b>0 & n>=1 implies n -Root (a/b) = n -Root a / n -Root b;
theorem :: PREPOWER:25
a>=0 & n>=1 & m>=1 implies n -Root (m -Root a) = (n*m) -Root a;
theorem :: PREPOWER:26
a>=0 & n>=1 & m>=1 implies n -Root a * m -Root a = (n*m) -Root ( a |^ (n+m));
theorem :: PREPOWER:27
0<=a & a<=b & n>=1 implies n -Root a <= n -Root b;
theorem :: PREPOWER:28
a>=0 & a**=1 implies n -Root a < n -Root b;
theorem :: PREPOWER:29
a>=1 & n>=1 implies n -Root a >= 1 & a >= n -Root a;
theorem :: PREPOWER:30
0<=a & a<1 & n>=1 implies a <= n -Root a & n -Root a < 1;
theorem :: PREPOWER:31
a>0 & n>=1 implies n -Root a - 1 <= (a-1)/n;
theorem :: PREPOWER:32
a>=0 implies 2-Root a = sqrt a;
theorem :: PREPOWER:33
for s being Real_Sequence st a > 0 & (for n st n>=1 holds s.n = n
-Root a) holds s is convergent & lim s = 1;
definition
let a be Real;
let k be Integer;
func a #Z k -> set equals
:: PREPOWER:def 3
a |^ |.k.| if k >= 0, (a |^ |.k.|)" if k < 0;
end;
registration
let a be Real;
let k be Integer;
cluster a #Z k -> real;
end;
theorem :: PREPOWER:34
a #Z 0 = 1;
theorem :: PREPOWER:35
a #Z 1 = a;
theorem :: PREPOWER:36
for n being Nat holds a #Z n = a |^ n;
theorem :: PREPOWER:37
1 #Z k = 1;
theorem :: PREPOWER:38
a<>0 implies a #Z k <> 0;
theorem :: PREPOWER:39
a>0 implies a #Z k > 0;
theorem :: PREPOWER:40
(a*b) #Z k = a #Z k * b #Z k;
theorem :: PREPOWER:41
a #Z (-k) = 1/a #Z k;
theorem :: PREPOWER:42
(1/a) #Z k = 1/a #Z k;
theorem :: PREPOWER:43
for m,n being Nat holds a<>0 implies a #Z (m-n) = a |^ m / a |^ n;
theorem :: PREPOWER:44
a<>0 implies a #Z (k+l) = a #Z k * a #Z l;
theorem :: PREPOWER:45
a #Z k #Z l = a #Z (k*l);
theorem :: PREPOWER:46
a>0 & n>=1 implies (n -Root a) #Z k = n -Root (a #Z k);
definition
let a be Real;
let p be Rational;
func a #Q p -> set equals
:: PREPOWER:def 4
(denominator p) -Root (a #Z numerator p);
end;
registration
let a be Real;
let p be Rational;
cluster a #Q p -> real;
end;
theorem :: PREPOWER:47
p = 0 implies a #Q p = 1;
theorem :: PREPOWER:48
a > 0 & p = 1 implies a #Q p = a;
theorem :: PREPOWER:49
for n be Nat st 0 <= a holds a #Q n = a |^ n;
theorem :: PREPOWER:50
for n be Nat holds n>=1 & p = n" implies a #Q p = n -Root a;
theorem :: PREPOWER:51
1 #Q p = 1;
theorem :: PREPOWER:52
a>0 implies a #Q p > 0;
theorem :: PREPOWER:53
a>0 implies a #Q p * a #Q q = a #Q (p+q);
theorem :: PREPOWER:54
a>0 implies 1 / a #Q p = a #Q (-p);
theorem :: PREPOWER:55
a>0 implies a #Q p / a #Q q = a #Q (p-q);
theorem :: PREPOWER:56
a>0 & b>0 implies (a*b) #Q p = a #Q p * b #Q p;
theorem :: PREPOWER:57
a>0 implies (1/a) #Q p = 1/a #Q p;
theorem :: PREPOWER:58
a>0 & b>0 implies (a/b) #Q p = a #Q p / b #Q p;
theorem :: PREPOWER:59
a > 0 implies a #Q p #Q q = a #Q (p*q);
theorem :: PREPOWER:60
a>=1 & p >= 0 implies a #Q p >= 1;
theorem :: PREPOWER:61
a>=1 & p<=0 implies a #Q p <= 1;
theorem :: PREPOWER:62
a>1 & p>0 implies a #Q p > 1;
theorem :: PREPOWER:63
a>=1 & p>=q implies a #Q p >= a #Q q;
theorem :: PREPOWER:64
a>1 & p>q implies a #Q p > a #Q q;
theorem :: PREPOWER:65
a>0 & a<1 & p>0 implies a #Q p < 1;
theorem :: PREPOWER:66
a>0 & a<=1 & p<=0 implies a #Q p >= 1;
registration
cluster RAT-valued for Real_Sequence;
end;
definition
::$CD
mode Rational_Sequence is RAT-valued Real_Sequence;
end;
theorem :: PREPOWER:67
for a be Real ex s being Rational_Sequence st
s is convergent & lim s = a & for n holds s.n<=a;
theorem :: PREPOWER:68
ex s being Rational_Sequence st s is convergent & lim s = a &
for n holds s.n>=a;
definition
let a be Real;
let s be Rational_Sequence;
func a #Q s -> Real_Sequence means
:: PREPOWER:def 6
for n holds it.n = a #Q (s.n);
end;
theorem :: PREPOWER:69
for s being Rational_Sequence st s is convergent & a>0 holds a
#Q s is convergent;
theorem :: PREPOWER:70
for s1,s2 being Rational_Sequence, a st s1 is convergent & s2 is
convergent & lim s1 = lim s2 & a>0 holds a #Q s1 is convergent & a #Q s2 is
convergent & lim a #Q s1 = lim a #Q s2;
definition
let a,b be Real;
assume
a > 0;
func a #R b -> Real means
:: PREPOWER:def 7
ex s being Rational_Sequence st s is convergent & lim s = b &
a #Q s is convergent & lim a #Q s = it;
end;
theorem :: PREPOWER:71
a > 0 implies a #R 0 = 1;
theorem :: PREPOWER:72
a > 0 implies a #R 1 = a;
theorem :: PREPOWER:73
1 #R a = 1;
theorem :: PREPOWER:74
a>0 implies a #R p = a #Q p;
theorem :: PREPOWER:75
a > 0 implies a #R (b+c) = a #R b * a #R c;
theorem :: PREPOWER:76
a > 0 implies a #R (-c) = 1 / a #R c;
theorem :: PREPOWER:77
a > 0 implies a #R (b-c) = a #R b / a #R c;
theorem :: PREPOWER:78
a > 0 & b > 0 implies (a * b) #R c = a #R c * b #R c;
theorem :: PREPOWER:79
a>0 implies (1/a) #R c = 1 / a #R c;
theorem :: PREPOWER:80
a > 0 & b > 0 implies (a/b) #R c = a #R c / b #R c;
theorem :: PREPOWER:81
a > 0 implies a #R b > 0;
theorem :: PREPOWER:82
a>=1 & c>=b implies a #R c >= a #R b;
theorem :: PREPOWER:83
a>1 & c>b implies a #R c > a #R b;
theorem :: PREPOWER:84
a>0 & a<=1 & c>=b implies a #R c <= a #R b;
theorem :: PREPOWER:85
a >= 1 & b >= 0 implies a #R b >= 1;
theorem :: PREPOWER:86
a > 1 & b > 0 implies a #R b > 1;
theorem :: PREPOWER:87
a >= 1 & b <= 0 implies a #R b <= 1;
theorem :: PREPOWER:88
a > 1 & b < 0 implies a #R b < 1;
theorem :: PREPOWER:89
s1 is convergent & s2 is convergent & lim s1 > 0 & (for n holds
s1.n>0 & s2.n = (s1.n) #Q p) implies lim s2 = (lim s1) #Q p;
theorem :: PREPOWER:90
a>0 & s1 is convergent & s2 is convergent & (for n holds s2.n =
a #R (s1.n)) implies lim s2 = a #R (lim s1);
theorem :: PREPOWER:91
a > 0 implies a #R b #R c = a #R (b * c);
begin :: Addenda
:: from PCOMPS_2, 2006.02.10, A.T.
reserve r, u for Real,
k for Nat;
theorem :: PREPOWER:92
r>0 & u > 0 implies ex k be Nat st u/(2 |^ k) <= r;
theorem :: PREPOWER:93
k>=n & r >= 1 implies r |^ k >= r |^ n;
:: from SCPINVAR, 2006.03.14, A.T.
theorem :: PREPOWER:94
for n,m,l be Nat st n divides m & n divides l holds n divides m-l;
theorem :: PREPOWER:95
m divides n iff m divides (n qua Integer);
theorem :: PREPOWER:96
m gcd n= m gcd |.n-m.|;
theorem :: PREPOWER:97
for a,b be Integer st a>=0 & b>=0 holds a gcd b = a gcd (b-a);
:: missing, 2008.03.05, A.T.
theorem :: PREPOWER:98
a>=0 implies a #Z l >= 0;
theorem :: PREPOWER:99
a > 0 implies a #Q l = a #Z l;
:: missing, 2010.02.13, A.T.
theorem :: PREPOWER:100
l <> 0 implies 0 #Z l = 0;
**