Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Integer and Rational Exponents

**by****Konrad Raczkowski**- Received September 21, 1990
- MML identifier: PREPOWER

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, INT_1, RAT_1, SEQ_1, SEQ_2, FUNCT_1, ORDINAL2, SEQM_3, GROUP_1, SQUARE_1, ARYTM_3, RELAT_1, ARYTM_1, SEQ_4, ABSVALUE, LATTICES, PREPOWER; notation SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1, NEWTON, FUNCT_1, SEQ_1, SEQ_2, SEQM_3, GROUP_1, INT_1, SQUARE_1, SEQ_4, RAT_1; constructors REAL_1, NAT_1, SEQ_2, SEQM_3, SQUARE_1, SEQ_4, RAT_1, PARTFUN1, NEWTON, GROUP_1, MEMBERED, XBOOLE_0; clusters INT_1, RAT_1, XREAL_0, SEQ_1, RELSET_1, NEWTON, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x for set; reserve a, b, c for real number; reserve m, n, m1, m2 for Nat; reserve k, l, i for Integer; reserve p, q for Rational; reserve s1, s2 for Real_Sequence; canceled; theorem :: PREPOWER:2 s1 is convergent & (for n holds s1.n>=a) implies lim s1 >= a; theorem :: PREPOWER:3 s1 is convergent & (for n holds s1.n<=a) implies lim s1 <= a; definition let a be real number; func a GeoSeq -> Real_Sequence means :: PREPOWER:def 1 for m holds it.m = a|^m; end; theorem :: PREPOWER:4 s1 = a GeoSeq iff s1.0 = 1 & for m holds s1.(m+1) = s1.m * a; theorem :: PREPOWER:5 for a st a <> 0 holds for m holds a GeoSeq.m <> 0; definition let a be real number; let n; redefine func a|^n; end; definition let a be Real; let n; redefine func a |^ n -> Real; end; canceled 6; theorem :: PREPOWER:12 0 <> a implies 0 <> a |^ n; theorem :: PREPOWER:13 0 < a implies 0 < a |^ n; theorem :: PREPOWER:14 (1/a) |^ n = 1 / a |^ n; theorem :: PREPOWER:15 (b/a) |^ n = b |^ n / a |^ n; canceled; theorem :: PREPOWER:17 0 < a & a <= b implies a |^ n <= b |^ n; theorem :: PREPOWER:18 0 <= a & a < b & 1 <= n implies a |^ n < b |^ n; theorem :: PREPOWER:19 a>=1 implies a |^ n >= 1; theorem :: PREPOWER:20 1 <= a & 1 <= n implies a <= a |^ n; theorem :: PREPOWER:21 1 < a & 2 <= n implies a < a |^ n; theorem :: PREPOWER:22 0 < a & a <= 1 & 1 <= n implies a |^ n <= a; theorem :: PREPOWER:23 0 < a & a < 1 & 2 <= n implies a |^ n < a; theorem :: PREPOWER:24 ::Bernoulli inequality -1 < a implies (1 + a) |^ n >= 1 + n * a; theorem :: PREPOWER:25 0 < a & a < 1 implies (1 + a) |^ n <= 1 + 3 |^ n * a; theorem :: PREPOWER:26 s1 is convergent & (for n holds s2.n = (s1.n) |^ m) implies s2 is convergent & lim s2 = (lim s1) |^ m; definition let n; let a be real number; assume 1 <= n; canceled; func n -Root a -> real number means :: PREPOWER:def 3 it |^ n = a & it > 0 if a>0, it = 0 if a=0; end; definition let n; let a be Real; redefine func n -Root a -> Real; end; canceled; theorem :: PREPOWER:28 a>=0 & n>=1 implies (n -Root a) |^ n = a & n -Root (a |^ n) = a; theorem :: PREPOWER:29 n>=1 implies n -Root 1 = 1; theorem :: PREPOWER:30 a>=0 implies 1 -Root a = a; theorem :: PREPOWER:31 a>=0 & b>=0 & n>=1 implies n -Root (a*b) = n -Root a * n -Root b; theorem :: PREPOWER:32 a>0 & n>=1 implies n -Root (1/a) = 1/(n -Root a); theorem :: PREPOWER:33 a>=0 & b>0 & n>=1 implies n -Root (a/b) = n -Root a / n -Root b; theorem :: PREPOWER:34 a>=0 & n>=1 & m>=1 implies n -Root (m -Root a) = (n*m) -Root a; theorem :: PREPOWER:35 a>=0 & n>=1 & m>=1 implies n -Root a * m -Root a = (n*m) -Root (a |^ (n+m)); theorem :: PREPOWER:36 0<=a & a<=b & n>=1 implies n -Root a <= n -Root b; theorem :: PREPOWER:37 a>=0 & a<b & n>=1 implies n -Root a < n -Root b; theorem :: PREPOWER:38 a>=1 & n>=1 implies n -Root a >= 1 & a >= n -Root a; theorem :: PREPOWER:39 0<=a & a<1 & n>=1 implies a <= n -Root a & n -Root a < 1; theorem :: PREPOWER:40 a>0 & n>=1 implies n -Root a - 1 <= (a-1)/n; theorem :: PREPOWER:41 a>=0 implies 2-Root a = sqrt a; theorem :: PREPOWER:42 for s being Real_Sequence, a 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 number; let k; func a #Z k equals :: PREPOWER:def 4 a |^ abs(k) if k >= 0, (a |^ abs(k))" if k < 0; end; definition let a be real number; let k; cluster a #Z k -> real; end; definition let a be Real; let k; redefine func a #Z k -> Real; end; canceled; theorem :: PREPOWER:44 a #Z 0 = 1; theorem :: PREPOWER:45 a #Z 1 = a; theorem :: PREPOWER:46 a<>0 & i=n implies a #Z i = a |^ n; theorem :: PREPOWER:47 1 #Z k = 1; theorem :: PREPOWER:48 a<>0 implies a #Z k <> 0; theorem :: PREPOWER:49 a>0 implies a #Z k > 0; theorem :: PREPOWER:50 (a*b) #Z k = a #Z k * b #Z k; theorem :: PREPOWER:51 a<>0 implies a #Z (-k) = 1/a #Z k; theorem :: PREPOWER:52 (1/a) #Z k = 1/a #Z k; theorem :: PREPOWER:53 a<>0 implies a #Z (m-n) = a |^ m / a |^ n; theorem :: PREPOWER:54 a<>0 implies a #Z (k+l) = a #Z k * a #Z l; theorem :: PREPOWER:55 a #Z k #Z l = a #Z (k*l); theorem :: PREPOWER:56 a>0 & n>=1 implies (n -Root a) #Z k = n -Root (a #Z k); definition let a be real number; let p; func a #Q p equals :: PREPOWER:def 5 (denominator(p)) -Root (a #Z numerator(p)); end; definition let a be real number; let p; cluster a #Q p -> real; end; definition let a be Real; let p; redefine func a #Q p -> Real; end; canceled; theorem :: PREPOWER:58 a > 0 & p = 0 implies a #Q p = 1; theorem :: PREPOWER:59 a > 0 & p = 1 implies a #Q p = a; theorem :: PREPOWER:60 a>0 & p=n implies a #Q p = a |^ n; theorem :: PREPOWER:61 a>0 & n>=1 & p = n" implies a #Q p = n -Root a; theorem :: PREPOWER:62 1 #Q p = 1; theorem :: PREPOWER:63 a>0 implies a #Q p > 0; theorem :: PREPOWER:64 a>0 implies a #Q p * a #Q q = a #Q (p+q); theorem :: PREPOWER:65 a>0 implies 1 / a #Q p = a #Q (-p); theorem :: PREPOWER:66 a>0 implies a #Q p / a #Q q = a #Q (p-q); theorem :: PREPOWER:67 a>0 & b>0 implies (a*b) #Q p = a #Q p * b #Q p; theorem :: PREPOWER:68 a>0 implies (1/a) #Q p = 1/a #Q p; theorem :: PREPOWER:69 a>0 & b>0 implies (a/b) #Q p = a #Q p / b #Q p; theorem :: PREPOWER:70 a > 0 implies a #Q p #Q q = a #Q (p*q); theorem :: PREPOWER:71 a>=1 & p >= 0 implies a #Q p >= 1; theorem :: PREPOWER:72 a>=1 & p<=0 implies a #Q p <= 1; theorem :: PREPOWER:73 a>1 & p>0 implies a #Q p > 1; theorem :: PREPOWER:74 a>=1 & p>=q implies a #Q p >= a #Q q; theorem :: PREPOWER:75 a>1 & p>q implies a #Q p > a #Q q; theorem :: PREPOWER:76 a>0 & a<1 & p>0 implies a #Q p < 1; theorem :: PREPOWER:77 a>0 & a<=1 & p<=0 implies a #Q p >= 1; definition let IT be Real_Sequence; attr IT is Rational_Sequence-like means :: PREPOWER:def 6 for n holds IT.n is Rational; end; definition cluster Rational_Sequence-like Real_Sequence; end; definition mode Rational_Sequence is Rational_Sequence-like Real_Sequence; end; definition let s be Rational_Sequence,n; redefine func s.n -> Rational; end; canceled; theorem :: PREPOWER:79 for a be real number ex s being Rational_Sequence st s is convergent & lim s = a & for n holds s.n<=a; theorem :: PREPOWER:80 for a ex s being Rational_Sequence st s is convergent & lim s = a & for n holds s.n>=a; definition let a be real number; let s be Rational_Sequence; func a #Q s -> Real_Sequence means :: PREPOWER:def 7 for n holds it.n = a #Q (s.n); end; canceled; theorem :: PREPOWER:82 for s being Rational_Sequence st s is convergent & a>0 holds a #Q s is convergent; theorem :: PREPOWER:83 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 number; assume a > 0; func a #R b -> real number means :: PREPOWER:def 8 ex s being Rational_Sequence st s is convergent & lim s = b & a #Q s is convergent & lim a #Q s = it; end; definition let a,b be Real; redefine func a #R b -> Real; end; canceled; theorem :: PREPOWER:85 a > 0 implies a #R 0 = 1; theorem :: PREPOWER:86 a > 0 implies a #R 1 = a; theorem :: PREPOWER:87 1 #R a = 1; theorem :: PREPOWER:88 a>0 implies a #R p = a #Q p; theorem :: PREPOWER:89 a > 0 implies a #R (b+c) = a #R b * a #R c; theorem :: PREPOWER:90 a > 0 implies a #R (-c) = 1 / a #R c; theorem :: PREPOWER:91 a > 0 implies a #R (b-c) = a #R b / a #R c; theorem :: PREPOWER:92 a > 0 & b > 0 implies (a * b) #R c = a #R c * b #R c; theorem :: PREPOWER:93 a>0 implies (1/a) #R c = 1 / a #R c; theorem :: PREPOWER:94 a > 0 & b > 0 implies (a/b) #R c = a #R c / b #R c; theorem :: PREPOWER:95 a > 0 implies a #R b > 0; theorem :: PREPOWER:96 a>=1 & c>=b implies a #R c >= a #R b; theorem :: PREPOWER:97 a>1 & c>b implies a #R c > a #R b; theorem :: PREPOWER:98 a>0 & a<=1 & c>=b implies a #R c <= a #R b; theorem :: PREPOWER:99 a >= 1 & b >= 0 implies a #R b >= 1; theorem :: PREPOWER:100 a > 1 & b > 0 implies a #R b > 1; theorem :: PREPOWER:101 a >= 1 & b <= 0 implies a #R b <= 1; theorem :: PREPOWER:102 a > 1 & b < 0 implies a #R b < 1; theorem :: PREPOWER:103 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:104 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:105 a > 0 implies a #R b #R c = a #R (b * c);

Back to top