:: Integer and Rational Exponents
:: by Konrad Raczkowski
::
:: Received September 21, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: PREPOWER:1
canceled;
theorem Th2: :: PREPOWER:2
theorem Th3: :: PREPOWER:3
:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :
theorem Th4: :: PREPOWER:4
theorem :: PREPOWER:5
theorem :: PREPOWER:6
canceled;
theorem :: PREPOWER:7
canceled;
theorem :: PREPOWER:8
canceled;
theorem :: PREPOWER:9
canceled;
theorem :: PREPOWER:10
canceled;
theorem :: PREPOWER:11
canceled;
theorem Th12: :: PREPOWER:12
theorem Th13: :: PREPOWER:13
theorem Th14: :: PREPOWER:14
theorem :: PREPOWER:15
theorem :: PREPOWER:16
canceled;
theorem Th17: :: PREPOWER:17
Lm1:
for a, b being real number
for n being natural number st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
theorem Th18: :: PREPOWER:18
theorem Th19: :: PREPOWER:19
theorem Th20: :: PREPOWER:20
theorem :: PREPOWER:21
theorem Th22: :: PREPOWER:22
theorem :: PREPOWER:23
theorem Th24: :: PREPOWER:24
theorem Th25: :: PREPOWER:25
theorem Th26: :: PREPOWER:26
:: deftheorem PREPOWER:def 2 :
canceled;
:: deftheorem Def3 defines -Root PREPOWER:def 3 :
Lm2:
for a being real number
for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
theorem :: PREPOWER:27
canceled;
theorem Th28: :: PREPOWER:28
theorem Th29: :: PREPOWER:29
theorem Th30: :: PREPOWER:30
theorem Th31: :: PREPOWER:31
theorem Th32: :: PREPOWER:32
theorem :: PREPOWER:33
theorem Th34: :: PREPOWER:34
theorem Th35: :: PREPOWER:35
theorem Th36: :: PREPOWER:36
theorem Th37: :: PREPOWER:37
theorem Th38: :: PREPOWER:38
theorem Th39: :: PREPOWER:39
theorem Th40: :: PREPOWER:40
theorem :: PREPOWER:41
Lm3:
for s being Real_Sequence
for a being real number st a >= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
theorem :: PREPOWER:42
:: deftheorem Def4 defines #Z PREPOWER:def 4 :
theorem :: PREPOWER:43
canceled;
theorem Th44: :: PREPOWER:44
theorem Th45: :: PREPOWER:45
theorem Th46: :: PREPOWER:46
Lm4:
( 1 " = 1 & 1 / 1 = 1 )
;
theorem Th47: :: PREPOWER:47
theorem :: PREPOWER:48
theorem Th49: :: PREPOWER:49
theorem Th50: :: PREPOWER:50
theorem Th51: :: PREPOWER:51
theorem Th52: :: PREPOWER:52
theorem Th53: :: PREPOWER:53
theorem Th54: :: PREPOWER:54
theorem Th55: :: PREPOWER:55
theorem Th56: :: PREPOWER:56
:: deftheorem defines #Q PREPOWER:def 5 :
theorem :: PREPOWER:57
canceled;
theorem Th58: :: PREPOWER:58
theorem Th59: :: PREPOWER:59
Lm49:
for a being real number
for k being Integer st a >= 0 holds
a #Z k >= 0
theorem Th60: :: PREPOWER:60
theorem Th61: :: PREPOWER:61
theorem Th62: :: PREPOWER:62
theorem Th63: :: PREPOWER:63
theorem Th64: :: PREPOWER:64
theorem Th65: :: PREPOWER:65
theorem Th66: :: PREPOWER:66
theorem Th67: :: PREPOWER:67
theorem Th68: :: PREPOWER:68
theorem Th69: :: PREPOWER:69
theorem Th70: :: PREPOWER:70
theorem Th71: :: PREPOWER:71
theorem Th72: :: PREPOWER:72
theorem Th73: :: PREPOWER:73
theorem Th74: :: PREPOWER:74
theorem Th75: :: PREPOWER:75
theorem Th76: :: PREPOWER:76
theorem :: PREPOWER:77
:: deftheorem Def6 defines Rational_Sequence-like PREPOWER:def 6 :
theorem :: PREPOWER:78
canceled;
theorem Th79: :: PREPOWER:79
theorem Th80: :: PREPOWER:80
:: deftheorem Def7 defines #Q PREPOWER:def 7 :
Lm5:
for s being Rational_Sequence
for a being real number st s is convergent & a >= 1 holds
a #Q s is convergent
theorem :: PREPOWER:81
canceled;
theorem Th82: :: PREPOWER:82
Lm6:
for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
theorem Th83: :: PREPOWER:83
:: deftheorem Def8 defines #R PREPOWER:def 8 :
theorem :: PREPOWER:84
canceled;
theorem Th85: :: PREPOWER:85
theorem :: PREPOWER:86
theorem Th87: :: PREPOWER:87
theorem Th88: :: PREPOWER:88
theorem Th89: :: PREPOWER:89
Lm7:
for a, b being real number st a > 0 holds
a #R b >= 0
Lm8:
for a, b being real number st a > 0 holds
a #R b <> 0
theorem Th90: :: PREPOWER:90
theorem Th91: :: PREPOWER:91
theorem Th92: :: PREPOWER:92
theorem Th93: :: PREPOWER:93
theorem :: PREPOWER:94
theorem Th95: :: PREPOWER:95
theorem Th96: :: PREPOWER:96
theorem Th97: :: PREPOWER:97
theorem Th98: :: PREPOWER:98
theorem Th99: :: PREPOWER:99
theorem Th100: :: PREPOWER:100
theorem Th101: :: PREPOWER:101
theorem :: PREPOWER:102
Lm9:
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 Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
theorem Th103: :: PREPOWER:103
Lm10:
for a, b being real number
for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
Lm11:
for a being real number
for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of NAT holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
theorem Th104: :: PREPOWER:104
theorem :: PREPOWER:105
theorem :: PREPOWER:106
theorem :: PREPOWER:107
theorem Th108: :: PREPOWER:108
theorem :: PREPOWER:109
theorem Th110: :: PREPOWER:110
theorem :: PREPOWER:111
theorem :: PREPOWER:112
theorem :: PREPOWER:113