:: EC_PF_1 semantic presentation begin definition let K be Field; mode Subfield of K -> Field means :Def1: :: EC_PF_1:def 1 ( the carrier of it c= the carrier of K & the addF of it = the addF of K || the carrier of it & the multF of it = the multF of K || the carrier of it & 1. it = 1. K & 0. it = 0. K ); existence ex b1 being Field st ( the carrier of b1 c= the carrier of K & the addF of b1 = the addF of K || the carrier of b1 & the multF of b1 = the multF of K || the carrier of b1 & 1. b1 = 1. K & 0. b1 = 0. K ) proof take K ; ::_thesis: ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K ) thus ( the carrier of K c= the carrier of K & the addF of K = the addF of K || the carrier of K & the multF of K = the multF of K || the carrier of K & 1. K = 1. K & 0. K = 0. K ) by RELSET_1:19; ::_thesis: verum end; end; :: deftheorem Def1 defines Subfield EC_PF_1:def_1_:_ for K, b2 being Field holds ( b2 is Subfield of K iff ( the carrier of b2 c= the carrier of K & the addF of b2 = the addF of K || the carrier of b2 & the multF of b2 = the multF of K || the carrier of b2 & 1. b2 = 1. K & 0. b2 = 0. K ) ); theorem Th1: :: EC_PF_1:1 for K being Field holds K is Subfield of K proof let K be Field; ::_thesis: K is Subfield of K A1: the addF of K = the addF of K || the carrier of K by RELSET_1:19; A2: the multF of K = the multF of K || the carrier of K by RELSET_1:19; ( the carrier of K c= the carrier of K & 1. K = 1. K & 0. K = 0. K ) ; hence K is Subfield of K by A1, A2, Def1; ::_thesis: verum end; theorem Th2: :: EC_PF_1:2 for K being Field for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds ST is Subfield of K proof let K be Field; ::_thesis: for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds ST is Subfield of K let ST be non empty doubleLoopStr ; ::_thesis: ( the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated implies ST is Subfield of K ) assume that A1: the carrier of ST is Subset of the carrier of K and A2: the addF of ST = the addF of K || the carrier of ST and A3: the multF of ST = the multF of K || the carrier of ST and A4: 1. ST = 1. K and A5: 0. ST = 0. K and A6: ( ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated ) ; ::_thesis: ST is Subfield of K set C1 = the carrier of ST; set AC = the addF of ST; set MC = the multF of ST; set d0 = 0. ST; set d1 = 1. ST; A7: now__::_thesis:_for_a,_x_being_Element_of_ST_holds_a_*_x_=_the_multF_of_K_._(a,x) let a, x be Element of ST; ::_thesis: a * x = the multF of K . (a,x) a * x = the multF of K . [a,x] by A3, FUNCT_1:49; hence a * x = the multF of K . (a,x) ; ::_thesis: verum end; A8: now__::_thesis:_for_x,_y_being_Element_of_ST_holds_x_+_y_=_the_addF_of_K_._(x,y) let x, y be Element of ST; ::_thesis: x + y = the addF of K . (x,y) x + y = the addF of K . [x,y] by A2, FUNCT_1:49; hence x + y = the addF of K . (x,y) ; ::_thesis: verum end; ( ST is Abelian & ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive ) proof set MK = the multF of K; set AK = the addF of K; hereby :: according to RLVECT_1:def_2 ::_thesis: ( ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive ) let x, y be Element of ST; ::_thesis: x + y = y + x reconsider x1 = x, y1 = y as Element of K by A1, TARSKI:def_3; ( x + y = x1 + y1 & y + x = y1 + x1 ) by A8; hence x + y = y + x ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive ) let x, y, z be Element of ST; ::_thesis: (x + y) + z = x + (y + z) reconsider x1 = x, y1 = y, z1 = z as Element of K by A1, TARSKI:def_3; x + (y + z) = the addF of K . (x1,(y + z)) by A8; then A9: x + (y + z) = x1 + (y1 + z1) by A8; (x + y) + z = the addF of K . ((x + y),z1) by A8; then (x + y) + z = (x1 + y1) + z1 by A8; hence (x + y) + z = x + (y + z) by A9, RLVECT_1:def_3; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: ( ST is associative & ST is well-unital & ST is distributive ) let x be Element of ST; ::_thesis: x + (0. ST) = x reconsider y = x, z = 0. ST as Element of K by A1, TARSKI:def_3; x + (0. ST) = y + (0. K) by A5, A8; hence x + (0. ST) = x by RLVECT_1:4; ::_thesis: verum end; hereby :: according to GROUP_1:def_3 ::_thesis: ( ST is well-unital & ST is distributive ) let a, b, x be Element of ST; ::_thesis: (a * b) * x = a * (b * x) reconsider y = x, a1 = a, b1 = b as Element of K by A1, TARSKI:def_3; a * (b * x) = the multF of K . (a,(b * x)) by A7; then A10: a * (b * x) = a1 * (b1 * y) by A7; a * b = a1 * b1 by A7; then (a * b) * x = (a1 * b1) * y by A7; hence (a * b) * x = a * (b * x) by A10, GROUP_1:def_3; ::_thesis: verum end; hereby :: according to VECTSP_1:def_6 ::_thesis: ST is distributive let x be Element of ST; ::_thesis: ( x * (1. ST) = x & (1. ST) * x = x ) reconsider y = x as Element of K by A1, TARSKI:def_3; ( x * (1. ST) = y * (1. K) & (1. ST) * x = (1. K) * y ) by A4, A7; hence ( x * (1. ST) = x & (1. ST) * x = x ) by VECTSP_1:def_6; ::_thesis: verum end; hereby :: according to VECTSP_1:def_7 ::_thesis: verum let a, x, y be Element of ST; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) reconsider x1 = x, y1 = y, a1 = a as Element of K by A1, TARSKI:def_3; (x + y) * a = the multF of K . ((x + y),a) by A7; then (x + y) * a = (x1 + y1) * a1 by A8; then (x + y) * a = (x1 * a1) + (y1 * a1) by VECTSP_1:def_7; then (x + y) * a = the addF of K . (( the multF of K . (x1,a1)),(y * a)) by A7; then A11: (x + y) * a = the addF of K . ((x * a),(y * a)) by A7; a * (x + y) = the multF of K . (a,(x + y)) by A7; then a * (x + y) = a1 * (x1 + y1) by A8; then a * (x + y) = (a1 * x1) + (a1 * y1) by VECTSP_1:def_7; then a * (x + y) = the addF of K . (( the multF of K . (a,x1)),(a * y)) by A7; then a * (x + y) = the addF of K . ((a * x),(a * y)) by A7; hence ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) by A8, A11; ::_thesis: verum end; end; hence ST is Subfield of K by A1, A2, A3, A4, A5, A6, Def1; ::_thesis: verum end; registration let K be Field; cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K; existence ex b1 being Subfield of K st b1 is strict proof set C1 = [#] K; A1: ( the addF of K = the addF of K || ([#] K) & the multF of K = the multF of K || ([#] K) ) by RELSET_1:19; set ST = doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); A2: ( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K ) ; ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated ) proof thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable ::_thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated ) proof let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider x1 = x as Element of K ; consider v being Element of K such that A3: x1 + v = 0. K by ALGSTR_0:def_11; reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) thus x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A3; ::_thesis: verum end; thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative ::_thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated ) proof let x, y be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x reconsider x1 = x, y1 = y as Element of K ; ( x * y = x1 * y1 & y * x = y1 * x1 ) ; hence x * y = y * x ; ::_thesis: verum end; thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible ::_thesis: not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated proof let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to VECTSP_1:def_9 ::_thesis: ( x = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) or ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ) assume A4: x <> 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; ::_thesis: ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) reconsider x1 = x as Element of K ; x1 is left_invertible by A4, ALGSTR_0:def_39; then consider v being Element of K such that A5: v * x1 = 1. K by ALGSTR_0:def_27; reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; take y ; ::_thesis: y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) thus y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A5; ::_thesis: verum end; ( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K & 0. K <> 1. K ) ; hence not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated by STRUCT_0:def_8; ::_thesis: verum end; then doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is Subfield of K by A1, A2, Th2; hence ex b1 being Subfield of K st b1 is strict ; ::_thesis: verum end; end; theorem Th3: :: EC_PF_1:3 for K1, K2 being Field st K1 is Subfield of K2 holds for x being set st x in K1 holds x in K2 proof let K1, K2 be Field; ::_thesis: ( K1 is Subfield of K2 implies for x being set st x in K1 holds x in K2 ) assume K1 is Subfield of K2 ; ::_thesis: for x being set st x in K1 holds x in K2 then A1: the carrier of K1 c= the carrier of K2 by Def1; for x being set st x in K1 holds x in K2 proof let x be set ; ::_thesis: ( x in K1 implies x in K2 ) assume x in K1 ; ::_thesis: x in K2 then x in the carrier of K1 by STRUCT_0:def_5; hence x in K2 by A1, STRUCT_0:def_5; ::_thesis: verum end; hence for x being set st x in K1 holds x in K2 ; ::_thesis: verum end; theorem Th4: :: EC_PF_1:4 for K1, K2 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K1 holds K1 = K2 proof let K1, K2 be strict Field; ::_thesis: ( K1 is Subfield of K2 & K2 is Subfield of K1 implies K1 = K2 ) assume A1: ( K1 is Subfield of K2 & K2 is Subfield of K1 ) ; ::_thesis: K1 = K2 A2: ( the carrier of K1 c= the carrier of K2 & the carrier of K2 c= the carrier of K1 ) by A1, Def1; then A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def_10; A4: the addF of K2 = the addF of K2 || the carrier of K1 by A3, RELSET_1:19 .= the addF of K1 by A1, Def1 ; A5: the multF of K2 = the multF of K2 || the carrier of K1 by A3, RELSET_1:19 .= the multF of K1 by A1, Def1 ; ( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1; hence K1 = K2 by A4, A5, A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: EC_PF_1:5 for K1, K2, K3 being strict Field st K1 is Subfield of K2 & K2 is Subfield of K3 holds K1 is Subfield of K3 proof let K1, K2, K3 be strict Field; ::_thesis: ( K1 is Subfield of K2 & K2 is Subfield of K3 implies K1 is Subfield of K3 ) assume A1: ( K1 is Subfield of K2 & K2 is Subfield of K3 ) ; ::_thesis: K1 is Subfield of K3 set C1 = the carrier of K1; set C2 = the carrier of K2; set C = the carrier of K3; set ADD = the addF of K3; set MULT = the multF of K3; A2: the carrier of K1 c= the carrier of K2 by A1, Def1; then A3: [: the carrier of K1, the carrier of K1:] c= [: the carrier of K2, the carrier of K2:] by ZFMISC_1:96; the carrier of K2 c= the carrier of K3 by A1, Def1; then A4: the carrier of K1 c= the carrier of K3 by A2, XBOOLE_1:1; A5: the addF of K2 = the addF of K3 || the carrier of K2 by A1, Def1; A6: the addF of K1 = the addF of K2 || the carrier of K1 by A1, Def1 .= the addF of K3 || the carrier of K1 by A3, A5, FUNCT_1:51 ; A7: the multF of K2 = the multF of K3 || the carrier of K2 by A1, Def1; A8: the multF of K1 = the multF of K2 || the carrier of K1 by A1, Def1 .= the multF of K3 || the carrier of K1 by A3, A7, FUNCT_1:51 ; ( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1; then ( 1. K1 = 1. K3 & 0. K1 = 0. K3 ) by A1, Def1; hence K1 is Subfield of K3 by A4, A6, A8, Def1; ::_thesis: verum end; theorem Th6: :: EC_PF_1:6 for K being Field for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 ) proof let K be Field; ::_thesis: for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 ) let SK1, SK2 be Subfield of K; ::_thesis: ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 ) set C1 = the carrier of SK1; set C2 = the carrier of SK2; set ADD = the addF of K; set MULT = the multF of K; thus ( SK1 is Subfield of SK2 implies the carrier of SK1 c= the carrier of SK2 ) by Def1; ::_thesis: ( the carrier of SK1 c= the carrier of SK2 implies SK1 is Subfield of SK2 ) assume A1: the carrier of SK1 c= the carrier of SK2 ; ::_thesis: SK1 is Subfield of SK2 then A2: [: the carrier of SK1, the carrier of SK1:] c= [: the carrier of SK2, the carrier of SK2:] by ZFMISC_1:96; the addF of SK2 = the addF of K || the carrier of SK2 by Def1; then A3: the addF of SK2 || the carrier of SK1 = the addF of K || the carrier of SK1 by A2, FUNCT_1:51 .= the addF of SK1 by Def1 ; the multF of SK2 = the multF of K || the carrier of SK2 by Def1; then A4: the multF of SK2 || the carrier of SK1 = the multF of K || the carrier of SK1 by A2, FUNCT_1:51 .= the multF of SK1 by Def1 ; ( 1. SK1 = 1. K & 0. SK1 = 0. K ) by Def1; then ( 1. SK1 = 1. SK2 & 0. SK1 = 0. SK2 ) by Def1; hence SK1 is Subfield of SK2 by A1, A3, A4, Def1; ::_thesis: verum end; theorem Th7: :: EC_PF_1:7 for K being Field for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds x in SK2 ) proof let K be Field; ::_thesis: for SK1, SK2 being Subfield of K holds ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds x in SK2 ) let SK1, SK2 be Subfield of K; ::_thesis: ( SK1 is Subfield of SK2 iff for x being set st x in SK1 holds x in SK2 ) thus ( SK1 is Subfield of SK2 implies for x being set st x in SK1 holds x in SK2 ) by Th3; ::_thesis: ( ( for x being set st x in SK1 holds x in SK2 ) implies SK1 is Subfield of SK2 ) assume A1: for x being set st x in SK1 holds x in SK2 ; ::_thesis: SK1 is Subfield of SK2 the carrier of SK1 c= the carrier of SK2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of SK1 or x in the carrier of SK2 ) assume x in the carrier of SK1 ; ::_thesis: x in the carrier of SK2 then reconsider x = x as Element of SK1 ; x in SK1 by STRUCT_0:def_5; then x in SK2 by A1; hence x in the carrier of SK2 by STRUCT_0:def_5; ::_thesis: verum end; hence SK1 is Subfield of SK2 by Th6; ::_thesis: verum end; theorem Th8: :: EC_PF_1:8 for K being Field for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 ) proof let K be Field; ::_thesis: for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 ) let SK1, SK2 be strict Subfield of K; ::_thesis: ( SK1 = SK2 iff the carrier of SK1 = the carrier of SK2 ) thus ( SK1 = SK2 implies the carrier of SK1 = the carrier of SK2 ) ; ::_thesis: ( the carrier of SK1 = the carrier of SK2 implies SK1 = SK2 ) assume A1: the carrier of SK1 = the carrier of SK2 ; ::_thesis: SK1 = SK2 then A2: SK2 is strict Subfield of SK1 by Th6; SK1 is strict Subfield of SK2 by A1, Th6; hence SK1 = SK2 by A2, Th4; ::_thesis: verum end; theorem :: EC_PF_1:9 for K being Field for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff for x being set holds ( x in SK1 iff x in SK2 ) ) proof let K be Field; ::_thesis: for SK1, SK2 being strict Subfield of K holds ( SK1 = SK2 iff for x being set holds ( x in SK1 iff x in SK2 ) ) let SK1, SK2 be strict Subfield of K; ::_thesis: ( SK1 = SK2 iff for x being set holds ( x in SK1 iff x in SK2 ) ) thus ( SK1 = SK2 implies for x being set holds ( x in SK1 iff x in SK2 ) ) ; ::_thesis: ( ( for x being set holds ( x in SK1 iff x in SK2 ) ) implies SK1 = SK2 ) assume for x being set holds ( x in SK1 iff x in SK2 ) ; ::_thesis: SK1 = SK2 then ( SK1 is strict Subfield of SK2 & SK2 is strict Subfield of SK1 ) by Th7; hence SK1 = SK2 by Th4; ::_thesis: verum end; registration let K be finite Field; cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for Subfield of K; existence ex b1 being Subfield of K st b1 is finite proof reconsider L = K as Subfield of K by Th1; take L ; ::_thesis: L is finite thus L is finite ; ::_thesis: verum end; end; definition let K be finite Field; :: original: card redefine func card K -> Element of NAT ; coherence card K is Element of NAT proof card the carrier of K in NAT ; hence card K is Element of NAT ; ::_thesis: verum end; end; registration cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed for doubleLoopStr ; existence ex b1 being Field st ( b1 is strict & b1 is finite ) proof Z_3 is finite by MOD_2:def_20; hence ex b1 being Field st ( b1 is strict & b1 is finite ) by MOD_2:27; ::_thesis: verum end; end; theorem :: EC_PF_1:10 for K being finite strict Field for SK1 being strict Subfield of K st card K = card SK1 holds SK1 = K proof let K be finite strict Field; ::_thesis: for SK1 being strict Subfield of K st card K = card SK1 holds SK1 = K let SK1 be strict Subfield of K; ::_thesis: ( card K = card SK1 implies SK1 = K ) assume A1: card K = card SK1 ; ::_thesis: SK1 = K A2: the carrier of SK1 = the carrier of K proof assume A3: the carrier of SK1 <> the carrier of K ; ::_thesis: contradiction A4: the carrier of SK1 c= the carrier of K by Def1; then the carrier of SK1 c< the carrier of K by A3, XBOOLE_0:def_8; hence contradiction by A1, A4, CARD_2:48; ::_thesis: verum end; K is Subfield of K by Th1; hence SK1 = K by A2, Th8; ::_thesis: verum end; definition let IT be Field; attrIT is prime means :Def2: :: EC_PF_1:def 2 for K1 being Field st K1 is strict Subfield of IT holds K1 = IT; end; :: deftheorem Def2 defines prime EC_PF_1:def_2_:_ for IT being Field holds ( IT is prime iff for K1 being Field st K1 is strict Subfield of IT holds K1 = IT ); notation let p be Prime; synonym GF p for INT.Ring p; end; registration let p be Prime; cluster GF p -> finite ; coherence GF p is finite ; end; registration let p be Prime; cluster GF p -> prime ; coherence GF p is prime proof set K = GF p; A1: p > 1 by INT_2:def_4; now__::_thesis:_for_K1_being_strict_Subfield_of_GF_p_holds_K1_=_GF_p let K1 be strict Subfield of GF p; ::_thesis: K1 = GF p set C = the carrier of (GF p); set C1 = the carrier of K1; set n1 = p - 1; reconsider n1 = p - 1 as Element of NAT by A1, NAT_1:20; A2: for x being set st x in GF p holds x in K1 proof A3: for n being Element of NAT st n in Segm p holds n in the carrier of K1 proof defpred S1[ Nat] means p in the carrier of K1; 0 in Segm p by NAT_1:44; then 0. (GF p) = 0 by FUNCT_7:def_1; then 0. K1 = 0 by Def1; then A4: S1[ 0 ] ; A5: now__::_thesis:_for_n_being_Element_of_NAT_st_0_<=_n_&_n_<_n1_&_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( 0 <= n & n < n1 & S1[n] implies S1[n + 1] ) assume A6: ( 0 <= n & n < n1 ) ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] A8: 1. K1 = 1. (GF p) by Def1 .= 1 by A1, INT_3:14 ; then A9: [1,n] in [: the carrier of K1, the carrier of K1:] by A7, ZFMISC_1:87; A10: the addF of K1 = the addF of (GF p) || the carrier of K1 by Def1; A11: 1 + n < n1 + 1 by A6, XREAL_1:6; n < n1 + 1 by A6, NAT_1:13; then A12: ( 1 in Segm p & n in Segm p ) by A1, NAT_1:44; the addF of K1 . (1,n) = (addint p) . (1,n) by A9, A10, FUNCT_1:49 .= (1 + n) mod p by A12, GR_CY_1:def_4 .= 1 + n by A11, NAT_D:63 ; hence S1[n + 1] by A7, A8, BINOP_1:17; ::_thesis: verum end; A13: for n being Element of NAT st 0 <= n & n <= n1 holds S1[n] from INT_1:sch_7(A4, A5); thus for n being Element of NAT st n in Segm p holds S1[n] ::_thesis: verum proof let n be Element of NAT ; ::_thesis: ( n in Segm p implies S1[n] ) assume A14: n in Segm p ; ::_thesis: S1[n] ( 0 <= n & n < n1 + 1 ) by A14, ALGSEQ_1:1; then ( 0 <= n & n <= n1 ) by NAT_1:13; hence S1[n] by A13; ::_thesis: verum end; end; thus for x being set st x in GF p holds x in K1 ::_thesis: verum proof let x be set ; ::_thesis: ( x in GF p implies x in K1 ) assume A15: x in GF p ; ::_thesis: x in K1 x in the carrier of (GF p) by A15, STRUCT_0:def_5; then x in the carrier of K1 by A3; hence x in K1 by STRUCT_0:def_5; ::_thesis: verum end; end; GF p is strict Subfield of GF p by Th1; then GF p is strict Subfield of K1 by A2, Th7; hence K1 = GF p by Th4; ::_thesis: verum end; then for K1 being Field st K1 is strict Subfield of GF p holds K1 = GF p ; hence GF p is prime by Def2; ::_thesis: verum end; end; registration cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed prime for doubleLoopStr ; existence ex b1 being Field st b1 is prime proof take GF the Prime ; ::_thesis: GF the Prime is prime thus GF the Prime is prime ; ::_thesis: verum end; end; begin Lm1: for M being non empty multMagma for a being Element of M for n being Nat holds (power M) . (a,n) is Element of M proof let M be non empty multMagma ; ::_thesis: for a being Element of M for n being Nat holds (power M) . (a,n) is Element of M let a be Element of M; ::_thesis: for n being Nat holds (power M) . (a,n) is Element of M defpred S1[ Nat] means (power M) . (a,$1) is Element of M; (power M) . (a,0) = 1_ M by GROUP_1:def_7; then A1: S1[ 0 ] ; A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then reconsider b = (power M) . (a,n) as Element of M ; n - 0 is Element of NAT by NAT_1:21; then (power M) . (a,(n + 1)) = b * a by GROUP_1:def_7; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence for n being Nat holds (power M) . (a,n) is Element of M ; ::_thesis: verum end; theorem Th11: :: EC_PF_1:11 for p being Prime holds 0 = 0. (GF p) proof let p be Prime; ::_thesis: 0 = 0. (GF p) 0 in Segm p by NAT_1:44; hence 0 = 0. (GF p) by FUNCT_7:def_1; ::_thesis: verum end; theorem Th12: :: EC_PF_1:12 for p being Prime holds 1 = 1. (GF p) proof let p be Prime; ::_thesis: 1 = 1. (GF p) 1 < p by INT_2:def_4; then 1 in Segm p by NAT_1:44; hence 1 = 1. (GF p) by FUNCT_7:def_1; ::_thesis: verum end; theorem Th13: :: EC_PF_1:13 for p being Prime for a being Element of (GF p) ex n1 being Nat st a = n1 mod p proof let p be Prime; ::_thesis: for a being Element of (GF p) ex n1 being Nat st a = n1 mod p let a be Element of (GF p); ::_thesis: ex n1 being Nat st a = n1 mod p reconsider a = a as Element of Segm p ; ( 0 <= a & a < p ) by ALGSEQ_1:1; then a = a mod p by NAT_D:63; hence ex n1 being Nat st a = n1 mod p ; ::_thesis: verum end; theorem Th14: :: EC_PF_1:14 for i being Integer for p being Prime holds i mod p is Element of (GF p) proof let i be Integer; ::_thesis: for p being Prime holds i mod p is Element of (GF p) let p be Prime; ::_thesis: i mod p is Element of (GF p) reconsider b = i mod p as Integer ; b in NAT by INT_1:3, INT_1:57; then reconsider b = b as Nat ; b < p by INT_1:58; then b in Segm p by ALGSEQ_1:1; hence i mod p is Element of (GF p) ; ::_thesis: verum end; theorem Th15: :: EC_PF_1:15 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a + b = (i + j) mod p proof let i, j be Integer; ::_thesis: for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a + b = (i + j) mod p let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a + b = (i + j) mod p let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a + b = (i + j) mod p ) assume A1: ( a = i mod p & b = j mod p ) ; ::_thesis: a + b = (i + j) mod p a + b = ((i mod p) + (j mod p)) mod p by A1, GR_CY_1:def_4; hence a + b = (i + j) mod p by NAT_D:66; ::_thesis: verum end; theorem Th16: :: EC_PF_1:16 for i being Integer for p being Prime for a being Element of (GF p) st a = i mod p holds - a = (p - i) mod p proof let i be Integer; ::_thesis: for p being Prime for a being Element of (GF p) st a = i mod p holds - a = (p - i) mod p let p be Prime; ::_thesis: for a being Element of (GF p) st a = i mod p holds - a = (p - i) mod p let a be Element of (GF p); ::_thesis: ( a = i mod p implies - a = (p - i) mod p ) assume A1: a = i mod p ; ::_thesis: - a = (p - i) mod p reconsider b = (p - i) mod p as Element of (GF p) by Th14; a + b = (i + (p - i)) mod p by A1, Th15 .= 0 by INT_1:50 .= 0. (GF p) by Th11 ; hence - a = (p - i) mod p by VECTSP_1:16; ::_thesis: verum end; theorem :: EC_PF_1:17 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a - b = (i - j) mod p proof let i, j be Integer; ::_thesis: for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a - b = (i - j) mod p let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a - b = (i - j) mod p let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a - b = (i - j) mod p ) assume A1: ( a = i mod p & b = j mod p ) ; ::_thesis: a - b = (i - j) mod p then A2: - b = (p - j) mod p by Th16; a - b = (i + (p - j)) mod p by A1, A2, Th15 .= ((i - j) + (1 * p)) mod p ; hence a - b = (i - j) mod p by NAT_D:61; ::_thesis: verum end; theorem Th18: :: EC_PF_1:18 for i, j being Integer for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a * b = (i * j) mod p proof let i, j be Integer; ::_thesis: for p being Prime for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a * b = (i * j) mod p let p be Prime; ::_thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds a * b = (i * j) mod p let a, b be Element of (GF p); ::_thesis: ( a = i mod p & b = j mod p implies a * b = (i * j) mod p ) assume ( a = i mod p & b = j mod p ) ; ::_thesis: a * b = (i * j) mod p then a * b = ((i mod p) * (j mod p)) mod p by INT_3:def_10; hence a * b = (i * j) mod p by NAT_D:67; ::_thesis: verum end; theorem :: EC_PF_1:19 for i, j being Integer for p being Prime for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds a " = j mod p proof let i, j be Integer; ::_thesis: for p being Prime for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds a " = j mod p let p be Prime; ::_thesis: for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds a " = j mod p let a be Element of (GF p); ::_thesis: ( a = i mod p & (i * j) mod p = 1 implies a " = j mod p ) assume A1: ( a = i mod p & (i * j) mod p = 1 ) ; ::_thesis: a " = j mod p reconsider b = j mod p as Element of (GF p) by Th14; A2: p > 1 by INT_2:def_4; A3: b * a = 1 by A1, Th18 .= 1. (GF p) by A2, INT_3:14 ; then a <> 0. (GF p) by VECTSP_1:7; hence a " = j mod p by A3, VECTSP_1:def_10; ::_thesis: verum end; theorem Th20: :: EC_PF_1:20 for p being Prime for a, b being Element of (GF p) holds ( ( a = 0 or b = 0 ) iff a * b = 0 ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) holds ( ( a = 0 or b = 0 ) iff a * b = 0 ) let a, b be Element of (GF p); ::_thesis: ( ( a = 0 or b = 0 ) iff a * b = 0 ) ( ( a = 0. (GF p) or b = 0. (GF p) ) iff a * b = 0. (GF p) ) by VECTSP_1:12; hence ( ( a = 0 or b = 0 ) iff a * b = 0 ) by Th11; ::_thesis: verum end; theorem Th21: :: EC_PF_1:21 for p being Prime for a being Element of (GF p) holds ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 ) proof let p be Prime; ::_thesis: for a being Element of (GF p) holds ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 ) let a be Element of (GF p); ::_thesis: ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 ) thus A1: a |^ 0 = 1_ (GF p) by BINOM:8; ::_thesis: a |^ 0 = 1 p > 1 by INT_2:def_4; hence a |^ 0 = 1 by A1, INT_3:14; ::_thesis: verum end; Lm2: for p being Prime for a being Element of (GF p) holds (power (GF p)) . (a,1) = a by GROUP_1:50; Lm3: for p being Prime for a being Element of (GF p) holds (power (GF p)) . (a,2) = a * a by GROUP_1:51; theorem :: EC_PF_1:22 for p being Prime for a being Element of (GF p) holds a |^ 2 = a * a by Lm3; theorem Th23: :: EC_PF_1:23 for n1, n being Nat for p being Prime for a being Element of (GF p) st a = n1 mod p holds a |^ n = (n1 |^ n) mod p proof let n1, n be Nat; ::_thesis: for p being Prime for a being Element of (GF p) st a = n1 mod p holds a |^ n = (n1 |^ n) mod p let p be Prime; ::_thesis: for a being Element of (GF p) st a = n1 mod p holds a |^ n = (n1 |^ n) mod p let a be Element of (GF p); ::_thesis: ( a = n1 mod p implies a |^ n = (n1 |^ n) mod p ) A1: p > 1 by INT_2:def_4; assume A2: a = n1 mod p ; ::_thesis: a |^ n = (n1 |^ n) mod p defpred S1[ Nat] means (power (GF p)) . (a,$1) = (n1 |^ $1) mod p; a |^ 0 = 1 by Th21; then A3: a |^ 0 = 1 mod p by A1, NAT_D:63; A4: S1[ 0 ] by A3, NEWTON:4; A5: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A6: S1[n] ; ::_thesis: S1[n + 1] reconsider b = (power (GF p)) . (a,n) as Element of (GF p) by Lm1; n - 0 is Element of NAT by NAT_1:21; then (power (GF p)) . (a,(n + 1)) = b * a by GROUP_1:def_7 .= ((n1 |^ n) * n1) mod p by A2, A6, Th18 .= (n1 |^ (n + 1)) mod p by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5); hence a |^ n = (n1 |^ n) mod p ; ::_thesis: verum end; theorem Th24: :: EC_PF_1:24 for K being non empty unital associative multMagma for a being Element of K for n being Nat holds a |^ (n + 1) = (a |^ n) * a proof let K be non empty unital associative multMagma ; ::_thesis: for a being Element of K for n being Nat holds a |^ (n + 1) = (a |^ n) * a let a be Element of K; ::_thesis: for n being Nat holds a |^ (n + 1) = (a |^ n) * a let n be Nat; ::_thesis: a |^ (n + 1) = (a |^ n) * a a |^ (n + 1) = (a |^ n) * (a |^ 1) by BINOM:10 .= (a |^ n) * a by BINOM:8 ; hence a |^ (n + 1) = (a |^ n) * a ; ::_thesis: verum end; theorem Th25: :: EC_PF_1:25 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 holds a |^ n <> 0 proof let n be Nat; ::_thesis: for p being Prime for a being Element of (GF p) st a <> 0 holds a |^ n <> 0 let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds a |^ n <> 0 let a be Element of (GF p); ::_thesis: ( a <> 0 implies a |^ n <> 0 ) assume A1: a <> 0 ; ::_thesis: a |^ n <> 0 consider n1 being Nat such that A2: a = n1 mod p by Th13; not p divides n1 by A1, A2, INT_1:62; then not p divides n1 |^ n by NAT_3:5; then (n1 |^ n) mod p <> 0 by INT_1:62; hence a |^ n <> 0 by A2, Th23; ::_thesis: verum end; theorem Th26: :: EC_PF_1:26 for F being non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for x, y being Element of F holds ( x * x = y * y iff ( x = y or x = - y ) ) proof let F be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y being Element of F holds ( x * x = y * y iff ( x = y or x = - y ) ) let x, y be Element of F; ::_thesis: ( x * x = y * y iff ( x = y or x = - y ) ) A1: (x - y) * (x + y) = ((x - y) * x) + ((x - y) * y) by VECTSP_1:4 .= ((x * x) - (x * y)) + ((x - y) * y) by VECTSP_1:11 .= ((x * x) - (x * y)) + ((y * x) - (y * y)) by VECTSP_1:11 .= (((x * x) - (x * y)) + (y * x)) + (- (y * y)) by RLVECT_1:def_3 .= ((x * x) + ((- (x * y)) + (y * x))) + (- (y * y)) by RLVECT_1:def_3 .= ((x * x) + ((y * x) - (x * y))) + (- (y * y)) .= ((x * x) + ((x - x) * y)) + (- (y * y)) by VECTSP_1:11 .= ((x * x) + ((0. F) * y)) - (y * y) by RLVECT_1:5 .= ((x * x) + (0. F)) - (y * y) by VECTSP_1:7 .= (x * x) - (y * y) by RLVECT_1:def_4 ; hereby ::_thesis: ( ( x = y or x = - y ) implies x * x = y * y ) assume A2: x * x = y * y ; ::_thesis: ( x = y or x = - y ) (x - y) * (x + y) = 0. F by A1, A2, RLVECT_1:5; then ( x - y = 0. F or x + y = 0. F ) by VECTSP_1:12; hence ( x = y or x = - y ) by RLVECT_1:6, RLVECT_1:21; ::_thesis: verum end; assume ( x = y or x = - y ) ; ::_thesis: x * x = y * y then ( x - y = 0. F or x + y = 0. F ) by RLVECT_1:5; hence x * x = y * y by A1, RLVECT_1:21, VECTSP_1:6; ::_thesis: verum end; theorem Th27: :: EC_PF_1:27 for p being Prime for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds x = 0. (GF p) proof let p be Prime; ::_thesis: for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds x = 0. (GF p) let x be Element of (GF p); ::_thesis: ( 2 < p & x + x = 0. (GF p) implies x = 0. (GF p) ) assume A1: ( 2 < p & x + x = 0. (GF p) ) ; ::_thesis: x = 0. (GF p) x in Segm p ; then reconsider Ix = x as Element of NAT ; A2: 1 = 1. (GF p) by Th12; A3: 1 + 1 < p by A1; A4: (1. (GF p)) + (1. (GF p)) = 2 by A2, A3, INT_3:7; set d = (1. (GF p)) + (1. (GF p)); A5: ((1. (GF p)) + (1. (GF p))) * x = (2 * Ix) mod p by A4, INT_3:def_10; x + x = ((1. (GF p)) * x) + x by VECTSP_1:def_6 .= ((1. (GF p)) * x) + ((1. (GF p)) * x) by VECTSP_1:def_6 .= (2 * Ix) mod p by A5, VECTSP_1:def_7 ; then (2 * Ix) mod p = 0 by A1, Th11; then (2 * Ix) - (((2 * Ix) div p) * p) = 0 by INT_1:def_10; then A6: p divides 2 * Ix by INT_1:def_3; p divides Ix by A1, A6, EULER_1:13, INT_2:28, INT_2:30; then Ix = p * (Ix div p) by NAT_D:3; then Ix - ((Ix div p) * p) = 0 ; then A7: Ix mod p = 0 by INT_1:def_10; Ix < p by NAT_1:44; then Ix = 0 by A7, NAT_D:63; hence x = 0. (GF p) by Th11; ::_thesis: verum end; theorem Th28: :: EC_PF_1:28 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 holds (a ") |^ n = (a |^ n) " proof let n be Nat; ::_thesis: for p being Prime for a being Element of (GF p) st a <> 0 holds (a ") |^ n = (a |^ n) " let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds (a ") |^ n = (a |^ n) " let a be Element of (GF p); ::_thesis: ( a <> 0 implies (a ") |^ n = (a |^ n) " ) assume A1: a <> 0 ; ::_thesis: (a ") |^ n = (a |^ n) " A2: p > 1 by INT_2:def_4; consider n1 being Nat such that A3: a = n1 mod p by Th13; consider n2 being Nat such that A4: a " = n2 mod p by Th13; A5: a |^ n = (n1 |^ n) mod p by A3, Th23; A6: (a ") |^ n = (n2 |^ n) mod p by A4, Th23; A7: ((n1 * n2) |^ n) mod p = ((n1 |^ n) * (n2 |^ n)) mod p by NEWTON:7 .= (a |^ n) * ((a ") |^ n) by A5, A6, Th18 ; a <> 0. (GF p) by A1, Th11; then (a ") * a = 1. (GF p) by VECTSP_1:def_10 .= 1 by Th12 ; then (n1 * n2) mod p = 1 by A3, A4, Th18; then ((n1 * n2) |^ n) mod p = 1 by A2, PEPIN:35; then A8: ((a ") |^ n) * (a |^ n) = 1. (GF p) by A2, A7, INT_3:14; then a |^ n <> 0. (GF p) by VECTSP_1:7; hence (a ") |^ n = (a |^ n) " by A8, VECTSP_1:def_10; ::_thesis: verum end; Lm4: for n1, n2 being Nat for p being Prime for a being Element of (GF p) holds (a |^ n1) * (a |^ n2) = a |^ (n1 + n2) by BINOM:10; Lm5: for n1, n2 being Nat for p being Prime for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2) by BINOM:11; registration let p be Prime; cluster MultGroup (GF p) -> cyclic ; coherence MultGroup (GF p) is cyclic proof MultGroup (GF p) is finite Subgroup of MultGroup (GF p) by GROUP_2:54; hence MultGroup (GF p) is cyclic by GR_CY_3:38; ::_thesis: verum end; end; theorem Th29: :: EC_PF_1:29 for p being Prime for x being Element of (MultGroup (GF p)) for x1 being Element of (GF p) for n being Nat st x = x1 holds x |^ n = x1 |^ n proof let p be Prime; ::_thesis: for x being Element of (MultGroup (GF p)) for x1 being Element of (GF p) for n being Nat st x = x1 holds x |^ n = x1 |^ n let x be Element of (MultGroup (GF p)); ::_thesis: for x1 being Element of (GF p) for n being Nat st x = x1 holds x |^ n = x1 |^ n let x1 be Element of (GF p); ::_thesis: for n being Nat st x = x1 holds x |^ n = x1 |^ n let n be Nat; ::_thesis: ( x = x1 implies x |^ n = x1 |^ n ) assume A1: x = x1 ; ::_thesis: x |^ n = x1 |^ n defpred S1[ Nat] means x |^ $1 = x1 |^ $1; A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: x |^ (n + 1) = (x |^ n) * x by GROUP_1:34; A4: x1 |^ (n + 1) = (x1 |^ n) * x1 by Th24; assume x |^ n = x1 |^ n ; ::_thesis: S1[n + 1] hence S1[n + 1] by A1, A3, A4, UNIROOTS:16; ::_thesis: verum end; x |^ 0 = 1_ (MultGroup (GF p)) by GROUP_1:25 .= 1_ (GF p) by UNIROOTS:17 .= x1 |^ 0 by Th21 ; then A5: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2); hence x |^ n = x1 |^ n ; ::_thesis: verum end; theorem Th30: :: EC_PF_1:30 for p being Prime ex g being Element of (GF p) st for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g |^ n proof let p be Prime; ::_thesis: ex g being Element of (GF p) st for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g |^ n consider g being Element of (MultGroup (GF p)) such that A1: for a being Element of (MultGroup (GF p)) ex n being Nat st a = g |^ n by GR_CY_1:18; reconsider g0 = g as Element of (GF p) by UNIROOTS:19; take g0 ; ::_thesis: for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g0 |^ n now__::_thesis:_for_a_being_Element_of_(GF_p)_st_a_<>_0._(GF_p)_holds_ ex_n_being_Nat_st_a_=_g0_|^_n let a be Element of (GF p); ::_thesis: ( a <> 0. (GF p) implies ex n being Nat st a = g0 |^ n ) assume a <> 0. (GF p) ; ::_thesis: ex n being Nat st a = g0 |^ n then A2: not a in {(0. (GF p))} by TARSKI:def_1; the carrier of (GF p) = the carrier of (MultGroup (GF p)) \/ {(0. (GF p))} by UNIROOTS:15; then reconsider a0 = a as Element of (MultGroup (GF p)) by A2, XBOOLE_0:def_3; consider n being Nat such that A3: a0 = g |^ n by A1; take n = n; ::_thesis: a = g0 |^ n thus a = g0 |^ n by A3, Th29; ::_thesis: verum end; hence for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g0 |^ n ; ::_thesis: verum end; begin definition let p be Prime; let a be Element of (GF p); attra is quadratic_residue means :Def3: :: EC_PF_1:def 3 ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ); attra is not_quadratic_residue means :Def4: :: EC_PF_1:def 4 ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ); end; :: deftheorem Def3 defines quadratic_residue EC_PF_1:def_3_:_ for p being Prime for a being Element of (GF p) holds ( a is quadratic_residue iff ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) ); :: deftheorem Def4 defines not_quadratic_residue EC_PF_1:def_4_:_ for p being Prime for a being Element of (GF p) holds ( a is not_quadratic_residue iff ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) ); theorem Th31: :: EC_PF_1:31 for p being Prime for a being Element of (GF p) st a <> 0 holds a |^ 2 is quadratic_residue proof let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds a |^ 2 is quadratic_residue let a be Element of (GF p); ::_thesis: ( a <> 0 implies a |^ 2 is quadratic_residue ) assume A1: a <> 0 ; ::_thesis: a |^ 2 is quadratic_residue reconsider b = a |^ 2 as Element of (GF p) ; b <> 0 by A1, Th25; hence a |^ 2 is quadratic_residue by Def3; ::_thesis: verum end; registration let p be Prime; cluster 1. (GF p) -> quadratic_residue ; correctness coherence 1. (GF p) is quadratic_residue ; proof A1: p > 1 by INT_2:def_4; reconsider a = 1. (GF p) as Element of (GF p) ; A2: a = 1 by A1, INT_3:14; a |^ 2 = (1. (GF p)) * (1. (GF p)) by Lm3 .= 1_ (GF p) by GROUP_1:def_4 ; hence 1. (GF p) is quadratic_residue by A2, Th31; ::_thesis: verum end; end; definition let p be Prime; let a be Element of (GF p); func Lege_p a -> Integer equals :Def5: :: EC_PF_1:def 5 0 if a = 0 1 if a is quadratic_residue otherwise - 1; coherence ( ( a = 0 implies 0 is Integer ) & ( a is quadratic_residue implies 1 is Integer ) & ( not a = 0 & not a is quadratic_residue implies - 1 is Integer ) ) ; consistency for b1 being Integer st a = 0 & a is quadratic_residue holds ( b1 = 0 iff b1 = 1 ) by Def3; end; :: deftheorem Def5 defines Lege_p EC_PF_1:def_5_:_ for p being Prime for a being Element of (GF p) holds ( ( a = 0 implies Lege_p a = 0 ) & ( a is quadratic_residue implies Lege_p a = 1 ) & ( not a = 0 & not a is quadratic_residue implies Lege_p a = - 1 ) ); theorem Th32: :: EC_PF_1:32 for p being Prime for a being Element of (GF p) holds ( a is not_quadratic_residue iff Lege_p a = - 1 ) proof let p be Prime; ::_thesis: for a being Element of (GF p) holds ( a is not_quadratic_residue iff Lege_p a = - 1 ) let a be Element of (GF p); ::_thesis: ( a is not_quadratic_residue iff Lege_p a = - 1 ) hereby ::_thesis: ( Lege_p a = - 1 implies a is not_quadratic_residue ) assume a is not_quadratic_residue ; ::_thesis: Lege_p a = - 1 then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by Def4; then ( a <> 0 & not a is quadratic_residue ) by Def3; hence Lege_p a = - 1 by Def5; ::_thesis: verum end; assume Lege_p a = - 1 ; ::_thesis: a is not_quadratic_residue then ( a <> 0 & not a is quadratic_residue ) by Def5; then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by Def3; hence a is not_quadratic_residue by Def4; ::_thesis: verum end; theorem Th33: :: EC_PF_1:33 for p being Prime for a being Element of (GF p) holds ( a is quadratic_residue iff Lege_p a = 1 ) proof let p be Prime; ::_thesis: for a being Element of (GF p) holds ( a is quadratic_residue iff Lege_p a = 1 ) let a be Element of (GF p); ::_thesis: ( a is quadratic_residue iff Lege_p a = 1 ) thus ( a is quadratic_residue implies Lege_p a = 1 ) by Def5; ::_thesis: ( Lege_p a = 1 implies a is quadratic_residue ) assume Lege_p a = 1 ; ::_thesis: a is quadratic_residue then ( a <> 0 & Lege_p a <> - 1 ) by Def5; hence a is quadratic_residue by Def5; ::_thesis: verum end; theorem Th34: :: EC_PF_1:34 for p being Prime for a being Element of (GF p) holds ( a = 0 iff Lege_p a = 0 ) proof let p be Prime; ::_thesis: for a being Element of (GF p) holds ( a = 0 iff Lege_p a = 0 ) let a be Element of (GF p); ::_thesis: ( a = 0 iff Lege_p a = 0 ) thus ( a = 0 implies Lege_p a = 0 ) by Def5; ::_thesis: ( Lege_p a = 0 implies a = 0 ) assume Lege_p a = 0 ; ::_thesis: a = 0 then ( not a is quadratic_residue & Lege_p a <> - 1 ) by Def5; hence a = 0 by Def5; ::_thesis: verum end; theorem :: EC_PF_1:35 for p being Prime for a being Element of (GF p) st a <> 0 holds Lege_p (a |^ 2) = 1 proof let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 holds Lege_p (a |^ 2) = 1 let a be Element of (GF p); ::_thesis: ( a <> 0 implies Lege_p (a |^ 2) = 1 ) assume a <> 0 ; ::_thesis: Lege_p (a |^ 2) = 1 then a |^ 2 is quadratic_residue by Th31; hence Lege_p (a |^ 2) = 1 by Th33; ::_thesis: verum end; theorem Th36: :: EC_PF_1:36 for p being Prime for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b) let a, b be Element of (GF p); ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) percases ( a is quadratic_residue or not a is quadratic_residue ) ; supposeA1: a is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A2: Lege_p a = 1 by Th33; percases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ; supposeA3: b is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A4: Lege_p b = 1 by Th33; A5: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1, Def3; ( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A3, Def3; then A6: a * b <> 0 by A5, Th20; ex x being Element of (GF p) st x |^ 2 = a * b proof consider a1 being Element of (GF p) such that A7: a1 |^ 2 = a by A1, Def3; consider b1 being Element of (GF p) such that A8: b1 |^ 2 = b by A3, Def3; (a1 |^ 2) * (b1 |^ 2) = (a1 * b1) |^ 2 by BINOM:9; hence ex x being Element of (GF p) st x |^ 2 = a * b by A7, A8; ::_thesis: verum end; then a * b is quadratic_residue by A6, Def3; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A4, Th33; ::_thesis: verum end; supposeA9: b = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then Lege_p b = 0 by Def5; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A9, Th20; ::_thesis: verum end; supposeA10: ( b <> 0 & not b is quadratic_residue ) ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A11: Lege_p b = - 1 by Def5; A12: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1, Def3; A13: a * b <> 0 by A10, A12, Th20; for x being Element of (GF p) holds not x |^ 2 = a * b proof given xab being Element of (GF p) such that A14: xab |^ 2 = a * b ; ::_thesis: contradiction consider xa being Element of (GF p) such that A15: xa |^ 2 = a by A1, Def3; A16: xa |^ 2 <> 0. (GF p) by A12, A15, Th11; A17: xa <> 0 proof assume xa = 0 ; ::_thesis: contradiction then xa = 0. (GF p) by Th11; then xa * xa = 0. (GF p) by VECTSP_1:12; then xa |^ 2 = 0. (GF p) by Lm3; hence contradiction by A15, A12, Th11; ::_thesis: verum end; ((xa ") * xab) |^ 2 = ((xa ") |^ 2) * (a * b) by A14, BINOM:9 .= (((xa ") |^ 2) * (xa |^ 2)) * b by A15, GROUP_1:def_3 .= (((xa |^ 2) ") * (xa |^ 2)) * b by Th28, A17 .= (1. (GF p)) * b by A16, VECTSP_1:def_10 .= b by VECTSP_1:def_8 ; hence contradiction by A10, Def3; ::_thesis: verum end; then a * b is not_quadratic_residue by A13, Def4; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A11, Th32; ::_thesis: verum end; end; end; supposeA18: not a is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) now__::_thesis:_Lege_p_(a_*_b)_=_(Lege_p_a)_*_(Lege_p_b) percases ( a = 0 or a <> 0 ) ; supposeA19: a = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then Lege_p a = 0 by Th34; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A19, Th20; ::_thesis: verum end; supposeA20: a <> 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A21: Lege_p a = - 1 by A18, Def5; percases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ; supposeA22: b is quadratic_residue ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A23: Lege_p b = 1 by Th33; A24: ( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A22, Def3; then A25: a * b <> 0 by A20, Th20; for x being Element of (GF p) holds not x |^ 2 = a * b proof given xab being Element of (GF p) such that A26: xab |^ 2 = a * b ; ::_thesis: contradiction consider xb being Element of (GF p) such that A27: xb |^ 2 = b by A22, Def3; A28: xb |^ 2 <> 0. (GF p) by A24, A27, Th11; A29: xb <> 0 proof assume xb = 0 ; ::_thesis: contradiction then xb = 0. (GF p) by Th11; then xb * xb = 0. (GF p) by VECTSP_1:12; then xb |^ 2 = 0. (GF p) by Lm3; hence contradiction by A27, A24, Th11; ::_thesis: verum end; (xab * (xb ")) |^ 2 = (a * b) * ((xb ") |^ 2) by A26, BINOM:9 .= a * ((xb |^ 2) * ((xb ") |^ 2)) by A27, GROUP_1:def_3 .= a * ((xb |^ 2) * ((xb |^ 2) ")) by Th28, A29 .= a * (1. (GF p)) by A28, VECTSP_1:def_10 .= a by VECTSP_1:def_8 ; hence contradiction by A18, A20, Def3; ::_thesis: verum end; then a * b is not_quadratic_residue by A25, Def4; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A23, Th32; ::_thesis: verum end; supposeA30: b = 0 ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then Lege_p b = 0 by Th34; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A30, Th20; ::_thesis: verum end; supposeA31: ( b <> 0 & not b is quadratic_residue ) ; ::_thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b) then A32: Lege_p b = - 1 by Def5; A33: a * b <> 0 by A20, A31, Th20; ex x being Element of (GF p) st x |^ 2 = a * b proof consider g being Element of (GF p) such that A34: for a being Element of (GF p) st a <> 0. (GF p) holds ex n being Nat st a = g |^ n by Th30; a <> 0. (GF p) by A20, Th11; then consider na being Nat such that A35: a = g |^ na by A34; b <> 0. (GF p) by A31, Th11; then consider nb being Nat such that A36: b = g |^ nb by A34; A37: na = ((na div 2) * 2) + (na mod 2) by NAT_D:2; A38: nb = ((nb div 2) * 2) + (nb mod 2) by NAT_D:2; na mod 2 <> 0 proof assume A39: na mod 2 = 0 ; ::_thesis: contradiction reconsider nn = na div 2 as Element of NAT ; a = (g |^ nn) |^ 2 by A35, A37, A39, Lm5; hence contradiction by A18, A20, Def3; ::_thesis: verum end; then A40: na mod 2 = 1 by NAT_D:12; nb mod 2 <> 0 proof assume A41: nb mod 2 = 0 ; ::_thesis: contradiction reconsider nn = nb div 2 as Element of NAT ; b = (g |^ nn) |^ 2 by A36, A38, A41, Lm5; hence contradiction by A31, Def3; ::_thesis: verum end; then A42: nb mod 2 = 1 by NAT_D:12; reconsider nc = ((na div 2) + (nb div 2)) + 1 as Nat ; A43: na + nb = (((na div 2) * 2) + 1) + nb by A40, NAT_D:2 .= (((na div 2) * 2) + 1) + (((nb div 2) * 2) + 1) by A42, NAT_D:2 .= nc * 2 ; a * b = g |^ (na + nb) by A35, A36, Lm4 .= (g |^ nc) |^ 2 by A43, Lm5 ; hence ex x being Element of (GF p) st x |^ 2 = a * b ; ::_thesis: verum end; then a * b is quadratic_residue by A33, Def3; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A32, Th33; ::_thesis: verum end; end; end; end; end; hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) ; ::_thesis: verum end; end; end; theorem Th37: :: EC_PF_1:37 for n being Nat for p being Prime for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds Lege_p (a |^ n) = 1 proof let n be Nat; ::_thesis: for p being Prime for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds Lege_p (a |^ n) = 1 let p be Prime; ::_thesis: for a being Element of (GF p) st a <> 0 & n mod 2 = 0 holds Lege_p (a |^ n) = 1 let a be Element of (GF p); ::_thesis: ( a <> 0 & n mod 2 = 0 implies Lege_p (a |^ n) = 1 ) assume A1: ( a <> 0 & n mod 2 = 0 ) ; ::_thesis: Lege_p (a |^ n) = 1 A2: n = ((n div 2) * 2) + (n mod 2) by INT_1:59 .= (n div 2) * 2 by A1 ; reconsider n1 = n div 2 as Nat ; (a |^ n1) |^ 2 is quadratic_residue by A1, Th31, Th25; then a |^ n is quadratic_residue by A2, Lm5; hence Lege_p (a |^ n) = 1 by Def5; ::_thesis: verum end; theorem :: EC_PF_1:38 for n being Nat for p being Prime for a being Element of (GF p) st n mod 2 = 1 holds Lege_p (a |^ n) = Lege_p a proof let n be Nat; ::_thesis: for p being Prime for a being Element of (GF p) st n mod 2 = 1 holds Lege_p (a |^ n) = Lege_p a let p be Prime; ::_thesis: for a being Element of (GF p) st n mod 2 = 1 holds Lege_p (a |^ n) = Lege_p a let a be Element of (GF p); ::_thesis: ( n mod 2 = 1 implies Lege_p (a |^ n) = Lege_p a ) assume A1: n mod 2 = 1 ; ::_thesis: Lege_p (a |^ n) = Lege_p a A2: n = ((n div 2) * 2) + 1 by A1, INT_1:59; reconsider n1 = n - 1 as Nat by A2; a |^ (n1 + 1) = (a |^ n1) * a by Th24; then A3: Lege_p (a |^ n) = (Lege_p (a |^ n1)) * (Lege_p a) by Th36; percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: Lege_p (a |^ n) = Lege_p a then Lege_p a = 0 by Def5; hence Lege_p (a |^ n) = Lege_p a by A3; ::_thesis: verum end; supposeA4: a <> 0 ; ::_thesis: Lege_p (a |^ n) = Lege_p a (n - 1) mod 2 = (0 + ((n div 2) * 2)) mod 2 by A2 .= 0 mod 2 by NAT_D:61 .= 0 by NAT_D:26 ; then Lege_p (a |^ n1) = 1 by A4, Th37; hence Lege_p (a |^ n) = Lege_p a by A3; ::_thesis: verum end; end; end; theorem Th39: :: EC_PF_1:39 for p being Prime for a being Element of (GF p) st 2 < p holds card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) proof let p be Prime; ::_thesis: for a being Element of (GF p) st 2 < p holds card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) let a be Element of (GF p); ::_thesis: ( 2 < p implies card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ) assume A1: 2 < p ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) percases ( a is quadratic_residue or not a is quadratic_residue ) ; supposeA2: a is quadratic_residue ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) then consider x being Element of (GF p) such that A3: x |^ 2 = a by Def3; A4: x in { b where b is Element of (GF p) : b |^ 2 = a } by A3; (- x) |^ 2 = (- x) * (- x) by Lm3 .= x * x by VECTSP_1:10 .= a by A3, Lm3 ; then - x in { b where b is Element of (GF p) : b |^ 2 = a } ; then A5: {x,(- x)} c= { b where b is Element of (GF p) : b |^ 2 = a } by A4, ZFMISC_1:32; A6: x <> - x proof assume x = - x ; ::_thesis: contradiction then x + x = 0. (GF p) by VECTSP_1:16; then A7: x = 0. (GF p) by A1, Th27; x |^ 2 = (0. (GF p)) * (0. (GF p)) by A7, Lm3 .= 0. (GF p) by VECTSP_1:12 .= 0 by Th11 ; hence contradiction by A3, A2, Def3; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__holds_ y_in_{x,(-_x)} let y be set ; ::_thesis: ( y in { b where b is Element of (GF p) : b |^ 2 = a } implies y in {x,(- x)} ) assume y in { b where b is Element of (GF p) : b |^ 2 = a } ; ::_thesis: y in {x,(- x)} then consider z being Element of (GF p) such that A8: ( y = z & z |^ 2 = a ) ; z * z = z |^ 2 by Lm3 .= x * x by A3, A8, Lm3 ; then ( z = x or z = - x ) by Th26; hence y in {x,(- x)} by A8, TARSKI:def_2; ::_thesis: verum end; then { b where b is Element of (GF p) : b |^ 2 = a } c= {x,(- x)} by TARSKI:def_3; hence card { b where b is Element of (GF p) : b |^ 2 = a } = card {x,(- x)} by A5, XBOOLE_0:def_10 .= 1 + 1 by A6, CARD_2:57 .= 1 + (Lege_p a) by A2, Def5 ; ::_thesis: verum end; supposeA9: not a is quadratic_residue ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) now__::_thesis:_card__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__=_1_+_(Lege_p_a) percases ( a = 0 or a <> 0 ) ; supposeA10: a = 0 ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ::_thesis: verum proof now__::_thesis:_for_x_being_set_st_x_in__{__b_where_b_is_Element_of_(GF_p)_:_b_|^_2_=_a__}__holds_ x_in_{(0._(GF_p))} let x be set ; ::_thesis: ( x in { b where b is Element of (GF p) : b |^ 2 = a } implies x in {(0. (GF p))} ) assume x in { b where b is Element of (GF p) : b |^ 2 = a } ; ::_thesis: x in {(0. (GF p))} then consider b being Element of (GF p) such that A11: ( x = b & b |^ 2 = 0 ) by A10; b = 0 by Th25, A11 .= 0. (GF p) by Th11 ; hence x in {(0. (GF p))} by A11, TARSKI:def_1; ::_thesis: verum end; then A12: { b where b is Element of (GF p) : b |^ 2 = a } c= {(0. (GF p))} by TARSKI:def_3; (0. (GF p)) |^ 2 = (0. (GF p)) * (0. (GF p)) by Lm3 .= 0. (GF p) by VECTSP_1:12 .= 0 by Th11 ; then 0. (GF p) in { b where b is Element of (GF p) : b |^ 2 = a } by A10; then {(0. (GF p))} c= { b where b is Element of (GF p) : b |^ 2 = a } by ZFMISC_1:31; then { b where b is Element of (GF p) : b |^ 2 = a } = {(0. (GF p))} by A12, XBOOLE_0:def_10; hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + 0 by CARD_2:42 .= 1 + (Lege_p a) by A10, Def5 ; ::_thesis: verum end; end; supposeA13: a <> 0 ; ::_thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) A14: { b where b is Element of (GF p) : b |^ 2 = a } = {} proof assume { b where b is Element of (GF p) : b |^ 2 = a } <> {} ; ::_thesis: contradiction then consider x being set such that A15: x in { b where b is Element of (GF p) : b |^ 2 = a } by XBOOLE_0:def_1; ex b being Element of (GF p) st ( x = b & b |^ 2 = a ) by A15; hence contradiction by A9, Def3, A13; ::_thesis: verum end; thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (- 1) by A14 .= 1 + (Lege_p a) by A9, A13, Def5 ; ::_thesis: verum end; end; end; hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ; ::_thesis: verum end; end; end; begin definition let K be Field; func ProjCo K -> non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] equals :: EC_PF_1:def 6 [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]}; correctness coherence [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:]; proof [(1. K),(1. K),(1. K)] <> [(0. K),(0. K),(0. K)] by XTUPLE_0:3; then not [(1. K),(1. K),(1. K)] in {[(0. K),(0. K),(0. K)]} by TARSKI:def_1; hence [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]} is non empty Subset of [: the carrier of K, the carrier of K, the carrier of K:] by XBOOLE_0:def_5; ::_thesis: verum end; end; :: deftheorem defines ProjCo EC_PF_1:def_6_:_ for K being Field holds ProjCo K = [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]}; theorem Th40: :: EC_PF_1:40 for p being Prime holds ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} proof let p be Prime; ::_thesis: ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} 0. (GF p) = 0 by Th11; hence ProjCo (GF p) = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} ; ::_thesis: verum end; definition let p be Prime; let a, b be Element of (GF p); func Disc (a,b,p) -> Element of (GF p) means :: EC_PF_1:def 7 for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds it = (g4 * (a |^ 3)) + (g27 * (b |^ 2)); existence ex b1 being Element of (GF p) st for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) proof reconsider g40 = 4 mod p as Element of (GF p) by Th14; reconsider g270 = 27 mod p as Element of (GF p) by Th14; reconsider d = (g40 * (a |^ 3)) + (g270 * (b |^ 2)) as Element of (GF p) ; take d ; ::_thesis: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) thus for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of (GF p) st ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) holds b1 = b2 proof let d1, d2 be Element of (GF p); ::_thesis: ( ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) & ( for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) implies d1 = d2 ) assume A1: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: ( ex g4, g27 being Element of (GF p) st ( g4 = 4 mod p & g27 = 27 mod p & not d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ) or d1 = d2 ) assume A2: for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds d2 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ; ::_thesis: d1 = d2 reconsider g4 = 4 mod p as Element of (GF p) by Th14; reconsider g27 = 27 mod p as Element of (GF p) by Th14; thus d1 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) by A1 .= d2 by A2 ; ::_thesis: verum end; end; :: deftheorem defines Disc EC_PF_1:def_7_:_ for p being Prime for a, b, b4 being Element of (GF p) holds ( b4 = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds b4 = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) ); definition let p be Prime; let a, b be Element of (GF p); func EC_WEqProjCo (a,b,p) -> Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) means :Def8: :: EC_PF_1:def 8 for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds it . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))); existence ex b1 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) proof set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; deffunc H1( Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]) -> Element of the carrier of (GF p) = ((($1 `2_3) |^ 2) * ($1 `3_3)) - (((($1 `1_3) |^ 3) + ((a * ($1 `1_3)) * (($1 `3_3) |^ 2))) + (b * (($1 `3_3) |^ 3))); consider f being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p) such that A1: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) thus for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) st ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b1 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b2 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) holds b1 = b2 proof set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; deffunc H1( Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]) -> Element of the carrier of (GF p) = ((($1 `2_3) |^ 2) * ($1 `3_3)) - (((($1 `1_3) |^ 3) + ((a * ($1 `1_3)) * (($1 `3_3) |^ 2))) + (b * (($1 `3_3) |^ 3))); let f, g be Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):], the carrier of (GF p); ::_thesis: ( ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) & ( for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ) implies f = g ) assume A2: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds f . x = H1(x) ; ::_thesis: ( ex P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st not g . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) or f = g ) assume A3: for x being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds g . x = H1(x) ; ::_thesis: f = g now__::_thesis:_for_x_being_Element_of_[:_the_carrier_of_(GF_p),_the_carrier_of_(GF_p),_the_carrier_of_(GF_p):]_holds_f_._x_=_g_._x let x be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; ::_thesis: f . x = g . x thus f . x = H1(x) by A2 .= g . x by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:def_8; ::_thesis: verum end; end; :: deftheorem Def8 defines EC_WEqProjCo EC_PF_1:def_8_:_ for p being Prime for a, b being Element of (GF p) for b4 being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds ( b4 = EC_WEqProjCo (a,b,p) iff for P being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] holds b4 . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) ); theorem Th41: :: EC_PF_1:41 for p being Prime for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) proof let p be Prime; ::_thesis: for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) let a, b be Element of (GF p); ::_thesis: for X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) let X, Y, Z be Element of (GF p); ::_thesis: (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; reconsider P = [X,Y,Z] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ; ( P `1_3 = X & P `2_3 = Y & P `3_3 = Z ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7; hence (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) by Def8; ::_thesis: verum end; Lm6: for p being Prime for a, b being Element of (GF p) holds ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) holds ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) let a, b be Element of (GF p); ::_thesis: ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) set P = [0,1,0]; hereby ::_thesis: (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) [0,1,0] <> [0,0,0] by XTUPLE_0:3; then A1: not [0,1,0] in {[0,0,0]} by TARSKI:def_1; A2: 0 in the carrier of (GF p) by NAT_1:44; 1. (GF p) in the carrier of (GF p) ; then 1 in the carrier of (GF p) by Th12; then [0,1,0] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] by A2, MCART_1:69; then [0,1,0] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by A1, XBOOLE_0:def_5; hence [0,1,0] is Element of ProjCo (GF p) by Th40; ::_thesis: verum end; then reconsider P = [0,1,0] as Element of ProjCo (GF p) ; set Px = P `1_3 ; set Py = P `2_3 ; set Pz = P `3_3 ; A3: P = [(0. (GF p)),1,0] by Th11 .= [(0. (GF p)),(1. (GF p)),0] by Th12 .= [(0. (GF p)),(1. (GF p)),(0. (GF p))] by Th11 ; then A4: P `1_3 = 0. (GF p) by MCART_1:def_5; A5: P `3_3 = 0. (GF p) by A3, MCART_1:def_7; A6: (P `1_3) |^ 3 = (P `1_3) |^ (2 + 1) .= ((P `1_3) |^ 2) * (P `1_3) by Th24 .= 0. (GF p) by A4, VECTSP_1:12 ; A7: (P `3_3) |^ 3 = (P `3_3) |^ (2 + 1) .= ((P `3_3) |^ 2) * (P `3_3) by Th24 .= 0. (GF p) by A5, VECTSP_1:12 ; A8: (P `3_3) |^ 2 = (P `3_3) |^ (1 + 1) .= ((P `3_3) |^ 1) * (P `3_3) by Th24 .= 0. (GF p) by A5, VECTSP_1:12 ; (EC_WEqProjCo (a,b,p)) . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by Def8 .= (0. (GF p)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A5, VECTSP_1:12 .= - (((0. (GF p)) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A6, RLVECT_1:4 .= - (((a * (P `1_3)) * ((P `3_3) |^ 2)) + (b * ((P `3_3) |^ 3))) by RLVECT_1:4 .= - ((0. (GF p)) + (b * ((P `3_3) |^ 3))) by A8, VECTSP_1:12 .= - (b * ((P `3_3) |^ 3)) by RLVECT_1:4 .= - (0. (GF p)) by A7, VECTSP_1:12 .= (0. (GF p)) - (0. (GF p)) by RLVECT_1:4 ; hence (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) by VECTSP_1:19; ::_thesis: verum end; definition let p be Prime; let a, b be Element of (GF p); func EC_SetProjCo (a,b,p) -> non empty Subset of (ProjCo (GF p)) equals :: EC_PF_1:def 9 { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; correctness coherence { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p)); proof A1: now__::_thesis:_for_x_being_set_st_x_in__{__P_where_P_is_Element_of_ProjCo_(GF_p)_:_(EC_WEqProjCo_(a,b,p))_._P_=_0._(GF_p)__}__holds_ x_in_ProjCo_(GF_p) let x be set ; ::_thesis: ( x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } implies x in ProjCo (GF p) ) assume x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; ::_thesis: x in ProjCo (GF p) then ex P being Element of ProjCo (GF p) st ( x = P & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ; hence x in ProjCo (GF p) ; ::_thesis: verum end; reconsider D0 = [0,1,0] as Element of ProjCo (GF p) by Lm6; (EC_WEqProjCo (a,b,p)) . D0 = 0. (GF p) by Lm6; then D0 in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; hence { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p)) by A1, TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines EC_SetProjCo EC_PF_1:def_9_:_ for p being Prime for a, b being Element of (GF p) holds EC_SetProjCo (a,b,p) = { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; Lm7: for p being Prime for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p) proof let p be Prime; ::_thesis: for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p) let d, Y be Element of (GF p); ::_thesis: [d,Y,1] is Element of ProjCo (GF p) set P = [d,Y,1]; [d,Y,1] <> [0,0,0] by XTUPLE_0:3; then A1: not [d,Y,1] in {[0,0,0]} by TARSKI:def_1; 1. (GF p) in the carrier of (GF p) ; then 1 in the carrier of (GF p) by Th12; then [d,Y,1] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] by MCART_1:69; then [d,Y,1] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by A1, XBOOLE_0:def_5; hence [d,Y,1] is Element of ProjCo (GF p) by Th40; ::_thesis: verum end; theorem Th42: :: EC_PF_1:42 for p being Prime for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p) let a, b be Element of (GF p); ::_thesis: [0,1,0] is Element of EC_SetProjCo (a,b,p) ( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) by Lm6; then [0,1,0] in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; hence [0,1,0] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: verum end; theorem Th43: :: EC_PF_1:43 for p being Prime for a, b, X, Y being Element of (GF p) holds ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) ) proof let p be Prime; ::_thesis: for a, b, X, Y being Element of (GF p) holds ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) ) let a, b, X, Y be Element of (GF p); ::_thesis: ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) ) A1: 1 = 1. (GF p) by Th12; reconsider Q = [X,Y,1] as Element of ProjCo (GF p) by Lm7; A2: Y |^ 2 = (Y |^ 2) * (1. (GF p)) by VECTSP_1:def_6; A3: a * X = (a * X) * (1. (GF p)) by VECTSP_1:def_6 .= (a * X) * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def_6 .= (a * X) * ((1. (GF p)) |^ 2) by Lm3 ; A4: b = b * (1. (GF p)) by VECTSP_1:def_6 .= b * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def_6 .= b * ((1. (GF p)) |^ 2) by Lm3 .= b * (((1. (GF p)) |^ 2) * (1. (GF p))) by VECTSP_1:def_6 .= b * ((1. (GF p)) |^ (2 + 1)) by Th24 .= b * ((1. (GF p)) |^ 3) ; hereby ::_thesis: ( [X,Y,1] is Element of EC_SetProjCo (a,b,p) implies Y |^ 2 = ((X |^ 3) + (a * X)) + b ) assume A5: Y |^ 2 = ((X |^ 3) + (a * X)) + b ; ::_thesis: [X,Y,1] is Element of EC_SetProjCo (a,b,p) (Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A5, VECTSP_1:19; then (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) by A1, A2, A3, A4, Th41; then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; hence [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: verum end; assume [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; ::_thesis: Y |^ 2 = ((X |^ 3) + (a * X)) + b then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; then ex P being Element of ProjCo (GF p) st ( P = Q & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ; then (Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A1, A2, A3, A4, Th41; hence Y |^ 2 = ((X |^ 3) + (a * X)) + b by VECTSP_1:19; ::_thesis: verum end; definition let p be Prime; let P, Q be Element of ProjCo (GF p); predP _EQ_ Q means :Def10: :: EC_PF_1:def 10 ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ); reflexivity for P being Element of ProjCo (GF p) ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) ) proof for R being Element of ProjCo (GF p) ex a being Element of (GF p) st ( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) proof let R be Element of ProjCo (GF p); ::_thesis: ex a being Element of (GF p) st ( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) reconsider a = 1. (GF p) as Element of (GF p) ; ( R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) by VECTSP_1:def_6; hence ex a being Element of (GF p) st ( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) ; ::_thesis: verum end; hence for P being Element of ProjCo (GF p) ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) ) ; ::_thesis: verum end; symmetry for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds ex a being Element of (GF p) st ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) proof thus for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds ex b being Element of (GF p) st ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) ::_thesis: verum proof let P, Q be Element of ProjCo (GF p); ::_thesis: ( ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) implies ex b being Element of (GF p) st ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) ) given a being Element of (GF p) such that A1: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ; ::_thesis: ex b being Element of (GF p) st ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) take b = a " ; ::_thesis: ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) A2: b <> 0. (GF p) proof assume b = 0. (GF p) ; ::_thesis: contradiction then b * a = 0. (GF p) by VECTSP_1:7; then 1. (GF p) = 0. (GF p) by A1, VECTSP_1:def_10; hence contradiction ; ::_thesis: verum end; A3: Q `1_3 = (1. (GF p)) * (Q `1_3) by VECTSP_1:def_6 .= (b * a) * (Q `1_3) by A1, VECTSP_1:def_10 .= b * (P `1_3) by A1, GROUP_1:def_3 ; A4: Q `2_3 = (1. (GF p)) * (Q `2_3) by VECTSP_1:def_6 .= (b * a) * (Q `2_3) by A1, VECTSP_1:def_10 .= b * (P `2_3) by A1, GROUP_1:def_3 ; Q `3_3 = (1. (GF p)) * (Q `3_3) by VECTSP_1:def_6 .= (b * a) * (Q `3_3) by A1, VECTSP_1:def_10 .= b * (P `3_3) by A1, GROUP_1:def_3 ; hence ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) by A2, A3, A4; ::_thesis: verum end; end; end; :: deftheorem Def10 defines _EQ_ EC_PF_1:def_10_:_ for p being Prime for P, Q being Element of ProjCo (GF p) holds ( P _EQ_ Q iff ex a being Element of (GF p) st ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ); theorem Th44: :: EC_PF_1:44 for p being Prime for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds P _EQ_ R proof let p be Prime; ::_thesis: for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds P _EQ_ R let P, Q, R be Element of ProjCo (GF p); ::_thesis: ( P _EQ_ Q & Q _EQ_ R implies P _EQ_ R ) assume A1: ( P _EQ_ Q & Q _EQ_ R ) ; ::_thesis: P _EQ_ R then consider a being Element of (GF p) such that A2: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) by Def10; consider b being Element of (GF p) such that A3: ( b <> 0. (GF p) & Q `1_3 = b * (R `1_3) & Q `2_3 = b * (R `2_3) & Q `3_3 = b * (R `3_3) ) by Def10, A1; take d = a * b; :: according to EC_PF_1:def_10 ::_thesis: ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) ) thus ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) ) by A2, A3, GROUP_1:def_3, VECTSP_1:12; ::_thesis: verum end; theorem Th45: :: EC_PF_1:45 for p being Prime for a, b being Element of (GF p) for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds Q in EC_SetProjCo (a,b,p) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds Q in EC_SetProjCo (a,b,p) let a, b be Element of (GF p); ::_thesis: for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds Q in EC_SetProjCo (a,b,p) let P, Q be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; ::_thesis: for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds Q in EC_SetProjCo (a,b,p) let d be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) implies Q in EC_SetProjCo (a,b,p) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) ) ; ::_thesis: Q in EC_SetProjCo (a,b,p) set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; consider PP being Element of ProjCo (GF p) such that A2: ( P = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) by A1; A3: (EC_WEqProjCo (a,b,p)) . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by Def8; A4: (EC_WEqProjCo (a,b,p)) . Q = (((d * (P `2_3)) |^ 2) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by A1, Def8 .= (((d |^ 2) * ((P `2_3) |^ 2)) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9 .= ((((d |^ 2) * ((P `2_3) |^ 2)) * d) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= ((((d |^ 2) * d) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= (((d |^ (2 + 1)) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by Th24 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d |^ 2) * ((P `3_3) |^ 2)))) + (b * ((d * (P `3_3)) |^ 3))) by BINOM:9 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((a * (d * (P `1_3))) * (d |^ 2)) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d * (P `1_3)) * (d |^ 2))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (((d |^ 2) * d) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d |^ (2 + 1)) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by Th24 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3))) by GROUP_1:def_3 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d |^ 3) * ((P `3_3) |^ 3)))) by BINOM:9 .= (((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3 .= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3 .= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + (((d |^ 3) * b) * ((P `3_3) |^ 3))) by GROUP_1:def_3 .= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3)))) by GROUP_1:def_3 .= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - (((d |^ 3) * (((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3)))) by VECTSP_1:4 .= ((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((d |^ 3) * ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))) by VECTSP_1:4 .= (d |^ 3) * ((((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))) by VECTSP_1:11 .= 0. (GF p) by A2, A3, VECTSP_1:12 ; PP in ProjCo (GF p) ; then PP in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by Th40; then A5: not P in {[0,0,0]} by A2, XBOOLE_0:def_5; A6: Q = [(Q `1_3),(Q `2_3),(Q `3_3)] by MCART_1:44; ( P `1_3 <> 0 or P `2_3 <> 0 or P `3_3 <> 0 ) proof assume ( not P `1_3 <> 0 & not P `2_3 <> 0 & not P `3_3 <> 0 ) ; ::_thesis: contradiction then P = [0,0,0] by MCART_1:44; hence contradiction by A5, TARSKI:def_1; ::_thesis: verum end; then ( P `1_3 <> 0. (GF p) or P `2_3 <> 0. (GF p) or P `3_3 <> 0. (GF p) ) by Th11; then ( d * (P `1_3) <> 0. (GF p) or d * (P `2_3) <> 0. (GF p) or d * (P `3_3) <> 0. (GF p) ) by A1, VECTSP_1:12; then ( Q `1_3 <> 0 or Q `2_3 <> 0 or Q `3_3 <> 0 ) by A1, Th11; then [(Q `1_3),(Q `2_3),(Q `3_3)] <> [0,0,0] by XTUPLE_0:3; then not Q in {[0,0,0]} by A6, TARSKI:def_1; then Q in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by XBOOLE_0:def_5; then Q in ProjCo (GF p) by Th40; hence Q in EC_SetProjCo (a,b,p) by A4; ::_thesis: verum end; definition let p be Prime; func R_ProjCo p -> Relation of (ProjCo (GF p)) equals :: EC_PF_1:def 11 { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; correctness coherence { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p)); proof set RX = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; now__::_thesis:_for_x_being_set_st_x_in__{__[P,Q]_where_P,_Q_is_Element_of_ProjCo_(GF_p)_:_P__EQ__Q__}__holds_ x_in_[:(ProjCo_(GF_p)),(ProjCo_(GF_p)):] let x be set ; ::_thesis: ( x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } implies x in [:(ProjCo (GF p)),(ProjCo (GF p)):] ) assume x in { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; ::_thesis: x in [:(ProjCo (GF p)),(ProjCo (GF p)):] then consider P, Q being Element of ProjCo (GF p) such that A1: ( x = [P,Q] & P _EQ_ Q ) ; thus x in [:(ProjCo (GF p)),(ProjCo (GF p)):] by A1; ::_thesis: verum end; hence { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } is Relation of (ProjCo (GF p)) by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines R_ProjCo EC_PF_1:def_11_:_ for p being Prime holds R_ProjCo p = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ; theorem Th46: :: EC_PF_1:46 for p being Prime for P, Q being Element of ProjCo (GF p) holds ( P _EQ_ Q iff [P,Q] in R_ProjCo p ) proof let p be Prime; ::_thesis: for P, Q being Element of ProjCo (GF p) holds ( P _EQ_ Q iff [P,Q] in R_ProjCo p ) let P, Q be Element of ProjCo (GF p); ::_thesis: ( P _EQ_ Q iff [P,Q] in R_ProjCo p ) thus ( P _EQ_ Q implies [P,Q] in R_ProjCo p ) ; ::_thesis: ( [P,Q] in R_ProjCo p implies P _EQ_ Q ) assume [P,Q] in R_ProjCo p ; ::_thesis: P _EQ_ Q then consider X0, Y0 being Element of ProjCo (GF p) such that A1: ( [P,Q] = [X0,Y0] & X0 _EQ_ Y0 ) ; ( P = X0 & Q = Y0 ) by A1, XTUPLE_0:1; hence P _EQ_ Q by A1; ::_thesis: verum end; registration let p be Prime; cluster R_ProjCo p -> total symmetric transitive ; coherence ( R_ProjCo p is total & R_ProjCo p is symmetric & R_ProjCo p is transitive ) proof set R = R_ProjCo p; for x being set holds ( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p ) proof let x be set ; ::_thesis: ( x in ProjCo (GF p) iff ex y being set st [x,y] in R_ProjCo p ) hereby ::_thesis: ( ex y being set st [x,y] in R_ProjCo p implies x in ProjCo (GF p) ) assume x in ProjCo (GF p) ; ::_thesis: ex y being set st [x,y] in R_ProjCo p then reconsider X = x as Element of ProjCo (GF p) ; X _EQ_ X ; then [x,x] in R_ProjCo p ; hence ex y being set st [x,y] in R_ProjCo p ; ::_thesis: verum end; given y being set such that A1: [x,y] in R_ProjCo p ; ::_thesis: x in ProjCo (GF p) consider X, Y being Element of ProjCo (GF p) such that A2: ( [x,y] = [X,Y] & X _EQ_ Y ) by A1; x = X by A2, XTUPLE_0:1; hence x in ProjCo (GF p) ; ::_thesis: verum end; then dom (R_ProjCo p) = ProjCo (GF p) by XTUPLE_0:def_12; hence R_ProjCo p is total by PARTFUN1:def_2; ::_thesis: ( R_ProjCo p is symmetric & R_ProjCo p is transitive ) for x, y being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p holds [y,x] in R_ProjCo p proof let x, y be set ; ::_thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p implies [y,x] in R_ProjCo p ) assume ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & [x,y] in R_ProjCo p ) ; ::_thesis: [y,x] in R_ProjCo p then consider X, Y being Element of ProjCo (GF p) such that A3: ( [x,y] = [X,Y] & X _EQ_ Y ) ; ( x = X & y = Y ) by A3, XTUPLE_0:1; hence [y,x] in R_ProjCo p by A3; ::_thesis: verum end; then R_ProjCo p is_symmetric_in field (R_ProjCo p) by RELAT_2:def_3; hence R_ProjCo p is symmetric by RELAT_2:def_11; ::_thesis: R_ProjCo p is transitive for x, y, z being set st x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p holds [x,z] in R_ProjCo p proof let x, y, z be set ; ::_thesis: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p implies [x,z] in R_ProjCo p ) assume A4: ( x in field (R_ProjCo p) & y in field (R_ProjCo p) & z in field (R_ProjCo p) & [x,y] in R_ProjCo p & [y,z] in R_ProjCo p ) ; ::_thesis: [x,z] in R_ProjCo p then consider X, Y being Element of ProjCo (GF p) such that A5: ( [x,y] = [X,Y] & X _EQ_ Y ) ; A6: ( x = X & y = Y ) by A5, XTUPLE_0:1; consider Y1, Z being Element of ProjCo (GF p) such that A7: ( [y,z] = [Y1,Z] & Y1 _EQ_ Z ) by A4; ( X _EQ_ Y & Y _EQ_ Z ) by A5, A6, A7, XTUPLE_0:1; then A8: X _EQ_ Z by Th44; [x,z] = [X,Z] by A6, A7, XTUPLE_0:1; hence [x,z] in R_ProjCo p by A8; ::_thesis: verum end; then R_ProjCo p is_transitive_in field (R_ProjCo p) by RELAT_2:def_8; hence R_ProjCo p is transitive by RELAT_2:def_16; ::_thesis: verum end; end; definition let p be Prime; let a, b be Element of (GF p); func R_EllCur (a,b,p) -> Equivalence_Relation of (EC_SetProjCo (a,b,p)) equals :: EC_PF_1:def 12 (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))); correctness coherence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)); proof set P = R_ProjCo p; set R = nabla (EC_SetProjCo (a,b,p)); reconsider PR = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) as Relation of (EC_SetProjCo (a,b,p)) ; for x being set holds ( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR ) proof let x be set ; ::_thesis: ( x in EC_SetProjCo (a,b,p) iff ex y being set st [x,y] in PR ) hereby ::_thesis: ( ex y being set st [x,y] in PR implies x in EC_SetProjCo (a,b,p) ) assume A1: x in EC_SetProjCo (a,b,p) ; ::_thesis: ex y being set st [x,y] in PR then reconsider X = x as Element of ProjCo (GF p) ; X _EQ_ X ; then A2: [x,x] in R_ProjCo p ; [x,x] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87; then [x,x] in PR by A2, XBOOLE_0:def_4; hence ex y being set st [x,y] in PR ; ::_thesis: verum end; thus ( ex y being set st [x,y] in PR implies x in EC_SetProjCo (a,b,p) ) by ZFMISC_1:87; ::_thesis: verum end; then dom PR = EC_SetProjCo (a,b,p) by XTUPLE_0:def_12; hence (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))) is Equivalence_Relation of (EC_SetProjCo (a,b,p)) by PARTFUN1:def_2; ::_thesis: verum end; end; :: deftheorem defines R_EllCur EC_PF_1:def_12_:_ for p being Prime for a, b being Element of (GF p) holds R_EllCur (a,b,p) = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p))); theorem Th47: :: EC_PF_1:47 for p being Prime for a, b being Element of (GF p) for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) let a, b be Element of (GF p); ::_thesis: for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) let P, Q be Element of ProjCo (GF p); ::_thesis: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) implies ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) ) assume A1: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) ) ; ::_thesis: ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) hereby ::_thesis: ( [P,Q] in R_EllCur (a,b,p) implies P _EQ_ Q ) assume P _EQ_ Q ; ::_thesis: [P,Q] in R_EllCur (a,b,p) then A2: [P,Q] in R_ProjCo p ; [P,Q] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87; hence [P,Q] in R_EllCur (a,b,p) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume [P,Q] in R_EllCur (a,b,p) ; ::_thesis: P _EQ_ Q then [P,Q] in R_ProjCo p by XBOOLE_0:def_4; hence P _EQ_ Q by Th46; ::_thesis: verum end; theorem Th48: :: EC_PF_1:48 for p being Prime for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) let a, b be Element of (GF p); ::_thesis: for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) let P be Element of ProjCo (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 implies ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 ) ; ::_thesis: ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) set d = (P `3_3) " ; A2: P `3_3 <> 0. (GF p) by A1, Th11; A3: (P `3_3) " <> 0. (GF p) proof assume A4: (P `3_3) " = 0. (GF p) ; ::_thesis: contradiction A5: ((P `3_3) ") * (P `3_3) = 1_ (GF p) by A2, VECTSP_1:def_10 .= 1 by Th12 ; ((P `3_3) ") * (P `3_3) = 0. (GF p) by A4, VECTSP_1:12 .= 0 by Th11 ; hence contradiction by A5; ::_thesis: verum end; reconsider Q = [(((P `3_3) ") * (P `1_3)),(((P `3_3) ") * (P `2_3)),(((P `3_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ; A6: ( Q `1_3 = ((P `3_3) ") * (P `1_3) & Q `2_3 = ((P `3_3) ") * (P `2_3) & Q `3_3 = ((P `3_3) ") * (P `3_3) ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7; then Q in EC_SetProjCo (a,b,p) by A1, A3, Th45; then consider PP being Element of ProjCo (GF p) such that A7: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ; reconsider Q = Q as Element of ProjCo (GF p) by A7; take Q ; ::_thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 ) thus Q in EC_SetProjCo (a,b,p) by A6, A1, A3, Th45; ::_thesis: ( Q _EQ_ P & Q `3_3 = 1 ) thus Q _EQ_ P by A6, A3, Def10; ::_thesis: Q `3_3 = 1 thus Q `3_3 = ((P `3_3) ") * (P `3_3) by MCART_1:def_7 .= 1_ (GF p) by A2, VECTSP_1:def_10 .= 1 by Th12 ; ::_thesis: verum end; theorem Th49: :: EC_PF_1:49 for p being Prime for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) let a, b be Element of (GF p); ::_thesis: for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) let P be Element of ProjCo (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 implies ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 ) ; ::_thesis: ex Q being Element of ProjCo (GF p) st ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) A2: P `3_3 = 0. (GF p) by A1, Th11; set d = (P `2_3) " ; A3: ex X0 being Element of ProjCo (GF p) st ( P = X0 & (EC_WEqProjCo (a,b,p)) . X0 = 0. (GF p) ) by A1; A4: (P `3_3) |^ 3 = (P `3_3) |^ (2 + 1) .= ((P `3_3) |^ 2) * (P `3_3) by Th24 .= 0. (GF p) by A2, VECTSP_1:12 ; A5: (P `3_3) |^ 2 = (P `3_3) |^ (1 + 1) .= ((P `3_3) |^ 1) * (P `3_3) by Th24 .= 0. (GF p) by A2, VECTSP_1:12 ; 0. (GF p) = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A3, Def8 .= (0. (GF p)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) by A2, VECTSP_1:12 .= (0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (b * ((P `3_3) |^ 3))) by A5, VECTSP_1:12 .= (0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (0. (GF p))) by A4, VECTSP_1:12 .= (0. (GF p)) - (((P `1_3) |^ 3) + (0. (GF p))) by RLVECT_1:4 .= (0. (GF p)) - ((P `1_3) |^ 3) by RLVECT_1:4 .= - ((P `1_3) |^ 3) by RLVECT_1:14 ; then A6: (P `1_3) |^ 3 = ((P `1_3) |^ 3) + (- ((P `1_3) |^ 3)) by RLVECT_1:4; A7: P `1_3 = 0. (GF p) proof assume A8: P `1_3 <> 0. (GF p) ; ::_thesis: contradiction then (P `1_3) * (P `1_3) <> 0. (GF p) by VECTSP_1:12; then ((P `1_3) |^ 1) * (P `1_3) <> 0. (GF p) by Lm2; then (P `1_3) |^ (1 + 1) <> 0. (GF p) by Th24; then ((P `1_3) |^ 2) * (P `1_3) <> 0. (GF p) by A8, VECTSP_1:12; then (P `1_3) |^ (2 + 1) <> 0. (GF p) by Th24; hence contradiction by A6, RLVECT_1:5; ::_thesis: verum end; A9: P `2_3 <> 0. (GF p) proof assume P `2_3 = 0. (GF p) ; ::_thesis: contradiction then P `2_3 = 0 by Th11; then [(P `1_3),(P `2_3),(P `3_3)] = [0,0,0] by A1, A7, Th11; then P = [0,0,0] by MCART_1:44; then P in {[0,0,0]} by TARSKI:def_1; then not P in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by XBOOLE_0:def_5; then not P in ProjCo (GF p) by Th40; hence contradiction ; ::_thesis: verum end; A10: (P `2_3) " <> 0. (GF p) proof assume A11: (P `2_3) " = 0. (GF p) ; ::_thesis: contradiction A12: ((P `2_3) ") * (P `2_3) = 1_ (GF p) by A9, VECTSP_1:def_10 .= 1 by Th12 ; ((P `2_3) ") * (P `2_3) = 0. (GF p) by A11, VECTSP_1:12 .= 0 by Th11 ; hence contradiction by A12; ::_thesis: verum end; reconsider Q = [(((P `2_3) ") * (P `1_3)),(((P `2_3) ") * (P `2_3)),(((P `2_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ; A13: ( Q `1_3 = ((P `2_3) ") * (P `1_3) & Q `2_3 = ((P `2_3) ") * (P `2_3) & Q `3_3 = ((P `2_3) ") * (P `3_3) ) by MCART_1:def_5, MCART_1:def_6, MCART_1:def_7; then Q in EC_SetProjCo (a,b,p) by A1, A10, Th45; then consider PP being Element of ProjCo (GF p) such that A14: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ; reconsider Q = Q as Element of ProjCo (GF p) by A14; take Q ; ::_thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) thus Q in EC_SetProjCo (a,b,p) by A13, A1, A10, Th45; ::_thesis: ( Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) thus Q _EQ_ P by A13, A10, Def10; ::_thesis: ( Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) thus Q `1_3 = ((P `2_3) ") * (P `1_3) by MCART_1:def_5 .= 0. (GF p) by A7, VECTSP_1:12 .= 0 by Th11 ; ::_thesis: ( Q `2_3 = 1 & Q `3_3 = 0 ) thus Q `2_3 = ((P `2_3) ") * (P `2_3) by MCART_1:def_6 .= 1_ (GF p) by A9, VECTSP_1:def_10 .= 1 by Th12 ; ::_thesis: Q `3_3 = 0 thus Q `3_3 = ((P `2_3) ") * (P `3_3) by MCART_1:def_7 .= 0. (GF p) by A2, VECTSP_1:12 .= 0 by Th11 ; ::_thesis: verum end; theorem Th50: :: EC_PF_1:50 for p being Prime for a, b being Element of (GF p) for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds ( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds ( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) let a, b be Element of (GF p); ::_thesis: for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds ( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) let x be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds ( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) implies ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) ) ; ::_thesis: ( ex P being Element of ProjCo (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) then consider y0 being Element of EC_SetProjCo (a,b,p) such that A2: x = Class ((R_EllCur (a,b,p)),y0) by EQREL_1:36; reconsider w = y0 as Element of ProjCo (GF p) ; percases ( w `3_3 = 0 or w `3_3 <> 0 ) ; suppose w `3_3 = 0 ; ::_thesis: ( ex P being Element of ProjCo (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) then consider y being Element of ProjCo (GF p) such that A3: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `1_3 = 0 & y `2_3 = 1 & y `3_3 = 0 ) by A1, Th49; [y,w] in R_EllCur (a,b,p) by A1, Th47, A3; then x = Class ((R_EllCur (a,b,p)),y) by A2, A3, EQREL_1:35; hence ( ex P being Element of ProjCo (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A3, MCART_1:44; ::_thesis: verum end; suppose w `3_3 <> 0 ; ::_thesis: ( ex P being Element of ProjCo (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) then consider y being Element of ProjCo (GF p) such that A4: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `3_3 = 1 ) by A1, Th48; set e = y `1_3 ; set f = y `2_3 ; A5: y = [(y `1_3),(y `2_3),1] by A4, MCART_1:44; [y,w] in R_EllCur (a,b,p) by A1, Th47, A4; then x = Class ((R_EllCur (a,b,p)),y) by A2, A4, EQREL_1:35; hence ( ex P being Element of ProjCo (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st ( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A5, A4; ::_thesis: verum end; end; end; theorem Th51: :: EC_PF_1:51 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } proof let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } set A = Class (R_EllCur (a,b,p)); set B = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; reconsider d0 = [0,1,0] as Element of EC_SetProjCo (a,b,p) by Th42; for x being set holds ( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) proof let x be set ; ::_thesis: ( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) hereby ::_thesis: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in Class (R_EllCur (a,b,p)) ) assume x in Class (R_EllCur (a,b,p)) ; ::_thesis: x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } then ( ex y being Element of ProjCo (GF p) st ( y in EC_SetProjCo (a,b,p) & y = [0,1,0] & x = Class ((R_EllCur (a,b,p)),y) ) or ex y being Element of ProjCo (GF p) ex e, f being Element of (GF p) st ( y in EC_SetProjCo (a,b,p) & y = [e,f,1] & x = Class ((R_EllCur (a,b,p)),y) ) ) by A1, Th50; then ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by TARSKI:def_1; hence x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by XBOOLE_0:def_3; ::_thesis: verum end; assume x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; ::_thesis: x in Class (R_EllCur (a,b,p)) then A2: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by XBOOLE_0:def_3; now__::_thesis:_x_in_Class_(R_EllCur_(a,b,p)) percases ( x = Class ((R_EllCur (a,b,p)),[0,1,0]) or ex y being Element of ProjCo (GF p) st ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ) by A2, TARSKI:def_1; supposeA3: x = Class ((R_EllCur (a,b,p)),[0,1,0]) ; ::_thesis: x in Class (R_EllCur (a,b,p)) EqClass ((R_EllCur (a,b,p)),d0) is Element of Class (R_EllCur (a,b,p)) ; hence x in Class (R_EllCur (a,b,p)) by A3; ::_thesis: verum end; suppose ex y being Element of ProjCo (GF p) st ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ; ::_thesis: x in Class (R_EllCur (a,b,p)) then consider y being Element of ProjCo (GF p) such that A4: ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ; reconsider y = y as Element of EC_SetProjCo (a,b,p) by A4; EqClass ((R_EllCur (a,b,p)),y) is Element of Class (R_EllCur (a,b,p)) ; hence x in Class (R_EllCur (a,b,p)) by A4; ::_thesis: verum end; end; end; hence x in Class (R_EllCur (a,b,p)) ; ::_thesis: verum end; hence Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:1; ::_thesis: verum end; theorem Th52: :: EC_PF_1:52 for p being Prime for a, b, d1, Y1, d2, Y2 being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) holds ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) proof let p be Prime; ::_thesis: for a, b, d1, Y1, d2, Y2 being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) holds ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) let a, b, d1, Y1, d2, Y2 be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) implies ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & [d1,Y1,1] in EC_SetProjCo (a,b,p) & [d2,Y2,1] in EC_SetProjCo (a,b,p) ) ; ::_thesis: ( Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) iff ( d1 = d2 & Y1 = Y2 ) ) hereby ::_thesis: ( d1 = d2 & Y1 = Y2 implies Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) ) assume Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) ; ::_thesis: ( d2 = d1 & Y2 = Y1 ) then [d2,Y2,1] in Class ((R_EllCur (a,b,p)),[d1,Y1,1]) by A1, EQREL_1:23; then A2: [[d1,Y1,1],[d2,Y2,1]] in R_EllCur (a,b,p) by EQREL_1:18; reconsider P = [d1,Y1,1], Q = [d2,Y2,1] as Element of ProjCo (GF p) by A1; P _EQ_ Q by Th47, A1, A2; then consider a being Element of (GF p) such that A3: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10; A4: p > 1 by INT_2:def_4; A5: 1. (GF p) = 1 by A4, INT_3:14 .= P `3_3 by MCART_1:def_7 ; A6: 1. (GF p) = 1 by A4, INT_3:14 .= a * (P `3_3) by A3, MCART_1:def_7 .= a by A5, VECTSP_1:def_8 ; thus d2 = a * (P `1_3) by A3, MCART_1:def_5 .= P `1_3 by A6, VECTSP_1:def_8 .= d1 by MCART_1:def_5 ; ::_thesis: Y2 = Y1 thus Y2 = a * (P `2_3) by A3, MCART_1:def_6 .= P `2_3 by A6, VECTSP_1:def_8 .= Y1 by MCART_1:def_6 ; ::_thesis: verum end; assume ( d1 = d2 & Y1 = Y2 ) ; ::_thesis: Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) hence Class ((R_EllCur (a,b,p)),[d1,Y1,1]) = Class ((R_EllCur (a,b,p)),[d2,Y2,1]) ; ::_thesis: verum end; theorem Th53: :: EC_PF_1:53 for p being Prime for a, b being Element of (GF p) for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds F1 misses F2 proof let p be Prime; ::_thesis: for a, b being Element of (GF p) for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds F1 misses F2 let a, b be Element of (GF p); ::_thesis: for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } holds F1 misses F2 let F1, F2 be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies F1 misses F2 ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) ; ::_thesis: F1 misses F2 assume F1 meets F2 ; ::_thesis: contradiction then F1 /\ F2 <> {} by XBOOLE_0:def_7; then consider z being set such that A2: z in F1 /\ F2 by XBOOLE_0:def_1; A3: ( z in F1 & z in F2 ) by A2, XBOOLE_0:def_4; consider P being Element of ProjCo (GF p) such that A4: ( z = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) by A1, A3; consider X1, Y1 being Element of (GF p) such that A5: P = [X1,Y1,1] by A4; A6: z = Class ((R_EllCur (a,b,p)),[0,1,0]) by A1, A3, TARSKI:def_1; reconsider Q = [0,1,0] as Element of ProjCo (GF p) by Lm6; A7: Q is Element of EC_SetProjCo (a,b,p) by Th42; Q in Class ((R_EllCur (a,b,p)),P) by A4, A6, EQREL_1:23; then [P,Q] in R_EllCur (a,b,p) by EQREL_1:18; then P _EQ_ Q by Th47, A1, A7, A4; then consider a being Element of (GF p) such that A8: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10; A9: p > 1 by INT_2:def_4; A10: 1. (GF p) = 1 by A9, INT_3:14 .= P `3_3 by A5, MCART_1:def_7 ; 0. (GF p) = 0 by Th11 .= a * (P `3_3) by A8, MCART_1:def_7 .= a by A10, VECTSP_1:def_8 ; hence contradiction by A8; ::_thesis: verum end; theorem Th54: :: EC_PF_1:54 for X being non empty finite set for R being Equivalence_Relation of X for S being Class b2 -valued Function for i being set st i in dom S holds S . i is finite Subset of X proof let X be non empty finite set ; ::_thesis: for R being Equivalence_Relation of X for S being Class b1 -valued Function for i being set st i in dom S holds S . i is finite Subset of X let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function for i being set st i in dom S holds S . i is finite Subset of X let S be Class R -valued Function; ::_thesis: for i being set st i in dom S holds S . i is finite Subset of X let i be set ; ::_thesis: ( i in dom S implies S . i is finite Subset of X ) assume i in dom S ; ::_thesis: S . i is finite Subset of X then S . i in Class R by FUNCT_1:102; hence S . i is finite Subset of X ; ::_thesis: verum end; theorem Th55: :: EC_PF_1:55 for X being non empty set for R being Equivalence_Relation of X for S being Class b2 -valued Function st S is one-to-one holds S is disjoint_valued proof let X be non empty set ; ::_thesis: for R being Equivalence_Relation of X for S being Class b1 -valued Function st S is one-to-one holds S is disjoint_valued let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function st S is one-to-one holds S is disjoint_valued let S be Class R -valued Function; ::_thesis: ( S is one-to-one implies S is disjoint_valued ) assume A1: S is one-to-one ; ::_thesis: S is disjoint_valued now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_ S_._x_misses_S_._y let x, y be set ; ::_thesis: ( x <> y implies S . b1 misses S . b2 ) assume A2: x <> y ; ::_thesis: S . b1 misses S . b2 percases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ; supposeA3: ( x in dom S & y in dom S ) ; ::_thesis: S . b1 misses S . b2 then A4: S . x <> S . y by A1, A2, FUNCT_1:def_4; ( S . x in Class R & S . y in Class R ) by A3, FUNCT_1:102; hence S . x misses S . y by A4, EQREL_1:def_4; ::_thesis: verum end; suppose ( not x in dom S or not y in dom S ) ; ::_thesis: S . b1 misses S . b2 then ( S . x = {} or S . y = {} ) by FUNCT_1:def_2; hence S . x misses S . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence S is disjoint_valued by PROB_2:def_2; ::_thesis: verum end; theorem Th56: :: EC_PF_1:56 for X being non empty set for R being Equivalence_Relation of X for S being Class b2 -valued Function st S is onto holds Union S = X proof let X be non empty set ; ::_thesis: for R being Equivalence_Relation of X for S being Class b1 -valued Function st S is onto holds Union S = X let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function st S is onto holds Union S = X let S be Class R -valued Function; ::_thesis: ( S is onto implies Union S = X ) assume A1: S is onto ; ::_thesis: Union S = X union (Class R) = X by EQREL_1:def_4; hence Union S = X by A1, FUNCT_2:def_3; ::_thesis: verum end; theorem :: EC_PF_1:57 for X being non empty finite set for R being Equivalence_Relation of X for S being Class b2 -valued Function for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) holds card X = Sum L proof let X be non empty finite set ; ::_thesis: for R being Equivalence_Relation of X for S being Class b1 -valued Function for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) holds card X = Sum L let R be Equivalence_Relation of X; ::_thesis: for S being Class R -valued Function for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) holds card X = Sum L let S be Class R -valued Function; ::_thesis: for L being FinSequence of NAT st S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) holds card X = Sum L let L be FinSequence of NAT ; ::_thesis: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) implies card X = Sum L ) assume A1: ( S is one-to-one & S is onto & dom S = dom L & ( for i being Nat st i in dom S holds L . i = card (S . i) ) ) ; ::_thesis: card X = Sum L A2: S is disjoint_valued by A1, Th55; A3: for i being Nat st i in dom S holds ( S . i is finite & L . i = card (S . i) ) by A1, Th54; Union S = X by Th56, A1; hence card X = Sum L by A1, A2, A3, DIST_1:17; ::_thesis: verum end; theorem Th58: :: EC_PF_1:58 for p being Prime for a, b, d being Element of (GF p) for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds ex I being Function of F,G st ( I is onto & I is one-to-one ) proof let p be Prime; ::_thesis: for a, b, d being Element of (GF p) for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds ex I being Function of F,G st ( I is onto & I is one-to-one ) let a, b, d be Element of (GF p); ::_thesis: for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds ex I being Function of F,G st ( I is onto & I is one-to-one ) let F, G be set ; ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } implies ex I being Function of F,G st ( I is onto & I is one-to-one ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,P,1])) where P is Element of (GF p) : [d,P,1] in EC_SetProjCo (a,b,p) } ) ; ::_thesis: ex I being Function of F,G st ( I is onto & I is one-to-one ) consider z being set such that A2: z in F by A1, XBOOLE_0:def_1; consider W being Element of (GF p) such that A3: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A2; [d,W,1] is Element of EC_SetProjCo (a,b,p) by A3, Th43; then A4: Class ((R_EllCur (a,b,p)),[d,W,1]) in G by A1; deffunc H1( set ) -> Element of bool (EC_SetProjCo (a,b,p)) = Class ((R_EllCur (a,b,p)),[d,$1,1]); A5: for x being set st x in F holds H1(x) in G proof let x be set ; ::_thesis: ( x in F implies H1(x) in G ) assume x in F ; ::_thesis: H1(x) in G then consider Y being Element of (GF p) such that A6: ( x = Y & Y |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1; [d,Y,1] is Element of EC_SetProjCo (a,b,p) by A6, Th43; hence H1(x) in G by A1, A6; ::_thesis: verum end; consider I being Function of F,G such that A7: for x being set st x in F holds I . x = H1(x) from FUNCT_2:sch_2(A5); take I ; ::_thesis: ( I is onto & I is one-to-one ) now__::_thesis:_for_y_being_set_st_y_in_G_holds_ y_in_rng_I let y be set ; ::_thesis: ( y in G implies y in rng I ) assume y in G ; ::_thesis: y in rng I then consider P being Element of (GF p) such that A8: ( y = Class ((R_EllCur (a,b,p)),[d,P,1]) & [d,P,1] in EC_SetProjCo (a,b,p) ) by A1; P |^ 2 = ((d |^ 3) + (a * d)) + b by A8, Th43; then A9: P in F by A1; then y = I . P by A7, A8; hence y in rng I by A9, A4, FUNCT_2:112; ::_thesis: verum end; then G c= rng I by TARSKI:def_3; then G = rng I by XBOOLE_0:def_10; hence I is onto by FUNCT_2:def_3; ::_thesis: I is one-to-one now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_I_&_x2_in_dom_I_&_I_._x1_=_I_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 implies x1 = x2 ) assume A10: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 ) ; ::_thesis: x1 = x2 A11: ( x1 in F & x2 in F ) by A10; then consider Y1 being Element of (GF p) such that A12: ( x1 = Y1 & Y1 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1; consider Y2 being Element of (GF p) such that A13: ( x2 = Y2 & Y2 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A11; A14: I . x1 = Class ((R_EllCur (a,b,p)),[d,x1,1]) by A10, A7; A15: Class ((R_EllCur (a,b,p)),[d,x1,1]) = Class ((R_EllCur (a,b,p)),[d,x2,1]) by A10, A7, A14; A16: [d,Y2,1] is Element of EC_SetProjCo (a,b,p) by Th43, A13; [d,Y1,1] is Element of EC_SetProjCo (a,b,p) by Th43, A12; hence x1 = x2 by A1, A12, A13, A15, A16, Th52; ::_thesis: verum end; hence I is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; theorem Th59: :: EC_PF_1:59 for p being Prime for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) proof let p be Prime; ::_thesis: for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) let a, b, d be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) set F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ; set G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ; percases ( { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} or { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ) ; supposeA2: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) A3: { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = {} proof assume { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } <> {} ; ::_thesis: contradiction then consider z being set such that A4: z in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by XBOOLE_0:def_1; consider Y being Element of (GF p) such that A5: ( z = Class ((R_EllCur (a,b,p)),[d,Y,1]) & [d,Y,1] in EC_SetProjCo (a,b,p) ) by A4; Y |^ 2 = ((d |^ 3) + (a * d)) + b by A5, Th43; then Y in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ; hence contradiction by A2; ::_thesis: verum end; 2 < p by A1, XXREAL_0:2; hence card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by A3, A2, Th39; ::_thesis: verum end; supposeA6: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ; ::_thesis: card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) then consider z being set such that A7: z in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by XBOOLE_0:def_1; consider W being Element of (GF p) such that A8: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A7; [d,W,1] is Element of EC_SetProjCo (a,b,p) by A8, Th43; then A9: Class ((R_EllCur (a,b,p)),[d,W,1]) in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ; consider I being Function of { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } , { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } such that A10: ( I is onto & I is one-to-one ) by A1, A6, Th58; A11: dom I = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A9, FUNCT_2:def_1; A12: rng I = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A10, FUNCT_2:def_3; then A13: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } c= card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A10, A11, CARD_1:10; reconsider h = I " as Function of { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } , { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A10, A12, FUNCT_2:25; ( (I ") * I = id { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & I * (I ") = id { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ) by A10, A12, A9, FUNCT_2:29; then A14: ( h is onto & h is one-to-one ) by FUNCT_2:23; then A15: rng h = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by FUNCT_2:def_3; dom h = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A6, FUNCT_2:def_1; then card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } c= card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A14, A15, CARD_1:10; then A16: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A13, XBOOLE_0:def_10; 2 < p by A1, XXREAL_0:2; hence card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by A16, Th39; ::_thesis: verum end; end; end; Lm8: for p being Prime for n being Nat st n in Seg p holds n - 1 is Element of (GF p) proof let p be Prime; ::_thesis: for n being Nat st n in Seg p holds n - 1 is Element of (GF p) let n be Nat; ::_thesis: ( n in Seg p implies n - 1 is Element of (GF p) ) assume n in Seg p ; ::_thesis: n - 1 is Element of (GF p) then ( 1 <= n & n <= p ) by FINSEQ_1:1; then A1: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9; then A2: n - 1 is Element of NAT by INT_1:3; p - 1 < p - 0 by XREAL_1:15; then n - 1 < p by A1, XXREAL_0:2; hence n - 1 is Element of (GF p) by A2, NAT_1:44; ::_thesis: verum end; Lm9: for p being Prime for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex S being Function st ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) proof let p be Prime; ::_thesis: for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex S being Function st ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) let a, b, c, d be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex S being Function st ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex S being Function st ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) deffunc H1( Nat) -> set = { (Class ((R_EllCur (a,b,p)),[($1 - 1),Y,1])) where Y is Element of (GF p) : [($1 - 1),Y,1] in EC_SetProjCo (a,b,p) } ; consider S being FinSequence such that A2: ( len S = p & ( for i being Nat st i in dom S holds S . i = H1(i) ) ) from FINSEQ_1:sch_2(); take S ; ::_thesis: ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) thus A3: dom S = Seg p by A2, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) thus for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2; ::_thesis: ( S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_ S_._x_misses_S_._y let x, y be set ; ::_thesis: ( x <> y implies S . b1 misses S . b2 ) assume A4: x <> y ; ::_thesis: S . b1 misses S . b2 percases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ; supposeA5: ( x in dom S & y in dom S ) ; ::_thesis: S . b1 misses S . b2 then reconsider n = x, m = y as Nat ; ( x in Seg p & y in Seg p ) by A5, A2, FINSEQ_1:def_3; then A6: ( n - 1 is Element of (GF p) & m - 1 is Element of (GF p) ) by Lm8; A7: S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A5, A2; A8: S . m = { (Class ((R_EllCur (a,b,p)),[(m - 1),Y,1])) where Y is Element of (GF p) : [(m - 1),Y,1] in EC_SetProjCo (a,b,p) } by A5, A2; thus S . x misses S . y ::_thesis: verum proof assume S . x meets S . y ; ::_thesis: contradiction then consider z being set such that A9: ( z in S . x & z in S . y ) by XBOOLE_0:3; consider Yx being Element of (GF p) such that A10: ( z = Class ((R_EllCur (a,b,p)),[(n - 1),Yx,1]) & [(n - 1),Yx,1] in EC_SetProjCo (a,b,p) ) by A7, A9; consider Yy being Element of (GF p) such that A11: ( z = Class ((R_EllCur (a,b,p)),[(m - 1),Yy,1]) & [(m - 1),Yy,1] in EC_SetProjCo (a,b,p) ) by A8, A9; n - 1 = m - 1 by Th52, A1, A10, A11, A6; hence contradiction by A4; ::_thesis: verum end; end; suppose ( not x in dom S or not y in dom S ) ; ::_thesis: S . b1 misses S . b2 then ( S . x = {} or S . y = {} ) by FUNCT_1:def_2; hence S . x misses S . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence S is disjoint_valued by PROB_2:def_2; ::_thesis: ( ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) thus for n being Nat st n in dom S holds S . n is finite ::_thesis: Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } proof let n be Nat; ::_thesis: ( n in dom S implies S . n is finite ) assume A12: n in dom S ; ::_thesis: S . n is finite then A13: S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2; ( 1 <= n & n <= p ) by A12, A3, FINSEQ_1:1; then A14: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9; then A15: n - 1 is Element of NAT by INT_1:3; p - 1 < p - 0 by XREAL_1:15; then n - 1 < p by A14, XXREAL_0:2; then reconsider d = n - 1 as Element of (GF p) by A15, NAT_1:44; A16: card (S . n) = card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } by A13 .= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by Th59, A1 ; 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) proof percases ( ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) or ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; suppose ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) then Lege_p (((d |^ 3) + (a * d)) + b) = - 1 by Def5; hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum end; supposeA17: ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) now__::_thesis:_0_<=_1_+_(Lege_p_(((d_|^_3)_+_(a_*_d))_+_b)) percases ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) by A17; suppose ((d |^ 3) + (a * d)) + b = 0 ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) then Lege_p (((d |^ 3) + (a * d)) + b) = 0 by Def5; hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum end; suppose ((d |^ 3) + (a * d)) + b is quadratic_residue ; ::_thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) then Lege_p (((d |^ 3) + (a * d)) + b) = 1 by Def5; hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum end; end; end; hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; ::_thesis: verum end; end; end; then card (S . n) in NAT by A16, INT_1:3; hence S . n is finite ; ::_thesis: verum end; set B = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; for x being set holds ( x in union (rng S) iff x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) proof let x be set ; ::_thesis: ( x in union (rng S) iff x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) hereby ::_thesis: ( x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in union (rng S) ) assume x in union (rng S) ; ::_thesis: x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } then consider Z being set such that A18: ( x in Z & Z in rng S ) by TARSKI:def_4; consider n being set such that A19: ( n in dom S & Z = S . n ) by A18, FUNCT_1:def_3; reconsider n = n as Nat by A19; S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A19, A2; then consider Y being Element of (GF p) such that A20: ( x = Class ((R_EllCur (a,b,p)),[(n - 1),Y,1]) & [(n - 1),Y,1] in EC_SetProjCo (a,b,p) ) by A18, A19; n - 1 is Element of (GF p) by A3, A19, Lm8; hence x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by A20; ::_thesis: verum end; assume x in { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; ::_thesis: x in union (rng S) then consider P being Element of ProjCo (GF p) such that A21: ( x = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) ; consider X, Y being Element of (GF p) such that A22: P = [X,Y,1] by A21; reconsider n1 = X as Nat ; A23: ( 0 <= n1 & n1 < p ) by NAT_1:44; A24: 0 + 1 <= n1 + 1 by XREAL_1:6; A25: n1 + 1 <= p by A23, NAT_1:13; set n = n1 + 1; A26: ( n1 + 1 in Seg p & (n1 + 1) - 1 = X ) by A24, A25; x in { (Class ((R_EllCur (a,b,p)),[((n1 + 1) - 1),Q,1])) where Q is Element of (GF p) : [((n1 + 1) - 1),Q,1] in EC_SetProjCo (a,b,p) } by A21, A22; then A27: x in S . (n1 + 1) by A26, A2, A3; S . (n1 + 1) in rng S by A26, A3, FUNCT_1:3; hence x in union (rng S) by A27, TARSKI:def_4; ::_thesis: verum end; hence Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:1; ::_thesis: verum end; theorem Th60: :: EC_PF_1:60 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of NAT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of NAT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex F being FinSequence of NAT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex F being FinSequence of NAT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) then consider S being Function such that A2: ( dom S = Seg p & ( for n being Nat st n in dom S holds S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) by Lm9; defpred S1[ Nat, Nat] means $2 = card (S . $1); A3: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_p_holds_ ex_x_being_Element_of_NAT_st_S1[i,x] let i be Nat; ::_thesis: ( i in Seg p implies ex x being Element of NAT st S1[i,x] ) assume i in Seg p ; ::_thesis: ex x being Element of NAT st S1[i,x] then S . i is finite by A2; then reconsider x = card (S . i) as Element of NAT by ORDINAL1:def_12; take x = x; ::_thesis: S1[i,x] thus S1[i,x] ; ::_thesis: verum end; consider L being FinSequence of NAT such that A4: ( dom L = Seg p & ( for i being Nat st i in Seg p holds S1[i,L . i] ) ) from FINSEQ_1:sch_5(A3); take L ; ::_thesis: ( len L = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) p is Element of NAT by ORDINAL1:def_12; hence len L = p by A4, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) A5: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_p_holds_ ex_d_being_Element_of_(GF_p)_st_ (_d_=_n_-_1_&_L_._n_=_1_+_(Lege_p_(((d_|^_3)_+_(a_*_d))_+_b))_) let n be Nat; ::_thesis: ( n in Seg p implies ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) assume A6: n in Seg p ; ::_thesis: ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) then ( 1 <= n & n <= p ) by FINSEQ_1:1; then A7: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9; then A8: n - 1 is Element of NAT by INT_1:3; p - 1 < p - 0 by XREAL_1:15; then n - 1 < p by A7, XXREAL_0:2; then reconsider d = n - 1 as Element of (GF p) by A8, NAT_1:44; take d = d; ::_thesis: ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) thus d = n - 1 ; ::_thesis: L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) thus L . n = card (S . n) by A4, A6 .= card { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2, A6 .= card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } .= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by Th59, A1 ; ::_thesis: verum end; for i being Nat st i in dom S holds ( S . i is finite & L . i = card (S . i) ) by A2, A4; hence ( ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) by A2, A4, A5, DIST_1:17; ::_thesis: verum end; theorem :: EC_PF_1:61 for p being Prime for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of INT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) proof let p be Prime; ::_thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds ex F being FinSequence of INT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) let a, b be Element of (GF p); ::_thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex F being FinSequence of INT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) ) assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; ::_thesis: ex F being FinSequence of INT st ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) then consider L being FinSequence of NAT such that A2: ( len L = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) by Th60; A3: p is Element of NAT by ORDINAL1:def_12; defpred S1[ Nat, set ] means ex d being Element of (GF p) st ( d = $1 - 1 & $2 = Lege_p (((d |^ 3) + (a * d)) + b) ); A4: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_p_holds_ ex_x_being_Element_of_INT_st_S1[n,x] let n be Nat; ::_thesis: ( n in Seg p implies ex x being Element of INT st S1[n,x] ) assume n in Seg p ; ::_thesis: ex x being Element of INT st S1[n,x] then ( 1 <= n & n <= p ) by FINSEQ_1:1; then A5: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9; then A6: n - 1 is Element of NAT by INT_1:3; p - 1 < p - 0 by XREAL_1:15; then n - 1 < p by A5, XXREAL_0:2; then reconsider d = n - 1 as Element of (GF p) by A6, NAT_1:44; reconsider x = Lege_p (((d |^ 3) + (a * d)) + b) as Element of INT by INT_1:def_2; take x = x; ::_thesis: S1[n,x] thus S1[n,x] ; ::_thesis: verum end; consider F being FinSequence of INT such that A7: ( dom F = Seg p & ( for i being Nat st i in Seg p holds S1[i,F . i] ) ) from FINSEQ_1:sch_5(A4); take F ; ::_thesis: ( len F = p & ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) thus A8: len F = p by A7, A3, FINSEQ_1:def_3; ::_thesis: ( ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) reconsider pp = p |-> 1 as Element of p -tuples_on REAL ; F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:15; then reconsider FF = F as Element of p -tuples_on REAL by A8, FINSEQ_2:92; A9: now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_p_holds_ L_._n_=_(pp_+_FF)_._n let n be Nat; ::_thesis: ( 1 <= n & n <= p implies L . n = (pp + FF) . n ) assume ( 1 <= n & n <= p ) ; ::_thesis: L . n = (pp + FF) . n then A10: n in Seg p by FINSEQ_1:1; then A11: ex d being Element of (GF p) st ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) by A2; ex f being Element of (GF p) st ( f = n - 1 & F . n = Lege_p (((f |^ 3) + (a * f)) + b) ) by A7, A10; then L . n = ((p |-> 1) . n) + (F . n) by A11, A10, FUNCOP_1:7; hence L . n = (pp + FF) . n by RVSUM_1:11; ::_thesis: verum end; len (pp + FF) = p by A3, FINSEQ_2:132; then L = pp + FF by A2, A9, FINSEQ_1:14; then Sum L = (Sum (p |-> 1)) + (Sum F) by RVSUM_1:89; then A12: Sum L = (p * 1) + (Sum F) by RVSUM_1:80; reconsider F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} as finite set ; reconsider F2 = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } as finite set by A2; A13: card F1 = 1 by CARD_2:42; card (Class (R_EllCur (a,b,p))) = card (F1 \/ F2) by A1, Th51 .= 1 + (p + (Sum F)) by A1, A13, A2, A12, Th53, CARD_2:40 ; hence ( ( for n being Nat st n in Seg p holds ex d being Element of (GF p) st ( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) by A7; ::_thesis: verum end;