:: Integer and Rational Exponents :: by Konrad Raczkowski :: :: Received September 21, 1990 :: Copyright (c) 1990-2021 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 -> number 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 -> number 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;