:: EULER_2 semantic presentation begin Lm1: for t being Integer holds ( t < 1 iff t <= 0 ) proof let t be Integer; ::_thesis: ( t < 1 iff t <= 0 ) ( t < 1 implies t <= 0 ) proof assume A1: t < 1 ; ::_thesis: t <= 0 assume A2: t > 0 ; ::_thesis: contradiction then reconsider t = t as Element of NAT by INT_1:3; t >= 1 by A2, NAT_1:14; hence contradiction by A1; ::_thesis: verum end; hence ( t < 1 iff t <= 0 ) ; ::_thesis: verum end; Lm2: for a being Nat st a <> 0 holds a - 1 >= 0 proof let a be Nat; ::_thesis: ( a <> 0 implies a - 1 >= 0 ) assume a <> 0 ; ::_thesis: a - 1 >= 0 then a >= 1 by NAT_1:14; then a - 1 >= 1 - 1 by XREAL_1:9; hence a - 1 >= 0 ; ::_thesis: verum end; Lm3: for z being Integer holds 1 gcd z = 1 proof let z be Integer; ::_thesis: 1 gcd z = 1 thus 1 gcd z = (abs 1) gcd (abs z) by INT_2:34 .= 1 gcd (abs z) by ABSVALUE:def_1 .= 1 by NEWTON:51 ; ::_thesis: verum end; theorem :: EULER_2:1 for a, b being Nat holds ( a,b are_relative_prime iff a,b are_relative_prime ) ; theorem Th2: :: EULER_2:2 for m being Nat for t being Integer st m * t >= 1 holds t >= 1 proof let m be Nat; ::_thesis: for t being Integer st m * t >= 1 holds t >= 1 let t be Integer; ::_thesis: ( m * t >= 1 implies t >= 1 ) assume A1: m * t >= 1 ; ::_thesis: t >= 1 assume t < 1 ; ::_thesis: contradiction then t <= 0 by Lm1; hence contradiction by A1; ::_thesis: verum end; Lm4: for m being Nat for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds z = 0 proof let m be Nat; ::_thesis: for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds z = 0 let z be Integer; ::_thesis: ( 1 - m <= z & z <= m - 1 & m divides z implies z = 0 ) assume that A1: 1 - m <= z and A2: z <= m - 1 and A3: m divides z ; ::_thesis: z = 0 consider t being Integer such that A4: z = m * t by A3, INT_1:def_3; assume A5: z <> 0 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( t > 0 or t < 0 ) by A5, A4; supposeA6: t > 0 ; ::_thesis: contradiction then reconsider t = t as Element of NAT by INT_1:3; m * t >= m by A6, NAT_1:14, NEWTON:33; then (m * t) + 1 > m by NAT_1:13; hence contradiction by A2, A4, XREAL_1:19; ::_thesis: verum end; supposeA7: t < 0 ; ::_thesis: contradiction reconsider r = t + 1 as Integer ; 1 <= (m * t) + (m * 1) by A1, A4, XREAL_1:20; then 1 <= m * (t + 1) ; then r >= 1 by Th2; then 1 - 1 <= t by XREAL_1:20; hence contradiction by A7; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th3: :: EULER_2:3 for a, b, m being Nat st a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime holds m,(a * b) mod m are_relative_prime proof let a, b, m be Nat; ::_thesis: ( a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime implies m,(a * b) mod m are_relative_prime ) assume that A1: a <> 0 and A2: b <> 0 and A3: m <> 0 and A4: ( a,m are_relative_prime & b,m are_relative_prime ) ; ::_thesis: m,(a * b) mod m are_relative_prime a * b,m are_relative_prime by A1, A3, A4, EULER_1:14; then A5: (a * b) gcd m = 1 by INT_2:def_3; consider t being Nat such that A6: a * b = (m * t) + ((a * b) mod m) and (a * b) mod m < m by A3, NAT_D:def_2; a * b <> a * 0 by A1, A2, XCMPLX_1:5; then ((a * b) + ((- t) * m)) gcd m = (a * b) gcd m by EULER_1:16; hence m,(a * b) mod m are_relative_prime by A6, A5, INT_2:def_3; ::_thesis: verum end; theorem Th4: :: EULER_2:4 for m, n, a, b being Nat st m > 1 & m,n are_relative_prime & n = (a * b) mod m holds m,b are_relative_prime proof let m, n, a, b be Nat; ::_thesis: ( m > 1 & m,n are_relative_prime & n = (a * b) mod m implies m,b are_relative_prime ) assume that A1: m > 1 and A2: m,n are_relative_prime and A3: n = (a * b) mod m ; ::_thesis: m,b are_relative_prime set k = m gcd b; m gcd b divides m by NAT_D:def_5; then consider km being Nat such that A4: m = (m gcd b) * km by NAT_D:def_3; A5: ( m gcd b <> 0 & km <> 0 ) by A1, A4; reconsider km = km as Element of NAT by ORDINAL1:def_12; m gcd b divides b by NAT_D:def_5; then consider kb being Nat such that A6: b = (m gcd b) * kb by NAT_D:def_3; consider p being Nat such that A7: a * ((m gcd b) * kb) = (((m gcd b) * km) * p) + ((a * ((m gcd b) * kb)) mod ((m gcd b) * km)) and (a * ((m gcd b) * kb)) mod ((m gcd b) * km) < (m gcd b) * km by A1, A4, NAT_D:def_2; set tm = (a * kb) - (km * p); A8: (a * ((m gcd b) * kb)) mod ((m gcd b) * km) = (m gcd b) * ((a * kb) - (km * p)) by A7; assume not m,b are_relative_prime ; ::_thesis: contradiction then A9: m gcd b <> 1 by INT_2:def_3; A10: m gcd b <> - 1 by NAT_1:2; A11: ( (a * kb) - (km * p) <> 0 implies m gcd n <> 1 ) proof assume (a * kb) - (km * p) <> 0 ; ::_thesis: m gcd n <> 1 m gcd n = (m gcd b) * (km gcd ((a * kb) - (km * p))) by A3, A4, A5, A6, A8, EULER_1:15; hence m gcd n <> 1 by A9, A10, INT_1:9; ::_thesis: verum end; ( (a * kb) - (km * p) = 0 implies m gcd n <> 1 ) by A1, A3, A4, A6, A8, NEWTON:52; hence contradiction by A2, A11, INT_2:def_3; ::_thesis: verum end; theorem Th5: :: EULER_2:5 for m, n being Nat holds (m mod n) mod n = m mod n proof let m, n be Nat; ::_thesis: (m mod n) mod n = m mod n percases ( n <> 0 or n = 0 ) ; suppose n <> 0 ; ::_thesis: (m mod n) mod n = m mod n then ex t being Nat st ( m = (n * t) + (m mod n) & m mod n < n ) by NAT_D:def_2; hence (m mod n) mod n = m mod n by NAT_D:24; ::_thesis: verum end; supposeA1: n = 0 ; ::_thesis: (m mod n) mod n = m mod n hence (m mod n) mod n = 0 by NAT_D:def_2 .= m mod n by A1, NAT_D:def_2 ; ::_thesis: verum end; end; end; theorem :: EULER_2:6 for l, m, n being Nat holds (l + m) mod n = ((l mod n) + (m mod n)) mod n proof let l, m, n be Nat; ::_thesis: (l + m) mod n = ((l mod n) + (m mod n)) mod n thus (l + m) mod n = ((l mod n) + m) mod n by NAT_D:22 .= ((l mod n) + (m mod n)) mod n by NAT_D:23 ; ::_thesis: verum end; theorem Th7: :: EULER_2:7 for l, m, n being Nat holds (l * m) mod n = (l * (m mod n)) mod n proof let l, m, n be Nat; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n percases ( n <> 0 or n = 0 ) ; suppose n <> 0 ; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n then consider t being Nat such that A1: m = (n * t) + (m mod n) and m mod n < n by NAT_D:def_2; (l * m) mod n = (((l * t) * n) + (l * (m mod n))) mod n by A1; hence (l * m) mod n = (l * (m mod n)) mod n by NAT_D:21; ::_thesis: verum end; supposeA2: n = 0 ; ::_thesis: (l * m) mod n = (l * (m mod n)) mod n hence (l * m) mod n = 0 by NAT_D:def_2 .= (l * (m mod n)) mod n by A2, NAT_D:def_2 ; ::_thesis: verum end; end; end; theorem :: EULER_2:8 for l, m, n being Nat holds (l * m) mod n = ((l mod n) * m) mod n by Th7; theorem Th9: :: EULER_2:9 for l, m, n being Nat holds (l * m) mod n = ((l mod n) * (m mod n)) mod n proof let l, m, n be Nat; ::_thesis: (l * m) mod n = ((l mod n) * (m mod n)) mod n (l * m) mod n = (l * (m mod n)) mod n by Th7; hence (l * m) mod n = ((l mod n) * (m mod n)) mod n by Th7; ::_thesis: verum end; begin definition let f be FinSequence of NAT ; let a be Nat; :: original: * redefine funca * f -> FinSequence of NAT ; coherence a * f is FinSequence of NAT proof rng (a * f) c= NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (a * f) or x in NAT ) assume x in rng (a * f) ; ::_thesis: x in NAT then consider xx being set such that A1: xx in dom (a * f) and A2: x = (a * f) . xx by FUNCT_1:def_3; reconsider xx = xx as Element of NAT by A1; (a * f) . xx = a * (f . xx) by RVSUM_1:44; hence x in NAT by A2; ::_thesis: verum end; hence a * f is FinSequence of NAT by FINSEQ_1:def_4; ::_thesis: verum end; end; theorem Th10: :: EULER_2:10 for R1, R2 being FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2 proof let R1, R2 be FinSequence of NAT ; ::_thesis: ( R1,R2 are_fiberwise_equipotent implies Product R1 = Product R2 ) defpred S1[ Nat] means for f, g being FinSequence of NAT st f,g are_fiberwise_equipotent & len f = $1 holds Product f = Product g; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] let f, g be FinSequence of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies Product f = Product g ) assume that A3: f,g are_fiberwise_equipotent and A4: len f = n + 1 ; ::_thesis: Product f = Product g reconsider a = f . (n + 1) as Element of NAT ; A5: rng f = rng g by A3, CLASSES1:75; set fn = f | n; A6: f = (f | n) ^ <*a*> by A4, RFINSEQ:7; 0 + 1 <= n + 1 by NAT_1:13; then n + 1 in dom f by A4, FINSEQ_3:25; then a in rng g by A5, FUNCT_1:def_3; then consider m being Nat such that A7: m in dom g and A8: g . m = a by FINSEQ_2:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; set gg = g /^ m; set gm = g | m; m <= len g by A7, FINSEQ_3:25; then A9: len (g | m) = m by FINSEQ_1:59; A10: 1 <= m by A7, FINSEQ_3:25; then max (0,(m - 1)) = m - 1 by FINSEQ_2:4; then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5; A11: m = m1 + 1 ; then m1 <= m by NAT_1:11; then A12: Seg m1 c= Seg m by FINSEQ_1:5; m in Seg m by A10, FINSEQ_1:1; then (g | m) . m = a by A7, A8, RFINSEQ:6; then A13: g | m = ((g | m) | m1) ^ <*a*> by A9, A11, RFINSEQ:7; A14: g = (g | m) ^ (g /^ m) by RFINSEQ:8; A15: (g | m) | m1 = (g | m) | (Seg m1) by FINSEQ_1:def_15 .= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def_15 .= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71 .= g | (Seg m1) by A12, XBOOLE_1:28 .= g | m1 by FINSEQ_1:def_15 ; now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_(((g_|_m1)_^_(g_/^_m)),x)) let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) card (Coim (f,x)) = card (Coim (g,x)) by A3, CLASSES1:def_9; then (card ((f | n) " {x})) + (card (<*a*> " {x})) = card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x}) by A14, A13, A15, A6, FINSEQ_3:57 .= (card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57 .= ((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57 .= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x})) .= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x})) by FINSEQ_3:57 ; hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; ::_thesis: verum end; then A16: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def_9; len (f | n) = n by A4, FINSEQ_1:59, NAT_1:11; then Product (f | n) = Product ((g | m1) ^ (g /^ m)) by A2, A16; hence Product f = (Product ((g | m1) ^ (g /^ m))) * (Product <*a*>) by A6, RVSUM_1:97 .= ((Product (g | m1)) * (Product (g /^ m))) * (Product <*a*>) by RVSUM_1:97 .= ((Product (g | m1)) * (Product <*a*>)) * (Product (g /^ m)) .= (Product (g | m)) * (Product (g /^ m)) by A13, A15, RVSUM_1:97 .= Product g by A14, RVSUM_1:97 ; ::_thesis: verum end; assume A17: R1,R2 are_fiberwise_equipotent ; ::_thesis: Product R1 = Product R2 A18: len R1 = len R1 ; A19: S1[ 0 ] proof let f, g be FinSequence of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Product f = Product g ) assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; ::_thesis: Product f = Product g then A20: ( len g = 0 & f = <*> NAT ) by RFINSEQ:3; then g = <*> NAT ; hence Product f = Product g by A20; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A19, A1); hence Product R1 = Product R2 by A17, A18; ::_thesis: verum end; begin definition let f be FinSequence of NAT ; let m be Nat; funcf mod m -> FinSequence of NAT means :Def1: :: EULER_2:def 1 ( len it = len f & ( for i being Nat st i in dom f holds it . i = (f . i) mod m ) ); existence ex b1 being FinSequence of NAT st ( len b1 = len f & ( for i being Nat st i in dom f holds b1 . i = (f . i) mod m ) ) proof deffunc H1( Nat) -> Element of NAT = (f . $1) mod m; consider g being FinSequence such that A1: len g = len f and A2: for k being Nat st k in dom g holds g . k = H1(k) from FINSEQ_1:sch_2(); rng g c= NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in NAT ) assume x in rng g ; ::_thesis: x in NAT then consider y being set such that A3: y in dom g and A4: x = g . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A3; g . y = (f . y) mod m by A2, A3; hence x in NAT by A4; ::_thesis: verum end; then reconsider g = g as FinSequence of NAT by FINSEQ_1:def_4; take g ; ::_thesis: ( len g = len f & ( for i being Nat st i in dom f holds g . i = (f . i) mod m ) ) thus len g = len f by A1; ::_thesis: for i being Nat st i in dom f holds g . i = (f . i) mod m let k be Nat; ::_thesis: ( k in dom f implies g . k = (f . k) mod m ) assume k in dom f ; ::_thesis: g . k = (f . k) mod m then k in dom g by A1, FINSEQ_3:29; hence g . k = (f . k) mod m by A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of NAT st len b1 = len f & ( for i being Nat st i in dom f holds b1 . i = (f . i) mod m ) & len b2 = len f & ( for i being Nat st i in dom f holds b2 . i = (f . i) mod m ) holds b1 = b2 proof let fa, fb be FinSequence of NAT ; ::_thesis: ( len fa = len f & ( for i being Nat st i in dom f holds fa . i = (f . i) mod m ) & len fb = len f & ( for i being Nat st i in dom f holds fb . i = (f . i) mod m ) implies fa = fb ) assume that A5: len f = len fa and A6: for i being Nat st i in dom f holds fa . i = (f . i) mod m and A7: len f = len fb and A8: for i being Nat st i in dom f holds fb . i = (f . i) mod m ; ::_thesis: fa = fb now__::_thesis:_for_X_being_set_st_dom_f_=_X_holds_ fa_=_fb let X be set ; ::_thesis: ( dom f = X implies fa = fb ) assume A9: dom f = X ; ::_thesis: fa = fb A10: for i being Nat st i in X holds fa . i = fb . i proof given j being Nat such that A11: j in X and A12: fa . j <> fb . j ; ::_thesis: contradiction fa . j <> (f . j) mod m by A8, A9, A11, A12; hence contradiction by A6, A9, A11; ::_thesis: verum end; A13: dom f = Seg (len f) by FINSEQ_1:def_3 .= dom fb by A7, FINSEQ_1:def_3 ; dom f = Seg (len f) by FINSEQ_1:def_3 .= dom fa by A5, FINSEQ_1:def_3 ; hence fa = fb by A9, A13, A10, FINSEQ_1:13; ::_thesis: verum end; hence fa = fb ; ::_thesis: verum end; end; :: deftheorem Def1 defines mod EULER_2:def_1_:_ for f being FinSequence of NAT for m being Nat for b3 being FinSequence of NAT holds ( b3 = f mod m iff ( len b3 = len f & ( for i being Nat st i in dom f holds b3 . i = (f . i) mod m ) ) ); theorem :: EULER_2:11 for m being Nat for f being FinSequence of NAT st m <> 0 holds (Product (f mod m)) mod m = (Product f) mod m proof let m be Nat; ::_thesis: for f being FinSequence of NAT st m <> 0 holds (Product (f mod m)) mod m = (Product f) mod m defpred S1[ Nat] means for f being FinSequence of NAT st m <> 0 & len f = $1 holds (Product (f mod m)) mod m = (Product f) mod m; let f be FinSequence of NAT ; ::_thesis: ( m <> 0 implies (Product (f mod m)) mod m = (Product f) mod m ) assume A1: m <> 0 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m A2: len f is Element of NAT ; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] let f be FinSequence of NAT ; ::_thesis: ( m <> 0 & len f = n + 1 implies (Product (f mod m)) mod m = (Product f) mod m ) assume that A5: m <> 0 and A6: len f = n + 1 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m reconsider fn = f | n as FinSequence of NAT ; A7: len fn = n by A6, FINSEQ_1:59, NAT_1:11; A8: len (f mod m) = n + 1 by A6, Def1; then A9: len ((f mod m) | n) = n by FINSEQ_1:59, NAT_1:11; A10: n <= len f by A6, NAT_1:11; A11: for i being Nat st 1 <= i & i <= len ((f mod m) | n) holds ((f mod m) | n) . i = (fn mod m) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len ((f mod m) | n) implies ((f mod m) | n) . i = (fn mod m) . i ) assume that A12: 1 <= i and A13: i <= len ((f mod m) | n) ; ::_thesis: ((f mod m) | n) . i = (fn mod m) . i A14: (f | n) . i = (f | (Seg n)) . i by FINSEQ_1:def_15; A15: i in Seg n by A9, A12, A13, FINSEQ_1:1; then A16: ((f mod m) | (Seg n)) . i = (f mod m) . i by FUNCT_1:49; i <= len f by A10, A9, A13, XXREAL_0:2; then A17: i in dom f by A12, FINSEQ_3:25; i in dom fn by A7, A9, A12, A13, FINSEQ_3:25; then (fn mod m) . i = (fn . i) mod m by Def1 .= (f . i) mod m by A15, A14, FUNCT_1:49 .= (f mod m) . i by A17, Def1 ; hence ((f mod m) | n) . i = (fn mod m) . i by A16, FINSEQ_1:def_15; ::_thesis: verum end; 0 + 1 <= n + 1 by NAT_1:13; then n + 1 in dom f by A6, FINSEQ_3:25; then A18: (f mod m) . (n + 1) = (f . (n + 1)) mod m by Def1; len ((f mod m) | n) = len (fn mod m) by A7, A9, Def1; then (f mod m) | n = fn mod m by A11, FINSEQ_1:14; then f mod m = (fn mod m) ^ <*((f . (n + 1)) mod m)*> by A8, A18, RFINSEQ:7; then A19: (Product (f mod m)) mod m = ((Product (fn mod m)) * ((f . (n + 1)) mod m)) mod m by RVSUM_1:96 .= (((Product (fn mod m)) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by Th9 .= (((Product fn) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by A4, A5, A7 .= (((Product fn) mod m) * ((f . (n + 1)) mod m)) mod m by Th5 ; (Product f) mod m = (Product (fn ^ <*(f . (n + 1))*>)) mod m by A6, RFINSEQ:7 .= ((Product fn) * (f . (n + 1))) mod m by RVSUM_1:96 ; hence (Product (f mod m)) mod m = (Product f) mod m by A19, Th9; ::_thesis: verum end; A20: S1[ 0 ] proof let f be FinSequence of NAT ; ::_thesis: ( m <> 0 & len f = 0 implies (Product (f mod m)) mod m = (Product f) mod m ) assume that m <> 0 and A21: len f = 0 ; ::_thesis: (Product (f mod m)) mod m = (Product f) mod m A22: ( f = <*> NAT & len (f mod m) = 0 ) by A21, Def1; then f mod m = <*> NAT ; hence (Product (f mod m)) mod m = (Product f) mod m by A22; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A20, A3); hence (Product (f mod m)) mod m = (Product f) mod m by A1, A2; ::_thesis: verum end; theorem Th12: :: EULER_2:12 for a, m, n being Nat st a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_relative_prime holds a mod m = 1 proof let a, m, n be Nat; ::_thesis: ( a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_relative_prime implies a mod m = 1 ) assume that A1: a <> 0 and A2: m > 1 and A3: (a * n) mod m = n mod m and A4: m,n are_relative_prime ; ::_thesis: a mod m = 1 consider k2 being Nat such that A5: n = (m * k2) + (n mod m) and n mod m < m by A2, NAT_D:def_2; consider k1 being Nat such that A6: a * n = (m * k1) + ((a * n) mod m) and (a * n) mod m < m by A2, NAT_D:def_2; (a - 1) * n = m * (k1 - k2) by A3, A6, A5; then A7: m divides (a - 1) * n by INT_1:def_3; reconsider t = a - 1, m = m as Integer ; m divides t by A4, A7, INT_2:25; then consider tt being Integer such that A8: a - 1 = m * tt by INT_1:def_3; a - 1 >= 0 by A1, Lm2; then A9: tt >= 0 by A2, A8, XREAL_1:158; A10: a = (m * tt) + 1 by A8; reconsider tt = tt, m = m as Element of NAT by A9, INT_1:3; a mod m = (((m * tt) mod m) + 1) mod m by A10, NAT_D:22 .= (0 + 1) mod m by NAT_D:13 .= 1 by A2, NAT_D:24 ; hence a mod m = 1 ; ::_thesis: verum end; theorem :: EULER_2:13 for m being Nat for F being FinSequence of NAT holds (F mod m) mod m = F mod m proof let m be Nat; ::_thesis: for F being FinSequence of NAT holds (F mod m) mod m = F mod m let F be FinSequence of NAT ; ::_thesis: (F mod m) mod m = F mod m A1: dom (F mod m) = Seg (len (F mod m)) by FINSEQ_1:def_3 .= Seg (len F) by Def1 .= dom F by FINSEQ_1:def_3 ; A2: for x being set st x in dom F holds ((F mod m) mod m) . x = (F mod m) . x proof let x be set ; ::_thesis: ( x in dom F implies ((F mod m) mod m) . x = (F mod m) . x ) assume A3: x in dom F ; ::_thesis: ((F mod m) mod m) . x = (F mod m) . x then reconsider x = x as Element of NAT ; ((F mod m) mod m) . x = ((F mod m) . x) mod m by A1, A3, Def1 .= ((F . x) mod m) mod m by A3, Def1 .= (F . x) mod m by Th5 .= (F mod m) . x by A3, Def1 ; hence ((F mod m) mod m) . x = (F mod m) . x ; ::_thesis: verum end; dom ((F mod m) mod m) = Seg (len ((F mod m) mod m)) by FINSEQ_1:def_3 .= Seg (len (F mod m)) by Def1 .= Seg (len F) by Def1 .= dom F by FINSEQ_1:def_3 ; hence (F mod m) mod m = F mod m by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem :: EULER_2:14 for a, m being Nat for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m proof let a, m be Nat; ::_thesis: for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m let F be FinSequence of NAT ; ::_thesis: (a * (F mod m)) mod m = (a * F) mod m A1: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def_3 .= Seg (len F) by NEWTON:2 .= dom F by FINSEQ_1:def_3 ; A2: dom (a * (F mod m)) = Seg (len (a * (F mod m))) by FINSEQ_1:def_3 .= Seg (len (F mod m)) by NEWTON:2 .= Seg (len F) by Def1 .= dom F by FINSEQ_1:def_3 ; A3: for x being set st x in dom F holds ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x proof let x be set ; ::_thesis: ( x in dom F implies ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x ) assume A4: x in dom F ; ::_thesis: ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x then reconsider x = x as Element of NAT ; ((a * (F mod m)) mod m) . x = ((a * (F mod m)) . x) mod m by A2, A4, Def1 .= (a * ((F mod m) . x)) mod m by RVSUM_1:44 .= (a * ((F . x) mod m)) mod m by A4, Def1 .= (a * (F . x)) mod m by Th7 .= ((a * F) . x) mod m by RVSUM_1:44 .= ((a * F) mod m) . x by A1, A4, Def1 ; hence ((a * (F mod m)) mod m) . x = ((a * F) mod m) . x ; ::_thesis: verum end; A5: dom ((a * F) mod m) = Seg (len ((a * F) mod m)) by FINSEQ_1:def_3 .= Seg (len (a * F)) by Def1 .= Seg (len F) by NEWTON:2 .= dom F by FINSEQ_1:def_3 ; dom ((a * (F mod m)) mod m) = Seg (len ((a * (F mod m)) mod m)) by FINSEQ_1:def_3 .= Seg (len (a * (F mod m))) by Def1 .= Seg (len (F mod m)) by NEWTON:2 .= Seg (len F) by Def1 .= dom F by FINSEQ_1:def_3 ; hence (a * (F mod m)) mod m = (a * F) mod m by A5, A3, FUNCT_1:2; ::_thesis: verum end; theorem :: EULER_2:15 for m being Nat for F, G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m) proof let m be Nat; ::_thesis: for F, G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m) let F, G be FinSequence of NAT ; ::_thesis: (F ^ G) mod m = (F mod m) ^ (G mod m) A1: dom ((F ^ G) mod m) = Seg (len ((F ^ G) mod m)) by FINSEQ_1:def_3 .= Seg (len (F ^ G)) by Def1 .= dom (F ^ G) by FINSEQ_1:def_3 ; A2: dom (G mod m) = Seg (len (G mod m)) by FINSEQ_1:def_3 .= Seg (len G) by Def1 .= dom G by FINSEQ_1:def_3 ; A3: dom (F mod m) = Seg (len (F mod m)) by FINSEQ_1:def_3 .= Seg (len F) by Def1 .= dom F by FINSEQ_1:def_3 ; A4: for x being set st x in dom (F ^ G) holds ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x proof let x be set ; ::_thesis: ( x in dom (F ^ G) implies ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x ) assume A5: x in dom (F ^ G) ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x then reconsider x = x as Element of NAT ; now__::_thesis:_((F_^_G)_mod_m)_._x_=_((F_mod_m)_^_(G_mod_m))_._x percases ( x in dom F or ex n being Nat st ( n in dom G & x = (len F) + n ) ) by A5, FINSEQ_1:25; supposeA6: x in dom F ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x A7: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1 .= (F . x) mod m by A6, FINSEQ_1:def_7 ; ((F mod m) ^ (G mod m)) . x = (F mod m) . x by A3, A6, FINSEQ_1:def_7 .= (F . x) mod m by A6, Def1 ; hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A7; ::_thesis: verum end; suppose ex n being Nat st ( n in dom G & x = (len F) + n ) ; ::_thesis: ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x then consider n being Element of NAT such that A8: n in dom G and A9: x = (len F) + n ; A10: ((F ^ G) mod m) . x = ((F ^ G) . x) mod m by A5, Def1 .= (G . n) mod m by A8, A9, FINSEQ_1:def_7 ; len (F mod m) = len F by Def1; then ((F mod m) ^ (G mod m)) . x = (G mod m) . n by A2, A8, A9, FINSEQ_1:def_7 .= (G . n) mod m by A8, Def1 ; hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x by A10; ::_thesis: verum end; end; end; hence ((F ^ G) mod m) . x = ((F mod m) ^ (G mod m)) . x ; ::_thesis: verum end; dom ((F mod m) ^ (G mod m)) = Seg (len ((F mod m) ^ (G mod m))) by FINSEQ_1:def_3 .= Seg ((len (F mod m)) + (len (G mod m))) by FINSEQ_1:22 .= Seg ((len F) + (len (G mod m))) by Def1 .= Seg ((len F) + (len G)) by Def1 .= Seg (len (F ^ G)) by FINSEQ_1:22 .= dom (F ^ G) by FINSEQ_1:def_3 ; hence (F ^ G) mod m = (F mod m) ^ (G mod m) by A1, A4, FUNCT_1:2; ::_thesis: verum end; theorem :: EULER_2:16 for a, m being Nat for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) proof let a, m be Nat; ::_thesis: for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) let F, G be FinSequence of NAT ; ::_thesis: (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) reconsider FG = F ^ G as FinSequence of NAT ; A1: dom (a * (F ^ G)) = Seg (len (a * FG)) by FINSEQ_1:def_3 .= Seg (len FG) by NEWTON:2 .= dom (F ^ G) by FINSEQ_1:def_3 ; A2: dom (a * G) = Seg (len (a * G)) by FINSEQ_1:def_3 .= Seg (len G) by NEWTON:2 .= dom G by FINSEQ_1:def_3 ; A3: dom ((a * G) mod m) = Seg (len ((a * G) mod m)) by FINSEQ_1:def_3 .= Seg (len (a * G)) by Def1 .= Seg (len G) by NEWTON:2 .= dom G by FINSEQ_1:def_3 ; A4: dom (a * F) = Seg (len (a * F)) by FINSEQ_1:def_3 .= Seg (len F) by NEWTON:2 .= dom F by FINSEQ_1:def_3 ; A5: dom ((a * F) mod m) = Seg (len ((a * F) mod m)) by FINSEQ_1:def_3 .= Seg (len (a * F)) by Def1 .= Seg (len F) by NEWTON:2 .= dom F by FINSEQ_1:def_3 ; A6: for x being set st x in dom (F ^ G) holds ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x proof reconsider H = F ^ G as FinSequence of NAT ; let x be set ; ::_thesis: ( x in dom (F ^ G) implies ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x ) assume A7: x in dom (F ^ G) ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x then reconsider x = x as Element of NAT ; now__::_thesis:_((a_*_(F_^_G))_mod_m)_._x_=_(((a_*_F)_mod_m)_^_((a_*_G)_mod_m))_._x percases ( x in dom F or ex n being Nat st ( n in dom G & x = (len F) + n ) ) by A7, FINSEQ_1:25; supposeA8: x in dom F ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x A9: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1 .= (a * (H . x)) mod m by RVSUM_1:44 .= (a * (F . x)) mod m by A8, FINSEQ_1:def_7 ; (((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * F) mod m) . x by A5, A8, FINSEQ_1:def_7 .= ((a * F) . x) mod m by A4, A8, Def1 .= (a * (F . x)) mod m by RVSUM_1:44 ; hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A9; ::_thesis: verum end; suppose ex n being Nat st ( n in dom G & x = (len F) + n ) ; ::_thesis: ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x then consider n being Element of NAT such that A10: n in dom G and A11: x = (len F) + n ; A12: ((a * (F ^ G)) mod m) . x = ((a * (F ^ G)) . x) mod m by A1, A7, Def1 .= (a * (H . x)) mod m by RVSUM_1:44 .= (a * (G . n)) mod m by A10, A11, FINSEQ_1:def_7 ; len ((a * F) mod m) = len (a * F) by Def1 .= len F by NEWTON:2 ; then (((a * F) mod m) ^ ((a * G) mod m)) . x = ((a * G) mod m) . n by A3, A10, A11, FINSEQ_1:def_7 .= ((a * G) . n) mod m by A2, A10, Def1 .= (a * (G . n)) mod m by RVSUM_1:44 ; hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x by A12; ::_thesis: verum end; end; end; hence ((a * (F ^ G)) mod m) . x = (((a * F) mod m) ^ ((a * G) mod m)) . x ; ::_thesis: verum end; A13: dom ((a * (F ^ G)) mod m) = Seg (len ((a * FG) mod m)) by FINSEQ_1:def_3 .= Seg (len (a * FG)) by Def1 .= Seg (len FG) by NEWTON:2 .= dom (F ^ G) by FINSEQ_1:def_3 ; dom (((a * F) mod m) ^ ((a * G) mod m)) = Seg (len (((a * F) mod m) ^ ((a * G) mod m))) by FINSEQ_1:def_3 .= Seg ((len ((a * F) mod m)) + (len ((a * G) mod m))) by FINSEQ_1:22 .= Seg ((len (a * F)) + (len ((a * G) mod m))) by Def1 .= Seg ((len (a * F)) + (len (a * G))) by Def1 .= Seg ((len F) + (len (a * G))) by NEWTON:2 .= Seg ((len F) + (len G)) by NEWTON:2 .= Seg (len (F ^ G)) by FINSEQ_1:22 .= dom (F ^ G) by FINSEQ_1:def_3 ; hence (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m) by A13, A6, FUNCT_1:2; ::_thesis: verum end; theorem :: EULER_2:17 for a, m being Nat st a <> 0 & m <> 0 & a,m are_relative_prime holds for b being Nat holds a |^ b,m are_relative_prime proof let a, m be Nat; ::_thesis: ( a <> 0 & m <> 0 & a,m are_relative_prime implies for b being Nat holds a |^ b,m are_relative_prime ) defpred S1[ Nat] means a |^ $1,m are_relative_prime ; assume A1: ( a <> 0 & m <> 0 & a,m are_relative_prime ) ; ::_thesis: for b being Nat holds a |^ b,m are_relative_prime A2: for b being Nat st S1[b] holds S1[b + 1] proof let b be Nat; ::_thesis: ( S1[b] implies S1[b + 1] ) A3: a |^ (b + 1) = (a |^ b) * (a |^ 1) by NEWTON:8 .= (a |^ b) * a by NEWTON:5 ; assume a |^ b,m are_relative_prime ; ::_thesis: S1[b + 1] hence S1[b + 1] by A1, A3, EULER_1:14; ::_thesis: verum end; ( (a |^ 0) gcd m = 1 gcd m & m gcd 1 = 1 ) by NEWTON:4, NEWTON:51; then A4: S1[ 0 ] by INT_2:def_3; for b being Nat holds S1[b] from NAT_1:sch_2(A4, A2); hence for b being Nat holds a |^ b,m are_relative_prime ; ::_thesis: verum end; begin theorem Th18: :: EULER_2:18 for a, m being Nat st a <> 0 & m > 1 & a,m are_relative_prime holds (a |^ (Euler m)) mod m = 1 proof let a, m be Nat; ::_thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ (Euler m)) mod m = 1 ) assume that A1: a <> 0 and A2: m > 1 and A3: a,m are_relative_prime ; ::_thesis: (a |^ (Euler m)) mod m = 1 set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; A4: a |^ (Euler m) <> 0 by A1, PREPOWER:5; set Y = { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; A5: for x being Nat st x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } holds (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } proof let x be Nat; ::_thesis: ( x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } implies (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } then consider t being Element of NAT such that A6: t = x and A7: m,t are_relative_prime and A8: t >= 1 and t <= m ; A9: a * t,m are_relative_prime by A1, A2, A3, A7, EULER_1:14; (a * t) mod m <> 0 proof assume (a * t) mod m = 0 ; ::_thesis: contradiction then consider s being Nat such that A10: a * t = (m * s) + 0 and 0 < m by A2, NAT_D:def_2; s gcd 1 = 1 by NEWTON:51; then (m * s) gcd (m * 1) = m by EULER_1:5; hence contradiction by A2, A9, A10, INT_2:def_3; ::_thesis: verum end; then A11: (a * t) mod m >= 1 by NAT_1:14; A12: (a * t) mod m <= m by A2, NAT_D:1; m,(a * t) mod m are_relative_prime by A1, A2, A3, A7, A8, Th3; hence (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A6, A11, A12; ::_thesis: verum end; A13: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } = { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } proof thus { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def_10 ::_thesis: { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ) assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } then consider xx being Element of NAT such that A14: x = xx and A15: m,xx are_relative_prime and xx >= 1 and A16: xx <= m ; consider i, j being Integer such that A17: (i * a) + (j * m) = xx by A3, EULER_1:10; xx <> m by A2, A15, EULER_1:1; then xx < m by A16, XXREAL_0:1; then A18: xx mod m = xx by NAT_D:24; reconsider im = i mod m as Element of NAT by INT_1:3, NEWTON:64; i mod m <> 0 proof assume i mod m = 0 ; ::_thesis: contradiction then 0 = i - ((i div m) * m) by A2, INT_1:def_10; then m gcd xx = (m * 1) gcd (m * (((i div m) * a) + j)) by A17 .= m * (1 gcd (((i div m) * a) + j)) by A2, EULER_1:15 .= m * 1 by Lm3 .= m ; hence contradiction by A2, A15, INT_2:def_3; ::_thesis: verum end; then A19: im >= 1 by NAT_1:14; A20: i = ((i div m) * m) + (i mod m) by A2, NEWTON:66; then reconsider ij = ((i mod m) * a) + ((((i div m) * a) + j) * m) as Element of NAT by A17; A21: im <= m by A2, NEWTON:65; A22: ij mod m = (im * a) mod m by EULER_1:12; then m,im are_relative_prime by A2, A15, A18, A17, A20, Th4; then im in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A19, A21; hence x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A14, A18, A17, A20, A22; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) assume y in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; ::_thesis: y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } then ex yy being Element of NAT st ( y = yy & ex u being Element of NAT st ( yy = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) ) ; hence y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A5; ::_thesis: verum end; A23: for xi, xj being Nat st xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj holds (a * xi) mod m <> (a * xj) mod m proof let xi, xj be Nat; ::_thesis: ( xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj implies (a * xi) mod m <> (a * xj) mod m ) assume that A24: xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and A25: xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and A26: xi <> xj ; ::_thesis: (a * xi) mod m <> (a * xj) mod m set tm = (a * xi) mod m; set sm = (a * xj) mod m; assume A27: (a * xi) mod m = (a * xj) mod m ; ::_thesis: contradiction consider s being Element of NAT such that A28: s = xj and m,s are_relative_prime and A29: ( s >= 1 & s <= m ) by A25; A30: (a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A2, A28, NEWTON:63; consider t being Element of NAT such that A31: t = xi and m,t are_relative_prime and A32: ( t >= 1 & t <= m ) by A24; (a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A2, A31, NEWTON:63; then 0 = (a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m))) by A27, A30; then A33: m divides a * (t - s) by INT_1:def_3; reconsider m = m, c = t - s as Integer ; ( 1 - m <= c & c <= m - 1 ) by A32, A29, XREAL_1:13; then t - s = 0 by A3, A33, Lm4, INT_2:25; hence contradiction by A26, A31, A28; ::_thesis: verum end; reconsider FX = Sgm { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as FinSequence of NAT ; reconsider FYY = a * FX as FinSequence of NAT ; reconsider FY = FYY mod m as FinSequence of NAT ; A34: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= Seg m proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in Seg m ) assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; ::_thesis: x in Seg m then ex xx being Element of NAT st ( x = xx & m,xx are_relative_prime & xx >= 1 & xx <= m ) ; hence x in Seg m by FINSEQ_1:1; ::_thesis: verum end; then reconsider X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as finite set ; dom FYY = Seg (len FYY) by FINSEQ_1:def_3 .= Seg (len FX) by NEWTON:2 ; then A35: dom FX = dom FYY by FINSEQ_1:def_3; A36: dom FY = Seg (len FY) by FINSEQ_1:def_3 .= Seg (len FYY) by Def1 .= Seg (len FX) by NEWTON:2 ; then A37: dom FX = dom FY by FINSEQ_1:def_3; A38: rng FY = { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } proof thus rng FY c= { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def_10 ::_thesis: { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= rng FY proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng FY or x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ) assume x in rng FY ; ::_thesis: x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } then consider y being set such that A39: y in dom FY and A40: x = FY . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A39; FX . y in rng FX by A37, A39, FUNCT_1:def_3; then A41: FX . y in X by A34, FINSEQ_1:def_13; y in dom FX by A36, A39, FINSEQ_1:def_3; then FY . y = (FYY . y) mod m by A35, Def1 .= (a * (FX . y)) mod m by RVSUM_1:44 ; hence x in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A40, A41; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in rng FY ) assume y in { l where l is Element of NAT : ex u being Element of NAT st ( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; ::_thesis: y in rng FY then consider yy being Element of NAT such that A42: y = yy and A43: ex u being Element of NAT st ( yy = (a * u) mod m & u in X ) ; consider uu being Element of NAT such that A44: yy = (a * uu) mod m and A45: uu in X by A43; uu in rng FX by A34, A45, FINSEQ_1:def_13; then consider xx being set such that A46: xx in dom FX and A47: uu = FX . xx by FUNCT_1:def_3; reconsider xx = xx as Element of NAT by A46; FY . xx = (FYY . xx) mod m by A35, A46, Def1 .= y by A42, A44, A47, RVSUM_1:44 ; hence y in rng FY by A37, A46, FUNCT_1:def_3; ::_thesis: verum end; A48: FY is one-to-one proof A49: FX is one-to-one by A34, FINSEQ_3:92; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom FY or not x2 in dom FY or not FY . x1 = FY . x2 or x1 = x2 ) assume that A50: x1 in dom FY and A51: x2 in dom FY and A52: FY . x1 = FY . x2 ; ::_thesis: x1 = x2 A53: x2 in dom FX by A36, A51, FINSEQ_1:def_3; reconsider x2 = x2 as Element of NAT by A51; A54: x1 in dom FX by A36, A50, FINSEQ_1:def_3; reconsider x1 = x1 as Element of NAT by A50; A55: ( FX . x1 in rng FX & FX . x2 in rng FX ) by A37, A50, A51, FUNCT_1:def_3; A56: FY . x2 = (FYY . x2) mod m by A35, A53, Def1 .= (a * (FX . x2)) mod m by RVSUM_1:44 ; FY . x1 = (FYY . x1) mod m by A35, A54, Def1 .= (a * (FX . x1)) mod m by RVSUM_1:44 ; then ( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A23, A52, A56; hence x1 = x2 by A34, A54, A53, A55, A49, FINSEQ_1:def_13, FUNCT_1:def_4; ::_thesis: verum end; for x being set holds card (Coim (FX,x)) = card (Coim (FY,x)) proof let x be set ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x)) now__::_thesis:_card_(Coim_(FX,x))_=_card_(Coim_(FY,x)) percases ( x in X or not x in X ) ; supposeA57: x in X ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x)) A58: FX is one-to-one by A34, FINSEQ_3:92; x in rng FX by A34, A57, FINSEQ_1:def_13; then A59: len (FX - {x}) = (len FX) - 1 by A58, FINSEQ_3:90; A60: ( (len (FX - {x})) - (len (FX - {x})) = ((len FX) - (card (FX " {x}))) - (len (FX - {x})) & len (FY - {x}) = (len FY) - (card (FY " {x})) ) by FINSEQ_3:59; len (FY - {x}) = (len FY) - 1 by A13, A38, A48, A57, FINSEQ_3:90; hence card (Coim (FX,x)) = card (Coim (FY,x)) by A59, A60; ::_thesis: verum end; suppose not x in X ; ::_thesis: card (Coim (FX,x)) = card (Coim (FY,x)) then ( not x in rng FX & FY " {x} = {} ) by A13, A34, A38, FINSEQ_1:def_13, FUNCT_1:72; hence card (Coim (FX,x)) = card (Coim (FY,x)) by FUNCT_1:72; ::_thesis: verum end; end; end; hence card (Coim (FX,x)) = card (Coim (FY,x)) ; ::_thesis: verum end; then A61: FX,FY are_fiberwise_equipotent by CLASSES1:def_9; then A62: len FX = len FY by RFINSEQ:3; A63: (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m proof defpred S1[ Nat] means ( $1 <= len FY implies (Product (FY | $1)) mod m = ((a |^ (len (FY | $1))) * (Product (FX | $1))) mod m ); FY | (len FY) = FY | (Seg (len FY)) by FINSEQ_1:def_15; then A64: FY = FY | (len FY) by FINSEQ_2:20; A65: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) now__::_thesis:_(_S1[n]_implies_S1[n_+_1]_) percases ( n + 1 <= len FY or n + 1 > len FY ) ; supposeA66: n + 1 <= len FY ; ::_thesis: ( S1[n] implies S1[n + 1] ) then len (FX | (n + 1)) = n + 1 by A62, FINSEQ_1:59; then A67: FX | (n + 1) = ((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> by RFINSEQ:7; assume A68: S1[n] ; ::_thesis: S1[n + 1] 0 + 1 <= n + 1 by NAT_1:13; then A69: n + 1 in dom FY by A66, FINSEQ_3:25; A70: (FY | (n + 1)) . (n + 1) = FY . (n + 1) by FINSEQ_3:112; A71: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:112; A72: n <= n + 1 by NAT_1:11; then A73: len (FY | n) = n by A66, FINSEQ_1:59, XXREAL_0:2; A74: (FX | (n + 1)) | n = FX | n by A72, FINSEQ_5:77; A75: (FY | (n + 1)) | n = FY | n by A72, FINSEQ_5:77; A76: len (FY | (n + 1)) = n + 1 by A66, FINSEQ_1:59; then FY | (n + 1) = ((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*> by RFINSEQ:7; then (Product (FY | (n + 1))) mod m = ((Product (FY | n)) * (FY . (n + 1))) mod m by A75, A70, RVSUM_1:96 .= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m by A66, A68, A72, Th9, XXREAL_0:2 .= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m by A37, A35, A69, Def1 .= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((a * FX) . (n + 1)) mod m)) mod m by Th5 .= (((a |^ (len (FY | n))) * (Product (FX | n))) * ((a * FX) . (n + 1))) mod m by Th9 .= (((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1)))) mod m by A73, RVSUM_1:44 .= (((a |^ n) * a) * ((Product (FX | n)) * (FX . (n + 1)))) mod m .= ((a |^ (len (FY | (n + 1)))) * ((Product (FX | n)) * (FX . (n + 1)))) mod m by A76, NEWTON:6 .= ((a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1)))) mod m by A67, A74, A71, RVSUM_1:96 ; hence S1[n + 1] ; ::_thesis: verum end; suppose n + 1 > len FY ; ::_thesis: ( S1[n] implies S1[n + 1] ) hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; end; end; hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; FX | (len FX) = FX | (Seg (len FX)) by FINSEQ_1:def_15; then A77: FX = FX | (len FY) by A62, FINSEQ_2:20; A78: S1[ 0 ] by NEWTON:4, RVSUM_1:94; for n being Nat holds S1[n] from NAT_1:sch_2(A78, A65); hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A64, A77; ::_thesis: verum end; A79: Product FX,m are_relative_prime proof defpred S1[ Nat] means ( $1 <= len FX implies Product (FX | $1),m are_relative_prime ); A80: FX | (len FX) = FX by FINSEQ_1:58; A81: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) now__::_thesis:_(_S1[n]_implies_S1[n_+_1]_) percases ( len FX >= n + 1 or len FX < n + 1 ) ; supposeA82: len FX >= n + 1 ; ::_thesis: ( S1[n] implies S1[n + 1] ) reconsider FF = FX | (n + 1) as FinSequence of NAT ; reconsider ff = FF . (n + 1) as Element of NAT ; len FF = n + 1 by A82, FINSEQ_1:59; then A83: FF = (FF | n) ^ <*ff*> by RFINSEQ:7; reconsider a = Product (FF | n), b = ff, m9 = m as Integer ; A84: n <= n + 1 by NAT_1:11; 0 + 1 <= n + 1 by XREAL_1:6; then ( (FX | (n + 1)) . (n + 1) = FX . (n + 1) & n + 1 in dom FX ) by A82, FINSEQ_3:25, FINSEQ_3:112; then A85: (FX | (n + 1)) . (n + 1) in rng FX by FUNCT_1:def_3; rng FX = X by A34, FINSEQ_1:def_13; then A86: ex p being Element of NAT st ( ff = p & m,p are_relative_prime & p >= 1 & p <= m ) by A85; assume S1[n] ; ::_thesis: S1[n + 1] then a,m9 are_relative_prime by A82, A84, FINSEQ_5:77, XXREAL_0:2; then a * b,m9 are_relative_prime by A86, INT_2:26; hence S1[n + 1] by A83, RVSUM_1:96; ::_thesis: verum end; suppose len FX < n + 1 ; ::_thesis: ( S1[n] implies S1[n + 1] ) hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; end; end; hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; (Product (FX | 0)) gcd m = 1 by NEWTON:51, RVSUM_1:94; then A87: S1[ 0 ] by INT_2:def_3; for n being Nat holds S1[n] from NAT_1:sch_2(A87, A81); hence Product FX,m are_relative_prime by A80; ::_thesis: verum end; len FX = card X by A34, FINSEQ_3:39 .= Euler m by EULER_1:def_1 ; then A88: len FY = Euler m by A61, RFINSEQ:3; (Product FX) mod m = (Product FY) mod m by A61, Th10; hence (a |^ (Euler m)) mod m = 1 by A2, A63, A88, A4, A79, Th12; ::_thesis: verum end; theorem :: EULER_2:19 for a, m being Nat st a <> 0 & m is prime & a,m are_relative_prime holds (a |^ m) mod m = a mod m proof let a, m be Nat; ::_thesis: ( a <> 0 & m is prime & a,m are_relative_prime implies (a |^ m) mod m = a mod m ) assume that A1: a <> 0 and A2: m is prime and A3: a,m are_relative_prime ; ::_thesis: (a |^ m) mod m = a mod m A4: m > 1 by A2, INT_2:def_4; then m - 1 > 1 - 1 by XREAL_1:9; then reconsider mm = m - 1 as Element of NAT by INT_1:3; Euler m = m - 1 by A2, EULER_1:20; then ((a |^ mm) mod m) * a = 1 * a by A1, A3, A4, Th18; then ( mm + 1 = m & ((a |^ mm) * a) mod m = a mod m ) by Th7; hence (a |^ m) mod m = a mod m by NEWTON:6; ::_thesis: verum end;