:: Rational Numbers, Irrational Roots and Numeral Representations
:: by Rafa{\l} Ziobro
::
:: Received July 2, 2026
:: Copyright (c) 2026 Association of Mizar Users


registration
let a be heavy positive Real;
let n be non zero Nat;
cluster n -root a -> heavy positive ;
coherence
( n -root a is heavy & n -root a is positive )
proof end;
end;

registration
let a be Integer;
let n be Nat;
reduce (a |^ (n + 1)) div (a |^ n) to a;
reducibility
(a |^ (n + 1)) div (a |^ n) = a
proof end;
end;

registration
let a be even Nat;
reduce (a / 2) mod a to a / 2;
reducibility
(a / 2) mod a = a / 2
proof end;
end;

registration
let a be even Nat;
let n be non trivial Nat;
cluster (a |^ n) mod (2 * a) -> zero ;
coherence
(a |^ n) mod (2 * a) is zero
proof end;
end;

registration
let a be odd Nat;
reduce ((a - 1) / 2) mod a to (a - 1) / 2;
reducibility
((a - 1) / 2) mod a = (a - 1) / 2
proof end;
let n be non zero Nat;
reduce (a |^ n) mod (2 * a) to a;
reducibility
(a |^ n) mod (2 * a) = a
proof end;
end;

registration
let a be Nat;
let b be non trivial Nat;
reduce a mod (a * b) to a;
reducibility
a mod (a * b) = a ;
end;

registration
let a be Nat;
let b be non trivial Nat;
cluster a div (a * b) -> zero ;
coherence
a div (a * b) is zero ;
end;

registration
let a, b be Nat;
let c be non zero Nat;
reduce (a mod b) mod (b * c) to a mod b;
reducibility
(a mod b) mod (b * c) = a mod b
proof end;
end;

registration
let a be non trivial odd Nat;
reduce ((a + 1) / 2) mod a to (a + 1) / 2;
reducibility
((a + 1) / 2) mod a = (a + 1) / 2
proof end;
end;

:: Subsequent integers
theorem NAT162: :: NUMERAL3:1
for a, b being Integer
for n being Nat st a <= b & b <= a + n holds
not not b = a + 0 & ... & not b = a + n
proof end;

theorem INT17: :: NUMERAL3:2
for a, b being Integer holds
( ( a <= b & b <= a + 1 ) iff ( b = a or b = a + 1 ) )
proof end;

:: Use of sgn for identifying classes of numbers
registration
let a be non integer Real;
cluster sgn (frac a) -> weightless positive ;
coherence
( sgn (frac a) is weightless & sgn (frac a) is positive ) by ABSVALUE:def 2;
end;

registration
let a be non integer Real;
reduce a * (sgn (frac a)) to a;
reducibility
a * (sgn (frac a)) = a
proof end;
end;

registration
let a be light non negative Real;
reduce frac a to a;
reducibility
frac a = a
proof end;
end;

theorem A17: :: NUMERAL3:3
for r being Real holds
( r * (sgn r) = |.r.| & r / (sgn r) = |.r.| & r = |.r.| / (sgn r) )
proof end;

theorem :: NUMERAL3:4
for r being Real holds [\|.r.|/] + (frac |.r.|) = r * (sgn r)
proof end;

theorem :: NUMERAL3:5
for r being heavy Real holds
( sgn r = sgn [\r/] & sgn r = sgn [/r\] )
proof end;

theorem :: NUMERAL3:6
for a being Real holds sgn (frac a) = sgn (frac (- a))
proof end;

theorem FL: :: NUMERAL3:7
for a being Real holds ([\a/] + [\(- a)/]) + (sgn (frac a)) = 0
proof end;

theorem FLM: :: NUMERAL3:8
for a being non integer Real holds [\a/] + [\(- a)/] = - 1
proof end;

theorem FAA: :: NUMERAL3:9
for a being non integer Real holds (frac a) + (frac (- a)) = 1
proof end;

theorem :: NUMERAL3:10
for r being Real holds frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))
proof end;

theorem :: NUMERAL3:11
for r being Real holds [/r\] = [\r/] + (sgn (frac r))
proof end;

theorem :: NUMERAL3:12
for a, b, c being Integer holds a mod b = ((b * c) + a) mod b
proof end;

theorem :: NUMERAL3:13
for a, b being non zero Nat
for c being Nat holds (c mod (a * b)) mod b = (c mod b) mod (a * b) by RADIX_1:3;

theorem FCA: :: NUMERAL3:14
for a being Real holds [\a/] = - [/(- a)\]
proof end;

theorem FCB: :: NUMERAL3:15
for a being Real holds [/a\] = - [\(- a)/]
proof end;

theorem :: NUMERAL3:16
for a being weightless negative Real holds [\a/] = - 1 by COMPLEX3:1;

theorem :: NUMERAL3:17
for a being weightless positive Real holds [/a\] = 1 by COMPLEX3:1;

theorem :: NUMERAL3:18
for a being Real holds
( frac a = frac (- a) iff 2 * a is integer )
proof end;

theorem :: NUMERAL3:19
for a, b being Integer holds a div (- b) = (- a) div b
proof end;

theorem NATD1: :: NUMERAL3:20
for a being Real
for b being non zero Nat holds (frac (a / b)) * b < b
proof end;

theorem AMB: :: NUMERAL3:21
for a, b being Integer st not b divides a holds
(a mod b) + ((- a) mod b) = b
proof end;

theorem MOD1: :: NUMERAL3:22
for a, b being Integer holds a mod b = - ((- a) mod (- b))
proof end;

theorem MOD2: :: NUMERAL3:23
for a, b being Integer holds
( a mod (- b) = - ((- a) mod b) & (- a) mod b = - (a mod (- b)) )
proof end;

theorem :: NUMERAL3:24
for a, b being Integer st not b divides a holds
(a mod b) - (a mod (- b)) = b
proof end;

theorem :: NUMERAL3:25
for a, b being Real holds [\(a + b)/] = ([\a/] + [\b/]) + [\((frac a) + (frac b))/]
proof end;

theorem MUL: :: NUMERAL3:26
for a, b being Real holds [\(a * b)/] = ([\a/] * [\b/]) + [\((([\a/] * (frac b)) + ([\b/] * (frac a))) + ((frac a) * (frac b)))/]
proof end;

theorem :: NUMERAL3:27
for a being Real
for b being Integer holds [\(a * b)/] = ([\a/] * b) + [\((frac a) * b)/]
proof end;

CF1: for a being Real holds [/a\] <= [\a/] + 1
proof end;

theorem CF2: :: NUMERAL3:28
for a, b being Real st a <= b holds
[/a\] <= [\b/] + 1
proof end;

theorem :: NUMERAL3:29
for a, b being Real st a <= b holds
[\a/] < [\b/] + 1
proof end;

theorem CFD: :: NUMERAL3:30
for a, b being Real holds [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/]
proof end;

theorem LFR: :: NUMERAL3:31
for a being Real
for b being non zero Nat holds (frac ([\a/] / b)) + ((frac a) / b) < 1
proof end;

theorem FFP: :: NUMERAL3:32
for a being Real
for b being positive Integer holds [\(a / b)/] = [\([\a/] / b)/]
proof end;

theorem :: NUMERAL3:33
for a being Real
for b being negative Integer holds [\(a / b)/] = [\([/a\] / b)/]
proof end;

theorem :: NUMERAL3:34
for a being Real
for b being positive Real holds - [\(a / (- b))/] >= [\(a / b)/]
proof end;

theorem FBC: :: NUMERAL3:35
for a, b being Real st [\a/] <= b & b <= [/a\] & not [\a/] = [\b/] holds
[/a\] = [/b\]
proof end;

theorem :: NUMERAL3:36
for a being Real
for b being non integer Real st [\a/] <= b & b <= [/a\] holds
( [\a/] = [\b/] & [/a\] = [/b\] )
proof end;

theorem N227: :: NUMERAL3:37
for a, b being Integer
for c being Nat holds [\(a / (b * c))/] = [\([\(a / b)/] / c)/]
proof end;

theorem :: NUMERAL3:38
for a being Integer
for b being non zero Integer
for c being negative Integer holds [\(a / (b * c))/] = [\([\(- (a / b))/] / (- c))/]
proof end;

theorem :: NUMERAL3:39
for a being Integer
for b being non zero Integer st [\(a / b)/] = - [\(- (a / b))/] holds
b divides a
proof end;

theorem :: NUMERAL3:40
for a being Integer
for b being negative Integer holds [\(a / b)/] = - ([\(a / (- b))/] + (sgn (frac (a / b))))
proof end;

NAT227: for a, b being Integer
for c being Nat holds (a div b) div c = a div (b * c)
proof end;

theorem ABC: :: NUMERAL3:41
for a being Integer
for b being non zero Integer
for c being non zero Nat holds a mod (b * c) = (a mod b) + (b * ((a div b) mod c))
proof end;

theorem :: NUMERAL3:42
for a being Nat
for b, c being non zero Nat holds a div c = ((a div c) mod b) + (b * (a div (b * c)))
proof end;

theorem ABLK: :: NUMERAL3:43
for a being Integer
for b being non zero Nat
for k, l being Nat holds a mod (b |^ (k + l)) = (a mod (b |^ k)) + (((a div (b |^ k)) mod (b |^ l)) * (b |^ k))
proof end;

theorem MD: :: NUMERAL3:44
for a, n being Nat
for b being non zero Nat holds a mod (b |^ n) = a - ((b |^ n) * (a div (b |^ n)))
proof end;

theorem DNK: :: NUMERAL3:45
for a, b, n, k being Nat holds a div (b |^ (n + k)) = (a div (b |^ n)) div (b |^ k)
proof end;

theorem RMD: :: NUMERAL3:46
for a, n, k being Nat
for b being non zero Nat holds (b |^ n) * ((a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k))) = (a mod (b |^ (n + k))) - (a mod (b |^ n))
proof end;

theorem :: NUMERAL3:47
for a, n, k being Nat
for b being non zero Nat holds a div (b |^ n) = ((a div (b |^ (n + k))) * (b |^ k)) + ((a div (b |^ n)) mod (b |^ k))
proof end;

theorem MRD: :: NUMERAL3:48
for a, n, k being Nat
for b being non zero Nat holds (a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k)) = ((a mod (b |^ (n + k))) - (a mod (b |^ n))) div (b |^ n)
proof end;

theorem :: NUMERAL3:49
for a, n being Nat
for b being non zero Nat holds (a div (b |^ n)) - ((a div (b |^ (n + 1))) * (b |^ 1)) = ((a mod (b |^ (n + 1))) - (a mod (b |^ n))) div (b |^ n) by MRD;

theorem :: NUMERAL3:50
for a, n being Nat
for b being non zero Nat holds (a mod (b |^ (n + 1))) div (b |^ n) < b
proof end;

theorem :: NUMERAL3:51
for a, n being Nat
for b being non zero Nat holds (a mod (b |^ (n + 1))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - (b * (a div (b |^ (n + 1)))))
proof end;

theorem DMK: :: NUMERAL3:52
for a, n, k being Nat
for b being non zero Nat holds (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k)))))
proof end;

theorem :: NUMERAL3:53
for a, n, k being Nat
for b being non zero Nat holds (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) mod (b |^ k))
proof end;

theorem DAS: :: NUMERAL3:54
for a, n, k being Nat
for b being non zero Nat holds b |^ n divides (a mod (b |^ (n + k))) - (a mod (b |^ n))
proof end;

theorem :: NUMERAL3:55
for a, n, k being Nat
for b being non zero Nat holds ((a mod (b |^ (n + k))) - (a mod (b |^ n))) mod (b |^ n) = 0
proof end;

theorem :: NUMERAL3:56
for a, n, k being Nat
for b being non zero Nat holds (a mod (b |^ (n + k))) + ((b |^ (n + k)) * (a div (b |^ (n + k)))) = (a mod (b |^ n)) + ((b |^ n) * (a div (b |^ n)))
proof end;

theorem DHS: :: NUMERAL3:57
for a, b, n being Nat holds a mod (b |^ n) <= a mod (b |^ (n + 1))
proof end;

registration
let a, b, n be Nat;
cluster (a mod (b |^ (n + 1))) - (a mod (b |^ n)) -> natural ;
coherence
(a mod (b |^ (n + 1))) - (a mod (b |^ n)) is natural
proof end;
end;

theorem :: NUMERAL3:58
for a, b being Nat holds a div (b |^ 2) = (a div b) div b
proof end;

theorem :: NUMERAL3:59
for a being Nat
for b being non trivial Nat holds a div b = ((a div (b |^ 0)) - (a mod (b |^ 1))) div b
proof end;

theorem :: NUMERAL3:60
for a being Nat
for b being non trivial Nat holds a div (b |^ 2) = ((a div (b |^ 0)) - (a mod (b |^ 2))) div (b |^ 2)
proof end;

theorem :: NUMERAL3:61
for a, n being Nat
for b being non zero Nat holds (a mod (b |^ (n + 1))) - (a mod (b |^ n)) = (((a mod (b |^ (n + 1))) - (a mod (b |^ n))) div (b |^ n)) * (b |^ n) by DAS, NAT_D:3;

theorem :: NUMERAL3:62
for a being Nat
for b being non trivial Nat ex n being Nat st a < b |^ n
proof end;

theorem :: NUMERAL3:63
for a, b being non trivial Nat ex n being Nat st
( b |^ n <= a & a < b |^ (n + 1) )
proof end;

registration
let n, k be Nat;
let f be n + k -element complex-valued XFinSequence;
cluster (f | n) ^ <%0%> -> complex-valued ;
coherence
(f | n) ^ <%0%> is complex-valued ;
end;

registration
let n be Nat;
let f be n + 1 -element complex-valued XFinSequence;
reduce (f | n) ^ <%(f . n)%> to f;
reducibility
(f | n) ^ <%(f . n)%> = f
proof end;
end;

registration
let k be Complex;
let f be complex-valued XFinSequence;
cluster f ^ <%k%> -> complex-valued ;
coherence
f ^ <%k%> is complex-valued ;
end;

registration
let m, n be Nat;
let D be non empty set ;
let f be D -valued m -element XFinSequence;
let g be D -valued n -element XFinSequence;
reduce (f ^ g) | m to f;
reducibility
(f ^ g) | m = f
proof end;
end;

theorem Th23: :: NUMERAL3:64
for n, i being Nat
for k being Complex st n <> i holds
((n --> 0) ^ <%k%>) . i = 0
proof end;

theorem RXF: :: NUMERAL3:65
for n being Nat
for f being b1 + 1 -element complex-valued XFinSequence holds f = ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>)
proof end;

registration
let n be Nat;
let f be n + 1 -element complex-valued XFinSequence;
reduce ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>) to f;
reducibility
((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>) = f by RXF;
end;

registration
let f be empty-yielding XFinSequence of NAT ;
let b be Nat;
cluster value (f,b) -> zero ;
coherence
value (f,b) is zero
proof end;
end;

registration
let n be Nat;
let b be non trivial Nat;
reduce value ((digits (n,b)),b) to n;
reducibility
value ((digits (n,b)),b) = n by NEWTON03:def 1, NUMERAL1:5;
end;

theorem ND0: :: NUMERAL3:66
for n, k being Nat
for b being non trivial Nat holds (digits (n,b)) . k < b
proof end;

theorem :: NUMERAL3:67
for b, n being Nat
for f, g being b2 -element XFinSequence of NAT holds value ((f + g),b) = (value (f,b)) + (value (g,b))
proof end;

theorem VFN: :: NUMERAL3:68
for b, k, n being Nat
for f being b2 -element XFinSequence of NAT holds value ((f ^ <%n%>),b) = (value (f,b)) + (n * (b |^ k))
proof end;

theorem :: NUMERAL3:69
for b, k being Nat
for f being b2 -element XFinSequence of NAT holds value ((f ^ <%0%>),b) = value (f,b)
proof end;

theorem KBN: :: NUMERAL3:70
for k, n, b being Nat holds value (<%n,k%>,b) = (k * b) + n
proof end;

theorem :: NUMERAL3:71
for k, n, b being Nat holds value (((k --> 0) ^ <%n%>),b) = n * (b |^ k)
proof end;

theorem :: NUMERAL3:72
for k, m, n, b being Nat holds value (<%n,m,k%>,b) = ((k * (b |^ 2)) + (m * b)) + n
proof end;

theorem :: NUMERAL3:73
for b being non zero Nat
for f being XFinSequence of NAT st value (f,b) = 0 holds
f is empty-yielding
proof end;

theorem Th26: :: NUMERAL3:74
for n being Nat
for b being non trivial Nat st digits (n,b) = <%n%> holds
n < b
proof end;

theorem :: NUMERAL3:75
for n being Nat
for b being non trivial Nat st n >= b holds
len (digits (n,b)) > 1
proof end;

theorem NMB: :: NUMERAL3:76
for n being Nat
for b being non trivial Nat holds (digits (n,b)) . 0 = n mod b
proof end;

theorem :: NUMERAL3:77
for n being Nat
for b being non trivial Nat holds n div b = value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)
proof end;

theorem :: NUMERAL3:78
for a being Nat
for b being non trivial Nat
for c being non zero Nat holds (value ((digits (a,b)),b)) mod c = value ((digits ((a mod c),b)),b) ;

theorem :: NUMERAL3:79
for a being Nat
for b being non trivial Nat
for n being non zero Nat holds (value ((digits (a,(b |^ n))),(b |^ n))) mod b = value ((digits ((a mod b),(b |^ n))),(b |^ n)) ;

registration
let a be non negative Real;
reduce sqrt (a ^2) to a;
reducibility
sqrt (a ^2) = a by SQUARE_1:22;
reduce (sqrt a) ^2 to a;
reducibility
(sqrt a) ^2 = a by SQUARE_1:def 2;
reduce (sqrt a) |^ 2 to a;
reducibility
(sqrt a) |^ 2 = a
proof end;
reduce (sqrt a) * (sqrt a) to a;
reducibility
(sqrt a) * (sqrt a) = a
proof end;
end;

registration
let a be Nat;
let b be Integer;
cluster a / (a gcd b) -> natural ;
coherence
a / (a gcd b) is natural ;
end;

registration
let a be Nat;
let b be Integer;
reduce (a * b) gcd a to a;
reducibility
(a * b) gcd a = a
proof end;
end;

theorem Th1: :: NUMERAL3:80
for a being Integer
for b being non zero Integer holds a / (b gcd a),b / (a gcd b) are_coprime
proof end;

theorem Th2: :: NUMERAL3:81
for a, n being Nat
for b being Real st (a + 1) |^ n > b |^ n & b |^ n > a |^ n holds
not b is integer
proof end;

theorem FLN: :: NUMERAL3:82
for a being non integer Real holds [\a/] + [\(- a)/] = - 1
proof end;

registration
let a be non integer Real;
cluster [\a/] + [\(- a)/] -> weightless negative ;
coherence
( [\a/] + [\(- a)/] is weightless & [\a/] + [\(- a)/] is negative )
proof end;
end;

theorem :: NUMERAL3:83
for a being Real holds [\a/] + [\(- a)/] is weightless
proof end;

Thx: ex k being Rational st
( k is light & k is positive & not k is integer )
proof end;

registration
cluster non zero complex real non integer light ext-real positive non negative non irrational for object ;
existence
ex b1 being positive Rational st
( b1 is light & not b1 is integer ) by Thx;
end;

theorem APB: :: NUMERAL3:84
for a, b being non zero Nat holds
( denominator (a / b) <= b & numerator (a / b) <= a )
proof end;

theorem :: NUMERAL3:85
for a being Rational holds denominator (denominator a) = 1 by NAT_2:def 1;

theorem :: NUMERAL3:86
for a being Rational holds denominator (numerator a) = 1 by NAT_2:def 1;

theorem :: NUMERAL3:87
for a being non trivial Nat
for b, c being non zero Nat st a divides b & a divides c holds
( denominator (b / c) < c & numerator (b / c) < b )
proof end;

registration
let a be Rational;
cluster (denominator a) gcd (numerator a) -> trivial non zero ;
coherence
( (denominator a) gcd (numerator a) is trivial & not (denominator a) gcd (numerator a) is zero )
proof end;
end;

theorem :: NUMERAL3:88
for a being Integer
for b being non zero Integer holds
( denominator (a / b) divides b & numerator (a / b) divides a )
proof end;

theorem :: NUMERAL3:89
for a being Integer
for b being non zero Nat st a,b are_coprime holds
denominator (a / b) = b
proof end;

theorem :: NUMERAL3:90
for a being non zero light Rational holds not denominator a divides numerator a
proof end;

theorem NDD: :: NUMERAL3:91
for a being Rational holds [\a/] = (numerator a) div (denominator a)
proof end;

theorem NFD: :: NUMERAL3:92
for a being Rational holds frac a = ((numerator a) mod (denominator a)) / (denominator a)
proof end;

theorem FRD: :: NUMERAL3:93
for a being Rational holds (frac a) * (denominator a) = (numerator a) mod (denominator a)
proof end;

registration
let a be Rational;
cluster frac a -> rational ;
coherence
not frac a is irrational
proof end;
cluster (frac a) * (denominator a) -> natural ;
coherence
(frac a) * (denominator a) is natural
proof end;
end;

theorem :: NUMERAL3:94
for a being Rational holds numerator (frac a), denominator (frac a) are_coprime by NAT_2:def 1;

theorem :: NUMERAL3:95
for a being Rational holds (numerator (frac a)) mod (denominator (frac a)) = numerator (frac a)
proof end;

theorem NMD: :: NUMERAL3:96
for a being Rational holds (numerator a) mod (denominator a), denominator a are_coprime
proof end;

theorem FRA: :: NUMERAL3:97
for a being Rational holds denominator (frac a) = denominator (frac (- a))
proof end;

theorem DF: :: NUMERAL3:98
for a being Rational holds denominator a = denominator (frac a)
proof end;

theorem :: NUMERAL3:99
for a being Rational
for b being Integer holds denominator (a + b) = denominator a
proof end;

theorem :: NUMERAL3:100
for a being non integer negative Rational holds frac a = 1 - (((numerator (- a)) mod (denominator a)) / (denominator a))
proof end;

theorem R144: :: NUMERAL3:101
for a being positive Rational holds
( numerator a = denominator (a ") & denominator a = numerator (a ") )
proof end;

registration
let a be positive Nat;
cluster numerator (a ") -> weightless positive ;
coherence
( numerator (a ") is weightless & numerator (a ") is positive )
proof end;
end;

registration
let a be positive Nat;
reduce denominator (a ") to a;
reducibility
denominator (a ") = a
proof end;
end;

theorem :: NUMERAL3:102
for a being positive Rational holds (numerator a) * (numerator (a ")) = (denominator a) * (denominator (a "))
proof end;

theorem ABI: :: NUMERAL3:103
for a, b being Rational holds (numerator (a * b)) / (denominator (a * b)) = ((numerator a) * (numerator b)) / ((denominator a) * (denominator b))
proof end;

theorem IND: :: NUMERAL3:104
for a, b being Rational holds ((numerator (a * b)) * (denominator a)) * (denominator b) = ((denominator (a * b)) * (numerator a)) * (numerator b)
proof end;

theorem NUM: :: NUMERAL3:105
for a, b being Rational holds numerator (a * b) divides (numerator a) * (numerator b)
proof end;

theorem DEN: :: NUMERAL3:106
for a, b being Rational holds denominator (a * b) divides (denominator a) * (denominator b)
proof end;

theorem :: NUMERAL3:107
for a, b being non zero Rational holds ((denominator a) * (denominator b)) / (denominator (a * b)) = ((numerator a) * (numerator b)) / (numerator (a * b))
proof end;

theorem DDN: :: NUMERAL3:108
for a, b being Rational st a * b is integer holds
denominator b divides numerator a
proof end;

theorem :: NUMERAL3:109
for a, b being Rational holds
( a * b is integer iff ( denominator b divides numerator a & denominator a divides numerator b ) )
proof end;

theorem :: NUMERAL3:110
for a, b being non negative Rational holds (numerator a) * (numerator b) >= numerator (a * b)
proof end;

theorem :: NUMERAL3:111
for a, b being Rational holds (denominator a) * (denominator b) >= denominator (a * b)
proof end;

theorem :: NUMERAL3:112
for a being Rational
for k being non zero Nat st a * k is integer holds
k >= denominator a
proof end;

theorem :: NUMERAL3:113
for a, b being non zero Rational holds ((numerator (a + b)) * (denominator a)) * (denominator b) = (((numerator b) * (denominator a)) + ((numerator a) * (denominator b))) * (denominator (a + b))
proof end;

theorem Th3: :: NUMERAL3:114
for n being non zero Nat
for a being non integer Rational holds not a |^ n is integer
proof end;

theorem Th4: :: NUMERAL3:115
for a, b, n being Nat st (a + 1) |^ n > b & b > a |^ n holds
n -root b is irrational
proof end;

theorem Th5: :: NUMERAL3:116
for a being Nat
for n being non zero Nat holds
( n -root a is irrational iff not n -root a is integer )
proof end;

registration
let a be non square Nat;
cluster 2 -root a -> irrational ;
coherence
2 -root a is irrational
proof end;
let n be non zero even Nat;
cluster n -root a -> irrational ;
coherence
n -root a is irrational
proof end;
end;

theorem Th6: :: NUMERAL3:117
for a being prime Nat
for n, m being non zero Nat holds (n + m) -root (a |^ m) is irrational
proof end;

theorem Th7: :: NUMERAL3:118
for n being non zero Nat
for a, b being Nat st a,b are_coprime & n -root (a * b) is Nat holds
n -root a is Nat
proof end;

theorem Th8: :: NUMERAL3:119
for n being non zero Nat
for a, b being Nat st a,b are_coprime & n -root (a * b) is rational holds
n -root a is rational
proof end;

theorem Th9: :: NUMERAL3:120
for a being prime Nat
for b, n, m being non zero Nat st not a divides b holds
(n + m) -root ((a |^ m) * b) is irrational
proof end;

theorem Th10: :: NUMERAL3:121
for n being non trivial Nat
for a being prime Nat
for b being Nat st a divides b & not a |^ n divides b holds
n -root b is irrational
proof end;

registration
let a be non trivial square-free Nat;
let n be non trivial Nat;
cluster n -root a -> irrational ;
coherence
n -root a is irrational
proof end;
end;

registration
let a be prime Nat;
let b be non zero rational number ;
cluster (sqrt a) * ((sqrt a) + b) -> irrational ;
coherence
(sqrt a) * ((sqrt a) + b) is irrational
proof end;
end;

theorem Th11: :: NUMERAL3:122
for a being prime Nat
for b, c being rational number holds
( ((sqrt a) + b) * ((sqrt a) + c) is rational iff b = - c )
proof end;

registration
let a be prime Nat;
let b be rational number ;
cluster ((sqrt a) + b) * ((sqrt a) - b) -> rational ;
coherence
not ((sqrt a) + b) * ((sqrt a) - b) is irrational
proof end;
end;

registration
let a be prime Nat;
let b be non zero rational number ;
cluster ((sqrt a) + b) * ((sqrt a) + b) -> irrational ;
coherence
((sqrt a) + b) * ((sqrt a) + b) is irrational
proof end;
end;

registration
let a be prime Nat;
let b, c be positive rational number ;
cluster ((sqrt a) + b) * ((sqrt a) + c) -> irrational ;
coherence
((sqrt a) + b) * ((sqrt a) + c) is irrational
proof end;
cluster ((sqrt a) - b) * ((sqrt a) - c) -> irrational ;
coherence
((sqrt a) - b) * ((sqrt a) - c) is irrational
proof end;
end;

theorem Th12: :: NUMERAL3:123
for n being non zero Nat
for a being non negative Real st a > 1 holds
n -root a > 1
proof end;

registration
let n be non zero Nat;
let a be trivial Nat;
cluster n -root a -> natural ;
coherence
n -root a is natural
proof end;
end;

registration
let a be non trivial square-free Nat;
let n, m be non zero Nat;
cluster (n + m) -root (a |^ m) -> irrational ;
coherence
(n + m) -root (a |^ m) is irrational
proof end;
end;

registration
let a be non trivial square-free Nat;
let b be non zero rational number ;
let n, m be non zero Nat;
cluster ((n + m) -root (a |^ n)) * (((n + m) -root (a |^ m)) + b) -> irrational ;
coherence
((n + m) -root (a |^ n)) * (((n + m) -root (a |^ m)) + b) is irrational
proof end;
end;

registration
let a be non trivial square-free Nat;
cluster sqrt a -> irrational ;
coherence
sqrt a is irrational
proof end;
end;

registration
let a be non trivial square-free Nat;
let b be non zero rational number ;
cluster (sqrt a) * ((sqrt a) + b) -> irrational ;
coherence
(sqrt a) * ((sqrt a) + b) is irrational
proof end;
end;

theorem Th13: :: NUMERAL3:124
for a, b being Nat holds a * b = ((a gcd b) |^ 2) * ((a lcm b) / (a gcd b))
proof end;

registration
let a be non zero Nat;
cluster a / (Radical a) -> natural ;
coherence
a / (Radical a) is natural
proof end;
end;

Th14: for a being Integer
for b being square-free Nat holds a gcd b is square-free
proof end;

registration
let a be Integer;
let b be square-free Nat;
cluster a gcd b -> square-free ;
coherence
not a gcd b is square-containing by Th14;
end;

theorem Th15: :: NUMERAL3:125
for a being non zero square-containing Nat holds a > Radical a
proof end;

registration
let a be non zero square-containing Nat;
cluster a / (Radical a) -> non trivial ;
coherence
not a / (Radical a) is trivial by Th15, XREAL_1:187;
end;

theorem Th16: :: NUMERAL3:126
for a being Integer st a <> 1 & a <> - 1 holds
ex p being prime Nat st p divides a
proof end;

registration
let a be non trivial square Nat;
let b be Nat;
cluster a * b -> square-containing ;
coherence
a * b is square-containing
proof end;
end;

registration
let a be Nat;
let b be square-containing Nat;
cluster a lcm b -> square-containing ;
coherence
a lcm b is square-containing
proof end;
end;

theorem Th17: :: NUMERAL3:127
for a, b being Nat st not a,b are_coprime holds
a * b is square-containing
proof end;

theorem Th18: :: NUMERAL3:128
for a being square-free Nat
for b being Nat holds a gcd b,a / (a gcd b) are_coprime
proof end;

theorem Th19: :: NUMERAL3:129
for b being square-free Nat
for a being Nat st not b divides a holds
ex p being prime Nat st
( not p divides a & p divides b )
proof end;

theorem Th20: :: NUMERAL3:130
for a being square-free Nat
for b, n, m being non zero Nat st not a divides b holds
(n + m) -root ((a |^ m) * b) is irrational
proof end;

theorem Th21: :: NUMERAL3:131
for a being square-free Nat
for b being non zero Nat
for n being non trivial Nat st b < a |^ n & a divides b holds
n -root b is irrational
proof end;

registration
let a be non zero Nat;
let n be non trivial Nat;
cluster n -root ((a |^ n) + 1) -> irrational ;
coherence
n -root ((a |^ n) + 1) is irrational
proof end;
end;

registration
let a, n be non trivial Nat;
cluster n -root ((a |^ n) - 1) -> irrational ;
coherence
n -root ((a |^ n) - 1) is irrational
proof end;
end;

theorem Th22: :: NUMERAL3:132
for b being Nat
for n being non zero Nat st n -root b is irrational holds
ex a being Nat st
( a |^ n < b & b < (a + 1) |^ n )
proof end;

theorem Th23: :: NUMERAL3:133
for a, b being Nat
for n being non zero Nat st n -root b is irrational & n -root b > a holds
ex c being Nat st
( a |^ n < b & b < (a + (2 * c)) |^ n )
proof end;

theorem :: NUMERAL3:134
for a being Nat
for n being non zero Nat st n -root a is irrational holds
ex b being Nat st
( 1 < a & a < ((2 * b) + 1) |^ n )
proof end;

theorem Th25: :: NUMERAL3:135
for a being non zero Nat
for n being non trivial Nat
for m being Nat holds n -root ((a |^ (n * m)) + 1) is irrational
proof end;

theorem :: NUMERAL3:136
for a, n being non trivial Nat
for m being non zero Nat holds n -root ((a |^ (n * m)) - 1) is irrational
proof end;

theorem Th27: :: NUMERAL3:137
for b being non zero Nat
for n being non trivial Nat st 2 -root b is natural holds
2 -root (b + 2) is irrational
proof end;

theorem :: NUMERAL3:138
for b being non zero Nat st 2 -root (b + 2) is natural holds
2 -root b is irrational
proof end;

theorem Th28: :: NUMERAL3:139
for a being prime Nat
for m being Nat
for n being non trivial Nat holds
( n -root (a |^ m) is rational iff n divides m )
proof end;

theorem Th29: :: NUMERAL3:140
for a being non trivial odd square-free Nat
for b being non zero Nat st a,b are_coprime holds
2 -root (a * ((2 * b) + a)) is irrational
proof end;

theorem :: NUMERAL3:141
for a being odd square-free Nat
for b being non zero Nat st a,b are_coprime & 2 -root (a * ((2 * b) + a)) is rational holds
a is trivial by Th29;

theorem :: NUMERAL3:142
for a being non trivial square-free Nat
for n being non trivial Nat holds n -root a is irrational ;

theorem :: NUMERAL3:143
for a being prime Nat
for n being non trivial Nat holds n -root a is irrational ;

theorem :: NUMERAL3:144
for b being non zero Nat holds 2 -root ((b |^ 2) + 2) is irrational
proof end;

theorem Th35: :: NUMERAL3:145
for a, b being non zero Nat st b <= 2 * a holds
2 -root ((a |^ 2) + b) is irrational
proof end;

theorem :: NUMERAL3:146
for a, b being non zero Nat st 2 -root ((a |^ 2) + (b |^ 2)) is natural holds
b |^ 2 > 2 * a by Th35;

theorem :: NUMERAL3:147
for a, b being Nat st a > b holds
2 -root (((a |^ 2) + (2 * b)) + 1) is irrational
proof end;

theorem :: NUMERAL3:148
for a, b being non zero Nat st b <= 2 * a holds
2 -root (((a + 1) |^ 2) - b) is irrational
proof end;

theorem :: NUMERAL3:149
for a being prime Nat
for b being non zero Nat
for n being non trivial Nat st b < a |^ n & a divides b holds
n -root b is irrational by Th21;

theorem :: NUMERAL3:150
for a, b being non zero Nat
for n being non trivial Nat st b < (Radical a) |^ n & Radical a divides b holds
n -root b is irrational by Th21;

theorem :: NUMERAL3:151
for a being prime Nat
for n being non trivial Nat
for b, m being Nat st not a divides b & not n divides m holds
n -root ((a |^ m) * b) is irrational
proof end;

theorem :: NUMERAL3:152
for a being square-free Nat
for n being non trivial Nat holds
( n -root a is Rational iff a = 1 )
proof end;

theorem :: NUMERAL3:153
for a being Nat
for n being non zero Nat st n -root a is rational holds
( n -root (Parity a) is rational & n -root (Oddity a) is rational )
proof end;

theorem :: NUMERAL3:154
for a, b being Nat holds (a + (((sqrt 2) * (1 + (sqrt 2))) * b)) * (a + (((sqrt 2) * ((sqrt 2) - 1)) * b)) is rational
proof end;

:: Examples of concrete facts
theorem :: NUMERAL3:155
2 -root ((123 |^ 4) - 1) is irrational
proof end;

theorem :: NUMERAL3:156
3 -root ((678 |^ 9) + 1) is irrational
proof end;