:: Niven's Theorem
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received December 15, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users


Lm1: 2 -' 1 = 2 - 1
by XREAL_0:def 2;

Lm2: 3 -' 1 = 3 - 1
by XREAL_0:def 2;

theorem Th1: :: NIVEN:1
for a, b, c, d being Complex st b <> 0 & a / b = c / d holds
a = (b * c) / d
proof end;

theorem Th2: :: NIVEN:2
for a, b being Real holds
( not |.a.| = b or a = b or a = - b )
proof end;

theorem Th3: :: NIVEN:3
for i being Integer holds
( not |.i.| <= 2 or i = - 2 or i = - 1 or i = 0 or i = 1 or i = 2 )
proof end;

theorem Th4: :: NIVEN:4
for i being Integer
for n being Nat st n <> 0 holds
i divides i |^ n
proof end;

theorem Th16: :: NIVEN:5
for r, t being Real st t > 0 holds
ex i being Integer st
( t * i <= r & r <= t * (i + 1) )
proof end;

theorem Th49: :: NIVEN:6
for p being FinSequence of F_Real
for q being real-valued FinSequence st p = q holds
Sum p = Sum q
proof end;

theorem Th48: :: NIVEN:7
for i being Nat
for r being Element of F_Real holds (power F_Real) . (r,i) = r |^ i
proof end;

theorem Th5: :: NIVEN:8
sin ((5 * PI) / 6) = 1 / 2
proof end;

theorem :: NIVEN:9
for i being Integer holds sin (((5 * PI) / 6) + ((2 * PI) * i)) = 1 / 2 by COMPLEX2:8, Th5;

theorem Th7: :: NIVEN:10
sin ((7 * PI) / 6) = - (1 / 2)
proof end;

theorem :: NIVEN:11
for i being Integer holds sin (((7 * PI) / 6) + ((2 * PI) * i)) = - (1 / 2) by COMPLEX2:8, Th7;

theorem Th9: :: NIVEN:12
sin ((11 * PI) / 6) = - (1 / 2)
proof end;

theorem :: NIVEN:13
for i being Integer holds sin (((11 * PI) / 6) + ((2 * PI) * i)) = - (1 / 2) by COMPLEX2:8, Th9;

theorem Th11: :: NIVEN:14
cos ((4 * PI) / 3) = - (1 / 2)
proof end;

theorem :: NIVEN:15
for i being Integer holds cos (((4 * PI) / 3) + ((2 * PI) * i)) = - (1 / 2) by COMPLEX2:9, Th11;

theorem Th13: :: NIVEN:16
cos ((5 * PI) / 3) = 1 / 2
proof end;

theorem :: NIVEN:17
for i being Integer holds cos (((5 * PI) / 3) + ((2 * PI) * i)) = 1 / 2 by COMPLEX2:9, Th13;

theorem Th15: :: NIVEN:18
for r being Real st 0 <= r & r <= PI / 2 & cos r = 1 / 2 holds
r = PI / 3
proof end;

theorem Th17: :: NIVEN:19
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being sequence of L holds (0_. L) *' p = 0_. L
proof end;

registration
let L be non empty ZeroStr ;
let z be Element of L;
let n be Nat;
cluster (0_. L) +* (n,z) -> finite-Support for sequence of L;
coherence
for b1 being sequence of L st b1 = (0_. L) +* (n,z) holds
b1 is finite-Support
proof end;
end;

theorem Th18: :: NIVEN:20
for n being Nat
for L being non empty ZeroStr
for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
len p = n + 1
proof end;

theorem :: NIVEN:21
for n being Nat
for L being non empty ZeroStr
for z being Element of L st z <> 0. L holds
for p being Polynomial of L st p = (0_. L) +* (n,z) holds
deg p = n
proof end;

registration
cluster 0_. F_Real -> INT -valued ;
coherence
0_. F_Real is INT -valued ;
cluster 1_. F_Real -> INT -valued ;
coherence
1_. F_Real is INT -valued ;
end;

registration
cluster complex V32() ext-real integer for Element of the carrier of F_Real;
existence
ex b1 being Element of F_Real st b1 is integer ;
end;

theorem Th20: :: NIVEN:22
for L being non empty ZeroStr
for z being Element of L holds rng <%z%> = {z,(0. L)}
proof end;

definition
let L be non empty ZeroStr ;
let z0, z1, z2 be Element of L;
func <%z0,z1,z2%> -> sequence of L equals :: NIVEN:def 1
(((0_. L) +* (0,z0)) +* (1,z1)) +* (2,z2);
coherence
(((0_. L) +* (0,z0)) +* (1,z1)) +* (2,z2) is sequence of L ;
end;

:: deftheorem defines <% NIVEN:def 1 :
for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds <%z0,z1,z2%> = (((0_. L) +* (0,z0)) +* (1,z1)) +* (2,z2);

theorem Th21: :: NIVEN:23
for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 0 = z0
proof end;

theorem Th22: :: NIVEN:24
for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 1 = z1
proof end;

theorem Th23: :: NIVEN:25
for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 2 = z2
proof end;

theorem Th24: :: NIVEN:26
for n being Nat
for L being non empty ZeroStr
for z0, z1, z2 being Element of L st 3 <= n holds
<%z0,z1,z2%> . n = 0. L
proof end;

registration
let L be non empty ZeroStr ;
let z0, z1, z2 be Element of L;
cluster <%z0,z1,z2%> -> finite-Support ;
coherence
<%z0,z1,z2%> is finite-Support
proof end;
end;

theorem Th25: :: NIVEN:27
for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds len <%z0,z1,z2%> <= 3
proof end;

theorem Th26: :: NIVEN:28
for L being non empty ZeroStr
for z0, z1, z2 being Element of L st z2 <> 0. L holds
len <%z0,z1,z2%> = 3
proof end;

theorem Th27: :: NIVEN:29
for L being non empty right_zeroed addLoopStr
for z0, z1 being Element of L holds <%z0%> + <%z1%> = <%(z0 + z1)%>
proof end;

theorem Th28: :: NIVEN:30
for L being non empty right_zeroed addLoopStr
for z0, z1, z2, z3 being Element of L holds <%z0,z1%> + <%z2,z3%> = <%(z0 + z2),(z1 + z3)%>
proof end;

theorem Th29: :: NIVEN:31
for L being non empty right_zeroed 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 end;

theorem Th30: :: NIVEN:32
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0 being Element of L holds - <%z0%> = <%(- z0)%>
proof end;

theorem Th31: :: NIVEN:33
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1 being Element of L holds - <%z0,z1%> = <%(- z0),(- z1)%>
proof end;

theorem Th32: :: NIVEN:34
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1, z2 being Element of L holds - <%z0,z1,z2%> = <%(- z0),(- z1),(- z2)%>
proof end;

theorem :: NIVEN:35
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1 being Element of L holds <%z0%> - <%z1%> = <%(z0 - z1)%>
proof end;

theorem :: NIVEN:36
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1, z2, z3 being Element of L holds <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>
proof end;

theorem :: NIVEN:37
for L being non empty right_complementable add-associative right_zeroed 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 end;

theorem Th36: :: NIVEN:38
for L being non empty right_complementable add-associative right_zeroed left-distributive unital associative doubleLoopStr
for z0, z1, z2, x being Element of L holds eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)
proof end;

registration
let a be integer Element of F_Real;
cluster <%a%> -> INT -valued ;
coherence
<%a%> is INT -valued
proof end;
end;

registration
let a, b be integer Element of F_Real;
cluster <%a,b%> -> INT -valued ;
coherence
<%a,b%> is INT -valued
proof end;
end;

registration
let a, b, c be integer Element of F_Real;
cluster <%a,b,c%> -> INT -valued ;
coherence
<%a,b,c%> is INT -valued
proof end;
end;

registration
cluster Relation-like NAT -defined INT -valued the carrier of F_Real -valued Function-like non empty total V18( NAT , the carrier of F_Real) complex-valued ext-real-valued real-valued finite-Support monic for Element of K19(K20(NAT, the carrier of F_Real));
existence
ex b1 being Polynomial of F_Real st
( b1 is monic & b1 is INT -valued )
proof end;
end;

registration
cluster Relation-like NAT -defined INT -valued the carrier of F_Real -valued Function-like V41() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V177() for FinSequence of the carrier of F_Real;
existence
ex b1 being FinSequence of F_Real st b1 is INT -valued
proof end;
end;

registration
let F be INT -valued FinSequence of F_Real;
cluster Sum F -> integer ;
coherence
Sum F is integer
proof end;
end;

registration
let f be INT -valued sequence of F_Real;
cluster - f -> INT -valued ;
coherence
- f is INT -valued
proof end;
let g be INT -valued sequence of F_Real;
cluster f + g -> INT -valued ;
coherence
f + g is INT -valued
proof end;
cluster f - g -> INT -valued ;
coherence
f - g is INT -valued ;
cluster f *' g -> INT -valued ;
coherence
f *' g is INT -valued
proof end;
end;

theorem Th37: :: NIVEN:39
for L being non empty non degenerated doubleLoopStr
for z being Element of L holds LC <%z,(1. L)%> = 1. L
proof end;

registration
let L be non empty non degenerated doubleLoopStr ;
let z be Element of L;
cluster <%z,(1. L)%> -> monic ;
coherence
<%z,(1. L)%> is monic by Th37;
end;

theorem Th38: :: NIVEN:40
for L being non empty non degenerated doubleLoopStr
for z1, z2 being Element of L holds LC <%z1,z2,(1. L)%> = 1. L
proof end;

registration
let L be non empty non degenerated doubleLoopStr ;
let z1, z2 be Element of L;
cluster <%z1,z2,(1. L)%> -> monic ;
coherence
<%z1,z2,(1. L)%> is monic by Th38;
end;

registration
let p be INT -valued Polynomial of F_Real;
cluster Leading-Coefficient p -> integer ;
coherence
LC p is integer ;
end;

theorem :: NIVEN:41
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds deg (- p) = deg p by POLYNOM4:8;

theorem Th40: :: NIVEN:42
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st deg p > deg q holds
deg (p + q) = deg p
proof end;

theorem Th41: :: NIVEN:43
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st deg p > deg q holds
deg (p - q) = deg p
proof end;

theorem :: NIVEN:44
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st deg p < deg q holds
deg (p - q) = deg q
proof end;

theorem :: NIVEN:45
for L being non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Polynomial of L holds LC p = - (LC (- p))
proof end;

lemmul: for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p, q being 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 end;

theorem Th44: :: NIVEN:46
for L being non degenerated right_complementable add-associative right_zeroed well-unital distributive associative domRing-like doubleLoopStr
for p, q being Polynomial of L holds LC (p *' q) = (LC p) * (LC q)
proof end;

Lm3: now :: thesis: for L being non degenerated doubleLoopStr
for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
q . ((len p) -' 1) = 0. L
let L be non degenerated doubleLoopStr ; :: thesis: for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
q . ((len p) -' 1) = 0. L
let p be monic Polynomial of L; :: thesis: for q being Polynomial of L st deg p > deg q holds
q . ((len p) -' 1) = 0. L
let q be Polynomial of L; :: thesis: ( deg p > deg q implies q . ((len p) -' 1) = 0. L )
assume A1: deg p > deg q ; :: thesis: q . ((len p) -' 1) = 0. L
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; :: thesis: verum
end;

theorem :: NIVEN:47
for L being non degenerated right_complementable add-associative right_zeroed distributive 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 end;

theorem Th46: :: NIVEN:48
for L being non degenerated right_complementable add-associative right_zeroed distributive 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 end;

registration
let L be non degenerated right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let p, q be monic Polynomial of L;
cluster p *' q -> monic ;
coherence
p *' q is monic
proof end;
end;

theorem Th47: :: NIVEN:49
for L being non empty right_complementable Abelian add-associative right_zeroed distributive unital 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 end;

:: WP: Rational root theorem
theorem Th50: :: 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 holds
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 end;

:: WP: Integral root theorem
theorem Th51: :: NIVEN:51
for p being INT -valued monic Polynomial of F_Real
for e being rational Element of F_Real st e is_a_root_of p holds
e is integer
proof end;

theorem Th52: :: NIVEN:52
for t being Real
for n being Nat
for e being Element of F_Real st 1 <= n & e = 2 * (cos t) holds
ex p being INT -valued monic 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 end;

theorem Th53: :: NIVEN:53
for r being Real st 0 <= r & r <= PI / 2 & r / PI is rational & cos r is rational holds
r in {0,(PI / 3),(PI / 2)}
proof end;

theorem :: NIVEN:54
for r being Real
for i being Integer st (2 * PI) * i <= r & r <= (PI / 2) + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {((2 * PI) * i),((PI / 3) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i))}
proof end;

theorem Th55: :: NIVEN:55
for r being Real st PI / 2 <= r & r <= PI & r / PI is rational & cos r is rational holds
r in {(PI / 2),((2 * PI) / 3),PI}
proof end;

theorem :: NIVEN:56
for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) <= r & r <= PI + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {((PI / 2) + ((2 * PI) * i)),(((2 * PI) / 3) + ((2 * PI) * i)),(PI + ((2 * PI) * i))}
proof end;

theorem Th57: :: NIVEN:57
for r being Real st PI <= r & r <= (3 * PI) / 2 & r / PI is rational & cos r is rational holds
r in {PI,((4 * PI) / 3),((3 * PI) / 2)}
proof end;

theorem :: NIVEN:58
for r being Real
for i being Integer st PI + ((2 * PI) * i) <= r & r <= ((3 * PI) / 2) + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))}
proof end;

theorem Th59: :: NIVEN:59
for r being Real st (3 * PI) / 2 <= r & r <= 2 * PI & r / PI is rational & cos r is rational holds
r in {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)}
proof end;

theorem :: NIVEN:60
for r being Real
for i being Integer st ((3 * PI) / 2) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))}
proof end;

Lm4: for r being Real st 0 <= r & r <= 2 * PI & r / PI is rational & cos r is rational holds
cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
proof end;

theorem :: NIVEN:61
for r being Real st r / PI is rational & cos r is rational holds
cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
proof end;

theorem Th62: :: NIVEN:62
for r being Real st 0 <= r & r <= PI / 2 & r / PI is rational & sin r is rational holds
r in {0,(PI / 6),(PI / 2)}
proof end;

theorem :: NIVEN:63
for r being Real
for i being Integer st (2 * PI) * i <= r & r <= (PI / 2) + ((2 * PI) * i) & r / PI is rational & sin r is rational holds
r in {((2 * PI) * i),((PI / 6) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i))}
proof end;

theorem Th64: :: NIVEN:64
for r being Real st PI / 2 <= r & r <= PI & r / PI is rational & sin r is rational holds
r in {(PI / 2),((5 * PI) / 6),PI}
proof end;

theorem :: NIVEN:65
for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) <= r & r <= PI + ((2 * PI) * i) & r / PI is rational & sin r is rational holds
r in {((PI / 2) + ((2 * PI) * i)),(((5 * PI) / 6) + ((2 * PI) * i)),(PI + ((2 * PI) * i))}
proof end;

theorem Th66: :: NIVEN:66
for r being Real st PI <= r & r <= (3 * PI) / 2 & r / PI is rational & sin r is rational holds
r in {PI,((7 * PI) / 6),((3 * PI) / 2)}
proof end;

theorem :: NIVEN:67
for r being Real
for i being Integer st PI + ((2 * PI) * i) <= r & r <= ((3 * PI) / 2) + ((2 * PI) * i) & r / PI is rational & sin r is rational holds
r in {(PI + ((2 * PI) * i)),(((7 * PI) / 6) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))}
proof end;

theorem Th68: :: NIVEN:68
for r being Real st (3 * PI) / 2 <= r & r <= 2 * PI & r / PI is rational & sin r is rational holds
r in {((3 * PI) / 2),((11 * PI) / 6),(2 * PI)}
proof end;

theorem :: NIVEN:69
for r being Real
for i being Integer st ((3 * PI) / 2) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) & r / PI is rational & sin r is rational holds
r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((11 * PI) / 6) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))}
proof end;

Lm5: for r being Real st 0 <= r & r <= 2 * PI & r / PI is rational & sin r is rational holds
sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
proof end;

:: WP: Niven's Theorem
theorem :: NIVEN:70
for r being Real st r / PI is rational & sin r is rational holds
sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
proof end;