:: 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 b₁ being sequence of L st b₁ = (0_. L) +* (n,z) holds
b₁ 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 b₁ being Element of F_Real st b₁ 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 b₁ being Polynomial of F_Real st
( b₁ is monic & b₁ 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 b₁ being FinSequence of F_Real st b₁ 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;

:: 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;

:: 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;

:: 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;