:: 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 :: NIVEN:9

theorem :: NIVEN:11

theorem :: NIVEN:13

theorem :: NIVEN:15

theorem :: NIVEN:17

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

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;

coherence

for b_{1} being sequence of L st b_{1} = (0_. L) +* (n,z) holds

b_{1} is finite-Support

end;
let z be Element of L;

let n be Nat;

coherence

for b

b

proof 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

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

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;

definition

let L be non empty ZeroStr ;

let z0, z1, z2 be Element of L;

coherence

(((0_. L) +* (0,z0)) +* (1,z1)) +* (2,z2) is sequence of L ;

end;
let z0, z1, z2 be Element of L;

coherence

(((0_. L) +* (0,z0)) +* (1,z1)) +* (2,z2) is sequence of L ;

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

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

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;

coherence

<%z0,z1,z2%> is finite-Support

end;
let z0, z1, z2 be Element of L;

coherence

<%z0,z1,z2%> is finite-Support

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

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)%>

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)%>

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)%>

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)%>

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)%>

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)%>

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)%>

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)%>

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)%>

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)

for z0, z1, z2, x being Element of L holds eval (<%z0,z1,z2%>,x) = (z0 + (z1 * x)) + ((z2 * x) * x)

proof end;

registration
end;

registration
end;

registration

ex b_{1} being Polynomial of F_Real st

( b_{1} is monic & b_{1} is INT -valued )
end;

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

( b

proof end;

registration

ex b_{1} being FinSequence of F_Real st b_{1} is INT -valued
end;

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

proof end;

registration

let f be INT -valued sequence of F_Real;

coherence

- f is INT -valued

coherence

f + g is INT -valued

f - g is INT -valued ;

coherence

f *' g is INT -valued

end;
coherence

- f is INT -valued

proof end;

let g be INT -valued sequence of F_Real;coherence

f + g is INT -valued

proof end;

coherence f - g is INT -valued ;

coherence

f *' g is INT -valued

proof 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

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;

coherence

<%z,(1. L)%> is monic by Th37;

end;
let z be Element of L;

coherence

<%z,(1. L)%> is monic by Th37;

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

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;

coherence

<%z1,z2,(1. L)%> is monic by Th38;

end;
let z1, z2 be Element of L;

coherence

<%z1,z2,(1. L)%> is monic by Th38;

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;

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

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

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

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))

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)

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

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

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

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

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;

coherence

p *' q is monic

end;
let p, q be monic Polynomial of L;

coherence

p *' q is monic

proof 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

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 )

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;

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

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)%> ) ) )

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)}

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))}

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}

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))}

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)}

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))}

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)}

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))}

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))}

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)}

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))}

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}

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))}

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)}

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))}

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)}

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))}

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;

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))}

sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

proof end;