:: Niven's Theorem
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received December 15, 2016
:: Copyright (c) 2016-2017 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,
RATFUNC1, FINSEQ_1, NEWTON, FINSEQ_2, WSIERP_1, VECTSP_2, ALGSTR_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
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;
theorem :: NIVEN:1
for a,b,c,d being Complex st b <> 0 & a/b = c/d holds a = b*c/d;
theorem :: NIVEN:2
for a,b being Real st |.a.| = b holds a = b or a = -b;
theorem :: NIVEN:3
|.i.| <= 2 implies i = -2 or i = -1 or i = 0 or i = 1 or i = 2;
theorem :: NIVEN:4
n <> 0 implies i divides i |^ n;
theorem :: NIVEN:5
t > 0 implies ex i st t*i <= r <= t*(i+1);
theorem :: NIVEN:6 ::: MATRPROB:36
for p being FinSequence of F_Real
for q being real-valued FinSequence st p = q holds Sum p = Sum q;
theorem :: NIVEN:7
for i being Nat, r being Element of F_Real
holds power(F_Real).(r,i) = r |^ i;
theorem :: NIVEN:8
sin(5*PI/6) = 1/2;
theorem :: NIVEN:9
sin(5*PI/6+2*PI*i) = 1/2;
theorem :: NIVEN:10
sin(7*PI/6) = -1/2;
theorem :: NIVEN:11
sin(7*PI/6+2*PI*i) = -1/2;
theorem :: NIVEN:12
sin(11*PI/6) = -1/2;
theorem :: NIVEN:13
sin(11*PI/6+2*PI*i) = -1/2;
theorem :: NIVEN:14
cos(4*PI/3) = -1/2;
theorem :: NIVEN:15
cos(4*PI/3+2*PI*i) = -1/2;
theorem :: NIVEN:16
cos(5*PI/3) = 1/2;
theorem :: NIVEN:17
cos(5*PI/3+2*PI*i) = 1/2;
theorem :: NIVEN:18
0 <= r <= PI/2 & cos r = 1/2 implies r = PI/3;
theorem :: NIVEN:19 :: 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;
registration
let L,z,n;
cluster 0_.L +* (n,z) -> finite-Support for sequence of L;
end;
theorem :: NIVEN:20
z <> 0.L implies
for p being Polynomial of L st p = 0_.L +* (n,z) holds len p = n+1;
theorem :: NIVEN:21
z <> 0.L implies
for p being Polynomial of L st p = 0_.L +* (n,z) holds deg p = n;
registration
cluster 0_.F_Real -> INT -valued;
cluster 1_.F_Real -> INT -valued;
end;
registration
cluster integer for Element of F_Real;
end;
theorem :: NIVEN:22
rng <%z%> = {z,0.L};
definition
let L,z0,z1,z2;
func <%z0,z1,z2%> -> sequence of L equals
:: NIVEN:def 1
0_.L +* (0,z0) +* (1,z1) +* (2,z2);
end;
theorem :: NIVEN:23
<%z0,z1,z2%>.0 = z0;
theorem :: NIVEN:24
<%z0,z1,z2%>.1 = z1;
theorem :: NIVEN:25
<%z0,z1,z2%>.2 = z2;
theorem :: NIVEN:26
3 <= n implies <%z0,z1,z2%>.n = 0.L;
registration
let L,z0,z1,z2;
cluster <%z0,z1,z2%> -> finite-Support;
end;
theorem :: NIVEN:27
len <%z0,z1,z2%> <= 3;
theorem :: NIVEN:28
z2 <> 0.L implies len <%z0,z1,z2%> = 3;
theorem :: NIVEN:29
for L being right_zeroed non empty addLoopStr
for z0,z1 being Element of L holds
<%z0%> + <%z1%> = <%z0+z1%>;
theorem :: NIVEN:30
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%>;
theorem :: NIVEN:31
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%>;
theorem :: NIVEN:32
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0 being Element of L holds
- <%z0%> = <%-z0%>;
theorem :: NIVEN:33
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1 being Element of L holds
- <%z0,z1%> = <%-z0,-z1%>;
theorem :: NIVEN:34
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%>;
theorem :: NIVEN:35
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for z0,z1 being Element of L holds
<%z0%> - <%z1%> = <%z0-z1%>;
theorem :: NIVEN:36
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%>;
theorem :: NIVEN:37
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%>;
theorem :: NIVEN:38
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;
registration
let a be integer Element of F_Real;
cluster <%a%> -> INT -valued;
end;
registration
let a,b be integer Element of F_Real;
cluster <%a,b%> -> INT -valued;
end;
registration
let a,b,c be integer Element of F_Real;
cluster <%a,b,c%> -> INT -valued;
end;
registration
cluster monic INT -valued for Polynomial of F_Real;
end;
registration
cluster INT -valued for FinSequence of F_Real;
end;
registration
let F be INT -valued FinSequence of F_Real;
cluster Sum F -> integer;
end;
registration
let f be INT -valued sequence of F_Real;
cluster -f -> INT -valued;
let g be INT -valued sequence of F_Real;
cluster f+g -> INT -valued;
cluster f-g -> INT -valued;
cluster f*'g -> INT -valued;
end;
theorem :: NIVEN:39
for L being non degenerated non empty doubleLoopStr, z being Element of L
holds LC <%z,1.L%> = 1.L;
registration
let L be non degenerated non empty doubleLoopStr;
let z be Element of L;
cluster <%z,1.L%> -> monic;
end;
theorem :: NIVEN:40
for L being non degenerated non empty doubleLoopStr, z1,z2 being Element of L
holds LC <%z1,z2,1.L%> = 1.L;
registration
let L be non degenerated non empty doubleLoopStr;
let z1,z2 be Element of L;
cluster <%z1,z2,1.L%> -> monic;
end;
registration
let p be INT -valued Polynomial of F_Real;
cluster LC p -> integer;
end;
theorem :: NIVEN:41
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p being Polynomial of L holds
deg(-p) = deg p;
theorem :: NIVEN:42
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;
theorem :: NIVEN:43
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;
theorem :: NIVEN:44
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;
theorem :: NIVEN:45
for L being add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr
for p being Polynomial of L holds
LC p = -LC -p;
theorem :: NIVEN:46
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);
theorem :: NIVEN:47
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;
theorem :: NIVEN:48
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;
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;
end;
theorem :: NIVEN:49
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;
::$N Rational root theorem
theorem :: NIVEN:50
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;
::$N Integral root theorem
theorem :: NIVEN:51
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;
theorem :: NIVEN:52
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%>);
theorem :: NIVEN:53
0 <= r <= PI/2 & r/PI is rational & cos r is rational implies
r in {0,PI/3,PI/2};
theorem :: NIVEN:54
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 };
theorem :: NIVEN:55
PI/2 <= r <= PI & r/PI is rational & cos r is rational implies
r in {PI/2,2*PI/3,PI};
theorem :: NIVEN:56
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 };
theorem :: NIVEN:57
PI <= r <= 3*PI/2 & r/PI is rational & cos r is rational implies
r in {PI,4*PI/3,3*PI/2};
theorem :: NIVEN:58
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 };
theorem :: NIVEN:59
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};
theorem :: NIVEN:60
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 };
theorem :: NIVEN:61
r/PI is rational & cos r is rational implies cos r in {0,1,-1,1/2,-1/2};
theorem :: NIVEN:62
0 <= r <= PI/2 & r/PI is rational & sin r is rational implies
r in {0,PI/6,PI/2};
theorem :: NIVEN:63
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 };
theorem :: NIVEN:64
PI/2 <= r <= PI & r/PI is rational & sin r is rational implies
r in {PI/2,5*PI/6,PI};
theorem :: NIVEN:65
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 };
theorem :: NIVEN:66
PI <= r <= 3*PI/2 & r/PI is rational & sin r is rational implies
r in {PI,7*PI/6,3*PI/2};
theorem :: NIVEN:67
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 };
theorem :: NIVEN:68
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};
theorem :: NIVEN:69
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 };
::$N Niven's Theorem
theorem :: NIVEN:70
r/PI is rational & sin r is rational implies sin r in {0, 1, -1, 1/2, -1/2};