:: Niven's Theorem
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received December 15, 2016
:: Copyright (c) 2016-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 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, XXREAL_0, CARD_1, SIN_COS, ARYTM_3, RAT_1, ARYTM_1,
RELAT_1, NAT_1, POLYNOM1, VECTSP_1, SUBSET_1, POLYNOM2, XCMPLX_0,
HURWITZ, POLYNOM3, FUNCT_4, STRUCT_0, XBOOLE_0, GROUP_1, ALGSTR_0,
ALGSEQ_1, FUNCT_1, SUPINF_2, NUMBERS, CAT_1, VALUED_0, MESFUNC1,
FINSEQ_1, AFINSQ_1, RLVECT_1, CARD_3, BINOP_1, TARSKI, SQUARE_1, INT_1,
XXREAL_1, COMPLEX1, RATFUNC1, POLYNOM5, PARTFUN1, LATTICES, ORDINAL4,
RFINSEQ, NEWTON, FINSEQ_2, VECTSP_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, INT_1, RAT_1, VALUED_0, COMPLEX1, INT_2, NAT_D,
XXREAL_1, FINSEQ_1, FINSEQ_2, RVSUM_1, RFINSEQ, FUNCT_7, NEWTON, SIN_COS,
STRUCT_0, ALGSTR_0, ALGSTR_1, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2,
VFUNCT_1, NORMSP_1, FVSUM_1, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5,
UPROOTS, HURWITZ, RATFUNC1, RING_4;
constructors SIN_COS, ALGSEQ_1, POLYNOM4, HURWITZ, FUNCT_7, TOPMETR, POLYNOM5,
BINOP_2, NAT_D, FINSEQ_4, SQUARE_1, RATFUNC1, RCOMP_1, NEWTON, VFUNCT_1,
UPROOTS, GR_CY_1, RFINSEQ, FVSUM_1, VECTSP_2, ALGSTR_1;
registrations XREAL_0, RELAT_1, FUNCT_1, ORDINAL1, RAT_1, SIN_COS, SIN_COS6,
INT_1, XXREAL_0, INT_6, VECTSP_1, CARD_1, POLYNOM3, FUNCT_7, PRE_POLY,
STRUCT_0, RLVECT_1, MEMBERED, RELSET_1, POLYNOM5, SQUARE_1, RING_4,
XCMPLX_0, NUMBERS, FUNCT_2, XBOOLE_0, NAT_1, VFUNCT_1, VALUED_0,
FINSEQ_1, NEWTON, FINSEQ_2, WSIERP_1, VECTSP_2, ALGSTR_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_2, ALGSEQ_1, RATFUNC1;
equalities XCMPLX_0, VECTSP_1, POLYNOM3, HURWITZ, POLYNOM5, STRUCT_0,
SQUARE_1, SIN_COS, RATFUNC1, ALGSTR_0;
expansions TARSKI, ALGSEQ_1, RATFUNC1, POLYNOM5, UPROOTS;
theorems ENUMSET1, XCMPLX_1, XREAL_1, SIN_COS, FUNCT_7, FUNCOP_1, ORDINAL1,
NAT_1, ALGSEQ_1, FUNCT_2, POLYNOM5, XREAL_0, POLYNOM4, FINSEQ_3, GROUP_1,
FINSEQ_1, RLVECT_1, SIN_COS5, RAT_1, COMPLEX2, COMPTRIG, XXREAL_1,
ABSVALUE, XXREAL_0, FUNCT_1, RELAT_1, EUCLID10, INT_1, TARSKI, COMPLEX1,
INT_2, WSIERP_1, POLYNOM3, VFUNCT_1, NORMSP_1, HURWITZ, RATFUNC1,
UPROOTS, SIN_COS4, FINSEQ_2, FINSEQ_5, RVSUM_1, PARTFUN1, NAT_D, FVSUM_1,
NEWTON, PREPOWER, CARD_4, ZFMISC_1, NEWTON03, NEWTON04, POLYNOM2;
schemes NAT_1, INT_1, FIB_NUM2, FINSEQ_1;
begin
reserve r,t for Real;
reserve i for Integer;
reserve k,n for Nat;
reserve p for Polynomial of F_Real;
reserve e for Element of F_Real;
reserve L for non empty ZeroStr;
reserve z,z0,z1,z2 for Element of L;
Lm1: 2-'1 = 2-1 by XREAL_0:def 2;
Lm2: 3-'1 = 3-1 by XREAL_0:def 2;
theorem Th1:
for a,b,c,d being Complex st b <> 0 & a/b = c/d holds a = b*c/d
proof
let a,b,c,d be Complex;
assume that
A1: b <> 0 and
A2: a/b = c/d;
thus a = b*(a/b) by A1,XCMPLX_1:87
.= b*c/d by A2,XCMPLX_1:74;
end;
theorem Th2:
for a,b being Real st |.a.| = b holds a = b or a = -b
proof
let a be Real;
|.a.| = a or |.a.| = -a by COMPLEX1:71;
hence thesis;
end;
theorem Th3:
|.i.| <= 2 implies i = -2 or i = -1 or i = 0 or i = 1 or i = 2
proof
assume |.i.| <= 2;
then |.i.| = 0 or ... or |.i.| = 2;
hence thesis by ABSVALUE:2,Th2;
end;
theorem Th4:
n <> 0 implies i divides i |^ n
proof
assume n <> 0;
then consider b being Nat such that
A1: n = b+1 by NAT_1:6;
reconsider b as Element of NAT by ORDINAL1:def 12;
i |^ 1 divides i |^ (b+1) by NAT_1:12,NEWTON03:16;
hence thesis by A1;
end;
theorem Th16:
t > 0 implies ex i st t*i <= r <= t*(i+1)
proof
assume
A0: t > 0;
defpred P[Integer] means t*$1 <= r;
g: ex i1 being Integer st P[i1]
proof
take i1=[\r/t/];
i1 <= r/t by INT_1:def 6;
then i1*t <= r/t*t by A0,XREAL_1:64;
then t*i1 <= r/(t/t) by XCMPLX_1:82;
hence t*i1 <= r by A0,XCMPLX_1:51;
end;
set F=[/r/t\];
f: for i1 being Integer st P[i1] holds i1 <= F
proof
let i1 be Integer;
assume P[i1];
then i1*t/t <= r/t by A0,XREAL_1:72;
then i1*(t/t) <= r/t;
then i1*1 <= r/t & r/t <= [/r/t\] by A0,XCMPLX_1:60,INT_1:def 7;
hence i1 <= F by XXREAL_0:2;
end;
consider i such that
i: P[i] & for i1 being Integer st P[i1] holds i1<=i from INT_1:sch 6(f,g);
take i;
thus t*i <= r by i;
i+1 > i+0 by XREAL_1:6;
hence r <= t*(i+1) by i;
end;
theorem Th49: ::: MATRPROB:36
for p being FinSequence of F_Real
for q being real-valued FinSequence st p = q holds Sum p = Sum q
proof
defpred P[FinSequence] means
for p being FinSequence of F_Real
for q being real-valued FinSequence st p=q & p=$1 holds
Sum p = Sum q;
A1: P[{}]
proof
let p be FinSequence of F_Real;
let q be real-valued FinSequence;
assume
A2: p = q & p={};
then p=<*>the carrier of F_Real & q=<*>REAL;
hence Sum p = 0.F_Real by RLVECT_1:43
.= Sum q by A2,RVSUM_1:72;
end;
A3: for f being FinSequence, x being object st P[f] holds P[f^<*x*>]
proof
let f be FinSequence, x be object;
assume A4: P[f];
thus P[f^<*x*>]
proof
let p1 be FinSequence of F_Real;
let q1 be real-valued FinSequence;
assume A5: p1=q1 & p1=f^<*x*>;
reconsider fp=f as FinSequence of F_Real by A5,FINSEQ_1:36;
rng fp c= REAL;
then
reconsider fq=f as real-valued FinSequence;
<*x*> is FinSequence of F_Real by A5,FINSEQ_1:36;
then
rng <*x*> c= the carrier of F_Real by FINSEQ_1:def 4;
then {x} c= the carrier of F_Real by FINSEQ_1:38;
then
reconsider xp=x as Element of F_Real by ZFMISC_1:31;
reconsider xq=xp as Real;
thus Sum p1 = Sum fp + Sum <*xp*> by A5,RLVECT_1:41
.= Sum fp + xp by RLVECT_1:44
.= Sum fq + xq by A4
.= Sum q1 by A5,RVSUM_1:74;
end;
end;
let p be FinSequence of F_Real;
let q be real-valued FinSequence;
for f being FinSequence holds P[f] from FINSEQ_1:sch 3(A1,A3);
hence thesis;
end;
theorem Th48:
for i being Nat, r being Element of F_Real
holds power(F_Real).(r,i) = r |^ i
proof
let i be Nat;
let r be Element of F_Real;
defpred P[Nat] means power(F_Real).(r,$1) = r |^ $1;
power(F_Real).(r,0) = 1_F_Real by GROUP_1:def 7
.= r |^ 0 by NEWTON:4;
then A1: P[0];
A2: now
let n be Nat;
assume A3: P[n];
power(F_Real).(r,n+1) = power(F_Real).(r,n)*r by GROUP_1:def 7
.= r |^ (n+1) by A3,NEWTON:6;
hence P[n+1];
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence power(F_Real).(r,i) = r |^ i;
end;
theorem Th5:
sin(5*PI/6) = 1/2
proof
5*PI/6 = PI-PI/6;
hence thesis by EUCLID10:1,17;
end;
theorem
sin(5*PI/6+2*PI*i) = 1/2 by COMPLEX2:8,Th5;
theorem Th7:
sin(7*PI/6) = -1/2
proof
7*PI/6 = PI+PI/6;
hence thesis by EUCLID10:17,SIN_COS:79;
end;
theorem
sin(7*PI/6+2*PI*i) = -1/2 by COMPLEX2:8,Th7;
theorem Th9:
sin(11*PI/6) = -1/2
proof
11*PI/6 = 2*PI-PI/6;
hence thesis by EUCLID10:3,17;
end;
theorem
sin(11*PI/6+2*PI*i) = -1/2 by COMPLEX2:8,Th9;
theorem Th11:
cos(4*PI/3) = -1/2
proof
4*PI/3 = PI+PI/3;
hence thesis by EUCLID10:14,SIN_COS:79;
end;
theorem
cos(4*PI/3+2*PI*i) = -1/2 by COMPLEX2:9,Th11;
theorem Th13:
cos(5*PI/3) = 1/2
proof
5*PI/3 = PI+2*PI/3;
hence cos(5*PI/3) = -cos(2*PI/3) by SIN_COS:79
.= 1/2 by EUCLID10:23;
end;
theorem
cos(5*PI/3+2*PI*i) = 1/2 by COMPLEX2:9,Th13;
theorem Th15:
0 <= r <= PI/2 & cos r = 1/2 implies r = PI/3
proof
set X = [.0,PI/2.];
set f = cos | X;
assume that
A1: 0 <= r and
A2: r <= PI/2;
A3: r in X by A1,A2,XXREAL_1:1;
assume
A4: cos r = 1/2;
A5: dom cos = REAL by FUNCT_2:def 1;
A6: PI/3 <= PI/2 by XREAL_1:76;
then
A7: PI/3 in X by XXREAL_1:1;
A8: dom f = X by A5,RELAT_1:62;
then f.r = cos(PI/3) by A1,A2,A4,EUCLID10:14,XXREAL_1:1,FUNCT_1:47
.= f.(PI/3) by A6,A8,XXREAL_1:1,FUNCT_1:47;
hence thesis by A3,A7,A8,FUNCT_1:def 4;
end;
theorem Th17: :: POLYNOM3:34'
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr
for p being sequence of L holds
(0_.L) *' p = 0_.L
proof
let L be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr;
let p be sequence of L;
now
let i be Element of NAT;
consider r be FinSequence of L such that
len r = i+1 and
A1: ((0_.L) *' p).i = Sum r and
A2: for k be Element of NAT st k in dom r holds
r.k = (0_.L).(k-'1) * p.(i+1-'k) by POLYNOM3:def 9;
now
let k be Element of NAT;
assume k in dom r;
hence r.k = (0_.L).(k-'1) * p.(i+1-'k) by A2
.= 0.L * p.(i+1-'k) by FUNCOP_1:7
.= 0.L;
end;
hence ((0_.L)*'p).i = 0.L by A1,POLYNOM3:1
.= (0_.L).i by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:def 8;
end;
registration
let L,z,n;
cluster 0_.L +* (n,z) -> finite-Support for sequence of L;
coherence
proof
let s be sequence of L such that
A1: s = 0_.L +* (n,z);
take n+1;
let i be Nat;
assume n+1 <= i;
then n < i by NAT_1:13;
hence s.i = (0_.L).i by A1,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
end;
theorem Th18:
z <> 0.L implies
for p being Polynomial of L st p = 0_.L +* (n,z) holds len p = n+1
proof
assume
A1: z <> 0.L;
let p be Polynomial of L;
assume
A2: p = 0_.L +* (n,z);
A3: n+1 is_at_least_length_of p
proof
let i be Nat such that
A4: i >= n+1;
i > n by A4,NAT_1:13;
hence p.i = (0_.L).i by A2,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
for m being Nat st m is_at_least_length_of p holds n+1 <= m
proof
let m be Nat;
assume
A5: m is_at_least_length_of p;
assume
A6: n+1 > m;
dom 0_.L = NAT by FUNCOP_1:13;
then p.n = z by A2,ORDINAL1:def 12,FUNCT_7:31;
hence contradiction by A1,A5,A6,NAT_1:13;
end;
hence thesis by A3,ALGSEQ_1:def 3;
end;
theorem
z <> 0.L implies
for p being Polynomial of L st p = 0_.L +* (n,z) holds deg p = n
proof
assume
A1: z <> 0.L;
let p be Polynomial of L;
assume p = 0_.L +* (n,z);
hence deg p = n+1-1 by A1,Th18
.= n;
end;
registration
cluster 0_.F_Real -> INT -valued;
coherence;
cluster 1_.F_Real -> INT -valued;
coherence;
end;
registration
cluster integer for Element of F_Real;
existence;
end;
theorem Th20:
rng <%z%> = {z,0.L}
proof
set p = <%z%>;
A1: p.0 = z by ALGSEQ_1:def 5;
A2: dom p = NAT by FUNCT_2:def 1;
thus rng p c= {z,0.L}
proof
let y be object;
assume y in rng p;
then consider x being object such that
A3: x in dom p and
A4: p.x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
per cases;
suppose x = 0;
hence thesis by A4,A1,TARSKI:def 2;
end;
suppose x <> 0;
then p.x = 0.L by POLYNOM5:32,NAT_1:14;
hence thesis by A4,TARSKI:def 2;
end;
end;
let y be object;
assume y in {z,0.L};
then per cases by TARSKI:def 2;
suppose y = z;
hence thesis by A1,A2,FUNCT_1:def 3;
end;
suppose
A5: y = 0.L;
p.1 = 0.L by POLYNOM5:32;
hence thesis by A2,A5,FUNCT_1:def 3;
end;
end;
definition
let L,z0,z1,z2;
func <%z0,z1,z2%> -> sequence of L equals
0_.L +* (0,z0) +* (1,z1) +* (2,z2);
coherence;
end;
theorem Th21:
<%z0,z1,z2%>.0 = z0
proof
A1: dom 0_.L = NAT by FUNCOP_1:13;
thus <%z0,z1,z2%>.0 = (0_.L+*(0,z0)+*(1,z1)).0 by FUNCT_7:32
.= (0_.L+*(0,z0)).0 by FUNCT_7:32
.= z0 by A1,FUNCT_7:31;
end;
theorem Th22:
<%z0,z1,z2%>.1 = z1
proof
A1: dom(0_.L+*(0,z0)) = dom 0_.L by FUNCT_7:30
.= NAT by FUNCOP_1:13;
thus <%z0,z1,z2%>.1 = (0_.L+*(0,z0)+*(1,z1)).1 by FUNCT_7:32
.= z1 by A1,FUNCT_7:31;
end;
theorem Th23:
<%z0,z1,z2%>.2 = z2
proof
dom(0_.L+*(0,z0)+*(1,z1)) = dom(0_.L+*(0,z0)) by FUNCT_7:30
.= dom 0_.L by FUNCT_7:30
.= NAT by FUNCOP_1:13;
hence <%z0,z1,z2%>.2 = z2 by FUNCT_7:31;
end;
theorem Th24:
3 <= n implies <%z0,z1,z2%>.n = 0.L
proof
assume
A1: 3 <= n;
then
A2: n <> 0 & n <> 1 & n <> 2;
hence <%z0,z1,z2%>.n = (0_.L +* (0,z0) +* (1,z1)).n by FUNCT_7:32
.= (0_.L +* (0,z0)).n by A2,FUNCT_7:32
.= (0_.L).n by A1,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
registration
let L,z0,z1,z2;
cluster <%z0,z1,z2%> -> finite-Support;
coherence
proof
take 3;
thus thesis by Th24;
end;
end;
theorem Th25:
len <%z0,z1,z2%> <= 3
proof
3 is_at_least_length_of <%z0,z1,z2%> by Th24;
hence thesis by ALGSEQ_1:def 3;
end;
theorem Th26:
z2 <> 0.L implies len <%z0,z1,z2%> = 3
proof
assume z2 <> 0.L;
then <%z0,z1,z2%>.2 <> 0.L by Th23;
then
A1: for n being Nat st n is_at_least_length_of <%z0,z1,z2%> holds 2+1 <= n
by NAT_1:13;
3 is_at_least_length_of <%z0,z1,z2%> by Th24;
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem Th27:
for L being right_zeroed non empty addLoopStr
for z0,z1 being Element of L holds
<%z0%> + <%z1%> = <%z0+z1%>
proof
let L be right_zeroed non empty addLoopStr;
let z0,z1 be Element of L;
set p = <%z0%>;
set q = <%z1%>;
set r = <%z0+z1%>;
let n be Element of NAT;
per cases;
suppose n = 0;
then p.n = z0 & q.n = z1 & r.n = z0+z1 by POLYNOM5:32;
hence thesis by NORMSP_1:def 2;
end;
suppose n > 0;
then n >= 0+1 by NAT_1:13;
then
A1: p.n = 0.L & q.n = 0.L & r.n = 0.L by POLYNOM5:32;
0.L + 0.L = 0.L by RLVECT_1:def 4;
hence thesis by A1,NORMSP_1:def 2;
end;
end;
theorem Th28:
for L being right_zeroed non empty addLoopStr
for z0,z1,z2,z3 being Element of L holds
<%z0,z1%> + <%z2,z3%> = <%z0+z2,z1+z3%>
proof
let L be right_zeroed non empty addLoopStr;
let z0,z1,z2,z3 be Element of L;
set p = <%z0,z1%>;
set q = <%z2,z3%>;
set r = <%z0+z2,z1+z3%>;
let n be Element of NAT;
(n = 0 or ... or n = 1) or n > 1;
then per cases;
suppose n = 0;
then p.n = z0 & q.n = z2 & r.n = z0+z2 by POLYNOM5:38;
hence thesis by NORMSP_1:def 2;
end;
suppose n = 1;
then p.n = z1 & q.n = z3 & r.n = z1+z3 by POLYNOM5:38;
hence thesis by NORMSP_1:def 2;
end;
suppose n > 1;
then n >= 1+1 by NAT_1:13;
then
A1: p.n = 0.L & q.n = 0.L & r.n = 0.L by POLYNOM5:38;
0.L + 0.L = 0.L by RLVECT_1:def 4;
hence thesis by A1,NORMSP_1:def 2;
end;
end;
theorem Th29:
for L being right_zeroed non empty addLoopStr
for z0,z1,z2,z3,z4,z5 being Element of L holds
<%z0,z1,z2%> + <%z3,z4,z5%> = <%z0+z3,z1+z4,z2+z5%>
proof
let L be right_zeroed non empty addLoopStr;
let z0,z1,z2,z3,z4,z5 be Element of L;
set p = <%z0,z1,z2%>;
set q = <%z3,z4,z5%>;
set r = <%z0+z3,z1+z4,z2+z5%>;
let n be Element of NAT;
(n = 0 or ... or n = 2) or n > 2;
then per cases;
suppose n = 0;
then p.n = z0 & q.n = z3 & r.n = z0+z3 by Th21;
hence thesis by NORMSP_1:def 2;
end;
suppose n = 1;
then p.n = z1 & q.n = z4 & r.n = z1+z4 by Th22;
hence thesis by NORMSP_1:def 2;
end;
suppose n = 2;
then p.n = z2 & q.n = z5 & r.n = z2+z5 by Th23;
hence thesis by NORMSP_1:def 2;
end;
suppose n > 2;
then n >= 2+1 by NAT_1:13;
then
A1: p.n = 0.L & q.n = 0.L & r.n = 0.L by Th24;
0.L + 0.L = 0.L by RLVECT_1:def 4;
hence thesis by A1,NORMSP_1:def 2;
end;
end;
theorem Th30:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0 being Element of L holds
- <%z0%> = <%-z0%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0 be Element of L;
set p = <%z0%>;
set r = <%-z0%>;
let n be Element of NAT;
A1: dom -p = NAT by FUNCT_2:def 1;
A2: (-p).n = (-p)/.n
.= -(p/.n) by A1,VFUNCT_1:def 5
.= -(p.n);
per cases;
suppose n = 0;
then p.n = z0 & r.n = -z0 by POLYNOM5:32;
hence thesis by A2;
end;
suppose n > 0;
then n >= 0+1 by NAT_1:13;
then p.n = 0.L & r.n = 0.L by POLYNOM5:32;
hence thesis by A2;
end;
end;
theorem Th31:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1 being Element of L holds
- <%z0,z1%> = <%-z0,-z1%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0,z1 be Element of L;
set p = <%z0,z1%>;
set r = <%-z0,-z1%>;
let n be Element of NAT;
A1: dom -p = NAT by FUNCT_2:def 1;
A2: (-p).n = (-p)/.n
.= -(p/.n) by A1,VFUNCT_1:def 5
.= -(p.n);
(n = 0 or ... or n = 1) or n > 1;
then per cases;
suppose n = 0;
then p.n = z0 & r.n = -z0 by POLYNOM5:38;
hence thesis by A2;
end;
suppose n = 1;
then p.n = z1 & r.n = -z1 by POLYNOM5:38;
hence thesis by A2;
end;
suppose n > 1;
then n >= 1+1 by NAT_1:13;
then p.n = 0.L & r.n = 0.L by POLYNOM5:38;
hence thesis by A2;
end;
end;
theorem Th32:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1,z2 being Element of L holds
- <%z0,z1,z2%> = <%-z0,-z1,-z2%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0,z1,z2 be Element of L;
set p = <%z0,z1,z2%>;
set r = <%-z0,-z1,-z2%>;
let n be Element of NAT;
A1: dom -p = NAT by FUNCT_2:def 1;
A2: (-p).n = (-p)/.n
.= -(p/.n) by A1,VFUNCT_1:def 5
.= -(p.n);
(n = 0 or ... or n = 2) or n > 2;
then per cases;
suppose n = 0;
then p.n = z0 & r.n = -z0 by Th21;
hence thesis by A2;
end;
suppose n = 1;
then p.n = z1 & r.n = -z1 by Th22;
hence thesis by A2;
end;
suppose n = 2;
then p.n = z2 & r.n = -z2 by Th23;
hence thesis by A2;
end;
suppose n > 2;
then n >= 2+1 by NAT_1:13;
then p.n = 0.L & r.n = 0.L by Th24;
hence thesis by A2;
end;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1 being Element of L holds
<%z0%> - <%z1%> = <%z0-z1%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0,z1 be Element of L;
thus <%z0%> - <%z1%> = <%z0%> + <%-z1%> by Th30
.= <%z0-z1%> by Th27;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1,z2,z3 being Element of L holds
<%z0,z1%> - <%z2,z3%> = <%z0-z2,z1-z3%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0,z1,z2,z3 be Element of L;
thus <%z0,z1%> - <%z2,z3%> = <%z0,z1%> + <%-z2,-z3%> by Th31
.= <%z0-z2,z1-z3%> by Th28;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1,z2,z3,z4,z5 being Element of L holds
<%z0,z1,z2%> - <%z3,z4,z5%> = <%z0-z3,z1-z4,z2-z5%>
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let z0,z1,z2,z3,z4,z5 be Element of L;
thus <%z0,z1,z2%> - <%z3,z4,z5%> = <%z0,z1,z2%> + <%-z3,-z4,-z5%> by Th32
.= <%z0-z3,z1-z4,z2-z5%> by Th29;
end;
theorem Th36:
for L being add-associative right_zeroed right_complementable
left-distributive unital associative non empty doubleLoopStr
for z0,z1,z2,x being Element of L
holds eval(<%z0,z1,z2%>,x) = z0+z1*x+z2*x*x
proof
let L be add-associative right_zeroed right_complementable left-distributive
unital associative non empty doubleLoopStr;
let z0,z1,z2,x be Element of L;
consider F being FinSequence of L such that
A1: eval(<%z0,z1,z2%>,x) = Sum F and
A2: len F = len <%z0,z1,z2%> and
A3: for n being Element of NAT st n in dom F holds
F.n = <%z0,z1,z2%>.(n-'1)*(power L).(x,n-'1) by POLYNOM4:def 2;
A4: now
assume 1 in dom F;
hence F.1 = <%z0,z1,z2%>.(1-'1) * (power L).(x,1-'1) by A3
.= <%z0,z1,z2%>.0 * (power L).(x,1-'1) by XREAL_1:232
.= <%z0,z1,z2%>.0 * (power L).(x,0) by XREAL_1:232
.= z0 * (power L).(x,0) by Th21
.= z0 * 1_L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
end;
A5: now
assume 2 in dom F;
hence F.2 = <%z0,z1,z2%>.(2-'1) * (power L).(x,2-'1) by A3
.= z1*(power L).(x,1) by Lm1,Th22
.= z1*x by GROUP_1:50;
end;
len F = 0 or ... or len F = 3 by A2,Th25;
then per cases;
suppose len F = 0; then
A6: <%z0,z1,z2%> = 0_.L by A2,POLYNOM4:5;
hence eval(<%z0,z1,z2%>,x) = 0.L by POLYNOM4:17
.= (0_.L).0 by FUNCOP_1:7
.= z0 + 0.L + 0.L by A6,Th21
.= z0 + (0_.L).1*x + 0.L*x*x by FUNCOP_1:7
.= z0 + (0_.L).1*x + (0_.L).2*x*x by FUNCOP_1:7
.= z0 + z1*x + (0_.L).2*x*x by A6,Th22
.= z0 + z1*x + z2*x*x by A6,Th23;
end;
suppose
A7: len F = 1;
then 0 + 1 in Seg len F by FINSEQ_1:1;
then F = <*z0*> by A4,A7,FINSEQ_1:def 3,40;
hence eval(<%z0,z1,z2%>,x) = z0 by A1,RLVECT_1:44
.= z0 + 0.L*x + <%z0,z1,z2%>.2*x*x by A2,A7,ALGSEQ_1:8
.= z0 + <%z0,z1,z2%>.1*x + <%z0,z1,z2%>.2*x*x by A2,A7,ALGSEQ_1:8
.= z0 + z1*x + <%z0,z1,z2%>.2*x*x by Th22
.= z0 + z1*x + z2*x*x by Th23;
end;
suppose
A8: len F = 2;
F = <*z0,z1*x*> by A4,A5,A8,FINSEQ_1:44,FINSEQ_3:25;
hence eval(<%z0,z1,z2%>,x) = z0+z1*x + 0.L*x*x by A1,RLVECT_1:45
.= z0+z1*x + <%z0,z1,z2%>.2*x*x by A2,A8,ALGSEQ_1:8
.= z0+z1*x + z2*x*x by Th23;
end;
suppose
A9: len F = 3;
F.3 = <%z0,z1,z2%>.(3-'1) * (power L).(x,3-'1) by A3,A9,FINSEQ_3:25
.= z2 * (power L).(x,2) by Lm2,Th23
.= z2*(x*x) by GROUP_1:51
.= z2*x*x by GROUP_1:def 3;
then F = <*z0,z1*x,z2*x*x*> by A4,A5,A9,FINSEQ_1:45,FINSEQ_3:25;
hence thesis by A1,RLVECT_1:46;
end;
end;
registration
let a be integer Element of F_Real;
cluster <%a%> -> INT -valued;
coherence
proof
rng <%a%> c= {a,0.F_Real} by Th20;
hence rng <%a%> c= INT by INT_1:def 2;
end;
end;
registration
let a,b be integer Element of F_Real;
cluster <%a,b%> -> INT -valued;
coherence
proof
reconsider a1 = a, b1 = b as Element of INT by INT_1:def 2;
<%a,b%> = 0_.F_Real +* (0,a1) +* (1,b1);
hence thesis;
end;
end;
registration
let a,b,c be integer Element of F_Real;
cluster <%a,b,c%> -> INT -valued;
coherence
proof
reconsider a1 = a, b1 = b, c1 = c as Element of INT by INT_1:def 2;
<%a,b,c%> = 0_.F_Real +* (0,a1) +* (1,b1) +* (2,c1);
hence thesis;
end;
end;
registration
cluster monic INT -valued for Polynomial of F_Real;
existence
proof
take 1_.F_Real;
thus thesis;
end;
end;
registration
cluster INT -valued for FinSequence of F_Real;
existence
proof
take <*>the carrier of F_Real;
thus thesis;
end;
end;
registration
let F be INT -valued FinSequence of F_Real;
cluster Sum F -> integer;
coherence
proof
consider f being sequence of F_Real such that
A1: Sum F = f.(len F) and
A2: f.0 = 0.F_Real and
A3: for j being Nat, v being Element of F_Real st j < len F & v = F.(j + 1)
holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Nat] means
$1 <= len F implies f.$1 is integer;
A4: P[0] by A2;
A5: P[k] implies P[k+1]
proof
assume that
A6: P[k] and
A7: k+1 <= len F;
reconsider v = F.(k+1) as Element of F_Real by XREAL_0:def 1;
A8: k+0 < k+1 by XREAL_1:8;
then k < len F by A7,XXREAL_0:2;
then f.(k+1) = f.k + v by A3;
hence thesis by A6,A8,A7,XXREAL_0:2;
end;
P[k] from NAT_1:sch 2(A4,A5);
hence thesis by A1;
end;
end;
registration
let f be INT -valued sequence of F_Real;
cluster -f -> INT -valued;
coherence
proof
let y be object;
assume y in rng(-f);
then consider x being object such that
A1: x in dom(-f) and
A2: (-f).x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A1;
(-f).x = (-f)/.x
.= -(f/.x) by A1,VFUNCT_1:def 5
.= -(f.x);
hence thesis by A2,INT_1:def 2;
end;
let g be INT -valued sequence of F_Real;
cluster f+g -> INT -valued;
coherence
proof
let y be object;
assume y in rng(f+g);
then consider x being object such that
A3: x in dom(f+g) and
A4: (f+g).x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
(f+g).x = f.x+g.x by NORMSP_1:def 2;
hence thesis by A4,INT_1:def 2;
end;
cluster f-g -> INT -valued;
coherence;
cluster f*'g -> INT -valued;
coherence
proof
let y be object;
assume y in rng(f*'g);
then consider x being object such that
A5: x in dom(f*'g) and
A6: (f*'g).x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A5;
consider r being FinSequence of F_Real such that
len r = x+1 and
A7: (f*'g).x = Sum r and
A8: for k being Element of NAT st k in dom r holds r.k = f.(k-'1) * g.(x+1-'k)
by POLYNOM3:def 9;
r is INT -valued
proof
let y be object;
assume y in rng r;
then consider a being object such that
A9: a in dom r and
A10: r.a = y by FUNCT_1:def 3;
reconsider a as Element of NAT by A9;
r.a = f.(a-'1) * g.(x+1-'a) by A8,A9;
hence y in INT by A10,INT_1:def 2;
end;
hence thesis by A6,A7,INT_1:def 2;
end;
end;
theorem Th37:
for L being non degenerated non empty doubleLoopStr, z being Element of L
holds LC <%z,1.L%> = 1.L
proof
let L be non degenerated non empty doubleLoopStr;
let z be Element of L;
len <%z,1.L%> = 2 by POLYNOM5:40;
hence thesis by Lm1,POLYNOM5:38;
end;
registration
let L be non degenerated non empty doubleLoopStr;
let z be Element of L;
cluster <%z,1.L%> -> monic;
coherence by Th37;
end;
theorem Th38:
for L being non degenerated non empty doubleLoopStr, z1,z2 being Element of L
holds LC <%z1,z2,1.L%> = 1.L
proof
let L be non degenerated non empty doubleLoopStr;
let z1,z2 be Element of L;
len <%z1,z2,1.L%> = 3 by Th26;
hence thesis by Lm2,Th23;
end;
registration
let L be non degenerated non empty doubleLoopStr;
let z1,z2 be Element of L;
cluster <%z1,z2,1.L%> -> monic;
coherence by Th38;
end;
registration
let p be INT -valued Polynomial of F_Real;
cluster LC p -> integer;
coherence;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p being Polynomial of L holds
deg(-p) = deg p by POLYNOM4:8;
theorem Th40:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p,q being Polynomial of L st deg p > deg q holds
deg(p+q) = deg p
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p,q be Polynomial of L;
assume
A1: deg p > deg q;
then deg(p+q) = max(deg(p),deg(q)) by HURWITZ:21;
hence thesis by A1,XXREAL_0:def 10;
end;
theorem Th41:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p,q being Polynomial of L st deg p > deg q holds
deg(p-q) = deg p
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p,q be Polynomial of L;
assume
A1: deg p > deg q;
A2: deg q = deg(-q) by POLYNOM4:8;
then deg(p+-q) = max(deg(p),deg(-q)) by A1,HURWITZ:21;
hence thesis by A1,A2,XXREAL_0:def 10;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p,q being Polynomial of L st deg p < deg q holds
deg(p-q) = deg q
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p,q be Polynomial of L;
assume
A1: deg p < deg q;
deg(-q) = deg q by POLYNOM4:8;
then deg(p+-q) = max(deg(p),deg(q)) by A1,HURWITZ:21;
hence thesis by A1,XXREAL_0:def 10;
end;
theorem
for L being add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr
for p being Polynomial of L holds
LC p = -LC -p
proof
let L be add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr;
let p be Polynomial of L;
A1: len p = len(-p) by POLYNOM4:8;
A2: dom(-p) = NAT by FUNCT_2:def 1;
thus LC p = --(p/.(len p-'1))
.= -((-p)/.(len(-p)-'1)) by A1,A2,VFUNCT_1:def 5
.= -LC -p;
end;
lemmul: for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for p,q be Polynomial of L
st p <> 0_.(L) & q <> 0_.(L)
holds (p*'q).(len p + len q - 1 -'1) = p.(len p-'1) * q.(len q-'1)
proof
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr; let p,q be Polynomial of L;
assume p <> 0_.(L) & q <> 0_.(L);
then B: len p >= 1 & len q >= 1 by NAT_1:14,POLYNOM4:5;
then len p + len q >= 1 + 1 by XREAL_1:7;
then A: len p + len q - 1 >= 1 + 1 - 1 by XREAL_1:9;
reconsider j = len p + len q - 1 as Element of NAT by B,INT_1:3;
set i = j -' 1;
consider r being FinSequence of the carrier of L such that
M: len r = i+1 & (p*'q).i = Sum r &
for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i+1-'k)
by POLYNOM3:def 9;
A7: j - 1 = i by A,XREAL_0:def 2;
reconsider x = len q - 1 as Element of NAT by B,INT_1:3;
A3: j = len p + x;
then j >= len p by NAT_1:11;
then A1: len p in dom r by A7,M,B,FINSEQ_3:25;
A2: i+1-'(len p)
= (len p + len q - 1 - 1 + 1) - (len p) by A3,A7,XREAL_0:def 2
.= len p - (len p) + len q - 1
.= len q -' 1 by B,XREAL_0:def 2;
now let k be Element of NAT;
assume E: k in dom r & k <> len p;
per cases by E,XXREAL_0:1;
suppose E1: k > len p;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
E2: k1 + 1 > len p by E1;
k -' 1 = k - 1 by E1,XREAL_0:def 2;
then p.(k-'1) = 0.L by E2,ALGSEQ_1:8,NAT_1:13;
then r.k = 0.L * q.(i+1-'k) by E,M;
hence r/.k = 0.L by E,PARTFUN1:def 6;
end;
suppose k < len p;
then k + 1 <= len p by INT_1:7;
then k + 1 - k <= len p - k by XREAL_1:9;
then len p - k + len q >= 1 + len q by XREAL_1:6;
then E2: len p - k + len q - 1 >= len q + 1 - 1 by XREAL_1:9;
i + 1 - k = (len p + len q - 1 - 1 + 1) - k by A,XREAL_0:def 2;
then i+1-'k = len p + len q - 1 - k by E2,XREAL_0:def 2;
then q.(i+1-'k) = 0.L by E2,ALGSEQ_1:8;
then r.k = p.(k-'1) * 0.L by E,M;
hence r/.k = 0.L by E,PARTFUN1:def 6;
end;
end;
then Sum r = r/.(len p) by A1,POLYNOM2:3
.= r.(len p) by A1,PARTFUN1:def 6
.= p.(len p-'1) * q.(i+1-'(len p)) by A1,M;
hence thesis by M,A2;
end;
theorem Th44:
for L being add-associative right_zeroed right_complementable
distributive associative well-unital domRing-like
non degenerated doubleLoopStr
for p,q being Polynomial of L holds LC(p *' q) = LC(p) * LC(q)
proof
let L be add-associative right_zeroed right_complementable
distributive associative well-unital domRing-like
non degenerated doubleLoopStr;
let p,q be Polynomial of L;
per cases;
suppose
AS: p <> 0_.(L) & q <> 0_.(L);
len(p*'q) = deg(p*'q) + 1
.= deg(p) + deg(q) + 1 by AS,HURWITZ:23
.= len(p) - 1 + (len(q) - 1) + 1;
hence LC(p *' q) = (p*'q).(len p + len q - 1 -'1)
.= LC(p) * LC(q) by AS,lemmul;
end;
suppose
A30: p is zero;
then p*'q=0_.L by Th17;
hence LC(p*'q) = 0.L * LC q by FUNCOP_1:7
.= LC p * LC q by A30,FUNCOP_1:7;
end;
suppose
A31: q is zero;
then p*'q=0_.L by POLYNOM3:34;
hence LC(p*'q) = LC p * 0.L by FUNCOP_1:7
.= LC p * LC q by A31,FUNCOP_1:7;
end;
end;
Lm3:
now
let L be non degenerated doubleLoopStr;
let p be monic Polynomial of L;
let q be Polynomial of L;
assume
A1: deg p > deg q;
p <> 0_.L;
then 0 <> len p by POLYNOM4:5;
then
A2: len p - 1 = len p -' 1 by XREAL_0:def 2;
len q <= len p - 1 by A1,INT_1:52;
hence q.(len p-'1) = 0.L by A2,ALGSEQ_1:8;
end;
theorem
for L being add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr
for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
p+q is monic
proof
let L be add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr;
let p be monic Polynomial of L;
let q be Polynomial of L;
assume
A1: deg p > deg q;
then
A2: q.(len p-'1) = 0.L by Lm3;
deg(p+q) = deg p by A1,Th40;
hence LC(p+q) = p.(len p-'1) + q.(len p-'1) by NORMSP_1:def 2
.= LC p by A2
.= 1.L by RATFUNC1:def 7;
end;
theorem Th46:
for L being add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr
for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
p-q is monic
proof
let L be add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr;
let p be monic Polynomial of L;
let q be Polynomial of L;
assume
A1: deg p > deg q;
then
A2: q.(len p-'1) = 0.L by Lm3;
deg(p-q) = deg p by A1,Th41;
hence LC(p-q) = p.(len p-'1) - q.(len p-'1) by NORMSP_1:def 3
.= LC p by A2
.= 1.L by RATFUNC1:def 7;
end;
registration
let L be add-associative right_zeroed right_complementable
associative well-unital almost_left_invertible distributive non
degenerated doubleLoopStr;
let p,q be monic Polynomial of L;
cluster p*'q -> monic;
coherence
proof
LC p = 1.L & LC q = 1.L by RATFUNC1:def 7;
hence 1.L = LC p * LC q
.= LC(p*'q) by Th44;
end;
end;
theorem Th47:
for L being Abelian add-associative right_zeroed right_complementable
unital distributive non empty doubleLoopStr
for z1,z2 being Element of L
for p being Polynomial of L st eval(p,z1) = z2
holds eval(p-<%z2%>,z1) = 0.L
proof
let L be Abelian add-associative right_zeroed right_complementable
unital distributive non empty doubleLoopStr;
let z1,z2 be Element of L;
let p be Polynomial of L such that
A1: eval(p,z1) = z2;
thus eval(p-<%z2%>,z1) = eval(p,z1) - eval(<%z2%>,z1) by POLYNOM4:21
.= z2 - z2 by A1,POLYNOM5:37
.= 0.L by RLVECT_1:15;
end;
::$N Rational root theorem
theorem Th50:
for p being INT -valued Polynomial of F_Real
for e being Element of F_Real st e is_a_root_of p
for k,l being Integer st l <> 0 & e = k/l & k,l are_coprime
holds k divides p.0 & l divides LC p
proof
let p be INT -valued Polynomial of F_Real;
let e be Element of F_Real such that
A1: e is_a_root_of p;
let k,l be Integer such that
A2: l <> 0 & e = k/l & k,l are_coprime;
consider F being FinSequence of F_Real such that
A3: 0.F_Real = Sum F & len F = len p & for n be Element of NAT st n in
dom F holds F.n = p.(n-'1) * (power F_Real).(e,n-'1) by A1,POLYNOM4:def 2;
per cases;
suppose len F = 0; then
A4: p = <%0.F_Real%> by A3,ALGSEQ_1:14;
then p.0=0.F_Real by ALGSEQ_1:16;
hence k divides p.0 by INT_2:12;
p=0_.F_Real by A4,POLYNOM5:34;
then LC p = 0.F_Real by FUNCOP_1:7;
hence l divides LC p by INT_2:12;
end;
suppose
A5: len F > 0;
set n = len p;
A6: n >= 1 by A5,A3,NAT_1:14;
reconsider n1=n-1 as Element of NAT by NAT_1:20,A5,A3;
A7: n-'1 = n1 by A5,A3,NAT_1:14,XREAL_1:233;
A8: l|^(n-'1) <> 0 by A2,CARD_4:3;
reconsider k1=k,l1 = l as Element of F_Real by XREAL_0:def 1;
set ln=(power F_Real).(l1,n1);
set G=ln*F;
reconsider FF=F as Element of (len F)-tuples_on the carrier of F_Real
by FINSEQ_2:92;
set GG=ln*FF;
A9: len GG = len F by FINSEQ_2:132;
then
A10: dom G = dom F by FINSEQ_3:29;
A11: Sum G = ln * Sum F by FVSUM_1:73;
rng G c= INT
proof
let o be object;
assume o in rng G;
then consider b being object such that
A12: b in dom G & o=G.b by FUNCT_1:def 3;
reconsider b as Element of NAT by A12;
b in Seg n by A12,A9,A3,FINSEQ_1:def 3;
then 1 <= b <= n & b-'1 <= b by FINSEQ_1:1,NAT_D:35;
then b-'1 = b-1 & b-1 <= n1 by XREAL_1:233,XREAL_1:9;
then consider c being Nat such that
A13: n1=b-'1+c by NAT_1:10;
rng F c= the carrier of F_Real; then
reconsider a9=F.b as Element of F_Real by A12,A10,FUNCT_1:3;
A14: l|^(b-'1) <> 0 by A2,CARD_4:3;
b in dom (ln*F) & a9 = F.b implies (ln*F).b = ln*a9 by FVSUM_1:50;
then
G.b = ln*(p.(b-'1) * (power F_Real).(e,b-'1)) by A3,A12,A10
.= p.(b-'1) * ((power F_Real).(l1,n1) * (power F_Real).(e,b-'1))
.= p.(b-'1) * ((l1|^n1) * (power F_Real).(e,b-'1)) by Th48
.= p.(b-'1) * ((l1|^n1) * ((k/l)|^(b-'1))) by A2,Th48
.= p.(b-'1) * ((l|^n1) * ((k|^(b-'1))/(l|^(b-'1)))) by PREPOWER:8
.= p.(b-'1) * (k|^(b-'1)) * ((l|^n1)/(l|^(b-'1)))
.= p.(b-'1) * (k|^(b-'1)) * ((l|^c)*(l|^(b-'1))/(l|^(b-'1)))
by A13,NEWTON:8
.= p.(b-'1) * (k|^(b-'1)) * ((l|^c)*((l|^(b-'1))/(l|^(b-'1))))
.= p.(b-'1) * (k|^(b-'1)) * ((l|^c) * 1) by XCMPLX_1:60,A14
.= p.(b-'1) * (k|^(b-'1)) * (l|^c);
hence o in INT by INT_1:def 2,A12;
end;
then reconsider G1=G as non empty INT -valued FinSequence
by A9,A5,RELAT_1:def 19;
A15: 1 in dom G by A9,A6,A3,FINSEQ_3:25;
A16: Sum G1 = Sum G by Th49;
A17: Sum G1 = 0 by A3,A11,Th49;
reconsider Gn0=G1/^1 as INT -valued FinSequence;
G = <*G/.1*>^Gn0 by FINSEQ_5:29;
then Sum Gn0 + G/.1 = 0 by RVSUM_1:76,A16,A11,A3;
then Sum Gn0 + G.1 = 0 by A15,PARTFUN1:def 6;
then
A18: Sum Gn0 = - G1.1;
rng F c= the carrier of F_Real; then
reconsider a9=F.1 as Element of F_Real by A15,A10,FUNCT_1:3;
A19: G1.1 = ln * a9 by FVSUM_1:50,A15
.= ln * (p.(1-'1) * (power F_Real).(e,1-'1)) by A6,A3,FINSEQ_3:25
.= p.(1-'1) * ln * (power F_Real).(e,1-'1)
.= p.(1-'1) * ln * (power F_Real).(e,0) by XREAL_1:232
.= p.0 * ln * (power F_Real).(e,0) by XREAL_1:232
.= p.0 * ln * 1_F_Real by GROUP_1:def 7
.= p.0 * (l|^n1) by Th48;
for i being Nat st i in dom Gn0 holds k divides Gn0.i
proof
let i be Nat;
assume
A20: i in dom Gn0; then
A21: 1+i in dom G1 by FINSEQ_5:26;
rng F c= the carrier of F_Real; then
reconsider a9=F.(1+i) as Element of F_Real by A21,A10,FUNCT_1:3;
A22: l|^i <> 0 by A2,CARD_4:3;
A23: 1 <= i <= len Gn0 by A20,FINSEQ_3:25;
i+1 in Seg n by A3,A21,A9,FINSEQ_1:def 3;
then i+1 <= n by FINSEQ_1:1;
then i+1-1 <= n-1 by XREAL_1:9;
then consider d being Nat such that
A24: n1=i+d by NAT_1:10;
Gn0.i = (G/^1)/.i by A20,PARTFUN1:def 6
.= G/.(1+i) by FINSEQ_5:27,A20
.= G.(1+i) by A21,PARTFUN1:def 6
.= ln * a9 by FVSUM_1:50,A21
.= ln*(p.(1+i-'1) * (power F_Real).(e,1+i-'1)) by A3,A21,A10
.= ln*(p.i * (power F_Real).(e,1+i-'1)) by NAT_D:34
.= ln*(p.i * (power F_Real).(e,i)) by NAT_D:34
.= p.i * ((power F_Real).(l1,n1) * (power F_Real).(e,i))
.= p.i * ((l1|^n1) * (power F_Real).(e,i)) by Th48
.= p.i * ((l1|^n1) * (e|^i)) by Th48
.= p.i * ((l|^n1) * ((k|^i)/(l|^i))) by A2,PREPOWER:8
.= p.i * (k|^i) * ((l|^(d+i)/(l|^i))) by A24
.= p.i * (k|^i) * ((l|^d)*(l|^i)/(l|^i)) by NEWTON:8
.= p.i * (k|^i) * ((l|^d)*((l|^i)/(l|^i)))
.= p.i * (k|^i) * ((l|^d) * 1) by XCMPLX_1:60,A22
.= p.i * (l|^d) * (k|^i);
hence k divides Gn0.i by A23,Th4,INT_2:2;
end;
then k divides G1.1 by A18,NEWTON04:80,INT_2:10;
hence k divides p.0 by A19,A2,WSIERP_1:10,INT_2:25;
reconsider Gn1=G1|(Seg n1) as INT -valued FinSequence by FINSEQ_1:15;
A25: len GG = len F by FINSEQ_2:132; then
A26: len G1 = n1+1 by A3;
G1 = Gn1^<*G1.(n1+1)*> by A25,A3,FINSEQ_3:55;
then Sum Gn1 + G1.(n1+1) = 0 by RVSUM_1:74,A17; then
A27: Sum Gn1 = - G1.(n1+1) .= - G1.n;
A28: n in dom F by FINSEQ_3:25,A6,A3;
rng F c= the carrier of F_Real; then
reconsider a9=F.n as Element of F_Real by A28,FUNCT_1:3;
n in dom G1 by A25,A3,FINSEQ_3:25,A6; then
A29: G1.n = ln * a9 by FVSUM_1:50
.= ln * (p.(n-'1) * (power F_Real).(e,n-'1)) by A6,A3,FINSEQ_3:25
.= p.(n-'1) * ((power F_Real).(l1,n1) * (power F_Real).(e,n-'1))
.= p.(n-'1) * ((l1|^n1) * (power F_Real).(e,n-'1)) by Th48
.= p.(n-'1) * ((l1|^n1) * (e|^(n-'1))) by Th48
.= p.(n-'1) * ((l|^n1) * ((k|^(n-'1))/(l|^(n-'1)))) by A2,PREPOWER:8
.= p.(n-'1) * (k|^(n-'1)) * ((l|^(n-'1))/(l|^(n-'1))) by A7
.= p.(n-'1) * (k|^(n-'1)) * 1 by A8,XCMPLX_1:60
.= LC p * (k|^(n-'1));
for i being Nat st i in dom Gn1 holds l divides Gn1.i
proof
let i be Nat;
assume
A30: i in dom Gn1;
then i in Seg n1 by A26,FINSEQ_3:54; then
A31: 1 <= i <= n1 & i-'1 <= i by FINSEQ_1:1,NAT_D:35;
then consider d being Nat such that
A32: n1=i-'1+d by XXREAL_0:2,NAT_1:10;
i-i <= n-1-i by A31,XREAL_1:9; then
A33: 0+1<=n-i-1+1 by XREAL_1:6;
A34: n-1=i-1+d by A32,A31,XREAL_1:233;
A35: Gn1.i = G1.i by A30,FUNCT_1:47;
A36: dom Gn1 c= dom G1 by RELAT_1:60;
rng F c= the carrier of F_Real; then
reconsider a9=F.i as Element of F_Real by A36,A10,A30,FUNCT_1:3;
A37: l|^(i-'1) <> 0 by A2,CARD_4:3;
G1.i = ln * a9 by A36,A30,FVSUM_1:50
.= ln*(p.(i-'1) * (power F_Real).(e,i-'1)) by A3,A36,A30,A10
.= p.(i-'1) * ((power F_Real).(l1,n1) * (power F_Real).(e,i-'1))
.= p.(i-'1) * ((l1|^n1) * (power F_Real).(e,i-'1)) by Th48
.= p.(i-'1) * ((l1|^n1) * (e|^(i-'1))) by Th48
.= p.(i-'1) * ((l|^n1) * ((k|^(i-'1))/(l|^(i-'1)))) by A2,PREPOWER:8
.= p.(i-'1) * (k|^(i-'1)) * ((l|^n1)/(l|^(i-'1)))
.= p.(i-'1) * (k|^(i-'1)) * ((l|^d)*(l|^(i-'1))/(l|^(i-'1)))
by A32,NEWTON:8
.= p.(i-'1) * (k|^(i-'1)) * ((l|^d)*((l|^(i-'1))/(l|^(i-'1))))
.= p.(i-'1) * (k|^(i-'1)) * ((l|^d) * 1) by XCMPLX_1:60,A37
.= p.(i-'1) * (k|^(i-'1)) * (l|^d);
hence l divides Gn1.i by A35,A34,A33,Th4,INT_2:2;
end;
then l divides G1.n by A27,NEWTON04:80,INT_2:10;
hence l divides LC p by A29,A2,WSIERP_1:10,INT_2:25;
end;
end;
::$N Integral root theorem
theorem Th51:
for p being monic INT -valued Polynomial of F_Real
for e being rational Element of F_Real st e is_a_root_of p
holds e is integer
proof
let p be monic INT -valued Polynomial of F_Real;
let e be rational Element of F_Real;
assume
A1: e is_a_root_of p;
set k = numerator(e);
set n = denominator(e);
A2: e = k/n;
A3: k,n are_coprime by WSIERP_1:22;
p is monic;
then n = 1 or n = -1 by A1,A2,A3,Th50,INT_2:13;
hence thesis by A2;
end;
theorem Th52:
1 <= n & e = 2*cos t implies
ex p being monic INT -valued Polynomial of F_Real
st eval(p,e) = 2*cos(n*t) & deg p = n &
(n = 1 implies p = <%0.F_Real,1.F_Real%>) &
(n = 2 implies
ex r being Element of F_Real st r = -2 & p = <%r,0.F_Real,1.F_Real%>)
proof
assume that
A1: 1 <= n and
A2: e = 2*cos t;
defpred P[Nat] means
1 <= $1 implies
ex p being monic INT -valued Polynomial of F_Real st
eval(p,e) = 2*cos($1*t) & deg p = $1 &
($1 = 1 implies p = <%0.F_Real,1.F_Real%>) &
($1 = 2 implies
ex r being Element of F_Real st r = -2 & p = <%r,0.F_Real,1.F_Real%>);
A3: P[1]
proof
assume 1 <= 1;
reconsider p = <%0.F_Real,1.F_Real%>
as monic INT -valued Polynomial of F_Real;
take p;
thus eval(p,e) = 2*cos(1*t) by A2,POLYNOM5:48;
len p = 2 by POLYNOM5:40;
hence deg p = 1;
thus thesis;
end;
A4: P[2]
proof
assume 1 <= 2;
reconsider r = -2 as Element of F_Real by XREAL_0:def 1;
reconsider p = <%r,0.F_Real,1.F_Real%>
as monic INT -valued Polynomial of F_Real;
take p;
cos(2*t) = 2*(cos t)^2-1 by SIN_COS5:7;
hence 2*cos(2*t) = r+0.F_Real*e+1.F_Real*e*e by A2
.= eval(p,e) by Th36;
len p = 3 by Th26;
hence deg p = 2;
thus thesis;
end;
A5: for k being non zero Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be non zero Nat such that
A6: P[k] and
A7: P[k+1] and
1 <= k+2;
per cases;
suppose k+2 = 1;
then k = -1;
hence thesis;
end;
suppose k+2 = 2;
hence thesis;
end;
suppose
A8: k+2 <> 1 & k+2 <> 2;
A9: 0+1 <= k by NAT_1:13;
then consider p2 being monic INT -valued Polynomial of F_Real
such that
A10: eval(p2,e) = 2*cos(k*t) and
A11: deg p2 = k by A6;
consider p1 being monic INT -valued Polynomial of F_Real
such that
A12: eval(p1,e) = 2*cos((k+1)*t) and
A13: deg p1 = k+1 by A7,A9,NAT_1:13;
set f = <%0.F_Real,1.F_Real%>;
set p = f*'p1 - p2;
p1 is non-zero; then
A14: len(f*'p1) = len p1 + 1 by UPROOTS:38; then
A15: deg(f*'p1) > deg p2 by A11,A13,XREAL_1:8;
then reconsider p as monic INT -valued Polynomial of F_Real by Th46;
take p;
A16: eval(f*'p1,e) = eval(f,e) * eval(p1,e) by POLYNOM4:24;
cos((k+2)*t) + cos(k*t)
= 2*(cos((((k+2)*t)+(k*t))/2)*cos((((k+2)*t)-(k*t))/2))
by SIN_COS4:17
.= cos t*(2*cos(k*t+t));
then 2*cos t*(2*cos(k*t+t)) - (2*cos(k*t)) = 2*cos((k+2)*t);
hence 2*cos((k+2)*t) = eval(f*'p1,e) - eval(p2,e)
by A2,A10,A12,A16,POLYNOM5:48
.= eval(p,e) by POLYNOM4:21;
thus deg p = k+2 by A13,A14,A15,Th41;
thus thesis by A8;
end;
end;
for k being non zero Nat holds P[k] from FIB_NUM2:sch 1(A3,A4,A5);
hence thesis by A1;
end;
theorem Th53:
0 <= r <= PI/2 & r/PI is rational & cos r is rational implies
r in {0,PI/3,PI/2}
proof
assume that
A1: 0 <= r and
A2: r <= PI/2 and
A3: r/PI is rational and
A4: cos r is rational;
consider k being Integer, n being Nat such that
A5: n > 0 and
A6: r/PI/2 = k/n by A3,RAT_1:8;
set e = 2*cos r;
reconsider c = e as Element of F_Real by XREAL_0:def 1;
consider p being monic INT -valued Polynomial of F_Real
such that
A7: eval(p,c) = 2*cos(n*r) and
A8: deg p = n and
(n = 1 implies p = <%0.F_Real,1.F_Real%>) &
(n = 2 implies
ex a being Element of F_Real st a = -2 & p = <%a,0.F_Real,1.F_Real%>)
by A5,NAT_1:14,Th52;
A9: n*(2*PI*k/n) = 2*PI*k by A5,XCMPLX_1:87;
A10: cos(2*PI*k+0) = 1 by SIN_COS:31,COMPLEX2:9;
reconsider r2 = 2 as Element of F_Real by XREAL_0:def 1;
r/PI/2 = r/(2*PI) by XCMPLX_1:78;
then r = 2*PI*k/n by A6,Th1;
then
A11: c is_a_root_of p-<%r2%> by A7,A9,A10,Th47;
len <%r2%> - 1 <= 1-1 by XREAL_1:9,ALGSEQ_1:def 5;
then deg p > deg <%r2%> by A5,A8;
then p-<%r2%> is monic by Th46;
then
A12: e is integer by A4,A11,Th51;
PI/2 < 2*PI by XREAL_1:68;
then
A13: r < 2*PI by A2,XXREAL_0:2;
A14: r in [.-PI/2,PI/2.] by A1,A2,XXREAL_1:1;
cos.r in [. -1,1 .] by COMPTRIG:27;
then -1 <= cos r <= 1 by XXREAL_1:1;
then 2*(-1) <= e <= 2*1 by XREAL_1:64;
then -2 <= e <= 2;
then |.e.| <= 2 by ABSVALUE:5;
then e = -2 or e = -1 or e = 0 or e = 1 or e = 2 by A12,Th3;
then cos r = -1 or cos r = -1/2 or cos r = 0 or cos r = 1/2 or cos r = 1;
then r = PI/2 or r = 3/2*PI or r = PI/3 or r = 0
by A1,A2,A13,A14,Th15,COMPTRIG:12,18,61;
hence thesis by A2,XREAL_1:68,ENUMSET1:def 1;
end;
theorem
2*PI*i <= r <= PI/2 + 2*PI*i & r/PI is rational & cos r is rational implies
r in { 2*PI*i , PI/3+2*PI*i , PI/2+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume a <= r <= PI/2 + a; then
A1: a-a <= R <= PI/2+a-a by XREAL_1:9;
assume
A2: r/PI is rational & cos r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89; then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then cos r = cos R by COMPLEX2:9;
then R in {0,PI/3,PI/2} by A1,A2,A3,Th53;
then R = 0 or R = PI/3 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th55:
PI/2 <= r <= PI & r/PI is rational & cos r is rational implies
r in {PI/2,2*PI/3,PI}
proof
set R = PI-r;
assume PI/2 <= r <= PI; then
A1: PI-PI <= R <= PI-PI/2 by XREAL_1:13;
assume
A2: r/PI is rational & cos r is rational;
A3: R/PI = PI/PI-r/PI
.= 1-r/PI by XCMPLX_1:60;
cos R = -cos r by EUCLID10:2;
then R in {0,PI/3,PI/2} by A1,A2,A3,Th53;
then R = 0 or R = PI/3 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
PI/2 + 2*PI*i <= r <= PI + 2*PI*i & r/PI is rational & cos r is rational
implies
r in { PI/2+2*PI*i , 2*PI/3+2*PI*i , PI+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume PI/2+a <= r <= PI+a; then
A1: PI/2+a-a <= R <= PI+a-a by XREAL_1:9;
assume
A2: r/PI is rational & cos r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89; then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then cos r = cos R by COMPLEX2:9;
then R in {PI/2,2*PI/3,PI} by A1,A2,A3,Th55;
then R = PI/2 or R = 2*PI/3 or R = PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th57:
PI <= r <= 3*PI/2 & r/PI is rational & cos r is rational implies
r in {PI,4*PI/3,3*PI/2}
proof
set R = r-PI;
assume PI <= r <= 3*PI/2;
then
A1: PI-PI <= R <= 3*PI/2-PI by XREAL_1:13;
assume
A2: r/PI is rational & cos r is rational;
A3: R/PI = r/PI-PI/PI
.= r/PI-1 by XCMPLX_1:60;
cos R = cos(-(PI-r))
.= cos(PI-r) by SIN_COS:31
.= -cos r by EUCLID10:2;
then R in {0,PI/3,PI/2} by A1,A2,A3,Th53;
then R = 0 or R = PI/3 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
PI + 2*PI*i <= r <= 3*PI/2 + 2*PI*i & r/PI is rational & cos r is rational
implies
r in { PI+2*PI*i , 4*PI/3+2*PI*i , 3*PI/2+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume PI+a <= r <= 3*PI/2+a;
then
A1: PI+a-a <= R <= 3*PI/2+a-a by XREAL_1:9;
assume
A2: r/PI is rational & cos r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then cos r = cos R by COMPLEX2:9;
then R in {PI,4*PI/3,3*PI/2} by A1,A2,A3,Th57;
then R = PI or R = 4*PI/3 or R = 3*PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th59:
3*PI/2 <= r <= 2*PI & r/PI is rational & cos r is rational implies
r in {3*PI/2,5*PI/3,2*PI}
proof
set R = 2*PI-r;
assume 3*PI/2 <= r <= 2*PI;
then
A1: 2*PI-2*PI <= R <= 2*PI-3*PI/2 by XREAL_1:13;
assume
A2: r/PI is rational & cos r is rational;
A3: R/PI = 2*PI/PI-r/PI
.= 2-r/PI by XCMPLX_1:89;
cos R = cos r by EUCLID10:4;
then R in {0,PI/3,PI/2} by A1,A2,A3,Th53;
then R = 0 or R = PI/3 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
3*PI/2 + 2*PI*i <= r <= 2*PI + 2*PI*i & r/PI is rational & cos r is rational
implies
r in { 3*PI/2+2*PI*i , 5*PI/3+2*PI*i , 2*PI+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume 3*PI/2+a <= r <= 2*PI+a;
then
A1: 3*PI/2+a-a <= R <= 2*PI+a-a by XREAL_1:9;
assume
A2: r/PI is rational & cos r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then cos r = cos R by COMPLEX2:9;
then R in {3*PI/2,5*PI/3,2*PI} by A1,A2,A3,Th59;
then R = 3*PI/2 or R = 5*PI/3 or R = 2*PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
Lm4:
0 <= r <= 2*PI & r/PI is rational & cos r is rational implies
cos r in {0,1,-1,1/2,-1/2}
proof
assume
A1: 0 <= r <= 2*PI;
assume
A2: r/PI is rational & cos r is rational;
per cases by A1;
suppose 0 <= r <= PI/2;
then r in {0,PI/3,PI/2} by A2,Th53;
then r = 0 or r = PI/3 or r = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,SIN_COS:31,77,EUCLID10:14;
end;
suppose PI/2 <= r <= PI;
then r in {PI/2,2*PI/3,PI} by A2,Th55;
then r = PI/2 or r = 2*PI/3 or r = PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,SIN_COS:77,EUCLID10:23;
end;
suppose PI <= r <= 3*PI/2;
then r in {PI,4*PI/3,3*PI/2} by A2,Th57;
then r = PI or r = 4*PI/3 or r = 3*PI/2 by ENUMSET1:def 1;
hence thesis by Th11,ENUMSET1:def 3,SIN_COS:77;
end;
suppose 3*PI/2 <= r <= 2*PI;
then r in {3*PI/2,5*PI/3,2*PI} by A2,Th59;
then r = 3*PI/2 or r = 5*PI/3 or r = 2*PI by ENUMSET1:def 1;
hence thesis by Th13,ENUMSET1:def 3,SIN_COS:77;
end;
end;
theorem
r/PI is rational & cos r is rational implies cos r in {0,1,-1,1/2,-1/2}
proof
consider i such that
A0: 2*PI*i <= r <= 2*PI*(i+1) by Th16;
set a = 2*PI*i;
set R = r-a;
A2: a-a <= R <= 2*PI+a-a by A0,XREAL_1:9;
assume
A3: r/PI is rational & cos r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A4: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then cos r = cos R by COMPLEX2:9;
hence thesis by A2,A3,A4,Lm4;
end;
theorem Th62:
0 <= r <= PI/2 & r/PI is rational & sin r is rational implies
r in {0,PI/6,PI/2}
proof
set t = PI/2-r;
assume 0 <= r;
then
A1: t <= PI/2-0 by XREAL_1:10;
assume r <= PI/2;
then
A2: PI/2-PI/2 <= t by XREAL_1:10;
assume
A3: r/PI is rational & sin r is rational;
A4: t/PI = PI/2/PI-r/PI;
A5: PI/2/PI = 1/2 by XCMPLX_1:203;
cos t = cos(PI/2)*cos(r)+sin(PI/2)*sin(r) by SIN_COS:83
.= sin r by SIN_COS:77;
then t in {0,PI/3,PI/2} by A1,A2,A3,A4,A5,Th53;
then t = 0 or t = PI/3 or t = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
2*PI*i <= r <= PI/2 + 2*PI*i & r/PI is rational & sin r is rational implies
r in { 2*PI*i , PI/6+2*PI*i , PI/2+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume a <= r <= PI/2+a;
then
A1: a-a <= R <= PI/2+a-a by XREAL_1:9;
assume
A2: r/PI is rational & sin r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then sin r = sin R by COMPLEX2:8;
then R in {0,PI/6,PI/2} by A1,A2,A3,Th62;
then R = 0 or R = PI/6 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th64:
PI/2 <= r <= PI & r/PI is rational & sin r is rational implies
r in {PI/2,5*PI/6,PI}
proof
set R = PI-r;
assume PI/2 <= r <= PI;
then
A1: PI-PI <= R <= PI-PI/2 by XREAL_1:13;
assume
A2: r/PI is rational & sin r is rational;
A3: R/PI = PI/PI-r/PI
.= 1-r/PI by XCMPLX_1:60;
sin R = sin r by EUCLID10:1;
then R in {0,PI/6,PI/2} by A1,A2,A3,Th62;
then R = 0 or R = PI/6 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
PI/2 + 2*PI*i <= r <= PI + 2*PI*i & r/PI is rational & sin r is rational
implies
r in { PI/2+2*PI*i , 5*PI/6+2*PI*i , PI+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume PI/2+a <= r <= PI+a;
then
A1: PI/2+a-a <= R <= PI+a-a by XREAL_1:9;
assume
A2: r/PI is rational & sin r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then sin r = sin R by COMPLEX2:8;
then R in {PI/2,5*PI/6,PI} by A1,A2,A3,Th64;
then R = PI/2 or R = 5*PI/6 or R = PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th66:
PI <= r <= 3*PI/2 & r/PI is rational & sin r is rational implies
r in {PI,7*PI/6,3*PI/2}
proof
set R = r-PI;
assume PI <= r <= 3*PI/2;
then
A1: PI-PI <= R <= 3*PI/2-PI by XREAL_1:13;
assume
A2: r/PI is rational & sin r is rational;
A3: R/PI = r/PI-PI/PI
.= r/PI-1 by XCMPLX_1:60;
sin R = sin(-(PI-r))
.= -sin(PI-r) by SIN_COS:31
.= -sin r by EUCLID10:1;
then R in {0,PI/6,PI/2} by A1,A2,A3,Th62;
then R = 0 or R = PI/6 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
PI + 2*PI*i <= r <= 3*PI/2 + 2*PI*i & r/PI is rational & sin r is rational
implies
r in { PI+2*PI*i , 7*PI/6+2*PI*i , 3*PI/2+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume PI+a <= r <= 3*PI/2+a;
then
A1: PI+a-a <= R <= 3*PI/2+a-a by XREAL_1:9;
assume
A2: r/PI is rational & sin r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then sin r = sin R by COMPLEX2:8;
then R in {PI,7*PI/6,3*PI/2} by A1,A2,A3,Th66;
then R = PI or R = 7*PI/6 or R = 3*PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem Th68:
3*PI/2 <= r <= 2*PI & r/PI is rational & sin r is rational implies
r in {3*PI/2,11*PI/6,2*PI}
proof
set R = 2*PI-r;
assume 3*PI/2 <= r <= 2*PI;
then
A1: 2*PI-2*PI <= R <= 2*PI-3*PI/2 by XREAL_1:13;
assume
A2: r/PI is rational & sin r is rational;
A3: R/PI = 2*PI/PI-r/PI
.= 2-r/PI by XCMPLX_1:89;
sin R = -sin r by EUCLID10:3;
then R in {0,PI/6,PI/2} by A1,A2,A3,Th62;
then R = 0 or R = PI/6 or R = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
theorem
3*PI/2 + 2*PI*i <= r <= 2*PI + 2*PI*i & r/PI is rational & sin r is rational
implies
r in { 3*PI/2+2*PI*i , 11*PI/6+2*PI*i , 2*PI+2*PI*i }
proof
set a = 2*PI*i;
set R = r-a;
assume 3*PI/2+a <= r <= 2*PI+a;
then
A1: 3*PI/2+a-a <= R <= 2*PI+a-a by XREAL_1:9;
assume
A2: r/PI is rational & sin r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89;
then
A3: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then sin r = sin R by COMPLEX2:8;
then R in {3*PI/2,11*PI/6,2*PI} by A1,A2,A3,Th68;
then R = 3*PI/2 or R = 11*PI/6 or R = 2*PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 1;
end;
Lm5:
0 <= r <= 2*PI & r/PI is rational & sin r is rational implies
sin r in {0,1,-1,1/2,-1/2}
proof
assume
A1: 0 <= r <= 2*PI;
assume
A2: r/PI is rational & sin r is rational;
per cases by A1;
suppose 0 <= r <= PI/2;
then r in {0,PI/6,PI/2} by A2,Th62;
then r = 0 or r = PI/6 or r = PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,SIN_COS:31,77,EUCLID10:17;
end;
suppose PI/2 <= r <= PI;
then r in {PI/2,5*PI/6,PI} by A2,Th64;
then r = PI/2 or r = 5*PI/6 or r = PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,Th5,SIN_COS:77;
end;
suppose PI <= r <= 3*PI/2;
then r in {PI,7*PI/6,3*PI/2} by A2,Th66;
then r = PI or r = 7*PI/6 or r = 3*PI/2 by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,Th7,SIN_COS:77;
end;
suppose 3*PI/2 <= r <= 2*PI;
then r in {3*PI/2,11*PI/6,2*PI} by A2,Th68;
then r = 3*PI/2 or r = 11*PI/6 or r = 2*PI by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 3,Th9,SIN_COS:77;
end;
end;
::$N Niven's Theorem
theorem
r/PI is rational & sin r is rational implies sin r in {0, 1, -1, 1/2, -1/2}
proof
consider i such that
A0: 2*PI*i <= r <= 2*PI*(i+1) by Th16;
set a = 2*PI*i;
set R = r-a;
A2: a-a <= R <= 2*PI+a-a by A0,XREAL_1:9;
assume
A3: r/PI is rational & sin r is rational;
a/PI = (2*i*PI)/PI
.= 2*i by XCMPLX_1:89; then
A4: R/PI = r/PI-2*i;
R = 2*PI*(-i)+r;
then sin r = sin R by COMPLEX2:8;
hence thesis by A2,A3,A4,Lm5;
end;