:: Integer and Rational Exponents
:: by Konrad Raczkowski
::
:: Received September 21, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

registration
let i be Integer;
cluster|.i.| ->  natural ;
coherence
 abs i is natural ;
end;

theorem Th1: :: PREPOWER:1
for a being real number
for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n >= a ) holds
lim s1 >= a
proofend;

theorem Th2: :: PREPOWER:2
for a being real number
for s1 being Real_Sequence st s1 is convergent &amp; ( for n being Element of NAT holds s1 . n <= a ) holds
lim s1 <= a
proofend;

definition
let a be real number ;
funca GeoSeq  ->  Real_Sequence means :Def1: :: PREPOWER:def 1
 for m being Element of NAT holds it . m = a |^ m;
existence
 ex b1 being Real_Sequence st
for m being Element of NAT holds b1 . m = a |^ m
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for m being Element of NAT holds b1 . m = a |^ m ) &amp; ( for m being Element of NAT holds b2 . m = a |^ m ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines GeoSeq PREPOWER:def_1_:_
 for a being real number
for b2 being Real_Sequence holds
( b2 = a GeoSeq iff for m being Element of NAT holds b2 . m = a |^ m );

theorem Th3: :: PREPOWER:3
for a being real number
for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 &amp; ( for m being Element of NAT holds s1 . (m + 1) = (s1 . m) * a ) ) )
proofend;

theorem :: PREPOWER:4
for a being real number st a <> 0 holds
for m being Element of NAT holds (a GeoSeq) . m <> 0
proofend;

theorem Th5: :: PREPOWER:5
for a being real number
for n being Nat st 0 <> a holds
0 <> a |^ n
proofend;

theorem Th6: :: PREPOWER:6
for a being real number
for n being Nat st 0 < a holds
0 < a |^ n
proofend;

theorem Th7: :: PREPOWER:7
for a being real number
for n being Nat holds (1 / a) |^ n = 1 / (a |^ n)
proofend;

theorem :: PREPOWER:8
for b, a being real number
for n being Nat holds (b / a) |^ n = (b |^ n) / (a |^ n)
proofend;

theorem Th9: :: PREPOWER:9
for a, b being real number
for n being Nat st 0 < a &amp; a <= b holds
a |^ n <= b |^ n
proofend;

Lm1:  for a, b being real number
for n being Nat st 0 < a &amp; a < b &amp; 1 <= n holds
a |^ n < b |^ n
proofend;

theorem Th10: :: PREPOWER:10
for a, b being real number
for n being Nat st 0 <= a &amp; a < b &amp; 1 <= n holds
a |^ n < b |^ n
proofend;

theorem Th11: :: PREPOWER:11
for a being real number
for n being Nat st a >= 1 holds
a |^ n >= 1
proofend;

theorem Th12: :: PREPOWER:12
for a being real number
for n being Nat st 1 <= a &amp; 1 <= n holds
a <= a |^ n
proofend;

theorem :: PREPOWER:13
for a being real number
for n being Nat st 1 < a &amp; 2 <= n holds
a < a |^ n
proofend;

theorem Th14: :: PREPOWER:14
for a being real number
for n being Nat st 0 < a &amp; a <= 1 &amp; 1 <= n holds
a |^ n <= a
proofend;

theorem :: PREPOWER:15
for a being real number
for n being Nat st 0 < a &amp; a < 1 &amp; 2 <= n holds
a |^ n < a
proofend;

theorem Th16: :: PREPOWER:16
for a being real number
for n being Nat st - 1 < a holds
(1 + a) |^ n >= 1 + (n * a)
proofend;

theorem Th17: :: PREPOWER:17
for a being real number
for n being Nat st 0 < a &amp; a < 1 holds
(1 + a) |^ n <= 1 + ((3 |^ n) * a)
proofend;

theorem Th18: :: PREPOWER:18
for m being Element of NAT
for s1, s2 being Real_Sequence st s1 is convergent &amp; ( for n being Element of NAT holds s2 . n = (s1 . n) |^ m ) holds
( s2 is convergent &amp; lim s2 = (lim s1) |^ m )
proofend;

definition
let n be Nat;
let a be real number ;
assume A1: 1 <= n ;
funcn -Root a ->  real number  means :Def2: :: PREPOWER:def 2
( it |^ n = a &amp; it > 0 ) if a > 0
it = 0  if a = 0
;
consistency
 for b1 being real number st a > 0 &amp; a = 0 holds
( ( b1 |^ n = a &amp; b1 > 0 ) iff b1 = 0 ) ;
existence
 ( ( a > 0 implies ex b1 being real number st
( b1 |^ n = a &amp; b1 > 0 ) ) &amp; ( a = 0 implies ex b1 being real number st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being real number holds
( ( a > 0 &amp; b1 |^ n = a &amp; b1 > 0 &amp; b2 |^ n = a &amp; b2 > 0 implies b1 = b2 ) &amp; ( a = 0 &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
end;

:: deftheorem Def2 defines -Root PREPOWER:def_2_:_
 for n being Nat
for a being real number st 1 <= n holds
for b3 being real number holds
( ( a > 0 implies ( b3 = n -Root a iff ( b3 |^ n = a &amp; b3 > 0 ) ) ) &amp; ( a = 0 implies ( b3 = n -Root a iff b3 = 0 ) ) );

definition
let n be Element of NAT ;
let a be Real;
:: original:-Root
redefine funcn -Root a ->  Real;
coherence
 n -Root a is Real by XREAL_0:def_1;
end;

Lm2:  for a being real number
for n being Nat st a > 0 &amp; n >= 1 holds
( (n -Root a) |^ n = a &amp; n -Root (a |^ n) = a )
proofend;

theorem Th19: :: PREPOWER:19
for a being real number
for n being Nat st a >= 0 &amp; n >= 1 holds
( (n -Root a) |^ n = a &amp; n -Root (a |^ n) = a )
proofend;

theorem Th20: :: PREPOWER:20
for n being Element of NAT st n >= 1 holds
n -Root 1 = 1
proofend;

theorem Th21: :: PREPOWER:21
for a being real number st a >= 0 holds
1 -Root a = a
proofend;

theorem Th22: :: PREPOWER:22
for a, b being real number
for n being Element of NAT st a >= 0 &amp; b >= 0 &amp; n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)
proofend;

theorem Th23: :: PREPOWER:23
for a being real number
for n being Element of NAT st a > 0 &amp; n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
proofend;

theorem :: PREPOWER:24
for a, b being real number
for n being Element of NAT st a >= 0 &amp; b > 0 &amp; n >= 1 holds
n -Root (a / b) = (n -Root a) / (n -Root b)
proofend;

theorem Th25: :: PREPOWER:25
for a being real number
for n, m being Element of NAT st a >= 0 &amp; n >= 1 &amp; m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a
proofend;

theorem Th26: :: PREPOWER:26
for a being real number
for n, m being Element of NAT st a >= 0 &amp; n >= 1 &amp; m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
proofend;

theorem Th27: :: PREPOWER:27
for a, b being real number
for n being Element of NAT st 0 <= a &amp; a <= b &amp; n >= 1 holds
n -Root a <= n -Root b
proofend;

theorem Th28: :: PREPOWER:28
for a, b being real number
for n being Element of NAT st a >= 0 &amp; a < b &amp; n >= 1 holds
n -Root a < n -Root b
proofend;

theorem Th29: :: PREPOWER:29
for a being real number
for n being Element of NAT st a >= 1 &amp; n >= 1 holds
( n -Root a >= 1 &amp; a >= n -Root a )
proofend;

theorem Th30: :: PREPOWER:30
for a being real number
for n being Element of NAT st 0 <= a &amp; a < 1 &amp; n >= 1 holds
( a <= n -Root a &amp; n -Root a < 1 )
proofend;

theorem Th31: :: PREPOWER:31
for a being real number
for n being Element of NAT st a > 0 &amp; n >= 1 holds
(n -Root a) - 1 <= (a - 1) / n
proofend;

theorem :: PREPOWER:32
for a being real number st a >= 0 holds
2 -Root a = sqrt a
proofend;

Lm3:  for s being Real_Sequence
for a being real number st a >= 1 &amp; ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent &amp; lim s = 1 )
proofend;

theorem :: PREPOWER:33
for a being real number
for s being Real_Sequence st a > 0 &amp; ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent &amp; lim s = 1 )
proofend;

definition
let a be real number ;
let k be Integer;
funca #Z k ->  set  equals :Def3: :: PREPOWER:def 3
a |^ (abs k) if k >= 0
(a |^ (abs k)) "  if k < 0
;
consistency
 for b1 being set st k >= 0 &amp; k < 0 holds
( b1 = a |^ (abs k) iff b1 = (a |^ (abs k)) " ) ;
coherence
 ( ( k >= 0 implies a |^ (abs k) is set ) &amp; ( k < 0 implies (a |^ (abs k)) " is set ) ) ;
end;

:: deftheorem Def3 defines #Z PREPOWER:def_3_:_
 for a being real number
for k being Integer holds
( ( k >= 0 implies a #Z k = a |^ (abs k) ) &amp; ( k < 0 implies a #Z k = (a |^ (abs k)) " ) );

registration
let a be real number ;
let k be Integer;
clustera #Z k ->  real ;
coherence
 a #Z k is real
proofend;
end;

definition
let a be Real;
let k be Integer;
:: original:#Z
redefine funca #Z k ->  Real;
coherence
 a #Z k is Real by XREAL_0:def_1;
end;

theorem Th34: :: PREPOWER:34
for a being real number holds a #Z 0 = 1
proofend;

theorem Th35: :: PREPOWER:35
for a being real number holds a #Z 1 = a
proofend;

theorem Th36: :: PREPOWER:36
for a being real number
for n being Nat holds a #Z n = a |^ n
proofend;

Lm4:  1 " = 1
;

theorem Th37: :: PREPOWER:37
for k being Integer holds 1 #Z k = 1
proofend;

theorem :: PREPOWER:38
for a being real number
for k being Integer st a <> 0 holds
a #Z k <> 0
proofend;

theorem Th39: :: PREPOWER:39
for a being real number
for k being Integer st a > 0 holds
a #Z k > 0
proofend;

theorem Th40: :: PREPOWER:40
for a, b being real number
for k being Integer holds (a * b) #Z k = (a #Z k) * (b #Z k)
proofend;

theorem Th41: :: PREPOWER:41
for a being real number
for k being Integer holds a #Z (- k) = 1 / (a #Z k)
proofend;

theorem Th42: :: PREPOWER:42
for a being real number
for k being Integer holds (1 / a) #Z k = 1 / (a #Z k)
proofend;

theorem Th43: :: PREPOWER:43
for a being real number
for m, n being Nat st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
proofend;

theorem Th44: :: PREPOWER:44
for a being real number
for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)
proofend;

theorem Th45: :: PREPOWER:45
for a being real number
for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
proofend;

theorem Th46: :: PREPOWER:46
for a being real number
for n being Element of NAT
for k being Integer st a > 0 &amp; n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
proofend;

definition
let a be real number ;
let p be Rational;
funca #Q p ->  set  equals :: PREPOWER:def 4
(denominator p) -Root (a #Z (numerator p));
coherence
 (denominator p) -Root (a #Z (numerator p)) is set ;
end;

:: deftheorem  defines #Q PREPOWER:def_4_:_
 for a being real number
for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));

registration
let a be real number ;
let p be Rational;
clustera #Q p ->  real ;
coherence
 a #Q p is real ;
end;

definition
let a be Real;
let p be Rational;
:: original:#Q
redefine funca #Q p ->  Real;
coherence
 a #Q p is Real by XREAL_0:def_1;
end;

theorem Th47: :: PREPOWER:47
for a being real number
for p being Rational st p = 0 holds
a #Q p = 1
proofend;

theorem Th48: :: PREPOWER:48
for a being real number
for p being Rational st a > 0 &amp; p = 1 holds
a #Q p = a
proofend;

Lm5:  for a being real number
for k being Integer st a >= 0 holds
a #Z k >= 0
proofend;

theorem Th49: :: PREPOWER:49
for a being real number
for n being Nat st 0 <= a holds
a #Q n = a |^ n
proofend;

theorem Th50: :: PREPOWER:50
for a being real number
for p being Rational
for n being Nat st n >= 1 &amp; p = n " holds
a #Q p = n -Root a
proofend;

theorem Th51: :: PREPOWER:51
for p being Rational holds 1 #Q p = 1
proofend;

theorem Th52: :: PREPOWER:52
for a being real number
for p being Rational st a > 0 holds
a #Q p > 0
proofend;

theorem Th53: :: PREPOWER:53
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) * (a #Q q) = a #Q (p + q)
proofend;

theorem Th54: :: PREPOWER:54
for a being real number
for p being Rational st a > 0 holds
1 / (a #Q p) = a #Q (- p)
proofend;

theorem Th55: :: PREPOWER:55
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)
proofend;

theorem Th56: :: PREPOWER:56
for a, b being real number
for p being Rational st a > 0 &amp; b > 0 holds
(a * b) #Q p = (a #Q p) * (b #Q p)
proofend;

theorem Th57: :: PREPOWER:57
for a being real number
for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)
proofend;

theorem Th58: :: PREPOWER:58
for a, b being real number
for p being Rational st a > 0 &amp; b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)
proofend;

theorem Th59: :: PREPOWER:59
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
proofend;

theorem Th60: :: PREPOWER:60
for a being real number
for p being Rational st a >= 1 &amp; p >= 0 holds
a #Q p >= 1
proofend;

theorem Th61: :: PREPOWER:61
for a being real number
for p being Rational st a >= 1 &amp; p <= 0 holds
a #Q p <= 1
proofend;

theorem Th62: :: PREPOWER:62
for a being real number
for p being Rational st a > 1 &amp; p > 0 holds
a #Q p > 1
proofend;

theorem Th63: :: PREPOWER:63
for a being real number
for p, q being Rational st a >= 1 &amp; p >= q holds
a #Q p >= a #Q q
proofend;

theorem Th64: :: PREPOWER:64
for a being real number
for p, q being Rational st a > 1 &amp; p > q holds
a #Q p > a #Q q
proofend;

theorem Th65: :: PREPOWER:65
for a being real number
for p being Rational st a > 0 &amp; a < 1 &amp; p > 0 holds
a #Q p < 1
proofend;

theorem :: PREPOWER:66
for a being real number
for p being Rational st a > 0 &amp; a <= 1 &amp; p <= 0 holds
a #Q p >= 1
proofend;

registration
cluster Relation-like NAT -defined REAL -valued RAT -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st b1 is RAT -valued
proofend;
end;

definition
canceled;
mode Rational_Sequence is RAT -valued Real_Sequence;
end;

:: deftheorem  PREPOWER:def_5_:_
canceled;

theorem Th67: :: PREPOWER:67
for a being real number ex s being Rational_Sequence st
( s is convergent &amp; lim s = a &amp; ( for n being Element of NAT holds s . n <= a ) )
proofend;

theorem Th68: :: PREPOWER:68
for a being real number ex s being Rational_Sequence st
( s is convergent &amp; lim s = a &amp; ( for n being Element of NAT holds s . n >= a ) )
proofend;

definition
let a be real number ;
let s be Rational_Sequence;
funca #Q s ->  Real_Sequence means :Def6: :: PREPOWER:def 6
 for n being Element of NAT holds it . n = a #Q (s . n);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = a #Q (s . n)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = a #Q (s . n) ) &amp; ( for n being Element of NAT holds b2 . n = a #Q (s . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines #Q PREPOWER:def_6_:_
 for a being real number
for s being Rational_Sequence
for b3 being Real_Sequence holds
( b3 = a #Q s iff for n being Element of NAT holds b3 . n = a #Q (s . n) );

Lm6:  for s being Rational_Sequence
for a being real number st s is convergent &amp; a >= 1 holds
a #Q s is convergent
proofend;

theorem Th69: :: PREPOWER:69
for a being real number
for s being Rational_Sequence st s is convergent &amp; a > 0 holds
a #Q s is convergent
proofend;

Lm7:  for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent &amp; s2 is convergent &amp; lim s1 = lim s2 &amp; a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
proofend;

theorem Th70: :: PREPOWER:70
for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent &amp; s2 is convergent &amp; lim s1 = lim s2 &amp; a > 0 holds
( a #Q s1 is convergent &amp; a #Q s2 is convergent &amp; lim (a #Q s1) = lim (a #Q s2) )
proofend;

definition
let a, b be real number ;
assume A1: a > 0 ;
funca #R b ->  real number  means :Def7: :: PREPOWER:def 7
 ex s being Rational_Sequence st
( s is convergent &amp; lim s = b &amp; a #Q s is convergent &amp; lim (a #Q s) = it );
existence
 ex b1 being real number ex s being Rational_Sequence st
( s is convergent &amp; lim s = b &amp; a #Q s is convergent &amp; lim (a #Q s) = b1 )
proofend;
uniqueness
 for b1, b2 being real number st ex s being Rational_Sequence st
( s is convergent &amp; lim s = b &amp; a #Q s is convergent &amp; lim (a #Q s) = b1 ) &amp; ex s being Rational_Sequence st
( s is convergent &amp; lim s = b &amp; a #Q s is convergent &amp; lim (a #Q s) = b2 ) holds
b1 = b2 by A1, Th70;
end;

:: deftheorem Def7 defines #R PREPOWER:def_7_:_
 for a, b being real number st a > 0 holds
for b3 being real number holds
( b3 = a #R b iff ex s being Rational_Sequence st
( s is convergent &amp; lim s = b &amp; a #Q s is convergent &amp; lim (a #Q s) = b3 ) );

definition
let a, b be Real;
:: original:#R
redefine funca #R b ->  Real;
coherence
 a #R b is Real by XREAL_0:def_1;
end;

theorem Th71: :: PREPOWER:71
for a being real number st a > 0 holds
a #R 0 = 1
proofend;

theorem :: PREPOWER:72
for a being real number st a > 0 holds
a #R 1 = a
proofend;

theorem Th73: :: PREPOWER:73
for a being real number holds 1 #R a = 1
proofend;

theorem Th74: :: PREPOWER:74
for a being real number
for p being Rational st a > 0 holds
a #R p = a #Q p
proofend;

theorem Th75: :: PREPOWER:75
for a, b, c being real number st a > 0 holds
a #R (b + c) = (a #R b) * (a #R c)
proofend;

Lm8:  for a, b being real number st a > 0 holds
a #R b >= 0
proofend;

Lm9:  for a, b being real number st a > 0 holds
a #R b <> 0
proofend;

theorem Th76: :: PREPOWER:76
for a, c being real number st a > 0 holds
a #R (- c) = 1 / (a #R c)
proofend;

theorem Th77: :: PREPOWER:77
for a, b, c being real number st a > 0 holds
a #R (b - c) = (a #R b) / (a #R c)
proofend;

theorem Th78: :: PREPOWER:78
for a, b, c being real number st a > 0 &amp; b > 0 holds
(a * b) #R c = (a #R c) * (b #R c)
proofend;

theorem Th79: :: PREPOWER:79
for a, c being real number st a > 0 holds
(1 / a) #R c = 1 / (a #R c)
proofend;

theorem :: PREPOWER:80
for a, b, c being real number st a > 0 &amp; b > 0 holds
(a / b) #R c = (a #R c) / (b #R c)
proofend;

theorem Th81: :: PREPOWER:81
for a, b being real number st a > 0 holds
a #R b > 0
proofend;

theorem Th82: :: PREPOWER:82
for a, c, b being real number st a >= 1 &amp; c >= b holds
a #R c >= a #R b
proofend;

theorem Th83: :: PREPOWER:83
for a, c, b being real number st a > 1 &amp; c > b holds
a #R c > a #R b
proofend;

theorem Th84: :: PREPOWER:84
for a, c, b being real number st a > 0 &amp; a <= 1 &amp; c >= b holds
a #R c <= a #R b
proofend;

theorem Th85: :: PREPOWER:85
for a, b being real number st a >= 1 &amp; b >= 0 holds
a #R b >= 1
proofend;

theorem Th86: :: PREPOWER:86
for a, b being real number st a > 1 &amp; b > 0 holds
a #R b > 1
proofend;

theorem Th87: :: PREPOWER:87
for a, b being real number st a >= 1 &amp; b <= 0 holds
a #R b <= 1
proofend;

theorem :: PREPOWER:88
for a, b being real number st a > 1 &amp; b < 0 holds
a #R b < 1
proofend;

Lm10:  for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent &amp; s2 is convergent &amp; lim s1 > 0 &amp; p >= 0 &amp; ( for n being Element of NAT holds
( s1 . n > 0 &amp; s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proofend;

theorem Th89: :: PREPOWER:89
for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent &amp; s2 is convergent &amp; lim s1 > 0 &amp; ( for n being Element of NAT holds
( s1 . n > 0 &amp; s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proofend;

Lm11:  for a, b being real number
for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
proofend;

Lm12:  for a being real number
for s1, s2 being Real_Sequence st a >= 1 &amp; s1 is convergent &amp; s2 is convergent &amp; ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proofend;

theorem Th90: :: PREPOWER:90
for a being real number
for s1, s2 being Real_Sequence st a > 0 &amp; s1 is convergent &amp; s2 is convergent &amp; ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proofend;

theorem :: PREPOWER:91
for a, b, c being real number st a > 0 holds
(a #R b) #R c = a #R (b * c)
proofend;

begin

theorem :: PREPOWER:92
for r, u being real number st r > 0 &amp; u > 0 holds
ex k being Element of NAT st u / (2 |^ k) <= r
proofend;

theorem :: PREPOWER:93
for n being Element of NAT
for r being real number
for k being Nat st k >= n &amp; r >= 1 holds
r |^ k >= r |^ n
proofend;

:: from SCPINVAR, 2006.03.14, A.T.
theorem Th94: :: PREPOWER:94
for n, m, l being Element of NAT st n divides m &amp; n divides l holds
n divides m - l
proofend;

theorem :: PREPOWER:95
for m, n being Element of NAT holds
( m divides n iff m divides n ) ;

theorem Th96: :: PREPOWER:96
for m, n being Element of NAT holds m gcd n = m gcd (abs (n - m))
proofend;

theorem :: PREPOWER:97
for a, b being Integer st a >= 0 &amp; b >= 0 holds
a gcd b = a gcd (b - a)
proofend;

:: missing, 2008.03.05, A.T.
theorem :: PREPOWER:98
for a being real number
for l being Integer st a >= 0 holds
a #Z l >= 0 by Lm5;

theorem :: PREPOWER:99
for a being real number
for l being Integer st a > 0 holds
a #Q l = a #Z l
proofend;

:: missing, 2010.02.13, A.T.
theorem :: PREPOWER:100
for l being Integer st l <> 0 holds
0 #Z l = 0
proofend;