:: Rational Numbers, Irrational Roots and Numeral Representations
:: by Rafa{\l} Ziobro
::
:: Received July 2, 2026
:: Copyright (c) 2026 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 4.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/4.0/.
environ
vocabularies ABIAN, NUMBERS, NAT_1, INT_1, FINSEQ_1, ARYTM_3, XXREAL_0,
CARD_1, ARYTM_1, COMPLEX1, RELAT_1, REAL_1, XCMPLX_0, ORDINAL1, ORDINAL4,
NEWTON, POWER, FUNCT_1, CARD_3, RFINSEQ, XBOOLE_0, ABSVALUE, ZFMISC_1,
COMPLEX3, NUMERAL1, AFINSQ_1, JORDAN3, VALUED_0, FUNCOP_1, INT_2,
PYTHTRIP, MOEBIUS1, NAT_3, IRRAT_1, RAT_1, SQUARE_1, NEWTON05;
notations ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0, POWER, INT_1, ABIAN,
TARSKI, XBOOLE_0, NAT_D, COMPLEX3, NUMERAL1, AFINSQ_1, VALUED_0,
AFINSQ_2, CARD_1, RELAT_1, VALUED_1, FUNCT_1, RELSET_1, FUNCOP_1,
COMSEQ_3, ABSVALUE, INT_2, IRRAT_1, PYTHTRIP, MOEBIUS1, NEWTON03, RAT_1,
SQUARE_1, NEWTON05;
constructors NAT_D, ABIAN, RELSET_1, COMPLEX3, NUMERAL1, RECDEF_1, AFINSQ_2,
RVSUM_4, PARTFUN3, ABSVALUE, MOEBIUS1, NEWTON03, PYTHTRIP, PEPIN,
NEWTON05;
registrations AFINSQ_1, ABIAN, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1,
NEWTON, XCMPLX_0, WSIERP_1, POWER, NAT_6, NEWTON01, NEWTON02, NEWTON03,
NEWTON04, NEWTON05, REAL_3, VALUED_0, COMPLEX3, RVSUM_4, RELAT_1,
AFINSQ_2, HILB10_2, FUNCOP_1, FUNCT_1, VALUED_1, MEMBERED, ABSVALUE,
NEWTON06, NUMBER11, PARTFUN3, FOMODEL0, SQUARE_1, MOEBIUS1, RAT_1,
BORSUK_5, IRRAT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities XBOOLE_0, ORDINAL1, SQUARE_1, XCMPLX_0;
expansions INT_1, ORDINAL1, FUNCT_1, INT_2, NAT_2, NEWTON03, COMPLEX3,
MOEBIUS1;
theorems INT_2, NAT_1, ABSVALUE, INT_1, NEWTON, XCMPLX_1, XREAL_1, XXREAL_0,
NAT_D, POWER, NUMERAL2, NEWTON03, FUNCT_1, TARSKI, NAT_2, VALUED_1,
COMPLEX3, PRE_FF, NUMERAL1, AFINSQ_1, CARD_1, AFINSQ_2, RVSUM_4,
NUMBER13, REAL_3, RADIX_1, NEWTON06, RING_3, PREPOWER, WSIERP_1,
COMPLEX1, INT_4, NEWTON01, NAT_5, INT_6, NAT_6, PEPIN, PYTHTRIP, NAT_3,
SERIES_4, NEWTON02, NTALGO_1, MOEBIUS1, SQUARE_1, RAT_1, NEWTON05;
begin :: Preliminaries
registration ::: partially present in COMPLEX3, move there
let a be heavy positive Real, n be non zero Nat;
cluster n-root a -> heavy positive;
coherence
proof
A1: a >= 0 & n >= 1 by NAT_1:14;
a > 1 by COMPLEX3:1; then
n-root a > n-root 1 by A1,POWER:17;
hence thesis;
end;
end;
registration ::: move to NEWTON06
let a be Integer, n be Nat;
reduce a|^(n + 1) div a|^n to a;
reducibility
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose a is non zero; then
reconsider a as non zero Integer;
(a*a|^n) div a|^n = a;
hence thesis by NEWTON:6;
end;
end;
end;
registration
let a be even Nat;
reduce a/2 mod a to a/2;
reducibility
proof
per cases;
suppose
a = 0;
hence thesis;
end;
suppose
a <> 0; then
reconsider b = a/2 as non zero Nat;
b + b > b + 0 by XREAL_1:6;
hence thesis;
end;
end;
end;
registration ::: to NEWTON06?
let a be even Nat;
let n be non trivial Nat;
cluster a|^n mod (2*a) -> zero;
coherence
proof
reconsider m = n - 1 as non zero Nat;
a|^n mod (2*a) = 2*a|^(m + 1)/2 mod (2*a)
.= 2*(a|^m*a)/2 mod (2*a) by NEWTON:6
.= (2*a)*(a|^m/2) mod (2*a);
hence thesis;
end;
end;
registration
let a be odd Nat;
reduce ((a - 1)/2) mod a to (a - 1)/2;
reducibility
proof
reconsider b = (a + 1)/2 as non zero Nat;
(a - 1)/2 + b > (a - 1)/2 + 0 by XREAL_1:6;
hence thesis;
end;
let n be non zero Nat;
reduce a|^n mod (2*a) to a;
reducibility
proof
reconsider m = n - 1 as Nat;
reconsider b = (a|^m - 1)/2 as Nat;
a|^n mod (2*a) = a|^(m+1) mod (2*a)
.= a*a|^m mod (2*a) by NEWTON:6
.= ((2*a)*b + a) mod (2*a)
.= (((2*a)*b) mod (2*a) + (a mod (a + a))) mod (2*a) by NAT_D:66;
hence thesis;
end;
end;
registration ::: NEWTON06
let a be Nat, b be non trivial Nat;
reduce a mod (a*b) to a;
reducibility;
end;
registration ::: NEWTON06
let a be Nat, b be non trivial Nat;
cluster a div (a*b) -> zero;
coherence;
end;
registration ::: similar present in NEWTON06
let a be Nat, b be Nat;
let c be non zero Nat;
reduce (a mod b) mod (b*c) to a mod b;
reducibility
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0; then
reconsider a as non zero Nat;
per cases;
suppose b = 0;
hence thesis;
end;
suppose b <> 0; then
reconsider b as non zero Nat;
b <= b*c by NEWTON:33,NAT_1:14;
hence thesis;
end;
end;
end;
end;
registration
let a be non trivial odd Nat;
reduce ((a + 1)/2) mod a to (a + 1)/2;
reducibility
proof
reconsider b = (a - 1)/2 as non zero Nat;
(a + 1)/2 + b > (a + 1)/2 + 0 by XREAL_1:6;
hence thesis;
end;
end;
:: Subsequent integers
theorem NAT162: ::: generalization of NAT_1:62 for integers
for a,b be Integer, n be Nat holds a <= b <= a + n implies
b = a + 0 or ... or b = a + n
proof
let a,b be Integer, n be Nat;
assume a <= b <= a + n; then
A2: a - a <= b - a <= (a + n) - a by XREAL_1:9; then
reconsider k = b - a as Nat;
b = a + k;
hence thesis by A2;
end;
theorem INT17: ::: kind of INT_1:7
for a,b be Integer holds a <= b <= a + 1 iff b = a or b = a + 1
proof
let a,b be Integer;
A1: a <= b <= a + 1 implies b = a + 0 or ... or b = a + 1 by NAT162;
b = a or b = a + 1 implies a <= b <= a + 1
proof
assume b = a or b = a + 1; then
per cases;
suppose
C1: b = a;
b + 0 < b + 1 by XREAL_1:6;
hence thesis by C1;
end;
suppose
C1: b = a + 1;
a + 0 < a + 1 by XREAL_1:6;
hence thesis by C1;
end;
end;
hence thesis by A1;
end;
:: Use of sgn for identifying classes of numbers
registration
let a be non integer Real;
cluster sgn frac a -> weightless positive;
coherence by ABSVALUE:def 2;
end;
registration
let a be non integer Real;
reduce a*(sgn (frac a)) to a;
reducibility
proof
sgn frac a = 1 by ABSVALUE:def 2;
hence thesis;
end;
end;
registration ::: for positive present in NEWTON06
let a be light non negative Real;
reduce frac a to a;
reducibility
proof
a = [\a/] + (frac a) by INT_1:42;
hence thesis;
end;
end;
theorem A17: :: see ABSVALUE:17
for r be Real holds
r*(sgn r) = |.r.| & r/(sgn r) = |.r.| & r = |.r.|/(sgn r)
proof
let r be Real;
per cases;
suppose r is zero;
hence thesis;
end;
suppose r is positive; then
sgn r = 1 & |.r.| = r by ABSVALUE:def 1,ABSVALUE:def 2;
hence thesis;
end;
suppose
r is negative; then
sgn r = -1 & |.r.| = -r by ABSVALUE:def 1,ABSVALUE:def 2;
hence thesis;
end;
end;
theorem
for r be Real holds [\|.r.|/] + frac |.r.| = r*(sgn r)
proof
let r be Real;
[\|.r.|/] + frac |.r.| = |.r.| by INT_1:42
.= r*(sgn r) by A17;
hence thesis;
end;
theorem
for r be heavy Real holds sgn r = sgn [\r/] & sgn r = sgn [/r\]
proof
let r be heavy Real;
per cases;
suppose
r is negative; then
reconsider r as negative Real;
sgn [\r/] = -1 & sgn [/r\] = -1 & sgn r = -1 by ABSVALUE:def 2;
hence thesis;
end;
suppose
r is positive; then
reconsider r as positive Real;
sgn [\r/] = 1 & sgn [/r\] = 1 & sgn r = 1 by ABSVALUE:def 2;
hence thesis;
end;
end;
theorem
for a be Real holds sgn (frac a) = sgn (frac -a)
proof
let a be Real;
per cases;
suppose a is integer;
hence thesis;
end;
suppose not a is integer; then
sgn frac a = 1 & sgn frac -a = 1 by COMPLEX3:1;
hence thesis;
end;
end;
theorem FL:
for a be Real holds [\a/] + [\-a/] + sgn (frac a) = 0
proof
let a be Real;
per cases;
suppose a is integer; then
reconsider a as Integer;
[\a/] = a & [\-a/] = -a & sgn (frac a) = 0;
hence thesis;
end;
suppose not a is integer; then
reconsider a as non integer Real;
[\a/] < a & [\-a/] < -a by INT_1:26; then
[\a/] + [\-a/] < a + (-a) by XREAL_1:8; then
A1: [\a/] + [\-a/] <= -1 by INT_1:8;
a - 1 < [\a/] & -a - 1 < [\-a/] by INT_1:def 6; then
(a - 1) + (-a - 1) < [\a/] + [\-a/] by XREAL_1:8; then
-2 + 1 <= [\a/] + [\-a/] by INT_1:7; then
[\a/] + [\-a/] = -1 by A1,XXREAL_0:1
.= -sgn (frac a) by COMPLEX3:1; then
[\a/] + [\-a/] + sgn (frac a) = 0;
hence thesis;
end;
end;
theorem FLM:
for a be non integer Real holds [\a/] + [\-a/] = -1
proof
let a be non integer Real;
sgn (frac a) = 1 by COMPLEX3:1; then
[\a/] + [\-a/] + 1 = 0 by FL;
hence thesis;
end;
theorem FAA:
for a be non integer Real holds frac a + (frac (-a)) = 1
proof
let a be non integer Real;
frac a = a - [\a/] & frac (-a) = -a -[\-a/] by INT_1:def 8; then
frac a + (frac (-a)) = -([\a/] + [\-a/])
.= -(-1) by FLM;
hence thesis;
end;
theorem
for r be Real holds
frac |.r.| = sgn(frac r)*(1/2 + (sgn r)*((frac r) -1/2))
proof
let r be Real;
per cases;
suppose r is integer; then
frac |.r.| = 0 & frac r = 0;
hence thesis;
end;
suppose not r is integer; then
reconsider r as non integer Real;
per cases;
suppose r is positive; then
reconsider r as positive Real;
r = |.r.| & sgn r = 1 & sgn (frac r) = 1 by ABSVALUE:def 2;
hence thesis;
end;
suppose r is negative; then
reconsider r as negative Real;
B2: sgn r = -1 & sgn (frac r) = 1 by ABSVALUE:def 2;
1/2 + (sgn r)*((frac r) - 1/2) = 1/2 + (-1)*((frac r) - 1/2)
by ABSVALUE:def 2
.= 1 - (frac r)
.= (frac r) + (frac (-r)) - (frac r) by FAA
.= frac |.r.| by ABSVALUE:def 1;
hence thesis by B2;
end;
end;
end;
theorem
for r be Real holds [/r\] = [\r/] + sgn frac r
proof
let r be Real;
per cases;
suppose r is integer; then
reconsider r as integer Real;
[/r\] = [\r/] + sgn (frac r);
hence thesis;
end;
suppose not r is integer; then
reconsider r as non integer Real;
reconsider f = frac r as positive Real;
[/r\] = [\r/] + 1 by INT_1:34,41
.= [\r/] + sgn f by ABSVALUE:def 2;
hence thesis;
end;
end;
theorem ::: NAT_D:21, move there
for a,b,c be Integer holds a mod b = (b*c + a) mod b
proof
let a,b,c be Integer;
per cases;
suppose b is zero;
hence thesis;
end;
suppose b is non zero; then
reconsider b as non zero Integer;
(a mod b) = a - b*(a div b) by INT_1:def 10
.= a + b*c - b*((a div b) + c)
.= (a + b*c) - b*((a + b*c) div b) by NAT_D:61
.= (a + b*c) mod b by INT_1:def 10;
hence thesis;
end;
end;
theorem
for a,b be non zero Nat, c be Nat holds
c mod (a*b) mod b = (c mod b) mod (a*b) by RADIX_1:3;
theorem FCA:
for a be Real holds [\a/] = -[/-a\]
proof
let a be Real;
per cases;
suppose a is integer; then
[\a/] = a & -(-a) = -[/-a\] by INT_1:30;
hence thesis;
end;
suppose not a is integer; then
reconsider a as non integer Real;
[\a/] + [\-a/] = -1 by FLM; then
[\a/] = -([\-a/] + 1) & not [/-a\] = [\-a/] by INT_1:34;
hence thesis by INT_1:41;
end;
end;
theorem FCB:
for a be Real holds [/a\] = -[\-a/]
proof
let a be Real;
reconsider b = -a as Real;
[\b/] = -[/-b\] by FCA;
hence thesis;
end;
theorem
for a be weightless negative Real holds [\a/] = -1 by COMPLEX3:1;
theorem
for a be weightless positive Real holds [/a\] = 1 by COMPLEX3:1;
theorem
for a be Real holds frac a = frac (-a) iff 2*a is integer
proof
let a be Real;
per cases;
suppose a is integer; then
frac a = 0 & 0 = frac (-a) & 2*a is integer;
hence thesis;
end;
suppose not a is integer; then
reconsider a as non integer Real;
B1: frac a = frac (-a) implies 2*a is integer
proof
assume frac a = frac (-a); then
(frac a) + (frac a) = 1 by FAA; then
2*[\a/] + 1 = 2*([\a/] + (frac a))
.= 2*a by INT_1:42;
hence thesis;
end;
2*a is integer implies frac a = frac (-a)
proof
assume
C1: 2*a is integer;
2*a = 2*([\a/] + frac a) by INT_1:42
.= 2*[\a/] + 2*(frac a); then
2*(frac a) is integer by C1; then
reconsider k = 2*(frac a) as Nat;
frac a < 1 by COMPLEX3:1; then
k < 2*1 by XREAL_1:68; then
C3: 2*(frac a) = 0 or 2*(frac a) = 1 by NAT_1:23;
frac a = 1/2 implies frac a + (frac (-a)) = 1 by FAA;
hence thesis by C3;
end;
hence thesis by B1;
end;
end;
theorem
for a,b be Integer holds a div (-b) = (-a) div b
proof
let a,b be Integer;
(a div (-b)) = (-a) div (-(-b)) by NEWTON06:35;
hence thesis;
end;
theorem NATD1: :: see NAT_D:1
for a be Real, b be non zero Nat holds (frac (a/b)) * b < b
proof
let a be Real, b be non zero Nat;
frac (a/b) < 1 by COMPLEX3:1; then
(frac (a/b))*b < 1*b by XREAL_1:68;
hence thesis;
end;
theorem AMB:
for a,b be Integer st not b divides a holds a mod b + ((-a) mod b) = b
proof
let a,b be Integer;
assume
A1: not b divides a; then
reconsider a as non zero Integer by INT_2:12;
per cases;
suppose b = 0; then
reconsider b as zero Integer;
a mod b = 0 & ((-a) mod b) = 0;
hence thesis;
end;
suppose b <> 0; then
reconsider b as non zero Integer;
reconsider r = a/b as non integer Real by A1,NUMBER13:4;
a mod b = b*(frac (a/b)) & -a mod b = b*(frac((-a)/b)) by REAL_3:6; then
(a mod b) + ((-a) mod b) = b*(frac (a/b)) + b*(frac (-a/b))
.= b*((frac r) + (frac (-r)))
.= b*1 by FAA;
hence thesis;
end;
end;
theorem MOD1:
for a,b be Integer holds a mod b = -((-a) mod (-b))
proof
let a,b be Integer;
per cases;
suppose
A1: b = 0; then
a mod b = 0
.= -((-a) mod (-b)) by A1;
hence thesis;
end;
suppose
A1: b <> 0; then
a mod b = a - (a div b)*b by INT_1:def 10
.= a - [\ a/b /]*b by INT_1:def 9
.= -(-a) +([\ a/b /]*(-b))
.= (-(-a) + [\((-a)/(-b))/]*(-b)) by XCMPLX_1:191
.= (-(-a) + ((-a) div (-b))*(-b)) by INT_1:def 9
.= -((-a) - ((-a) div (-b))*(-b))
.= -((-a) mod (-b)) by INT_1:def 10,A1;
hence thesis;
end;
end;
theorem MOD2:
for a,b be Integer holds
a mod (-b) = -((-a) mod b) & (-a) mod b = -(a mod (-b))
proof
let a,b be Integer;
(-a) mod b = - (-(-a) mod (-b)) &
(a mod (-b)) = - ((-a) mod (-(-b))) by MOD1;
hence thesis;
end;
theorem
for a,b be Integer st not b divides a holds a mod b - (a mod (-b)) = b
proof
let a,b be Integer;
assume not b divides a; then
b = a mod b + ((-a) mod b) by AMB
.= a mod b + -(a mod (-b)) by MOD2;
hence thesis;
end;
theorem
for a,b be Real holds
[\a + b/] = [\a/] + [\b/] + [\(frac a) + (frac b)/]
proof
let a,b be Real;
reconsider k = [\a/], l = [\b/] as Integer;
a = k + frac a & b = l + frac b by INT_1:42; then
[\a + b/] = [\(k + l) + ((frac a) + (frac b))/]
.= (k + l) + [\(frac a) + (frac b)/] by INT_1:28;
hence thesis;
end;
theorem MUL:
for a,b be Real holds [\a*b/] = [\a/]*[\b/] +
[\ [\a/]*(frac b) + [\b/]*(frac a) + (frac a)*(frac b) /]
proof
let a,b be Real;
reconsider k = [\a/], l = [\b/] as Integer;
a = k + frac a & b = l + frac b by INT_1:42; then
[\(a * b)/] = [\ (k*l) + (k*(frac b) + l*(frac a) + (frac a)*(frac b))/]
.= (k*l) + [\k*(frac b) + l*(frac a) + (frac a)*(frac b)/] by INT_1:28;
hence thesis;
end;
theorem
for a be Real, b be Integer holds [\a*b/] = [\a/]*b + [\(frac a)*b/]
proof
let a be Real, b be Integer;
[\a*b/] = [\a/]*[\b/] + [\ [\a/]*(frac b) +
[\b/]*(frac a) + (frac a)*(frac b) /] by MUL
.= [\a/]*b + [\(frac a)*b/];
hence thesis;
end;
:: ceiling - floor relations
CF1:
for a be Real holds [/a\] <= [\a/] + 1
proof
let a be Real;
per cases;
suppose a is integer; then
reconsider a as Integer;
[/a\] <= a + 1 by INT_1:def 7;
hence thesis;
end;
suppose not a is integer;
hence thesis by INT_1:34,INT_1:41;
end;
end;
theorem CF2:
for a,b be Real st a <= b holds [/a\] <= [\b/] + 1
proof
let a,b be Real;
assume a <= b; then
A2: [\a/] <= [\b/] & [/a\] <= [/b\] by PRE_FF:9;
[/b\] <= [\b/] + 1 by CF1;
hence thesis by A2,XXREAL_0:2;
end;
theorem
for a,b be Real st a <= b holds [\a/] < [\b/] + 1
proof
let a,b be Real;
assume
A1: a <= b; then
A2: [/a\] <= [\b/] + 1 by CF2;
per cases;
suppose a is integer; then
reconsider a as Integer;
[\a/] = a;
hence thesis by A1,INT_1:29,XXREAL_0:2;
end;
suppose not a is integer;
hence thesis by A2,XXREAL_0:2,INT_1:35;
end;
end;
theorem CFD:
for a,b be Real holds
[\a/b/] = [\[\a/]/b/] + [\frac ([\a/]/b) + (frac a)/b/]
proof
let a,b be Real;
per cases;
suppose
b = 0; then
reconsider b as zero Real;
a/b = 0 & [\a/]/b = 0 & (frac a)/b = 0;
hence thesis;
end;
suppose
b <> 0; then
reconsider b as non zero Real;
[\a/b/] = [\([\a/] + frac a)/b/] by INT_1:42
.= [\[\a/]/b + (frac a)/b/]
.= [\[\[\a/]/b/] + frac ([\a/]/b) + (frac a)/b/] by INT_1:42
.= [\[\[\a/]/b/] + (frac ([\a/]/b) + (frac a)/b)/]
.= [\[\a/]/b/] + [\frac ([\a/]/b) + (frac a)/b/] by INT_1:28;
hence thesis;
end;
end;
theorem LFR:
for a be Real, b be non zero Nat holds
frac ([\a/]/b) + (frac a)/b < 1
proof
let a be Real, b be non zero Nat;
b*(frac ([\a/]/b)) = b*([\a/]/b - [\[\a/]/b/]) by INT_1:def 8
.= b*([\a/]/b) - b*[\[\a/]/b/]
.= [\a/] - b*[\[\a/]/b/] by XCMPLX_1:87; then
reconsider c = b*(frac ([\a/]/b)) as Integer;
A2: c + 1 <= b by INT_1:7,NATD1;
frac a < 1 by COMPLEX3:1; then
c + (frac a) < c + 1 by XREAL_1:6; then
c + (frac a) < b by A2,XXREAL_0:2; then
(c + (frac a))/b < b/b by XREAL_1:74; then
c/b + (frac a)/b < 1 by XCMPLX_1:60;
hence thesis by XCMPLX_1:89;
end;
theorem FFP:
for a be Real, b be positive Integer holds [\a/b/] = [\[\a/]/b/]
proof
let a be Real, b be positive Integer;
b in NAT by INT_1:3; then
reconsider b as non zero Nat;
0 <= frac ([\a/]/b) + (frac a)/b < 1 by LFR; then
reconsider c = frac ([\a/]/b) + (frac a)/b as light non negative
Real by COMPLEX3:1;
[\a/b/] = [\[\a/]/b/] + [\c/] by CFD;
hence thesis;
end;
theorem
for a be Real, b be negative Integer holds [\a/b/] = [\[/a\]/b/]
proof
let a be Real, b be negative Integer;
reconsider k = -b as positive Integer;
[\a/b/] = [\a/(-k)/]
.= [\(-a)/k/] by XCMPLX_1:192
.= [\[\-a/]/k/] by FFP
.= [\(-[\-a/])/b/] by XCMPLX_1:192;
hence thesis by FCB;
end;
theorem
for a be Real, b be positive Real holds -[\a/-b/] >= [\a/b/]
proof
let a be Real, b be positive Real;
-[\a/-b/] = -[\-(a/b)/] by XCMPLX_1:188
.= [/a/b\] by FCB;
hence thesis by INT_1:34,INT_1:35;
end;
theorem FBC:
for a,b be Real holds
[\a/] <= b <= [/a\] implies [\a/] = [\b/] or [/a\] = [/b\]
proof
let a,b be Real;
assume
A1: [\a/] <= b <= [/a\]; then
A2: [\[\a/]/] <= [\b/] & [/b\] <= [/[/a\]\] by PRE_FF:9;
A3: [/a\] <= [\a/] + 1 & [/b\] <= [\b/] + 1 by CF1; then
per cases by XXREAL_0:1;
suppose
B1: [/b\] = [\b/] + 1;
[\a/] + 1 <= [/b\] & [/b\] <= [\a/] + 1
by XREAL_1:6,B1,A2,A3,XXREAL_0:2; then
[\a/] + 1 = [/b\] by XXREAL_0:1;
hence thesis by B1;
end;
suppose
[/b\] < [\b/] + 1; then
reconsider b as Integer by INT_1:41,INT_1:34;
B3: [\a/] <= b <= [\a/] + 1 by A1,A3,XXREAL_0:2;
per cases by INT_1:41;
suppose
[\a/] = [/a\]; then
reconsider a as Integer by INT_1:34;
b = a by A1,XXREAL_0:1;
hence thesis;
end;
suppose
[\a/] + 1 = [/a\];
hence thesis by B3,INT17;
end;
end;
end;
theorem
for a be Real, b be non integer Real st [\a/] <= b <= [/a\] holds
[\a/] = [\b/] & [/a\] = [/b\]
proof
let a be Real, b be non integer Real;
assume
A1: [\a/] <= b <= [/a\]; then
reconsider a as non integer Real by XXREAL_0:1;
[\a/] < [/a\] & [\b/] < [/b\] by INT_1:35; then
A3: [\a/] + 1 = [/a\] & [\b/] + 1 = [/b\] by INT_1:41;
per cases by A1,FBC;
suppose
[\a/] = [\b/];
hence thesis by A3;
end;
suppose
[/a\] = [/b\];
hence thesis by A3;
end;
end;
theorem N227: :: see NAT_2:27
for a,b be Integer, c be Nat holds [\a/(b*c)/] = [\[\a/b/]/c/]
proof
let a,b be Integer, c be Nat;
per cases;
suppose b = 0 or c = 0; then
a/(b*c) = 0 & (a/b = 0 or [\a/b/]/c = 0);
hence thesis;
end;
suppose
B1: b <> 0 & c <> 0; then
reconsider b as non zero Integer;
reconsider c as positive Integer by B1;
[\a/(b*c)/] = [\(a/b)/c/] by XCMPLX_1:78
.= [\[\a/b/]/c/] by FFP;
hence thesis;
end;
end;
theorem
for a be Integer, b be non zero Integer, c be negative Integer holds
[\a/(b*c)/] = [\[\-a/b/]/(-c)/]
proof
let a be Integer, b be non zero Integer, c be negative Integer;
-c in NAT by INT_1:3; then
reconsider k = -c as Nat;
[\[\-a/b/]/(-c)/] = [\[\(-a)/b/]/k/]
.= [\(-a)/(b*k)/] by N227
.= [\(-a)/(-(b*c))/]
.= [\a/(b*c)/] by XCMPLX_1:191;
hence thesis;
end;
theorem
for a be Integer, b be non zero Integer holds
[\a/b/] = -[\-a/b/] implies b divides a
proof
let a be Integer,b be non zero Integer;
assume
A1: [\a/b/] = -[\-a/b/];
0 = [\a/b/] + [\-a/b/] + sgn (frac (a/b)) by FL
.= sgn (frac (a/b)) by A1; then
reconsider x = a/b as Integer;
a = x*b by XCMPLX_1:87;
hence thesis;
end;
theorem
for a be Integer, b be negative Integer holds
[\a/b/] = - ([\a/-b/] + sgn frac (a/b))
proof
let a be Integer, b be negative Integer;
0 = [\a/b/] + [\-a/b/] + sgn (frac (a/b)) by FL
.= [\a/b/] + [\a/-b/] + sgn (frac (a/b)) by XCMPLX_1:188;
hence thesis;
end;
:: Divisibility
NAT227: ::: version of PRE_FF:5, see NAT_2:27
for a,b be Integer, c be Nat holds (a div b) div c = a div (b*c)
proof
let a,b be Integer, c be Nat;
a div b = [\a/b/] & [\a/b/] div c = [\[\a/b/]/c/] &
a div (b*c) = [\a/(b*c)/] by INT_1:def 9;
hence thesis by N227;
end;
theorem ABC:
for a be Integer, b be non zero Integer, c be non zero Nat holds
a mod (b*c) = a mod b + b*((a div b) mod c)
proof
let a be Integer, b be non zero Integer, c be non zero Nat;
A1: (a div b) = ((a div b) mod c) + c*((a div b) div c) &
a mod (b*c) + b*c*(a div (b*c)) = a &
a = a mod b + b*(a div b) by INT_1:59; then
a mod (b*c)
= a mod b + b*((a div b) - c*(a div (b*c)))
.= a mod b + b*((a div b) - c*((a div b)div c)) by NAT227
.= a mod b + b*((a div b)mod c) by A1;
hence thesis;
end;
theorem
for a be Nat, b,c be non zero Nat holds
a div c = ((a div c) mod b) + b*(a div (b*c))
proof
let a be Nat,b,c be non zero Nat;
(a div c) = ((a div c) mod b) + b*((a div c) div b) by NAT_D:2
.= (a div c) mod b + b*(a div (b*c)) by NAT_2:27;
hence thesis;
end;
theorem ABLK:
for a be Integer, b be non zero Nat, k,l be Nat holds (a mod b|^(k+l)) =
(a mod b|^k) + ((a div b|^k) mod b|^l)*b|^k
proof
let a be Integer, b be non zero Nat, k,l be Nat;
b|^(k + l) = b|^k*b|^l by NEWTON:8;
hence thesis by ABC;
end;
theorem MD:
for a,n be Nat, b be non zero Nat holds a mod b|^n = a - b|^n*(a div b|^n)
proof
let a,n be Nat, b be non zero Nat;
a = (a mod b|^n) + (b|^n)*(a div b|^n) by NAT_D:2;
hence thesis;
end;
theorem DNK:
for a,b,n,k be Nat holds a div b|^(n + k) = (a div b|^n) div b|^k
proof
let a,b,n,k be Nat;
a div (b|^n*b|^k) = (a div b|^n) div b|^k by NAT_2:27;
hence thesis by NEWTON:8;
end;
theorem RMD:
for a,n,k be Nat, b be 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
let a,n,k be Nat, b be non zero Nat;
a = b|^(n+k)*(a div b|^(n + k)) + (a mod b|^(n+k)) &
a = b|^n*(a div b|^n) + (a mod b|^n) by NAT_D:2; then
a mod b|^(n+k) - (a mod b|^n) =
b|^n*(a div b|^n) - b|^(n+k)*(a div b|^(n + k))
.= b|^n*(a div b|^n) - b|^n*b|^k*(a div b|^(n + k)) by NEWTON:8
.= b|^n*((a div b|^n) - b|^k*(a div b|^(n + k)));
hence thesis;
end;
theorem
for a,n,k be Nat, b be non zero Nat holds
a div b|^n = (a div b|^(n + k))*b|^k + ((a div b|^n) mod b|^k)
proof
let a,n,k be Nat, b be non zero Nat;
(a mod b|^(n+k)) - (a mod b|^n) =
(a mod b|^n) + ((a div b|^n) mod b|^k)*b|^n - (a mod b|^n)
by ABLK; then
b|^n*((a div b|^n)-(a div b|^(n + k))*b|^k) =
((a div b|^n) mod b|^k)*b|^n by RMD; then
((a div b|^n) - (a div b|^(n + k))*b|^k) = ((a div b|^n) mod b|^k)
by XCMPLX_1:5;
hence thesis;
end;
theorem MRD:
for a,n,k be Nat, b be 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
let a,n,k be Nat, b be non zero Nat;
(a div b|^n) - (a div b|^(n + k))*b|^k =
(b|^n*((a div b|^n)-(a div b|^(n + k))*b|^k)) div b|^n
.= ((a mod b|^(n+k)) - (a mod b|^n)) div b|^n by RMD;
hence thesis;
end;
theorem
for a,n be Nat, b be 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
for a,n be Nat, b be non zero Nat holds
a mod b|^(n+1) div b|^n < b
proof
let a,n be Nat, b be non zero Nat;
A1: (a mod b|^(n+1)) div b|^(n + 1) = (a mod b|^(n + 1)) div (b|^n*b)
by NEWTON:6
.= (a mod b|^(n + 1) div b|^n) div b by PRE_FF:5;
assume not thesis; then
((a mod b|^(n + 1)) div b|^n) div b >= b div b by NAT_2:24;
hence contradiction by A1;
end;
theorem
for a,n be Nat, b be 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
let a,n be Nat, b be non zero Nat;
(a mod b|^n) = a - b|^n*(a div b|^n) &
(a mod b|^(n + 1)) = a - b|^(n + 1)*(a div b|^(n+1)) by MD; then
(a mod b|^(n + 1)) - (a mod b|^n) =
b|^n*(a div b|^n) - b|^(n + 1)*(a div b|^(n + 1))
.= b|^n*(a div b|^n) - b|^n*b*(a div b|^(n + 1)) by NEWTON:6
.= b|^n*((a div b|^n) - b*(a div b|^(n + 1)));
hence thesis;
end;
theorem DMK:
for a,n,k be Nat, b be 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
let a,n,k be Nat, b be non zero Nat;
(a mod b|^n) = a - b|^n*(a div b|^n) &
(a mod b|^(n + k)) = a - b|^(n + k)*(a div b|^(n+k)) by MD; then
(a mod b|^(n + k)) - (a mod b|^n) =
b|^n*(a div b|^n) - b|^(n + k)*(a div b|^(n + k))
.= b|^n*(a div b|^n) - b|^n*b|^k*(a div b|^(n + k)) by NEWTON:8
.= b|^n*((a div b|^n) - b|^k*(a div b|^(n + k)));
hence thesis;
end;
theorem
for a,n,k be Nat, b be non zero Nat holds
(a mod b|^(n+k)) - (a mod b|^n) = b|^n*((a div b|^n) mod b|^k)
proof
let a,n,k be Nat, b be non zero Nat;
A1: (a div b|^n) = b|^k*((a div b|^n) div b|^k) + ((a div b|^n) mod b|^k)
by NAT_D:2;
(a mod b|^(n+k)) - (a mod b|^n) = b|^n*((a div b|^n) -
b|^k*(a div b|^(n+k))) by DMK
.= b|^n*((a div b|^n) - b|^k*((a div b|^n) div b|^k)) by DNK
.= b|^n*((a div b|^n) mod b|^k) by A1;
hence thesis;
end;
theorem DAS:
for a,n,k be Nat, b be non zero Nat holds
b|^n divides (a mod b|^(n + k)) - (a mod b|^n)
proof
let a,n,k be Nat, b be non zero Nat;
(a mod b|^(n+k)) - (a mod b|^n) =
b|^n*((a div b|^n) - b|^k*(a div b|^(n+k))) by DMK;
hence thesis;
end;
theorem
for a,n,k be Nat, b be non zero Nat holds
((a mod b|^(n+k)) - (a mod b|^n)) mod b|^n = 0
proof
let a,n,k be Nat, b be non zero Nat;
b|^n divides (a mod b|^(n + k)) - (a mod b|^n) by DAS;
hence thesis;
end;
theorem
for a,n,k be Nat, b be 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
let a,n,k be Nat, b be non zero Nat;
a mod b|^(n + k) + b|^(n + k)*(a div b|^(n + k)) = a &
a = a mod b|^n + b|^n *(a div b|^n) by NAT_D:2;
hence thesis;
end;
theorem DHS:
for a,b,n be Nat holds a mod b|^n <= a mod b|^(n + 1)
proof
let a,b,n be Nat;
per cases;
suppose b = 0; then
reconsider b as zero Nat;
per cases;
suppose n = 0;
a mod b|^n = a mod 1;
hence thesis;
end;
suppose n <> 0;
a mod b|^n = a mod 0;
hence thesis;
end;
end;
suppose b > 0; then
b >= 1 by NAT_1:14; then
per cases by XXREAL_0:1;
suppose b = 1;
hence thesis;
end;
suppose b > 1; then
reconsider b as non trivial Nat by NEWTON03:def 1;
assume
A1: not thesis;
a mod b|^n < b|^n by NAT_D:1; then
(a mod b|^(n+1)) < b|^n by A1,XXREAL_0:2; then
(a mod b|^n) mod b|^n > (a mod b|^(n +1)) mod b|^n by A1,NAT_D:24; then
(a mod b|^n) mod b|^n > (a mod (b*b|^n)) mod b|^n by NEWTON:6;
hence contradiction by RADIX_1:3;
end;
end;
end;
registration
let a,b,n be Nat;
cluster (a mod b|^(n + 1)) - (a mod b|^n) -> natural;
coherence
proof
a mod b|^n - (a mod b|^n) <= (a mod b|^(n + 1)) - (a mod b|^n)
by XREAL_1:9,DHS;
hence thesis;
end;
end;
theorem
for a be Nat, b be Nat holds a div b|^2 = (a div b) div b
proof
let a be Nat, b be Nat;
a div b|^2 = a div (b*b) by NEWTON:81
.= (a div b) div b by NAT_2:27;
hence thesis;
end;
theorem
for a be Nat, b be non trivial Nat holds
(a div b) = ((a div b|^0) - (a mod b|^1)) div b
proof
let a be Nat, b be non trivial Nat;
(a mod b|^1) = a - b|^1*(a div b|^1) by MD; then
a div b = ((a div 1*b|^0) - (a mod b|^1)) div b;
hence thesis;
end;
theorem
for a be Nat, b be non trivial Nat holds
a div b|^2 = ((a div b|^0) - (a mod b|^2)) div b|^2
proof
let a be Nat, b be non trivial Nat;
(a mod b|^2) = a - b|^2*(a div b|^2) by MD; then
a div b|^2 = ((a div 1*b|^0) - (a mod b|^2)) div b|^2;
hence thesis;
end;
theorem
for a,n be Nat, b be 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
for a be Nat, b be non trivial Nat holds
ex n be Nat st a < b|^n
proof
let a be Nat, b be non trivial Nat;
reconsider d = log (b,a + 1) as Real;
reconsider c = [/d\] as Integer;
A1: b >= 1 & d <= [/d\] by INT_1:def 7,NEWTON03:def 1; then
A2: b to_power d <= b to_power [/d\] by PRE_FF:8;
a + 0 < a + 1 by XREAL_1:6; then
A3: a < b to_power c by A2,XXREAL_0:2;
per cases;
suppose
c <= 0; then
b to_power c <= b to_power 0 by A1,PRE_FF:8; then
a < b to_power 0 by A3,XXREAL_0:2;
hence thesis;
end;
suppose
c > 0; then
c in NAT by INT_1:3; then
reconsider c as Nat;
a < b |^c by A3,POWER:41;
hence thesis;
end;
end;
theorem
for a,b be non trivial Nat holds
ex n be Nat st b|^n <= a < b|^(n + 1)
proof
let a,b be non trivial Nat;
reconsider c = log (b,a) as Real;
A1: b > 1 by NEWTON03:def 1;
b to_power c > 1 by NEWTON03:def 1; then
c >= 0; then
[\c/] in NAT by INT_1:3; then
reconsider d = [\c/] as Nat;
d <= c & c < d + 1 by INT_1:def 6,INT_1:29; then
b to_power d <= b to_power c < b to_power (d + 1) by POWER:39,PRE_FF:8,A1;
hence thesis;
end;
begin :: Some registrations for (X)FinSequences
registration ::: AFINSQ_1
let n,k be Nat;
let f be (n+k)-element complex-valued XFinSequence;
cluster (f|n)^<%0%> -> complex-valued;
coherence;
end;
registration ::: AFINSQ_1
let n be Nat;
let f be (n+1)-element complex-valued XFinSequence;
reduce (f|n)^<%f.n%> to f;
reducibility
proof
dom ((f|n)^<%f.n%>) = n + 1 & dom f = n + 1 by CARD_1:def 7;
hence thesis by AFINSQ_1:56;
end;
end;
registration ::: AFINSQ_1
let k be Complex, f be complex-valued XFinSequence;
cluster f^<%k%> -> complex-valued;
coherence;
end;
registration ::: AFINSQ_1
let m,n be Nat, D be non empty set;
let f be m-element D-valued XFinSequence,
g be n-element D-valued XFinSequence;
reduce (f^g)|m to f;
reducibility
proof
A0: len (f^g) = m + n by CARD_1:def 7;
A0a: m + 0 <= m + n by XREAL_1:6;
A1: len ((f^g) | m) = m by CARD_1:def 7
.= len f by CARD_1:def 7;
for k be Nat st k in dom f holds f.k = ((f^g) |m).k
proof
let k be Nat such that
B1: k in dom f;
dom f = m by CARD_1:def 7; then
((f^g) |m).k = (f^g).k by A0,A0a,B1,AFINSQ_1:53
.= f.k by B1,AFINSQ_1:def 3;
hence thesis;
end;
hence thesis by A1;
end;
end;
theorem Th23:
for n,i be Nat, k be Complex st n <> i holds ((n --> 0)^<%k%>).i = 0
proof
let n,i be Nat, k be Complex such that
A1: n <> i;
per cases by A1,XXREAL_0:1;
suppose
n > i; then
len (n --> 0) > i; then
((n --> 0)^<%k%>).i = (n --> 0).i by AFINSQ_1:51
.= 0;
hence thesis;
end;
suppose
n < i; then
i >= n + 1 by INT_1:7; then
i >= len ((n --> 0)^<%k%>) by CARD_1:def 7; then
not i in dom ((n --> 0)^<%k%>) by AFINSQ_1:86;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem RXF:
for n be Nat, f be (n+1)-element complex-valued XFinSequence holds
f = ((f|n)^<%0%>) + ((n --> 0)^<%f.n%>)
proof
let n be Nat, f be (n+1)-element complex-valued XFinSequence;
reconsider g = (f|n)^<%0%> as (n+1)-element complex-valued XFinSequence;
reconsider h = (n --> 0)^<%f.n%>
as (n+1)-element complex-valued XFinSequence;
A1: dom (g + h) = (n + 1) /\ (n+1) by CARD_1:def 7;
for i be Nat st i in dom f holds f.i = (g + h).i
proof
let i be Nat such that
B1: i in dom f;
per cases;
suppose
C1: i = n;
i in dom (g + h) by CARD_1:def 7,A1,B1; then
(g + h).i = g.i + h.i by VALUED_1:def 1;
hence thesis by C1;
end;
suppose
C1: i <> n;
i in Segm (n + 1) by CARD_1:def 7,B1; then
i < n + 1 by NAT_1:44; then
i <= n by INT_1:7; then
C3: i < n by C1,XXREAL_0:1; then
i in Segm n by NAT_1:44; then
i in dom (n --> 0) & i in dom (f|n) by CARD_1:def 7; then
C5: (f|n).i = ((f|n)^(f/^n)).i by AFINSQ_1:def 3
.= f.i;
len (n --> 0) = n & len (f|n) = n by CARD_1:def 7; then
((n --> 0)^<%f.n%>).i = (n --> 0).i & ((f|n)^<%0%>).i = (f|n).i
by C3,AFINSQ_1:51; then
C6: g.i = f.i & h.i = 0 by C5;
i in dom (g + h) by CARD_1:def 7,A1,B1; then
(g + h).i = g.i + h.i by VALUED_1:def 1;
hence thesis by C6;
end;
end;
hence thesis by CARD_1:def 7,A1;
end;
registration
let n be Nat, f be (n+1)-element complex-valued XFinSequence;
reduce ((f|n)^<%0%>) + ((n --> 0)^<%f.n%>) to f;
reducibility by RXF;
end;
begin :: Digits and Values
registration
let f be empty-yielding XFinSequence of NAT;
let b be Nat;
cluster value (f,b) -> zero;
coherence
proof
consider x be XFinSequence of NAT such that
A1: (dom x = dom f & for i be Nat st i in dom x
holds x.i = (f.i)*(b|^i)) & value(f,b) = Sum x by NUMERAL1:def 1;
for i be Nat st i in dom x holds x.i = f.i
proof
let i be Nat such that
B1: i in dom x;
x.i = (f.i)*(b|^i) by B1,A1;
hence thesis;
end; then
x = f by A1;
hence thesis by A1;
end;
end;
registration
let n be Nat, b be non trivial Nat;
reduce value (digits (n,b),b) to n;
reducibility by NEWTON03:def 1,NUMERAL1:5;
end;
theorem ND0:
for n,k be Nat, b be non trivial Nat holds digits (n,b).k < b
proof
let n,k be Nat, b be non trivial Nat;
A1: b > 1 by NEWTON03:def 1;
reconsider x = digits (n,b) as XFinSequence of NAT;
per cases;
suppose
n = 0; then
x = <%0%> by A1,NUMERAL1:def 2;
hence thesis;
end;
suppose
B1: n <> 0; then
reconsider n as non zero Nat;
per cases;
suppose k in dom x;
hence thesis by A1,B1,NUMERAL1:def 2;
end;
suppose
not k in dom x;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
theorem
for b,n be Nat, f,g be n-element XFinSequence of NAT holds
value (f + g,b) = value (f,b) + value (g,b)
proof
let b,n be Nat, f,g be n-element XFinSequence of NAT;
consider p be XFinSequence of NAT such that
A1: (dom p = dom (f + g) &
for i be Nat st i in dom p holds p.i = (f + g).i*(b|^i)) &
value ((f + g),b) = Sum p by NUMERAL1:def 1;
consider p1 be XFinSequence of NAT such that
A2: (dom p1 = dom f & for i be Nat st i in dom p1 holds p1.i = f.i*(b|^i)) &
value (f,b) = Sum p1 by NUMERAL1:def 1;
consider p2 be XFinSequence of NAT such that
A3: (dom p2 = dom g & for i be Nat st i in dom p2 holds p2.i = g.i*(b|^i)) &
value (g,b) = Sum p2 by NUMERAL1:def 1;
A4: dom p = n & dom p1 = n & dom p2 = n &
dom f = n & dom g = n & dom (f + g) = n by A1,A2,A3,CARD_1:def 7;
reconsider p as n-element XFinSequence of NAT by A4,CARD_1:def 7;
reconsider p1 as n-element XFinSequence of NAT by A4,CARD_1:def 7;
reconsider p2 as n-element XFinSequence of NAT by A4,CARD_1:def 7;
A5: dom (p1 + p2) = (dom p1) /\(dom p2) by VALUED_1:def 1;
p = p1 + p2
proof
for k be Nat st k in dom p holds p.k = (p1 + p2).k
proof
let k be Nat such that
B1: k in dom p;
B3: p.k = (f + g).k *b|^k & p1.k = f.k *b|^k & p2.k = g.k *b|^k
by B1,A1,A2,A3,A4;
p.k = ((f + g).k)*b|^k by B1,A1
.= (f.k + g.k)*b|^k by B1,VALUED_1:def 1, A1
.= p1.k + p2.k by B3;
hence thesis by B1,A4,A5,VALUED_1:def 1;
end;
hence thesis by A4,A5;
end;
hence thesis by A1,A2,A3,RVSUM_4:49;
end;
theorem VFN:
for b,k,n be Nat, f be k-element XFinSequence of NAT holds
value (f^<%n%>,b) = value (f,b) + n*b|^k
proof
let b,k,n be Nat, f be k-element XFinSequence of NAT;
reconsider g = f^<%n%> as (k+1)-element XFinSequence of NAT;
consider g1 be XFinSequence of NAT such that
A1: (dom g1 = dom g & for i be Nat st i in dom g1 holds
g1.i = (g.i)*(b|^i)) & value (g,b) = Sum g1 by NUMERAL1:def 1;
consider f1 be XFinSequence of NAT such that
A2: (dom f1 = dom f & for i be Nat st i in dom f1 holds
f1.i = (f.i)*(b|^i)) & value (f,b) = Sum f1 by NUMERAL1:def 1;
A3: dom g1 = k + 1 & dom f1 = k by A1,A2,CARD_1:def 7;
A5: k + 0 < k + 1 by XREAL_1:6; then
A6: dom (g1|k) = k & k = dom f1 by A3,AFINSQ_1:54;
A7: g1|k = f1
proof
for i be Nat st i in dom f1 holds f1.i = (g1|k).i
proof
let i be Nat such that
C1: i in dom f1;
k + 0 < k + 1 by XREAL_1:6; then
i < len g by C1,AFINSQ_1:86,A1,A3,XXREAL_0:2; then
g1.i = (g.i)*(b|^i) by A1,AFINSQ_1:86
.= (f.i)*(b|^i) by AFINSQ_1:def 3,C1,A2
.= f1.i by A2,C1;
hence thesis by C1,A3,FUNCT_1:49;
end;
hence thesis by A6;
end;
g1.k = g.k*b|^k by A1,A3,A5,AFINSQ_1:86
.= n*b|^k; then
g1 = (f1^<%n*b|^k%>) by A7,A1,CARD_1:def 7,AFINSQ_1:56; then
value (g,b) = Sum f1 + Sum <%n*b|^k%> by A1,AFINSQ_2:55
.= value (f,b) + n*b|^k by A2;
hence thesis;
end;
theorem
for b,k be Nat, f be k-element XFinSequence of NAT holds
value ((f^<%0%>),b) = value (f,b)
proof
let b,k be Nat, f be k-element XFinSequence of NAT;
value ((f^<%0%>),b) = 0*b|^k + value (f,b) by VFN;
hence thesis;
end;
theorem KBN:
for k,n,b be Nat holds value(<%n,k%>,b) = k*b + n
proof
let k,n,b be Nat;
consider x be XFinSequence of NAT such that
A2: (dom x = dom <%n,k%> & for i be Nat st i in dom x
holds x.i = (<%n,k%>.i)*(b|^i)) & value(<%n,k%>,b) = Sum x
by NUMERAL1:def 1;
A3: dom x = 2 & dom <%n,k%> = 2 & <%n,k%>.0 = n & <%n,k%>.1 = k
by A2,AFINSQ_1:38;
A4: dom x = {0,1} by A2,AFINSQ_1:38,CARD_1:50;
A5: x.0 = n*(1*b|^0)
proof
0 in dom x by A4,TARSKI:def 2; then
x.0 = (<%n,k%>.0)*(b|^0) by A2;
hence thesis;
end;
x.1 = k*(b|^1)
proof
1 in dom x by A4,TARSKI:def 2; then
x.1 = (<%n,k%>.1)*(b|^1) by A2;
hence thesis;
end; then
x = <%n,k*b%> by A3,A5,AFINSQ_1:38;
hence thesis by A2,AFINSQ_2:54;
end;
theorem
for k,n be Nat, b be Nat holds value ((k --> 0)^<%n%>,b) = n*b|^k
proof
let k,n be Nat, b be Nat;
consider x be XFinSequence of NAT such that
A2: (dom x = dom ((k --> 0)^<%n%>) & for i be Nat st i in dom x
holds x.i = ((k --> 0)^<%n%>).i*(b|^i)) & value(((k --> 0)^<%n%>),b) =
Sum x by NUMERAL1:def 1;
A3: dom x = k + 1 & dom ((k --> 0)^<%n%>) = k + 1 by A2,CARD_1:def 7; then
reconsider x as (k+1)-element XFinSequence of NAT by CARD_1:def 7;
A4: k + 0 < k + 1 by XREAL_1:6;
A5: ((k --> 0)^<%n%>).k = n;
A6: for i be Nat st i in dom (x|k) holds (x|k).i = (k --> 0).i
proof
let i be Nat such that
B1: i in dom (x|k);
dom (x|k) = k by CARD_1:def 7; then
B2: i < k by B1,AFINSQ_1:86;
B3: (x|k).i = x.i & i in dom x by AFINSQ_1:53,A3,A4,B1; then
x.i = ((k --> 0)^<%n%>).i*(b|^i) by A2 .= 0*(b|^i) by Th23,B2;
hence thesis by B3;
end;
A7: x = (x|k)^<%x.k%>;
A8: x|k = k --> 0 by A6,CARD_1:def 7;
Sum x = Sum (x|k) + Sum <%x.k%> by A7,AFINSQ_2:55
.= 0*k + x.k by A8
.= n*b|^k by A2,A3,A4,A5,AFINSQ_1:86;
hence thesis by A2;
end;
theorem
for k,m,n be Nat, b be Nat holds value (<%n,m,k%>,b) = k*b|^2 + m*b + n
proof
let k,m,n be Nat, b be Nat;
reconsider f = <%n,m%> as 2-element XFinSequence of NAT;
<%n,m,k%> = f^<%k%> by AFINSQ_1:37; then
value (<%n,m,k%>,b) = k*b|^2 + value (<%n,m%>,b) by VFN
.= k*b|^2 + (m*b + n) by KBN;
hence thesis;
end;
theorem
for b be non zero Nat, f be XFinSequence of NAT holds
value (f,b) = 0 implies f is empty-yielding
proof
let b be non zero Nat, f be XFinSequence of NAT;
assume
A1: value (f,b) = 0;
consider x be XFinSequence of NAT such that
A2: (dom x = dom f & for i be Nat st i in dom x holds
x.i = (f.i)*(b|^i)) & value (f,b) = Sum x by NUMERAL1:def 1;
for k be Nat st k in dom x holds f.k = 0
proof
assume not thesis; then
consider k be Nat such that
B1: k in dom x & f.k <> 0;
B2: x.k = (f.k)*(b|^k) by A2,B1;
reconsider x as natural-valued XFinSequence;
Sum x >= x.k by NAT_1:3,AFINSQ_2:61,B1;
hence contradiction by A1,A2,B2,B1;
end;
hence thesis by A2;
end;
theorem Th26:
for n be Nat, b be non trivial Nat holds digits (n,b) = <%n%> implies n < b
proof
let n be Nat, b be non trivial Nat;
A1: b > 1 by NEWTON03:def 1;
assume
A2: digits (n,b) = <%n%>; then
A3: len (digits (n,b)) = 1 & (digits (n,b)).0 = n by AFINSQ_1:def 4;
per cases;
suppose
n = 0;
hence thesis;
end;
suppose
n <> 0; then
reconsider n as non zero Nat;
0 in dom <%n%> by A2,A3,CARD_1:49,TARSKI:def 1;
hence thesis by A1,A2,A3,NUMERAL1:def 2;
end;
end;
theorem
for n be Nat, b be non trivial Nat holds
n >= b implies len digits (n,b) > 1
proof
let n be Nat, b be non trivial Nat;
assume
A1: n >= b;
assume
A2: not thesis;
A3: len digits (n,b) >= 1 by NUMERAL1:4,NEWTON03:def 1; then
A4: len digits (n,b) = 1 by A2,XXREAL_0:1;
A5: 0 in 1 by CARD_1:49,TARSKI:def 1;
consider x be XFinSequence of NAT such that
A6: (dom x = dom (digits(n,b)) & for i be Nat st i in dom x
holds x.i = ((digits(n,b)).i)*(b|^i)) & value(digits(n,b),b) =
Sum x by NUMERAL1:def 1;
reconsider f = x as 1-element complex-valued XFinSequence
by A2,A3,XXREAL_0:1,A6,CARD_1:def 7;
n = Sum (x|dom x) by A6
.= x.0 by A4,A6,RVSUM_4:48
.= (digits (n,b)).0*(b|^0) by A4,A6,A5
.= (digits (n,b)).0*1 by NEWTON:4; then
digits (n,b) = <%n%> by A4,AFINSQ_1:def 4;
hence contradiction by A1,Th26;
end;
theorem NMB:
for n be Nat, b be non trivial Nat holds (digits (n,b)).0 = n mod b
proof
let n be Nat, b be non trivial Nat;
n mod b = (b*value(mid(digits(n,b),2,len(digits(n,b))),b) +
digits(n,b).0) mod b by NEWTON03:def 1,NUMERAL2:19
.= (digits (n,b).0) mod b by NAT_D:21;
hence thesis by ND0,NAT_D:24;
end;
theorem
for n be Nat, b be non trivial Nat holds
n div b = value(mid(digits(n,b),2,len(digits(n,b))),b)
proof
let n be Nat, b be non trivial Nat;
(n div b)*b + (n mod b) = n by NAT_D:2
.= b*value(mid(digits(n,b),2,len(digits(n,b))),b) +
digits(n,b).0 by NEWTON03:def 1,NUMERAL2:19
.= b*value(mid(digits(n,b),2,len(digits(n,b))),b) + (n mod b) by NMB;
hence thesis by XCMPLX_1:5;
end;
theorem
for a be Nat, b be non trivial Nat, c be non zero Nat holds
(value (digits (a,b),b)) mod c = value (digits ((a mod c),b),b);
theorem
for a be Nat, b be non trivial Nat, n be non zero Nat holds
(value (digits (a,b|^n),b|^n)) mod b =
value (digits ((a mod b),b|^n),b|^n);
begin :: On Integer Numbers
registration ::: to SQUARE_1
let a be non negative Real;
reduce sqrt a^2 to a;
reducibility by SQUARE_1:22;
reduce (sqrt a)^2 to a;
reducibility by SQUARE_1:def 2;
reduce (sqrt a)|^2 to a;
reducibility
proof
(sqrt a)|^2 = (sqrt a)^2 by NEWTON03:def 2;
hence thesis;
end;
reduce (sqrt a)*(sqrt a) to a;
reducibility
proof
(sqrt a)*(sqrt a) = (sqrt a)|^2 by NEWTON:81;
hence thesis;
end;
end;
registration let a be Nat, b be Integer;
cluster a / (a gcd b) -> natural; ::: to NEWTON03
coherence;
end;
registration let a be Nat, b be Integer; ::: to NEWTON03
reduce a*b gcd a to a;
reducibility
proof
a*b gcd a = |.a.|;
hence thesis;
end;
end;
theorem Th1:
for a be Integer, b be non zero Integer holds
a/(b gcd a), b/(a gcd b) are_coprime
proof
let a be Integer, b be non zero Integer;
consider k,l be Integer such that
A1: a = (a gcd b)*k & b = (a gcd b)*l & k,l are_coprime by INT_2:23;
k = a/(a gcd b) & l = b/(a gcd b) by A1,XCMPLX_1:89;
hence thesis by A1;
end;
theorem Th2:
for a,n be Nat, b be Real st (a+1)|^n > b|^n > a|^n holds
not b is integer
proof
let a,n be Nat, b be Real;
assume
A1: (a+1)|^n > b|^n > a|^n;
assume not thesis;
then reconsider b as Integer;
per cases;
suppose b >= 0; then
b in NAT by INT_1:3;
then reconsider b as Nat;
b > a by A1,NEWTON02:41; then
b >= a+1 by INT_1:7;
hence contradiction by A1,NEWTON02:41;
end;
suppose b < 0; then
-b in NAT by INT_1:3; then
reconsider c = -b as Nat;
B1: c|^n = b|^n or c|^n = -b|^n by POWER:1,2; then
c > a by A1,NEWTON02:41; then
c >= a+1 by INT_1:7;
hence contradiction by A1,B1,NEWTON02:41;
end;
end;
theorem FLN:
for a be non integer Real holds [\a/] + [\-a/] = -1
proof
let a be non integer Real;
A1: a = [\a/] + frac a & -a = [\-a/] + frac (-a) by INT_1:42;
frac a + frac (-a) = 1 by NEWTON06:10;
hence thesis by A1;
end;
registration
let a be non integer Real;
cluster [\a/] + [\-a/] -> weightless negative;
coherence
proof
[\a/] + [\-a/] = -1 by FLN;
hence thesis;
end;
end;
theorem
for a be Real holds [\a/] + [\-a/] is weightless
proof
let a be Real;
per cases;
suppose a is integer; then
-[\a/] = [\-a/];
hence thesis;
end;
suppose
a is non integer;
hence thesis;
end;
end;
begin :: On Rational Numbers
Thx:
ex k be Rational st k is light positive non integer
proof
take a = 1/2;
|.a.| < 1;
hence thesis by COMPLEX3:def 2;
end;
registration
cluster light non integer for positive Rational;
existence by Thx;
end;
theorem APB:
for a,b be non zero Nat holds denominator (a/b) <= b & numerator (a/b) <= a
proof
let a,b be non zero Nat;
A1: numerator (a/b) = (a/b)*(denominator (a/b)) by RAT_1:def 4;
denominator (a/b) <= b by RAT_1:def 3; then
(a/b)*(denominator (a/b)) <= (a/b)*b by XREAL_1:64;
hence thesis by A1,XCMPLX_1:87,RAT_1:def 3;
end;
theorem
for a be Rational holds denominator denominator a = 1 by NAT_2:def 1;
theorem
for a be Rational holds denominator numerator a = 1 by NAT_2:def 1;
theorem
for a be non trivial Nat, b,c be non zero Nat holds
a divides b & a divides c implies
denominator (b/c) < c & numerator (b/c) < b
proof
let a be non trivial Nat, b,c be non zero Nat;
assume
A1: a divides b & a divides c; then
b/a is integer by NEWTON05:1; then
reconsider x = b/a as non zero Nat;
c/a is integer by A1,NEWTON05:1; then
reconsider y = c/a as non zero Nat;
A2: denominator (x/y) <= y & numerator (x/y) <= x by APB;
A4: b/c = (x/y) by XCMPLX_1:91;
a*x > 1*x & a*y > 1*y by XREAL_1:68,NEWTON03:def 1; then
b > x & c > y by XCMPLX_1:87;
hence thesis by A2,A4,XXREAL_0:2;
end;
registration
let a be Rational;
cluster (denominator a) gcd (numerator a) -> trivial non zero;
coherence
proof
denominator a, numerator a are_coprime by WSIERP_1:22;
hence thesis;
end;
end;
theorem
for a be Integer, b be non zero Integer holds
denominator (a/b) divides b & numerator (a/b) divides a
proof
let a be Integer, b be non zero Integer;
b*numerator (a/b) = b*((a/b)*(denominator (a/b))) by RAT_1:def 4
.= b*(a/b)*(denominator (a/b))
.= a*denominator (a/b) by XCMPLX_1:87; then
A2: numerator (a/b) divides a*denominator (a/b) &
denominator (a/b) divides b*numerator (a/b);
numerator (a/b), denominator (a/b) are_coprime by NAT_2:def 1;
hence thesis by A2,INT_2:25;
end;
theorem
for a be Integer, b be non zero Nat st a,b are_coprime holds
denominator (a/b) = b
proof
let a be Integer, b be non zero Nat;
assume a,b are_coprime; then
denominator (a/b) = b div 1 by RING_3:15;
hence thesis;
end;
theorem
for a be non zero light Rational holds
not denominator a divides numerator a
proof
let a be non zero light Rational;
|.(numerator a)/(denominator a).| < 1 by COMPLEX3:1; then
|.numerator a.|/|.denominator a.| < 1 by COMPLEX1:67; then
|.numerator a.| < |.denominator a.| by XREAL_1:181;
hence thesis by INT_2:16,NAT_D:7;
end;
theorem NDD: :: see REAL_3:3
for a be Rational holds [\a/] = (numerator a) div (denominator a)
proof
let a be Rational;
reconsider x = numerator a as Integer;
reconsider y = denominator a as non zero Nat;
[\a/] = [\(numerator a)/(denominator a)/]
.= x div y by INT_1:def 9;
hence thesis;
end;
theorem NFD: :: see REAL_3:6
for a be Rational holds
frac a = ((numerator a) mod (denominator a))/(denominator a)
proof
let a be Rational;
[\a/] + frac a = (numerator a)/(denominator a) by INT_1:42
.= (((numerator a) div (denominator a))*(denominator a) +
((numerator a) mod (denominator a)))/(denominator a) by INT_1:59
.= ((numerator a) div (denominator a))*(denominator a)/(denominator a) +
((numerator a) mod (denominator a))/(denominator a)
.= ((numerator a) div (denominator a))*1 + ((numerator a) mod
(denominator a))/(denominator a) by XCMPLX_1:89
.= [\a/] + (((numerator a) mod (denominator a))/(denominator a)) by NDD;
hence thesis;
end;
theorem FRD:
for a be Rational holds
(frac a)*denominator a = (numerator a) mod (denominator a)
proof
let a be Rational;
(frac a)*(denominator a) =
((numerator a) mod (denominator a))/(denominator a)*(denominator a)
by NFD;
hence thesis by XCMPLX_1:87;
end;
registration
let a be Rational;
cluster frac a -> rational;
coherence
proof
per cases;
suppose a is integer;
hence thesis;
end;
suppose a is non integer; then
reconsider a as non integer Rational;
reconsider b = -a as non integer Rational;
A1: (frac a) + (frac b) = 1 by NEWTON06:10;
frac a = ((numerator a) mod (denominator a))/(denominator a) or
frac b = ((numerator b) mod (denominator b))/(denominator b) by NFD;
hence thesis by A1;
end;
end;
cluster (frac a)*(denominator a) -> natural;
coherence
proof
(frac a)*(denominator a) = (numerator a) mod (denominator a) by FRD;
hence thesis;
end;
end;
theorem
for a be Rational holds
numerator (frac a), denominator (frac a) are_coprime
by NAT_2:def 1;
theorem
for a be Rational holds
(numerator frac a) mod (denominator frac a) = numerator frac a
proof
let a be Rational;
numerator (frac a) in NAT by INT_1:3; then
reconsider x = numerator (frac a) as Nat;
frac a < 1 by COMPLEX3:1;
hence thesis by NAT_D:24,RAT_1:35;
end;
theorem NMD:
for a be Rational holds
(numerator a) mod (denominator a), denominator a are_coprime
proof
let a be Rational;
1 = (numerator a) gcd (denominator a) by NAT_2:def 1
.= ((numerator a) mod (denominator a)) gcd (denominator a) by NTALGO_1:9;
hence thesis;
end;
theorem FRA:
for a be Rational holds denominator (frac a) = denominator (frac -a)
proof
let a be Rational;
A2: frac a = ((numerator a) mod (denominator a))/denominator a &
frac (-a) = ((numerator (-a)) mod (denominator (-a)))/(denominator (-a))
by NFD;
A3: (numerator a) mod (denominator a), denominator a are_coprime &
(numerator (-a)) mod (denominator (-a)), denominator (-a) are_coprime
by NMD;
denominator (frac (-a)) = denominator (-a) div (denominator (-a) gcd
((numerator (-a)) mod (denominator (-a)))) by A2,RING_3:15
.= (denominator a) div ((denominator a) gcd ((numerator a) mod
(denominator a))) by A3,RAT_1:43
.= denominator (((numerator a) mod (denominator a))/denominator a)
by RING_3:15
.= denominator (frac a) by NFD;
hence thesis;
end;
theorem DF:
for a be Rational holds denominator a = denominator frac a
proof
let a be Rational;
per cases;
suppose
a is non negative; then
reconsider a as non negative Rational;
reconsider x = numerator a mod denominator a as Nat;
A2: (numerator a) mod (denominator a), denominator a are_coprime by NMD;
frac a = ((numerator a) mod (denominator a))/(denominator a) by NFD; then
denominator (frac a) = (denominator a) div 1 by A2,RING_3:15;
hence thesis;
end;
suppose
a is negative; then
reconsider b = -a as positive Rational;
reconsider x = numerator b mod denominator b as Nat;
A2: numerator b mod denominator b, denominator b are_coprime by NMD;
frac b = ((numerator b) mod (denominator b))/(denominator b) by NFD; then
A3: denominator (frac b) = (denominator b) div 1 by A2,RING_3:15;
denominator a = denominator -a &
denominator (frac a) = denominator (frac -a) by RAT_1:43,FRA;
hence thesis by A3;
end;
end;
theorem
for a be Rational, b be Integer holds denominator (a + b) = denominator a
proof
let a be Rational, b be Integer;
denominator (a + b) = denominator (frac (a + b)) by DF
.= denominator (frac a) by INT_1:66
.= denominator a by DF;
hence thesis;
end;
theorem
for a be negative non integer Rational holds
frac a = 1 - ((numerator (-a)) mod (denominator a))/(denominator a)
proof
let a be negative non integer Rational;
A1: denominator a = denominator (-a) by RAT_1:43;
frac a + (frac (-a)) = 1 by NEWTON06:10; then
frac a = 1 - frac (-a)
.= 1 - ((numerator (-a)) mod (denominator (-a)))/(denominator (-a)) by NFD;
hence thesis by A1;
end;
theorem R144:
for a be positive Rational holds numerator a = denominator (a") &
denominator a = numerator (a")
proof
let a be positive Rational;
a" = 1/a;
hence thesis by RAT_1:44;
end;
registration
let a be positive Nat;
cluster numerator (a") -> weightless positive;
coherence
proof
numerator (a") = denominator a by R144;
hence thesis;
end;
end;
registration
let a be positive Nat;
reduce denominator (a") to a;
reducibility
proof
denominator (a") = numerator a by R144;
hence thesis;
end;
end;
theorem
for a be positive Rational holds
(numerator a)*(numerator (a")) = (denominator a)*(denominator (a"))
proof
let a be positive Rational;
numerator a = denominator (a") & numerator (a") = denominator a by R144;
hence thesis;
end;
theorem ABI:
for a,b be Rational holds
(numerator (a*b))/(denominator (a*b)) =
((numerator a)*(numerator b))/((denominator a)*(denominator b))
proof
let a,b be Rational;
((numerator a)*(numerator b))/((denominator a)*(denominator b)) =
((numerator a)/(denominator a))*((numerator b)/(denominator b))
by XCMPLX_1:76;
hence thesis;
end;
theorem IND:
for a,b be Rational holds
(numerator (a*b))*(denominator a)*(denominator b) =
(denominator (a*b))*(numerator a)*(numerator b)
proof
let a,b be Rational;
(numerator (a*b))*((denominator a)*(denominator b)) =
(((denominator a)*(denominator b))*(denominator (a*b)))*
((numerator (a*b))/(denominator (a*b))) by XCMPLX_1:90
.= (((denominator a)*(denominator b))*(denominator (a*b)))*
((((numerator a)*(numerator b)))/((denominator a)*(denominator b)))
by ABI
.= (denominator (a*b))*((((denominator a)*(denominator b)))*
((((numerator a)*(numerator b)))/((denominator a)*(denominator b))))
.= (denominator (a*b))*((numerator a)*(numerator b)) by XCMPLX_1:87;
hence thesis;
end;
theorem NUM:
for a,b be Rational holds
numerator (a*b) divides (numerator a)*(numerator b)
proof
let a,b be Rational;
A1: numerator (a*b), denominator (a*b) are_coprime by NAT_2:def 1;
numerator (a*b) divides
(numerator (a*b))*((denominator a)*(denominator b)); then
numerator (a*b) divides
(numerator (a*b))*(denominator a)*(denominator b); then
numerator (a*b) divides
(denominator (a*b))*(numerator a)*(numerator b) by IND; then
numerator (a*b) divides (denominator (a*b))*((numerator a)*(numerator b));
hence thesis by A1,INT_2:25;
end;
theorem DEN:
for a,b be Rational holds
denominator (a*b) divides (denominator a)*(denominator b)
proof
let a,b be Rational;
A1: numerator (a*b), denominator (a*b) are_coprime by NAT_2:def 1;
denominator (a*b) divides
(denominator (a*b))*((numerator a)*(numerator b)); then
denominator (a*b) divides
(denominator (a*b))*(numerator a)*(numerator b); then
denominator (a*b) divides
(numerator (a*b))*(denominator a)*(denominator b) by IND; then
denominator (a*b) divides
(numerator (a*b))*((denominator a)*(denominator b));
hence thesis by A1,INT_2:25;
end;
theorem
for a,b be non zero Rational holds
(denominator a)*(denominator b)/(denominator (a*b)) =
(numerator a)*(numerator b)/(numerator (a*b))
proof
let a,b be non zero Rational;
(denominator a)*(denominator b)/(denominator (a*b))
= (((denominator a)*(denominator b))*(numerator (a*b)))/
((denominator (a*b))*(numerator (a*b))) by XCMPLX_1:91
.= ((denominator a)*(denominator b))/(numerator (a*b))*
((numerator (a*b))/(denominator (a*b))) by XCMPLX_1:76
.= ((denominator a)*(denominator b))/(numerator (a*b))*
(((numerator a)/(denominator a))*((numerator b)/(denominator b)))
.= ((denominator a)*(denominator b))/(numerator (a*b))*
(((numerator a)*(numerator b))/((denominator a)*(denominator b)))
by XCMPLX_1:76
.= (((denominator a)*(denominator b))*(((numerator a)*(numerator b))))/
(((numerator (a*b)))*((denominator a)*(denominator b))) by XCMPLX_1:76
.= ((numerator a)*(numerator b))/(numerator (a*b)) by XCMPLX_1:91;
hence thesis;
end;
theorem DDN:
for a,b be Rational holds a*b is integer implies
denominator b divides numerator a
proof
let a,b be Rational;
assume a*b is integer; then
reconsider x = a*b as Integer;
a*(denominator a) = numerator a &
b*(denominator b) = numerator b by RAT_1:def 4; then
(x*(denominator a))*(denominator b) = (numerator a)*(numerator b); then
A2: denominator b divides (numerator a)*(numerator b);
numerator b, denominator b are_coprime by NAT_2:def 1;
hence thesis by A2,INT_2:25;
end;
theorem
for a,b be Rational holds a*b is integer iff
denominator b divides numerator a & denominator a divides numerator b
proof
let a,b be Rational;
denominator b divides numerator a & denominator a divides numerator b
implies a*b is integer
proof
assume
B1: denominator b divides numerator a & denominator a divides numerator b;
then
reconsider x = (numerator a)/(denominator b) as Integer by NEWTON05:1;
reconsider y = (numerator b)/(denominator a) as Integer by NEWTON05:1,B1;
a = (numerator a)/(denominator a) & b = (numerator b)/(denominator b);
then
x*y = a*b;
hence thesis;
end;
hence thesis by DDN;
end;
theorem
for a,b be non negative Rational holds
(numerator a)*(numerator b) >= numerator (a*b)
proof
let a,b be non negative Rational;
per cases;
suppose a is zero or b is zero;
hence thesis;
end;
suppose
B1: not a is zero & not b is zero; then
reconsider a as positive Rational;
reconsider b as positive Rational by B1;
numerator (a*b) <= (numerator a)*(numerator b) by NUM,NAT_D:7;
hence thesis;
end;
end;
theorem
for a,b be Rational holds
(denominator a)*(denominator b) >= denominator (a*b)
proof
let a,b be Rational;
per cases;
suppose a is zero or b is zero; then
(denominator a)*(denominator b) >= 1 &
denominator (a*b) = 1 by COMPLEX3:1;
hence thesis;
end;
suppose not a is zero & not b is zero; then
reconsider a, b as non zero Rational;
thus thesis by NAT_D:7,DEN;
end;
end;
theorem
for a be Rational, k be non zero Nat holds a*k is integer implies
k >= denominator a
proof
let a be Rational, k be non zero Nat;
A3: numerator a, denominator a are_coprime by NAT_2:def 1;
assume a*k is integer; then
reconsider x = a*k as Integer;
(denominator a)*x = (denominator a)*((numerator a)/(denominator a)*k)
.= (denominator a)*(numerator a)/(denominator a)*k
.= (numerator a)*k by XCMPLX_1:89; then
denominator a divides (numerator a)*k;
hence thesis by A3,INT_2:25,NAT_D:7;
end;
theorem
for a,b be non zero Rational holds
numerator(a + b)*(denominator a)*(denominator b) =
((numerator b)*(denominator a) +
(numerator a)*(denominator b))*(denominator (a + b))
proof
let a,b be non zero Rational;
(numerator a)/(denominator a) = ((numerator a)*(denominator b))/
((denominator a)*(denominator b)) &
(numerator b)/(denominator b) = ((numerator b)*(denominator a))/
((denominator b)*(denominator a)) by XCMPLX_1:91; then
A1: (numerator a)/(denominator a) + (numerator b)/(denominator b) =
((numerator a)*(denominator b))/((denominator a)*(denominator b)) +
((numerator b)*(denominator a))/((denominator b)*(denominator a))
.= ((numerator a)*(denominator b) + (numerator b)*(denominator a))/
((denominator b)*(denominator a));
((denominator b)*(denominator a))*(numerator (a + b))
= ((((numerator a)*(denominator b)) + (numerator b)*(denominator a))/
((denominator a)*(denominator b)))*(denominator (a + b))*
((denominator b)*(denominator a)) by A1,RAT_1:def 4
.= (((((numerator a)*(denominator b)) + (numerator b)*(denominator a))/
((denominator a)*(denominator b)))*((denominator b)*(denominator a)))*
(denominator (a + b))
.= (((numerator a)*(denominator b)) + (numerator b)*(denominator a))*
(denominator (a + b)) by XCMPLX_1:87;
hence thesis;
end;
begin :: On Irrational Numbers
theorem Th3:
for n be non zero Nat, a be non integer Rational holds a|^n is non integer
proof
let n be non zero Nat, a be non integer Rational;
consider l be Integer, k be Nat such that
A1: k > 0 & a = l/k by RAT_1:8;
k = 1 implies l/k is integer; then
reconsider k as non trivial Nat by A1,NAT_2:def 1;
reconsider l1 = l/(k gcd l) as Integer;
(k gcd l) divides k & |.k.| <> (k gcd l) by A1,INT_2:def 2; then
k >= k gcd l & k <> k gcd l by NAT_D:7; then
k > k gcd l by XXREAL_0:1; then
reconsider k1 = k/(k gcd l) as non trivial Nat
by XREAL_1:187,NEWTON03:def 1;
k1|^n,l1|^n are_coprime by Th1,WSIERP_1:11; then
A2: not k1|^n divides l1|^n by NAT_2:def 1;
a|^n = (l1/k1)|^n by A1,XCMPLX_1:55
.= (l1|^n)/(k1|^n) by PREPOWER:8;
hence thesis by A2,WSIERP_1:17;
end;
theorem Th4:
for a,b,n be Nat st (a+1)|^n > b > a|^n holds n-root b is irrational
proof
let a,b,n be Nat such that
A1: (a+1)|^n > b > a|^n;
1*(a+1)|^0 = 1*a|^0; then
reconsider n as non zero Nat by A1;
reconsider x = n-root b as positive Real by A1;
A2: x|^n = b; then
not x is integer by A1,Th2;
hence thesis by Th3,A2;
end;
theorem Th5:
for a be Nat, n be non zero Nat holds
n-root a is irrational iff n-root a is non integer
proof
let a be Nat, n be non zero Nat;
n-root a is non integer implies n-root a is irrational
proof
assume
A1: n-root a is non integer;
n-root a >= 0 by NAT_1:14,POWER:7; then
reconsider b = n-root a as non integer positive Real by A1;
[\b/] is natural; then
reconsider x = [\b/] as Nat;
x < b < x + 1 by INT_1:29,INT_1:26; then
x|^n < b|^n < (x + 1)|^n by NEWTON02:40;
hence thesis by Th4;
end;
hence thesis;
end;
registration
let a be non square Nat;
cluster 2-root a -> irrational;
coherence
proof
(2-root a)|^2 = a; then
not 2-root a is integer;
hence thesis by Th5;
end;
let n be non zero even Nat;
cluster n-root a -> irrational;
coherence
proof
(n-root a)|^n = a; then
not n-root a is integer;
hence thesis by Th5;
end;
end;
theorem Th6:
for a be prime Nat, n,m be non zero Nat holds
(n+m)-root (a|^m) is irrational
proof
let a be prime Nat, n,m be non zero Nat;
reconsider x = (n+m) - 1 as non zero Nat;
assume not thesis; then
consider p be Integer, q be Nat such that
A1: q <> 0 & p/q = (n+m)-root (a|^m) &
for u be Integer,w be Nat st w <> 0 &
(n+m)-root (a|^m) = u/w holds q<=w by RAT_1:9;
A2: q >= 0 + 1 by A1,INT_1:7;
A3: a is non trivial;
(n + m)-root (a|^m) is heavy positive; then
p/q*q > 1*q by A1,XREAL_1:68; then
p > q by A1,XCMPLX_1:87; then
p > 1 & p in NAT by A2,XXREAL_0:2,INT_1:3; then
reconsider p as heavy Nat by COMPLEX3:1;
:: or: non trivial Nat by NEWTON03:def 1;
(p/q)|^(n+m) = ((n+m)-root (a|^m))|^(n+m) by A1; then
A4: p|^(n+m)/q|^(n+m) * q|^(n+m) = a|^m*q|^(n+m) by PREPOWER:8; then
p|^(n+m) = a|^m*q|^(n+m) by A1,XCMPLX_1:87; then
a divides p|^(n+m) by NAT_3:3,INT_2:2; then
consider k be Nat such that
A5: p = a*k by NAT_3:5,NAT_D:def 3;
a|^m*q|^(n+m) = (k*a)|^(n+m) by A4,A1,XCMPLX_1:87,A5
.= k|^(n+m) * a|^(n+m) by NEWTON:7; then
a|^(n+m) divides a|^m*q|^(n+m); then
a|^m*a|^n divides a|^m*q|^(n+m) by NEWTON:8; then
a divides a|^n & a|^n divides q|^(n+m) by INT_4:7,NAT_3:3; then
a divides q|^(n+m) by INT_2:9; then
consider l be Nat such that
A6: q = a*l by NAT_3:5,NAT_D:def 3;
A7: l > 0 by A1,A6; then
A8: a*l > 1*l by A3,XREAL_1:68;
(n+m)-root (a|^m) = k/l by A1,A5,A6,XCMPLX_1:91;
hence contradiction by A1,A7,A6,A8;
end;
theorem Th7:
for n be non zero Nat, a,b be Nat st a,b are_coprime holds
n-root (a*b) is Nat implies n-root a is Nat
proof
let n be non zero Nat,a,b be Nat such that
A1: a,b are_coprime;
assume n-root (a*b) is Nat; then
reconsider k = n-root (a*b) as Nat;
k|^n = (n-root(a*b))|^n = a*b; then
(n-root a) in NAT by A1,NEWTON03:14;
hence thesis;
end;
theorem Th8:
for n be non zero Nat, a,b be Nat st a,b are_coprime holds
n-root (a*b) is rational implies n-root a is rational
proof
let n be non zero Nat, a,b be Nat such that
A1: a,b are_coprime;
assume n-root (a*b) is rational; then
consider p be Integer, q be Nat such that
A3: q <> 0 & p/q = n-root (a*b) &
for u be Integer, w be Nat st w <> 0 & n-root (a*b) = u/w holds q<=w
by RAT_1:9;
p >= 0 by A3,POWER:7,NAT_1:14; then
p in NAT by INT_1:3; then
reconsider p as Nat;
p|^n = (p|^n/q|^n)*q|^n by A3,XCMPLX_1:87
.= (n-root(a*b))|^n*q|^n by A3,PREPOWER:8
.= a*b*q|^n; then
q|^n divides p|^n; then
consider x be Nat such that
A4: p = q*x by NAT_D:def 3,NEWTON03:15;
n-root (a*b) = x by A3,A4,XCMPLX_1:89;
hence thesis by A1,Th7;
end;
theorem Th9:
for a be prime Nat, b,n,m be non zero Nat st not a divides b holds
(n+m)-root (a|^m*b) is irrational
proof
let a be prime Nat, b,n,m be non zero Nat;
assume not a divides b; then
a gcd b <> |.a.| by NEWTON02:3; then
A1: a, b are_coprime by PEPIN:2;
(n+m)-root (a|^m) is irrational by Th6;
hence thesis by A1,WSIERP_1:10,Th8;
end;
theorem Th10:
for n be non trivial Nat, a be prime Nat, b be Nat st a divides b &
not a|^n divides b holds n-root b is irrational
proof
let n be non trivial Nat, a be prime Nat, b be Nat such that
A1: a divides b;
assume
A2: not a|^n divides b; then
reconsider b as non zero Integer by INT_2:12;
a|^1 divides b by A1; then
reconsider m = a |-count b as non zero Nat by NEWTON03:59;
m < n by A2,NEWTON03:59; then
consider c be Nat such that
A4: n = m + c by NAT_1:10;
|.a.| > 1 by INT_2:def 4; then
a|^m divides b by NEWTON03:def 7; then
consider k be Nat such that
A5: b = (a|^m)*k by NAT_D:def 3;
reconsider k as non zero Nat by A5;
m + c > m + 0 by A2,NEWTON03:59,A4; then
(c+m)-root ((a|^m)*k) is irrational by A5,Th9,NEWTON03:76;
hence thesis by A4,A5;
end;
registration
let a be non trivial square-free Nat;
let n be non trivial Nat;
cluster n-root a -> irrational;
coherence
proof
consider p be prime Nat such that
A1: p divides a by NEWTON03:29;
n > 1 by NEWTON03:def 1; then
n >= 1+1 by NAT_1:13; then
A2: p|^2 divides p|^n by NEWTON:89;
not p|^n divides a by MOEBIUS1:def 1,A2,INT_2:9;
hence thesis by A1,Th10;
end;
end;
registration
let a be prime Nat;
let b be non zero rational number;
cluster (sqrt a)*(sqrt a + b) -> irrational;
coherence
proof
(sqrt a)*(sqrt a) + b*(sqrt a) is irrational;
hence thesis;
end;
end;
theorem Th11:
for a be prime Nat, b,c be rational number holds
((sqrt a)+b)*((sqrt a)+c) is rational iff b = -c
proof
let a be prime Nat, b,c be rational number;
((sqrt a)+b)*((sqrt a)+c) =
(sqrt a)*(sqrt a)+ (sqrt a)*c+(sqrt a)*b + b*c
.=(a+ b*c) + sqrt a*(c+b); then
((sqrt a)+b)*((sqrt a)+c) is rational iff b+c = 0;
hence thesis;
end;
registration
let a be prime Nat, b be rational number;
cluster ((sqrt a)+b)*((sqrt a)-b) -> rational;
coherence
proof
reconsider c = 0-b as rational number;
((sqrt a)+b)*((sqrt a)+c) is rational by Th11;
hence thesis;
end;
end;
registration
let a be prime Nat, b be non zero rational number;
cluster ((sqrt a)+b)*((sqrt a)+b) -> irrational;
coherence
proof
b > 0 > -b or -b > 0 > b;
hence thesis by Th11;
end;
end;
registration
let a be prime Nat, b,c be positive rational number;
cluster ((sqrt a)+b)*((sqrt a)+c) -> irrational;
coherence
proof
b <> -c;
hence thesis by Th11;
end;
cluster ((sqrt a)-b)*((sqrt a)-c) -> irrational;
coherence
proof
reconsider b1 = 0-b as rational number;
reconsider c1 = 0-c as rational number;
b1 <> -c1;
hence thesis by Th11;
end;
end;
theorem Th12:
for n be non zero Nat, a be non negative Real st
a > 1 holds n-root a > 1
proof
let n be non zero Nat, a be non negative Real such that
A1: a > 1;
n >= 1 by NAT_1:14; then
n-root a > n-root 1 by A1,POWER:17;
hence thesis;
end;
registration ::: revise: MOVE to NAT_2
let n be non zero Nat, a be trivial Nat;
cluster n-root a -> natural;
coherence
proof
n-root 0 = 0 & n-root 1 = 1;
hence thesis by NAT_2:def 1;
end;
end;
begin :: Square-free Numbers and Radicals
registration let a be non trivial square-free Nat, n,m be non zero Nat;
cluster (n+m)-root (a|^m) -> irrational;
coherence
proof
reconsider k = m+n as non trivial Nat;
consider p be prime Nat such that
A1: p divides a by NEWTON03:29;
consider b be Nat such that
A2: a = p*b by A1,NAT_D:def 3;
reconsider b as non zero Nat by A2;
not p|^2 divides a by MOEBIUS1:def 1; then
not p*p divides p*b by NEWTON:81,A2; then
not p divides b by NEWTON03:5; then
(n+m)-root (p|^m*b|^m) is irrational by NAT_3:5,Th9;
hence thesis by A2,NEWTON:7;
end;
end;
registration
let a be non trivial square-free Nat,
b be non zero rational number,
n,m be non zero Nat;
cluster ((n+m)-root (a|^n))*(((n+m)-root (a|^m))+ b) -> irrational;
coherence
proof
n >= 1 by NAT_1:14; then
A0: n+m > 1+ 0 by XREAL_1:8;
((n+m)-root (a|^n))*(((n+m)-root (a|^m))+ b) =
((n+m)-root (a|^n))*((n+m)-root (a|^m)) + ((n+m)-root (a|^n))* b
.= ((n+m)-root (a|^n*a|^m)) + ((n+m)-root (a|^n))*b by A0,POWER:11
.= ((n+m)-root (a|^(n+m))) + ((n+m)-root (a|^n))* b by NEWTON:8
.= a + ((n+m)-root (a|^n))* b;
hence thesis;
end;
end;
registration
let a be non trivial square-free Nat;
cluster sqrt a -> irrational;
coherence
proof
A1: 2 is non trivial;
reconsider k = sqrt a as non negative Real;
reconsider l = 2-root a as non negative Real;
(2-root a)|^2 = (sqrt a)|^2;
hence thesis by A1;
end;
end;
registration
let a be non trivial square-free Nat,
b be non zero rational number;
cluster (sqrt a)*(sqrt a + b) -> irrational;
coherence
proof
(sqrt a)*(sqrt a) + b*(sqrt a) is irrational;
hence thesis;
end;
end;
theorem Th13:
for a,b be Nat holds
a*b = (a gcd b)|^2*((a lcm b)/(a gcd b))
proof
let a, b be Nat;
per cases;
suppose a = 0;
hence thesis;
end;
suppose
a <> 0; then
reconsider a as non zero Nat;
reconsider c = a gcd b as non zero Nat;
a*b = (a gcd b)*(a lcm b) by NAT_D:29
.= (a gcd b)*((a gcd b)*(a lcm b))/(a gcd b) by XCMPLX_1:89
.= (a gcd b)*(a gcd b)*(a lcm b)/(a gcd b)
.= ((a gcd b)|^2)*(a lcm b)/(a gcd b) by NEWTON:81;
hence thesis;
end;
end;
registration
let a be non zero Nat;
cluster a/(Radical a) -> natural;
coherence
proof
consider b be Nat such that
A1: a = (Radical a)*b by MOEBIUS1:55,NAT_D:def 3;
thus thesis by A1,XCMPLX_1:89;
end;
end;
Th14:
for a be Integer, b be square-free Nat holds a gcd b is square-free
proof
let a be Integer, b be square-free Nat;
assume not thesis; then
consider p be prime Nat such that
A1: p|^2 divides (a gcd b);
(a gcd b) divides b by INT_2:def 2;
hence contradiction by A1,INT_2:9,MOEBIUS1:def 1;
end;
registration
let a be Integer, b be square-free Nat;
cluster a gcd b -> square-free;
coherence by Th14;
end;
theorem Th15:
for a be non zero square-containing Nat holds a > Radical a
proof
let a be non zero square-containing Nat;
Radical a <> a & Radical a <= a by MOEBIUS1:58;
hence thesis by XXREAL_0:1;
end;
registration
let a be non zero square-containing Nat;
cluster a/(Radical a) -> non trivial;
coherence by Th15,XREAL_1:187;
end;
theorem Th16: ::: revise NEWTON03:29
for a be Integer holds a <> 1 & a <> -1 implies
ex p be prime Nat st p divides a
proof
let a be Integer;
reconsider b = |.a.| as Nat;
assume a <> 1 & a <> -1; then
|.a.| <> |.1.| by ABSVALUE:28; then
per cases by XXREAL_0:1;
suppose |.a.| < 1; then
a = 0 by NAT_1:14;
hence thesis by INT_2:28,INT_2:12;
end;
suppose |.a.| > 1; then
reconsider b as non trivial Nat by NEWTON03:def 1;
B1: b divides a by INT_6:13;
ex p be prime Nat st p divides b by NEWTON03:29;
hence thesis by B1,INT_2:9;
end;
end;
registration
let a be non trivial square Nat, b be Nat;
cluster a*b -> square-containing;
coherence
proof
consider k be Nat such that
A1: a = k^2 by PYTHTRIP:def 3;
k <> 1 by A1,NEWTON03:def 1; then
consider p be prime Nat such that
A3: p divides k by Th16;
p|^2 divides k|^2 by NEWTON03:15,A3; then
p|^2 divides a by A1,NEWTON:81;
hence thesis by INT_2:2;
end;
end;
registration
let a be Nat, b be square-containing Nat;
cluster a lcm b -> square-containing;
coherence
proof
consider p be prime Nat such that
A1: p|^2 divides b by MOEBIUS1:def 1;
b divides a lcm b by NAT_D:def 4;
hence thesis by A1,INT_2:9;
end;
end;
theorem Th17:
for a,b be Nat st not a,b are_coprime holds a*b is square-containing
proof
let a,b be Nat;
assume not a,b are_coprime; then
per cases by XXREAL_0:1;
suppose a gcd b < 1; then
a = 0 & b = 0 by NAT_1:14;
hence thesis;
end;
suppose a gcd b > 1; then
a gcd b is non trivial; then
reconsider k = (a gcd b)|^2 as non trivial square Nat;
reconsider l = ((a lcm b)/(a gcd b)) as Nat;
a*b = k*l by Th13;
hence thesis;
end;
end;
theorem Th18:
for a be square-free Nat, b be Nat holds
(a gcd b), a/(a gcd b) are_coprime
proof
let a be square-free Nat, b be Nat;
(a gcd b)*(a/(a gcd b)) = a by XCMPLX_1:87;
hence thesis by Th17;
end;
theorem Th19:
for b be square-free Nat, a be Nat holds not b divides a
implies ex p be prime Nat st not p divides a & p divides b
proof
let b be square-free Nat, a be Nat;
assume
A0: not b divides a; then
consider c be Nat such that
A1: c divides b & not c divides a;
c <> 0 by A1; then
c >= 1 & c <> 1 by A1,INT_2:12,NAT_1:14; then
c > 1 by XXREAL_0:1; then
reconsider c as non trivial Nat by NEWTON03:def 1;
reconsider k = (a gcd b) as square-free Nat;
reconsider l = b/(a gcd b) as non zero Nat;
A3: k*l = b by XCMPLX_1:87; then
reconsider l as square-free Nat by MOEBIUS1:25;
A5: l >= 1 by NAT_1:14;
l = 1 implies b divides a by A3,INT_2:def 2; then
l > 1 by A0,A5,XXREAL_0:1; then
reconsider l as non trivial Nat by NEWTON03:def 1;
consider p be prime Nat such that
A6: p divides l by NEWTON03:29;
consider q be Nat such that
A7: l = p*q by A6,NAT_D:def 3;
A8: p divides b by A6,A3,INT_2:2;
(a gcd b)
= ((a gcd b) gcd a)*(l gcd a) by A3,Th18,NAT_5:17
.= (a gcd b)*(l gcd a); then
a*1,p*q are_coprime by XCMPLX_1:7,A7; then
a,p are_coprime by NEWTON01:41;
hence thesis by A8,NAT_6:6;
end;
begin :: Irrational Roots
theorem Th20:
for a be square-free Nat, b,n,m be non zero Nat st not a divides b holds
(n+m)-root (a|^m*b) is irrational
proof
let a be square-free Nat, b,n,m be non zero Nat;
assume not a divides b; then
consider p be prime Nat such that
A1: not p divides b & p divides a by Th19;
consider k be Nat such that
A2: a = p*k by A1,NAT_D:def 3;
a/(a gcd p), (a gcd p) are_coprime by Th18; then
k,p are_coprime by A2,XCMPLX_1:89; then
A3: k|^m,p|^m are_coprime by WSIERP_1:11;
A4: a|^m*b = p|^m*k|^m*b by A2,NEWTON:7 .= p|^m*(k|^m*b);
p gcd b <> |.p.| by A1,NEWTON02:3; then
b,p are_coprime by PEPIN:2; then
b,p|^m are_coprime by WSIERP_1:10; then
A5: b*k|^m, p|^m are_coprime by A3,INT_2:26;
(n+m)-root (p|^m) is irrational;
hence thesis by A4,A5,Th8;
end;
theorem Th21:
for a be square-free Nat, b be non zero Nat, n be non trivial Nat st
b < a|^n & a divides b holds n-root b is irrational
proof
let a be square-free Nat, b be non zero Nat, n be non trivial Nat;
assume
A1: b < a|^n & a divides b;
A1a: b >= 1 by NAT_1:14; then
a|^n > 1|^n by A1,XXREAL_0:2; then
A2: |.a.| > 1 by NEWTON02:40;
reconsider a as non trivial Nat by NAT_2:def 1,A1,A1a;
reconsider m = a |-count b as Nat;
a|^1 divides b by A1; then
reconsider m as non zero Nat by NEWTON03:59;
m < n by A1,NEWTON03:62; then
consider k be Nat such that
A3: n = m+k by NAT_1:10;
reconsider k as non zero Nat by A1,NEWTON03:62,A3;
a|^(a|-count b) divides b by A2,NEWTON03:def 7; then
consider c be Nat such that
A4: b = a|^(a|-count b)*c by NAT_D:def 3;
reconsider c as non zero Nat by A4;
(m+k)-root (a|^m*c) is irrational by Th20,A4,NEWTON03:76;
hence thesis by A3,A4;
end;
registration
let a be non zero Nat, n be non trivial Nat;
cluster n-root(a|^n+1) -> irrational;
coherence
proof
A1: a|^n + 0 < a|^n + 1 by XREAL_1:6;
(a|^n + 1|^n) < (a+1)|^n by NEWTON03:103;
hence thesis by A1,Th4;
end;
end;
registration
let a,n be non trivial Nat;
cluster n-root (a|^n - 1) -> irrational;
coherence
proof
reconsider b = a - 1 as non zero Nat;
(b+1)|^n > b|^n + 1|^n by NEWTON03:103; then
A1: (b+1)|^n - 1 > b|^n + 1 - 1 by XREAL_1:9;
a|^n - 1 + 1 > a|^n - 1 + 0 by XREAL_1:6;
hence thesis by A1,Th4;
end;
end;
theorem Th22:
for b be Nat, n be non zero Nat st n-root b is irrational holds
ex a be Nat st a|^n < b < (a+1)|^n
proof
let b be Nat,n be non zero Nat such that
A1: n-root b is irrational;
reconsider m = n-1 as Nat;
consider a be Nat such that
A2: a|^(m+1) <= b < (a+1)|^(m+1) by NEWTON02:43;
not b = a|^n by A1; then
a|^n < b < (a+1)|^n by A2,XXREAL_0:1;
hence thesis;
end;
theorem Th23:
for a,b be Nat, n be non zero Nat st n-root b is irrational & n-root b > a
holds ex c be Nat st a|^n < b < (a+2*c)|^n
proof
let a,b be Nat, n be non zero Nat;
assume
A1: n-root b is irrational & n-root b > a; then
consider k be Nat such that
A2: k|^n < b < (k+1)|^n by Th22;
A3: (n-root b)|^n > a|^n by A1,NEWTON02:40; then
a|^n < (k+1)|^n by A2,XXREAL_0:2; then
a < k+1 by NEWTON02:41; then
consider l be Nat such that
A5: k + 1 = a + l by NAT_1:10;
reconsider l as non zero Nat by A3,A2,A5;
(a+l)+l > (a+l) + 0 by XREAL_1:6; then
(a+2*l)|^n > (k+1)|^n by A5,NEWTON02:40; then
(a+2*l)|^n > b by A2,XXREAL_0:2;
hence thesis by A3;
end;
theorem
for a be Nat, n be non zero Nat st n-root a is irrational
holds ex b be Nat st 1 < a < (2*b + 1)|^n
proof
let a be Nat, n be non zero Nat;
assume
A1: n-root a is irrational; then
a <> 0; then
a <> 1 & a >= 1 by NAT_1:14,A1; then
a > 1 by XXREAL_0:1; then
ex b be Nat st 1|^n < a < (1 + 2*b)|^n by Th12,A1,Th23;
hence thesis;
end;
theorem Th25:
for a be non zero Nat, n be non trivial Nat, m be Nat holds
n-root (a|^(n*m) + 1) is irrational
proof
let a be non zero Nat, n be non trivial Nat, m be Nat;
a|^(n*m) = (a|^m)|^n by NEWTON:9;
hence thesis;
end;
theorem
for a,n be non trivial Nat, m be non zero Nat holds
n-root (a|^(n*m) - 1) is irrational
proof
let a,n be non trivial Nat, m be non zero Nat;
a|^(n*m) = (a|^m)|^n by NEWTON:9;
hence thesis;
end;
theorem Th27:
for b be non zero Nat, n be non trivial Nat st
2-root b is natural holds 2-root (b+2) is irrational
proof
let b be non zero Nat, n be non trivial Nat;
reconsider a = b+1 as non trivial Nat;
(2-root b)*(2-root (b+2)) = 2-root ((a-1)*(a+1)) by POWER:11
.= 2-root (a|^2 - 1|^2) by NEWTON01:1
.= 2-root (a|^2 - 1);
hence thesis;
end;
theorem
for b be non zero Nat st
2-root (b+2) is natural holds 2-root b is irrational
proof
let b be non zero Nat;
A1: (2-root b)|^2 = b;
assume
A2: 2-root (b+2) is natural;
2-root b is non integer rational implies not b is natural by A1,Th3;
hence thesis by A2,Th27;
end;
theorem Th28:
for a be prime Nat, m be Nat, n be non trivial Nat holds
n-root (a|^m) is rational iff n divides m
proof
let a be prime Nat, m be Nat, n be non trivial Nat;
thus n-root (a|^m) is rational implies n divides m
proof
assume
A: n-root (a|^m) is rational;
assume not n divides m; then
reconsider d = (m mod n) as non zero Nat by INT_1:62;
reconsider c = (m div n) as Nat;
B1: n >= 1 by NEWTON03:def 1;
d < n by NAT_D:1; then
consider k be Nat such that
B2: n = d + k by NAT_1:10;
reconsider k as non zero Nat by B2,NAT_D:1;
B3: ((d+k)-root (a|^d)) is irrational;
n-root (a|^m) = n-root (a|^(c*n + d)) by NAT_D:2
.= n-root ((a|^(n*c))*(a|^d)) by NEWTON:8
.= (n-root (a|^(n*c))) * (n-root (a|^d)) by POWER:11,B1
.= (n-root((a|^c)|^n))* (n-root(a|^d)) by NEWTON:9
.= a|^c * (n-root (a|^d));
hence thesis by A,B2,B3;
end;
assume n divides m; then
n-root (a|^m) = n-root (a|^(n*(m div n)))
.= n-root ((a|^(m div n))|^n) by NEWTON:9;
hence thesis;
end;
theorem Th29:
for a be non trivial square-free odd Nat, b be non zero Nat st
a,b are_coprime holds 2-root (a*(2*b+a)) is irrational
proof
let a be non trivial square-free odd Nat, b be non zero Nat;
assume
A1: a,b are_coprime;
b + a gcd b = a+1*b gcd b .= 1 by NEWTON02:5,A1; then
(2*b + a) gcd a = 1 by NEWTON02:59; then
a gcd (2*b + a) <> |.a.| by NEWTON03:def 1; then
(1+1)-root (a|^1*(2*b+a)) is irrational by Th20,NEWTON02:3;
hence thesis;
end;
theorem
for a be square-free odd Nat, b be non zero Nat st a,b are_coprime &
2-root (a*(2*b+a)) is rational holds a is trivial by Th29;
theorem ::: obvious for the checker
for a be non trivial square-free Nat, n be non trivial Nat holds
n-root a is irrational;
theorem ::: obvious for the checker
for a be prime Nat, n be non trivial Nat holds n-root a is irrational;
theorem
for b be non zero Nat holds
2-root (b|^2 + 2) is irrational
proof
let b be non zero Nat;
2-root (b|^2) is natural;
hence thesis by Th27;
end;
theorem Th35:
for a,b be non zero Nat st
b <= 2*a holds 2-root (a|^2 + b) is irrational
proof
let a,b be non zero Nat;
A1: (a+1+0)|^2 = a|^2 + 1|^2 + 0|^2 + 2*a*1 + 2*a*0 + 2*1*0 by SERIES_4:1;
assume b <= 2*a; then
b < 2*a + 1 by NAT_1:13; then
2*a + 1 + a|^2 > b + a|^2 by XREAL_1:6; then
(a+1)|^2 > a|^2 + b > a|^2 + 0 by A1,XREAL_1:6;
hence thesis by Th4;
end;
theorem
for a,b be non zero Nat holds
2-root (a|^2 + b|^2) is natural implies b|^2 > 2*a by Th35;
theorem
for a,b be Nat st a > b holds 2-root (a|^2 + 2*b + 1) is irrational
proof
let a be Nat, b be Nat;
assume a > b; then
a - b > b - b by XREAL_1:9; then
reconsider x = a - b as non zero Nat;
A2: (b + x)|^2 + 0 < (b + x)|^2 + (2*b + 1) by XREAL_1:6;
A3: ((b + x) + 1)|^2 = ((b + x) + 1)*((b + x) + 1) &
(b + x)|^2 = (b + x)*(b + x) by NEWTON:81;
((b + x)|^2 + 2*b + 1) + 0 < ((b + x)|^2 + (2*b + 1)) + 2*x by XREAL_1:6;
hence thesis by A2,A3,Th4;
end;
theorem
for a,b be non zero Nat st
b <= 2*a holds 2-root ((a+1)|^2 - b) is irrational
proof
let a,b be non zero Nat;
A1: (a+1+0)|^2 = a|^2 + 1|^2 + 0|^2 + 2*a*1 + 2*a*0 + 2*1*0 by SERIES_4:1;
assume b <= 2*a; then
b < 2*a + 1 by NAT_1:13; then
(a+1)|^2 - (2*a + 1) < (a+1)|^2 - b by XREAL_1:10; then
(a+1)|^2 - 0 > (a+1)|^2 - b > a|^2 + 0 by A1,XREAL_1:10;
hence thesis by Th4;
end;
theorem
for a be prime Nat, b be non zero Nat, n be non trivial Nat holds
b < a|^n & a divides b implies n-root b is irrational by Th21;
theorem
for a,b be non zero Nat, n be non trivial Nat holds
b < (Radical a)|^n & (Radical a) divides b implies
n-root b is irrational by Th21;
theorem
for a be prime Nat, n be non trivial Nat, b, m be Nat st
not a divides b & not n divides m holds n-root (a|^m*b) is irrational
proof
let a be prime Nat, n be non trivial Nat, b, m be Nat such that
A0: not a divides b & not n divides m;
reconsider b,m as non zero Nat by A0,INT_2:12;
a gcd b <> |.a.| by A0,NEWTON02:3; then
A1: a, b are_coprime by PEPIN:2;
n-root (a|^m) is irrational by A0,Th28;
hence thesis by A1,WSIERP_1:10,Th8;
end;
theorem
for a be square-free Nat, n be non trivial Nat holds
n-root a is Rational iff a = 1
proof
let a be square-free Nat, n be non trivial Nat;
per cases;
suppose a = 1;
hence thesis;
end;
suppose
a <> 1; then
reconsider a as non trivial Nat by NAT_2:def 1;
n-root a is irrational;
hence thesis;
end;
end;
theorem
for a be Nat, n be non zero Nat holds n-root a is rational implies
n-root (Parity a) is rational & n-root (Oddity a) is rational
proof
let a be Nat, n be non zero Nat;
assume
A1: n-root a is rational;
reconsider m = Parity a as Nat;
Oddity a is natural; then
reconsider k = Oddity a as Nat;
per cases;
suppose a is zero; then
reconsider a as zero Nat;
Parity a = 0 by NEWTON05:def 3; then
Oddity a = a/0 by NEWTON05:def 4;
hence thesis;
end;
suppose a is non zero; then
reconsider a as non zero Nat;
A2: n-root (m*k) is rational by A1;
Parity a, Oddity a are_coprime by NEWTON05:87;
hence thesis by A2,Th8;
end;
end;
theorem
for a,b be Nat holds
(a+(sqrt 2)*(1+sqrt 2)*b)*(a+(sqrt 2)*(sqrt 2-1)*b) is rational
proof
let a,b be Nat;
(a+(sqrt 2)*(1+sqrt 2)*b)*(a+(sqrt 2)*(sqrt 2-1)*b)
= a*a+ (sqrt 2)*((sqrt 2)*2)*a*b +
(sqrt 2)*(sqrt 2+1)*b*(sqrt 2)*(sqrt 2-1)*b
.= a*a+ (sqrt 2)*(sqrt 2)*2*a*b +
(sqrt 2)*(sqrt 2+1)*b*(sqrt 2)*(sqrt 2-1)*b by XCMPLX_1:4
.= a*a+ 4*a*b + (sqrt 2)*(sqrt 2+1)*(sqrt 2)*(sqrt 2-1)*b*b
.= a*a+ 4*a*b + ((sqrt 2)*(sqrt 2))*(sqrt 2 + 1)*(sqrt 2 -1)*b*b
by XCMPLX_1:4
.= a*a+ 4*a*b + ((sqrt 2)*(sqrt 2))*((sqrt 2 + 1)*(sqrt 2 -1))*b*b
.= a*a + 4*a*b + 2*((sqrt 2)|^2 - 1|^2)*b*b by NEWTON01:1
.= a*a + 4*a*b + 2*(2-1)*b*b;
hence thesis;
end;
:: Examples of concrete facts
theorem
2-root (123|^4 - 1) is irrational
proof
2 is non trivial & 123 is non trivial; then
2-root (123|^(2*2) - 1) is irrational;
hence thesis;
end;
theorem
3-root (678|^9 + 1) is irrational
proof
3 is non trivial & 678 is non zero; then
3-root (678|^(3*3) + 1) is irrational by Th25;
hence thesis;
end;