:: NTALGO_1 semantic presentation begin theorem LMTh3: :: NTALGO_1:1 for x, p being Integer holds (x mod p) mod p = x mod p proof let x, p be Integer; ::_thesis: (x mod p) mod p = x mod p x mod p = (x + 0) mod p .= ((x mod p) + (0 mod p)) mod p by NAT_D:66 .= ((x mod p) + 0) mod p by INT_4:12 ; hence (x mod p) mod p = x mod p ; ::_thesis: verum end; LM6: for a being Element of NAT holds a gcd 0 = a proof let a be Element of NAT ; ::_thesis: a gcd 0 = a 0 = 0 * a ; then P2: a divides 0 by INT_1:def_3; for m being Integer st m divides a & m divides 0 holds m divides a ; hence a gcd 0 = a by P2, INT_2:def_2; ::_thesis: verum end; LM1: for a, b being Element of INT ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) proof let a, b be Element of INT ; ::_thesis: ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) defpred S1[ Nat, Nat, Nat, Nat, Nat] means ( $4 = $3 & $5 = $2 mod $3 ); Q1: for n, x, y being Element of NAT ex x1, y1 being Element of NAT st S1[n,x,y,x1,y1] ; consider A, B being Function of NAT,NAT such that P2: ( A . 0 = abs a & B . 0 = abs b & ( for n being Element of NAT holds S1[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) ) from RECDEF_2:sch_3(Q1); take A ; ::_thesis: ex B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) take B ; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) thus ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by P2; ::_thesis: verum end; LM2: for a, b being Element of INT for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds ( A1 = A2 & B1 = B2 ) proof let a, b be Element of INT ; ::_thesis: for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds ( A1 = A2 & B1 = B2 ) let A1, B1, A2, B2 be sequence of NAT; ::_thesis: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) implies ( A1 = A2 & B1 = B2 ) ) assume P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) ) ; ::_thesis: ( not A2 . 0 = abs a or not B2 . 0 = abs b or ex i being Element of NAT st ( A2 . (i + 1) = B2 . i implies not B2 . (i + 1) = (A2 . i) mod (B2 . i) ) or ( A1 = A2 & B1 = B2 ) ) assume P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) ) ; ::_thesis: ( A1 = A2 & B1 = B2 ) defpred S1[ Nat] means ( A1 . $1 = A2 . $1 & B1 . $1 = B2 . $1 ); P0: S1[ 0 ] by P1, P2; PN: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume PN1: S1[n] ; ::_thesis: S1[n + 1] PN2: A1 . (n + 1) = B1 . n by P1 .= A2 . (n + 1) by P2, PN1 ; B1 . (n + 1) = (A1 . n) mod (B1 . n) by P1 .= B2 . (n + 1) by P2, PN1 ; hence S1[n + 1] by PN2; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, PN); hence ( A1 = A2 & B1 = B2 ) by FUNCT_2:def_8; ::_thesis: verum end; definition let a, b be Element of INT ; func ALGO_GCD (a,b) -> Element of NAT means :defALGOGCD: :: NTALGO_1:def 1 ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & it = A . (min* { i where i is Element of NAT : B . i = 0 } ) ); existence ex b1 being Element of NAT ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) proof consider A, B being sequence of NAT such that P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by LM1; set m = A . (min* { i where i is Element of NAT : B . i = 0 } ); A . (min* { i where i is Element of NAT : B . i = 0 } ) is Element of NAT ; hence ex b1 being Element of NAT ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by P1; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) holds b1 = b2 proof let m1, m2 be Element of NAT ; ::_thesis: ( ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) implies m1 = m2 ) assume ex A1, B1 being sequence of NAT st ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ; ::_thesis: ( for A, B being sequence of NAT holds ( not A . 0 = abs a or not B . 0 = abs b or ex i being Element of NAT st ( A . (i + 1) = B . i implies not B . (i + 1) = (A . i) mod (B . i) ) or not m2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) or m1 = m2 ) then consider A1, B1 being sequence of NAT such that P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ; assume ex A2, B2 being sequence of NAT st ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ; ::_thesis: m1 = m2 then consider A2, B2 being sequence of NAT such that P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ; ( A1 = A2 & B1 = B2 ) by LM2, P1, P2; hence m1 = m2 by P1, P2; ::_thesis: verum end; end; :: deftheorem defALGOGCD defines ALGO_GCD NTALGO_1:def_1_:_ for a, b being Element of INT for b3 being Element of NAT holds ( b3 = ALGO_GCD (a,b) iff ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b3 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) ); LM3: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) ) assume AS: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) let i be Element of NAT ; ::_thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) ) assume AS1: B . i <> 0 ; ::_thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) set k = (A . i) gcd (B . i); Q1: A . (i + 1) = B . i by AS; Q2: B . (i + 1) = (A . i) mod (B . i) by AS; P1: (A . i) gcd (B . i) divides A . (i + 1) by Q1, INT_2:def_2; P2: (A . i) gcd (B . i) divides B . (i + 1) proof X1: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1; X2: (A . i) gcd (B . i) divides A . i by INT_2:def_2; X3: (A . i) gcd (B . i) divides B . i by INT_2:def_2; X4: ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by X2, INT_1:def_3; ex t being Integer st B . i = ((A . i) gcd (B . i)) * t by X3, INT_1:def_3; then consider s, t being Integer such that X5: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by X1, X4; B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by X5; hence (A . i) gcd (B . i) divides B . (i + 1) by INT_1:def_3; ::_thesis: verum end; for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds m divides (A . i) gcd (B . i) proof let m be Integer; ::_thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) ) assume P3: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; ::_thesis: m divides (A . i) gcd (B . i) then P31: m divides B . i by AS; P32: m divides A . i proof B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1; then X1: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ; X21: ex s being Integer st B . i = m * s by INT_1:def_3, P31; X22: ex t being Integer st B . (i + 1) = m * t by INT_1:def_3, P3; consider s, t being Integer such that X4: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by X1, X21, X22; A . i = m * (s + (((A . i) div (B . i)) * t)) by X4; hence m divides A . i by INT_1:def_3; ::_thesis: verum end; thus m divides (A . i) gcd (B . i) by P31, P32, INT_2:def_2; ::_thesis: verum end; hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by P1, P2, INT_2:def_2; ::_thesis: verum end; LM4: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) ) assume AS1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) defpred S1[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) ); P0: S1[ 0 ] ; PN: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume PN1: S1[i] ; ::_thesis: S1[i + 1] ( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) ) proof assume PN2: B . (i + 1) <> 0 ; ::_thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) B . i <> 0 proof assume PN4: B . i = 0 ; ::_thesis: contradiction B . (i + 1) = (A . i) mod (B . i) by AS1; hence contradiction by PN2, PN4, INT_1:def_10; ::_thesis: verum end; hence (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) by PN1, AS1, LM3; ::_thesis: verum end; hence S1[i + 1] ; ::_thesis: verum end; for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, PN); hence for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; ::_thesis: verum end; LM5: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT ) assume AS1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT P1: for x being set st x in { i where i is Element of NAT : B . i = 0 } holds x in NAT proof let x be set ; ::_thesis: ( x in { i where i is Element of NAT : B . i = 0 } implies x in NAT ) assume x in { i where i is Element of NAT : B . i = 0 } ; ::_thesis: x in NAT then ex i being Element of NAT st ( x = i & B . i = 0 ) ; hence x in NAT ; ::_thesis: verum end; ex m0 being Element of NAT st B . m0 = 0 proof assume A2: for m0 being Element of NAT holds not B . m0 = 0 ; ::_thesis: contradiction A3: for i being Element of NAT holds B . (i + 1) <= (B . i) - 1 proof let i be Element of NAT ; ::_thesis: B . (i + 1) <= (B . i) - 1 A31: B . i <> 0 by A2; B . (i + 1) = (A . i) mod (B . i) by AS1; then B . (i + 1) < B . i by A31, INT_1:58; then (B . (i + 1)) + 1 <= B . i by NAT_1:13; then ((B . (i + 1)) + 1) - 1 <= (B . i) - 1 by XREAL_1:9; hence B . (i + 1) <= (B . i) - 1 ; ::_thesis: verum end; defpred S1[ Nat] means B . $1 <= (B . 0) - $1; P0: S1[ 0 ] ; P1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume P11: S1[i] ; ::_thesis: S1[i + 1] P12: B . (i + 1) <= (B . i) - 1 by A3; (B . i) - 1 <= ((B . 0) - i) - 1 by P11, XREAL_1:9; hence S1[i + 1] by XXREAL_0:2, P12; ::_thesis: verum end; A4: for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1); B . (B . 0) <= (B . 0) - (B . 0) by A4; hence contradiction by A2, NAT_1:14; ::_thesis: verum end; then consider m0 being Element of NAT such that X1: B . m0 = 0 ; m0 in { i where i is Element of NAT : B . i = 0 } by X1; hence { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by P1, TARSKI:def_3; ::_thesis: verum end; theorem :: NTALGO_1:2 for a, b being Element of INT holds ALGO_GCD (a,b) = a gcd b proof let a, b be Element of INT ; ::_thesis: ALGO_GCD (a,b) = a gcd b consider A, B being sequence of NAT such that P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by defALGOGCD; set m0 = min* { i where i is Element of NAT : B . i = 0 } ; X0: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by P1, LM5; then min* { i where i is Element of NAT : B . i = 0 } in { i where i is Element of NAT : B . i = 0 } by NAT_1:def_1; then P4: ex i being Element of NAT st ( min* { i where i is Element of NAT : B . i = 0 } = i & B . i = 0 ) ; percases ( min* { i where i is Element of NAT : B . i = 0 } = 0 or min* { i where i is Element of NAT : B . i = 0 } <> 0 ) ; supposeC1: min* { i where i is Element of NAT : B . i = 0 } = 0 ; ::_thesis: ALGO_GCD (a,b) = a gcd b thus ALGO_GCD (a,b) = (A . 0) gcd (B . 0) by P4, C1, LM6, P1 .= a gcd b by INT_2:34, P1 ; ::_thesis: verum end; suppose min* { i where i is Element of NAT : B . i = 0 } <> 0 ; ::_thesis: ALGO_GCD (a,b) = a gcd b then 1 <= min* { i where i is Element of NAT : B . i = 0 } by NAT_1:14; then 1 - 1 <= (min* { i where i is Element of NAT : B . i = 0 } ) - 1 by XREAL_1:9; then reconsider m1 = (min* { i where i is Element of NAT : B . i = 0 } ) - 1 as Element of NAT by INT_1:3; X1: B . m1 <> 0 proof assume B . m1 = 0 ; ::_thesis: contradiction then X11: m1 in { i where i is Element of NAT : B . i = 0 } ; (min* { i where i is Element of NAT : B . i = 0 } ) - 1 < (min* { i where i is Element of NAT : B . i = 0 } ) - 0 by XREAL_1:15; hence contradiction by X11, X0, NAT_1:def_1; ::_thesis: verum end; then X2: (A . 0) gcd (B . 0) = (A . m1) gcd (B . m1) by P1, LM4; P3: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by LM3, X1, P1; (A . (min* { i where i is Element of NAT : B . i = 0 } )) gcd (B . (min* { i where i is Element of NAT : B . i = 0 } )) = ALGO_GCD (a,b) by P1, LM6, P4; hence ALGO_GCD (a,b) = a gcd b by P3, INT_2:34, X2, P1; ::_thesis: verum end; end; end; begin scheme :: NTALGO_1:sch 1 QuadChoiceRec{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F3(), F8() -> Element of F4(), P1[ set , set , set , set , set , set , set , set , set ] } : ex f being Function of NAT,F1() ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,F4() st ( f . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) ) provided A1: for n being Element of NAT for x being Element of F1() for y being Element of F2() for z being Element of F3() for w being Element of F4() ex x1 being Element of F1() ex y1 being Element of F2() ex z1 being Element of F3() ex w1 being Element of F4() st P1[n,x,y,z,w,x1,y1,z1,w1] proof defpred S1[ set , set , set , set , set ] means P1[$1,$2 `1 ,$2 `2 ,$3 `1 ,$3 `2 ,$4 `1 ,$4 `2 ,$5 `1 ,$5 `2 ]; A2: for n being Element of NAT for x being Element of [:F1(),F2():] for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w] proof let n be Element of NAT ; ::_thesis: for x being Element of [:F1(),F2():] for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w] let x be Element of [:F1(),F2():]; ::_thesis: for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w] let y be Element of [:F3(),F4():]; ::_thesis: ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w] ( x `1 is Element of F1() & x `2 is Element of F2() & y `1 is Element of F3() & y `2 is Element of F4() ) by MCART_1:10; then consider ai being Element of F1(), bi being Element of F2(), ci being Element of F3(), di being Element of F4() such that A3: P1[n,x `1 ,x `2 ,y `1 ,y `2 ,ai,bi,ci,di] by A1; reconsider z = [ai,bi] as Element of [:F1(),F2():] by ZFMISC_1:87; reconsider w = [ci,di] as Element of [:F3(),F4():] by ZFMISC_1:87; take z ; ::_thesis: ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w] take w ; ::_thesis: S1[n,x,y,z,w] ( [ai,bi] `1 = ai & [ai,bi] `2 = bi & [ci,di] `1 = ci & [ci,di] `2 = di ) by MCART_1:7; hence S1[n,x,y,z,w] by A3; ::_thesis: verum end; reconsider AB0 = [F5(),F6()] as Element of [:F1(),F2():] by ZFMISC_1:87; reconsider CD0 = [F7(),F8()] as Element of [:F3(),F4():] by ZFMISC_1:87; consider fg being Function of NAT,[:F1(),F2():], hi being Function of NAT,[:F3(),F4():] such that A4: fg . 0 = AB0 and A41: hi . 0 = CD0 and A5: for e being Element of NAT holds S1[e,fg . e,hi . e,fg . (e + 1),hi . (e + 1)] from RECDEF_2:sch_3(A2); take pr1 fg ; ::_thesis: ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,F4() st ( (pr1 fg) . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,g . n,h . n,i . n,(pr1 fg) . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) ) take pr2 fg ; ::_thesis: ex h being Function of NAT,F3() ex i being Function of NAT,F4() st ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,h . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),h . (n + 1),i . (n + 1)] ) ) take pr1 hi ; ::_thesis: ex i being Function of NAT,F4() st ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),i . (n + 1)] ) ) take pr2 hi ; ::_thesis: ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)] ) ) ( (fg . 0) `1 = (pr1 fg) . 0 & (fg . 0) `2 = (pr2 fg) . 0 & (hi . 0) `1 = (pr1 hi) . 0 & (hi . 0) `2 = (pr2 hi) . 0 ) by FUNCT_2:def_5, FUNCT_2:def_6; hence ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() ) by A4, A41, XTUPLE_0:def_2, XTUPLE_0:def_3; ::_thesis: for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)] let i be Element of NAT ; ::_thesis: P1[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)] A6: ( (fg . (i + 1)) `1 = (pr1 fg) . (i + 1) & (fg . (i + 1)) `2 = (pr2 fg) . (i + 1) & (hi . (i + 1)) `1 = (pr1 hi) . (i + 1) & (hi . (i + 1)) `2 = (pr2 hi) . (i + 1) ) by FUNCT_2:def_5, FUNCT_2:def_6; ( (fg . i) `1 = (pr1 fg) . i & (fg . i) `2 = (pr2 fg) . i & (hi . i) `1 = (pr1 hi) . i & (hi . i) `2 = (pr2 hi) . i ) by FUNCT_2:def_5, FUNCT_2:def_6; hence P1[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)] by A5, A6; ::_thesis: verum end; EXLM1: for x, y being Element of INT ex g, w, q, t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) proof let x, y be Element of INT ; ::_thesis: ex g, w, q, t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) defpred S1[ Nat, Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer] means ( $6 = $4 div $5 & $7 = $4 mod $5 & $8 = $5 & $9 = $7 ); A1: for n being Element of NAT for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1] proof let n be Element of NAT ; ::_thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1] let x, y, z, w be Element of INT ; ::_thesis: ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1] reconsider x1 = z div w as Element of INT by INT_1:def_2; reconsider y1 = z mod w as Element of INT by INT_1:def_2; set z1 = w; set w1 = y1; take x1 ; ::_thesis: ex y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1] take y1 ; ::_thesis: ex z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1] take w ; ::_thesis: ex w1 being Element of INT st S1[n,x,y,z,w,x1,y1,w,w1] take y1 ; ::_thesis: S1[n,x,y,z,w,x1,y1,w,y1] thus S1[n,x,y,z,w,x1,y1,w,y1] ; ::_thesis: verum end; reconsider i1 = 1 as Element of INT by INT_1:def_2; reconsider i0 = 0 as Element of INT by INT_1:def_2; consider q, t, g, w being sequence of INT such that P1: ( q . 0 = i0 & t . 0 = i0 & g . 0 = x & w . 0 = y & ( for i being Element of NAT holds S1[i,q . i,t . i,g . i,w . i,q . (i + 1),t . (i + 1),g . (i + 1),w . (i + 1)] ) ) from NTALGO_1:sch_1(A1); defpred S2[ Nat, Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer] means ( $6 = $4 & $7 = $5 & $8 = $2 - ((q . ($1 + 1)) * $4) & $9 = $3 - ((q . ($1 + 1)) * $5) ); A2: for n being Element of NAT for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1] proof let n be Element of NAT ; ::_thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1] let x, y, z, w be Element of INT ; ::_thesis: ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1] reconsider qn1 = q . (n + 1) as Element of INT ; set x1 = z; set y1 = w; reconsider z1 = x - ((q . (n + 1)) * z) as Element of INT by INT_1:def_2; reconsider w1 = y - ((q . (n + 1)) * w) as Element of INT by INT_1:def_2; take z ; ::_thesis: ex y1, z1, w1 being Element of INT st S2[n,x,y,z,w,z,y1,z1,w1] take w ; ::_thesis: ex z1, w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1] take z1 ; ::_thesis: ex w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1] take w1 ; ::_thesis: S2[n,x,y,z,w,z,w,z1,w1] thus S2[n,x,y,z,w,z,w,z1,w1] ; ::_thesis: verum end; consider a, b, u, v being sequence of INT such that P2: ( a . 0 = i1 & b . 0 = i0 & u . 0 = i0 & v . 0 = i1 & ( for i being Element of NAT holds S2[i,a . i,b . i,u . i,v . i,a . (i + 1),b . (i + 1),u . (i + 1),v . (i + 1)] ) ) from NTALGO_1:sch_1(A2); take g ; ::_thesis: ex w, q, t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take w ; ::_thesis: ex q, t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take q ; ::_thesis: ex t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take t ; ::_thesis: ex a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take a ; ::_thesis: ex b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take b ; ::_thesis: ex v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take v ; ::_thesis: ex u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) take u ; ::_thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) thus ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by P1, P2; ::_thesis: verum end; EXLM2: for x, y being Element of INT for g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT st a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) holds ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) proof let x, y be Element of INT ; ::_thesis: for g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT st a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) holds ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) let g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 be sequence of INT; ::_thesis: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) implies ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) ) assume P1: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) ) ; ::_thesis: ( not a2 . 0 = 1 or not b2 . 0 = 0 or not g2 . 0 = x or not q2 . 0 = 0 or not u2 . 0 = 0 or not v2 . 0 = 1 or not w2 . 0 = y or not t2 . 0 = 0 or ex i being Element of NAT st ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) implies not w2 . (i + 1) = t2 . (i + 1) ) or ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) ) assume P2: ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) ) ; ::_thesis: ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) defpred S1[ Nat] means ( g1 . $1 = g2 . $1 & w1 . $1 = w2 . $1 & q1 . $1 = q2 . $1 & t1 . $1 = t2 . $1 & a1 . $1 = a2 . $1 & b1 . $1 = b2 . $1 & v1 . $1 = v2 . $1 & u1 . $1 = u2 . $1 ); P0: S1[ 0 ] by P1, P2; PN: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume PN1: S1[n] ; ::_thesis: S1[n + 1] X1: q1 . (n + 1) = (g2 . n) div (w2 . n) by P1, PN1 .= q2 . (n + 1) by P2 ; X2: t1 . (n + 1) = (g2 . n) mod (w2 . n) by P1, PN1 .= t2 . (n + 1) by P2 ; X3: a1 . (n + 1) = u2 . n by P1, PN1 .= a2 . (n + 1) by P2 ; X4: b1 . (n + 1) = v2 . n by PN1, P1 .= b2 . (n + 1) by P2 ; X5: g1 . (n + 1) = w2 . n by PN1, P1 .= g2 . (n + 1) by P2 ; X6: u1 . (n + 1) = (a2 . n) - ((q1 . (n + 1)) * (u2 . n)) by P1, PN1 .= u2 . (n + 1) by P2, X1 ; X7: v1 . (n + 1) = (b2 . n) - ((q1 . (n + 1)) * (v2 . n)) by PN1, P1 .= v2 . (n + 1) by P2, X1 ; w1 . (n + 1) = t2 . (n + 1) by X2, P1 .= w2 . (n + 1) by P2 ; hence S1[n + 1] by X1, X2, X3, X4, X5, X6, X7; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, PN); hence ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) by FUNCT_2:def_8; ::_thesis: verum end; definition let x, y be Element of INT ; func ALGO_EXGCD (x,y) -> Element of [:INT,INT,INT:] means :defALGOEXGCD: :: NTALGO_1:def 2 ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies it = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies it = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ); existence ex b1 being Element of [:INT,INT,INT:] ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) proof consider g, w, q, t, a, b, v, u being sequence of INT such that P1: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by EXLM1; set istop = min* { i where i is Element of NAT : w . i = 0 } ; now__::_thesis:_ex_xx_being_Element_of_[:INT,INT,INT:]_st_ (_(_0_<=_g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)_implies_xx_=_[(a_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)),(b_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)),(g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))]_)_&_(_g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)_<_0_implies_xx_=_[(-_(a_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))),(-_(b_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))),(-_(g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)))]_)_) percases ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) or g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ) ; supposeC1: 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) ; ::_thesis: ex xx being Element of [:INT,INT,INT:] st ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] in [:INT,INT,INT:] by MCART_1:69; hence ex xx being Element of [:INT,INT,INT:] st ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C1; ::_thesis: verum end; supposeC2: g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ; ::_thesis: ex xx being Element of [:INT,INT,INT:] st ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) X1: - (g . (min* { i where i is Element of NAT : w . i = 0 } )) in INT by INT_1:def_2; ( - (a . (min* { i where i is Element of NAT : w . i = 0 } )) in INT & - (b . (min* { i where i is Element of NAT : w . i = 0 } )) in INT ) by INT_1:def_2; then [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] in [:INT,INT,INT:] by MCART_1:69, X1; hence ex xx being Element of [:INT,INT,INT:] st ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C2; ::_thesis: verum end; end; end; then consider xx being Element of [:INT,INT,INT:] such that P2: ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) ; take xx ; ::_thesis: ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) thus ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) by P1, P2; ::_thesis: verum end; uniqueness for b1, b2 being Element of [:INT,INT,INT:] st ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) holds b1 = b2 proof let s1, s2 be Element of [:INT,INT,INT:]; ::_thesis: ( ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies s1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies s2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) implies s1 = s2 ) assume A1: ex g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT ex istop1 being Element of NAT st ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { i where i is Element of NAT : w1 . i = 0 } & ( 0 <= g1 . istop1 implies s1 = [(a1 . istop1),(b1 . istop1),(g1 . istop1)] ) & ( g1 . istop1 < 0 implies s1 = [(- (a1 . istop1)),(- (b1 . istop1)),(- (g1 . istop1))] ) ) ; ::_thesis: ( for g, w, q, t, a, b, v, u being sequence of INT for istop being Element of NAT holds ( not a . 0 = 1 or not b . 0 = 0 or not g . 0 = x or not q . 0 = 0 or not u . 0 = 0 or not v . 0 = 1 or not w . 0 = y or not t . 0 = 0 or ex i being Element of NAT st ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) implies not w . (i + 1) = t . (i + 1) ) or not istop = min* { i where i is Element of NAT : w . i = 0 } or ( 0 <= g . istop & not s2 = [(a . istop),(b . istop),(g . istop)] ) or ( g . istop < 0 & not s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) or s1 = s2 ) assume A2: ex g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT ex istop2 being Element of NAT st ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { i where i is Element of NAT : w2 . i = 0 } & ( 0 <= g2 . istop2 implies s2 = [(a2 . istop2),(b2 . istop2),(g2 . istop2)] ) & ( g2 . istop2 < 0 implies s2 = [(- (a2 . istop2)),(- (b2 . istop2)),(- (g2 . istop2))] ) ) ; ::_thesis: s1 = s2 consider g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT, istop1 being Element of NAT such that P1: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { k where k is Element of NAT : w1 . k = 0 } & ( 0 <= g1 . istop1 implies s1 = [(a1 . istop1),(b1 . istop1),(g1 . istop1)] ) & ( g1 . istop1 < 0 implies s1 = [(- (a1 . istop1)),(- (b1 . istop1)),(- (g1 . istop1))] ) ) by A1; consider g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT, istop2 being Element of NAT such that P2: ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { k where k is Element of NAT : w2 . k = 0 } & ( 0 <= g2 . istop2 implies s2 = [(a2 . istop2),(b2 . istop2),(g2 . istop2)] ) & ( g2 . istop2 < 0 implies s2 = [(- (a2 . istop2)),(- (b2 . istop2)),(- (g2 . istop2))] ) ) by A2; ( g1 = g2 & w1 = w2 & a1 = a2 & b1 = b2 ) by P1, P2, EXLM2; hence s1 = s2 by P1, P2; ::_thesis: verum end; end; :: deftheorem defALGOEXGCD defines ALGO_EXGCD NTALGO_1:def_2_:_ for x, y being Element of INT for b3 being Element of [:INT,INT,INT:] holds ( b3 = ALGO_EXGCD (x,y) iff ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b3 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b3 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) ); LM3G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) ) assume AS: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) let i be Element of NAT ; ::_thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) ) assume AS1: B . i <> 0 ; ::_thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) set k = (A . i) gcd (B . i); Q1: A . (i + 1) = B . i by AS; Q2: B . (i + 1) = (A . i) mod (B . i) by AS; P1: (A . i) gcd (B . i) divides A . (i + 1) by Q1, INT_2:def_2; P2: (A . i) gcd (B . i) divides B . (i + 1) proof X1: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1; X2: (A . i) gcd (B . i) divides A . i by INT_2:def_2; X3: (A . i) gcd (B . i) divides B . i by INT_2:def_2; X4: ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by X2, INT_1:def_3; ex t being Integer st B . i = ((A . i) gcd (B . i)) * t by X3, INT_1:def_3; then consider s, t being Integer such that X5: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by X1, X4; B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by X5; hence (A . i) gcd (B . i) divides B . (i + 1) by INT_1:def_3; ::_thesis: verum end; for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds m divides (A . i) gcd (B . i) proof let m be Integer; ::_thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) ) assume P3: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; ::_thesis: m divides (A . i) gcd (B . i) then P31: m divides B . i by AS; P32: m divides A . i proof B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1; then X1: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ; X21: ex s being Integer st B . i = m * s by INT_1:def_3, P31; X22: ex t being Integer st B . (i + 1) = m * t by INT_1:def_3, P3; consider s, t being Integer such that X4: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by X1, X21, X22; A . i = m * (s + (((A . i) div (B . i)) * t)) by X4; hence m divides A . i by INT_1:def_3; ::_thesis: verum end; thus m divides (A . i) gcd (B . i) by P31, P32, INT_2:def_2; ::_thesis: verum end; hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by P1, P2, INT_2:def_2; ::_thesis: verum end; LM4G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) ) assume AS1: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) defpred S1[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) ); P0: S1[ 0 ] ; PN: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume PN1: S1[i] ; ::_thesis: S1[i + 1] ( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) ) proof assume PN2: B . (i + 1) <> 0 ; ::_thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) B . i <> 0 proof assume PN4: B . i = 0 ; ::_thesis: contradiction B . (i + 1) = (A . i) mod (B . i) by AS1; hence contradiction by PN2, PN4, INT_1:def_10; ::_thesis: verum end; hence (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) by PN1, AS1, LM3G; ::_thesis: verum end; hence S1[i + 1] ; ::_thesis: verum end; for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, PN); hence for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; ::_thesis: verum end; theorem INT157A: :: NTALGO_1:3 for i2, i1 being Integer st i2 <= 0 holds i1 mod i2 <= 0 proof let i2, i1 be Integer; ::_thesis: ( i2 <= 0 implies i1 mod i2 <= 0 ) assume A1: i2 <= 0 ; ::_thesis: i1 mod i2 <= 0 percases ( i2 < 0 or i2 = 0 ) by A1; supposeA2: i2 < 0 ; ::_thesis: i1 mod i2 <= 0 [\(i1 / i2)/] <= i1 / i2 by INT_1:def_6; then (i1 / i2) * i2 <= (i1 div i2) * i2 by A2, XREAL_1:65; then i1 <= (i1 div i2) * i2 by A2, XCMPLX_1:87; then i1 - ((i1 div i2) * i2) <= 0 by XREAL_1:47; hence i1 mod i2 <= 0 by INT_1:def_10; ::_thesis: verum end; suppose i2 = 0 ; ::_thesis: i1 mod i2 <= 0 hence i1 mod i2 <= 0 by INT_1:def_10; ::_thesis: verum end; end; end; theorem INT158A: :: NTALGO_1:4 for i2, i1 being Integer st i2 < 0 holds - (i1 mod i2) < - i2 proof let i2, i1 be Integer; ::_thesis: ( i2 < 0 implies - (i1 mod i2) < - i2 ) assume A1: i2 < 0 ; ::_thesis: - (i1 mod i2) < - i2 (i1 / i2) - 1 < [\(i1 / i2)/] by INT_1:def_6; then (i1 div i2) * i2 < ((i1 / i2) - 1) * i2 by A1, XREAL_1:69; then (i1 div i2) * i2 < ((i1 / i2) * i2) - (1 * i2) ; then (i1 div i2) * i2 < i1 - i2 by A1, XCMPLX_1:87; then ((i1 div i2) * i2) - i1 < (i1 - i2) - i1 by XREAL_1:14; then - (i1 - ((i1 div i2) * i2)) < - i2 ; hence - (i1 mod i2) < - i2 by A1, INT_1:def_10; ::_thesis: verum end; theorem LM5G1: :: NTALGO_1:5 for x, y being Element of INT st abs y <> 0 holds abs (x mod y) < abs y proof let x, y be Element of INT ; ::_thesis: ( abs y <> 0 implies abs (x mod y) < abs y ) assume A1: abs y <> 0 ; ::_thesis: abs (x mod y) < abs y percases ( 0 < y or y <= 0 ) ; supposeC1: 0 < y ; ::_thesis: abs (x mod y) < abs y then C2: x mod y < y by INT_1:58; 0 <= x mod y by INT_1:57, C1; then C3: abs (x mod y) < y by ABSVALUE:def_1, C2; y <= abs y by ABSVALUE:4; hence abs (x mod y) < abs y by C3, XXREAL_0:2; ::_thesis: verum end; supposeC4: y <= 0 ; ::_thesis: abs (x mod y) < abs y C40P: y <> 0 by ABSVALUE:2, A1; C41: - (x mod y) < - y by INT158A, C40P, C4; XX1: x mod y <= 0 by C4, INT157A; C42: abs (x mod y) = - (x mod y) proof percases ( x mod y = 0 or x mod y <> 0 ) ; suppose x mod y = 0 ; ::_thesis: abs (x mod y) = - (x mod y) hence abs (x mod y) = - (x mod y) by ABSVALUE:2; ::_thesis: verum end; suppose x mod y <> 0 ; ::_thesis: abs (x mod y) = - (x mod y) hence abs (x mod y) = - (x mod y) by ABSVALUE:def_1, XX1; ::_thesis: verum end; end; end; thus abs (x mod y) < abs y by C42, C41, C40P, C4, ABSVALUE:def_1; ::_thesis: verum end; end; end; LM5G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT proof let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT ) assume AS1: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT LMM: for x being set st x in { i where i is Element of NAT : B . i = 0 } holds x in NAT proof let x be set ; ::_thesis: ( x in { i where i is Element of NAT : B . i = 0 } implies x in NAT ) assume x in { i where i is Element of NAT : B . i = 0 } ; ::_thesis: x in NAT then ex i being Element of NAT st ( x = i & B . i = 0 ) ; hence x in NAT ; ::_thesis: verum end; ex m0 being Element of NAT st B . m0 = 0 proof assume A20: for m0 being Element of NAT holds not B . m0 = 0 ; ::_thesis: contradiction A2: for m0 being Element of NAT holds abs (B . m0) <> 0 proof let m0 be Element of NAT ; ::_thesis: abs (B . m0) <> 0 B . m0 <> 0 by A20; hence abs (B . m0) <> 0 by ABSVALUE:2; ::_thesis: verum end; A3: for i being Element of NAT holds abs (B . (i + 1)) <= (abs (B . i)) - 1 proof let i be Element of NAT ; ::_thesis: abs (B . (i + 1)) <= (abs (B . i)) - 1 abs (B . (i + 1)) = abs ((A . i) mod (B . i)) by AS1; then abs (B . (i + 1)) < abs (B . i) by A2, LM5G1; then (abs (B . (i + 1))) + 1 <= abs (B . i) by NAT_1:13; then ((abs (B . (i + 1))) + 1) - 1 <= (abs (B . i)) - 1 by XREAL_1:9; hence abs (B . (i + 1)) <= (abs (B . i)) - 1 ; ::_thesis: verum end; defpred S1[ Nat] means abs (B . $1) <= (abs (B . 0)) - $1; P0: S1[ 0 ] ; P1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume P11: S1[i] ; ::_thesis: S1[i + 1] P12: abs (B . (i + 1)) <= (abs (B . i)) - 1 by A3; (abs (B . i)) - 1 <= ((abs (B . 0)) - i) - 1 by P11, XREAL_1:9; hence S1[i + 1] by XXREAL_0:2, P12; ::_thesis: verum end; A4: for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1); abs (B . (abs (B . 0))) <= (abs (B . 0)) - (abs (B . 0)) by A4; hence contradiction by A2, NAT_1:14; ::_thesis: verum end; then consider m0 being Element of NAT such that X1: B . m0 = 0 ; m0 in { i where i is Element of NAT : B . i = 0 } by X1; hence { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by LMM, TARSKI:def_3; ::_thesis: verum end; LM6G: for a being Element of INT holds a gcd 0 = abs a by WSIERP_1:8; LM7G: for x, y being Element of INT for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) proof let x, y be Element of INT ; ::_thesis: for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) let g, w, q, t be sequence of INT; ::_thesis: for a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) let a, b, v, u be sequence of INT; ::_thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) implies for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) ) assume AS: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) ; ::_thesis: for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) defpred S1[ Nat] means ( w . $1 <> 0 implies ( ((a . $1) * x) + ((b . $1) * y) = g . $1 & ((a . ($1 + 1)) * x) + ((b . ($1 + 1)) * y) = g . ($1 + 1) ) ); P0: S1[ 0 ] proof assume w . 0 <> 0 ; ::_thesis: ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) ) reconsider I0 = 0 as Element of NAT ; ((a . (I0 + 1)) * x) + ((b . (I0 + 1)) * y) = ((u . 0) * x) + ((b . (I0 + 1)) * y) by AS .= (0 * x) + (1 * y) by AS .= g . (I0 + 1) by AS ; hence ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) ) by AS; ::_thesis: verum end; P1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume P12A: S1[i] ; ::_thesis: S1[i + 1] assume ASX: w . (i + 1) <> 0 ; ::_thesis: ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) ) XX1: w . i <> 0 proof assume XX2: w . i = 0 ; ::_thesis: contradiction t . (i + 1) = (g . i) mod (w . i) by AS .= 0 by XX2, INT_1:def_10 ; hence contradiction by AS, ASX; ::_thesis: verum end; ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = ((u . (i + 1)) * x) + ((b . ((i + 1) + 1)) * y) by AS .= ((u . (i + 1)) * x) + ((v . (i + 1)) * y) by AS .= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + ((v . (i + 1)) * y) by AS .= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + (((b . i) - ((q . (i + 1)) * (v . i))) * y) by AS .= (g . i) - ((q . (i + 1)) * (((u . i) * x) + ((v . i) * y))) by XX1, P12A .= (g . i) - ((q . (i + 1)) * (((a . (i + 1)) * x) + ((v . i) * y))) by AS .= (g . i) - ((q . (i + 1)) * (g . (i + 1))) by XX1, P12A, AS .= (g . i) - (((g . i) div (w . i)) * (g . (i + 1))) by AS .= (g . i) - (((g . i) div (w . i)) * (w . i)) by AS .= (g . i) mod (w . i) by INT_1:def_10, XX1 .= t . (i + 1) by AS .= w . (i + 1) by AS .= g . ((i + 1) + 1) by AS ; hence ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) ) by XX1, P12A; ::_thesis: verum end; for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1); hence for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) ; ::_thesis: verum end; theorem Th2: :: NTALGO_1:6 for x, y being Element of INT holds ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ) proof let x, y be Element of INT ; ::_thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ) consider g, w, q, t, a, b, v, u being sequence of INT, istop being Element of NAT such that P0: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies ALGO_EXGCD (x,y) = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies ALGO_EXGCD (x,y) = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) by defALGOEXGCD; P2X: now__::_thesis:_for_i_being_Element_of_NAT_holds_ (_g_._(i_+_1)_=_w_._i_&_w_._(i_+_1)_=_(g_._i)_mod_(w_._i)_) let i be Element of NAT ; ::_thesis: ( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) ) thus g . (i + 1) = w . i by P0; ::_thesis: w . (i + 1) = (g . i) mod (w . i) thus w . (i + 1) = t . (i + 1) by P0 .= (g . i) mod (w . i) by P0 ; ::_thesis: verum end; X0: { i where i is Element of NAT : w . i = 0 } is non empty Subset of NAT by P0, P2X, LM5G; then istop in { i where i is Element of NAT : w . i = 0 } by P0, NAT_1:def_1; then P4: ex i being Element of NAT st ( istop = i & w . i = 0 ) ; XX3: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) proof percases ( 0 <= g . istop or g . istop < 0 ) ; suppose 0 <= g . istop ; ::_thesis: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) then abs (g . istop) = g . istop by ABSVALUE:def_1; hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, MCART_1:def_7; ::_thesis: verum end; supposeXX32: g . istop < 0 ; ::_thesis: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) then abs (g . istop) = - (g . istop) by ABSVALUE:def_1; hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, XX32, MCART_1:def_7; ::_thesis: verum end; end; end; percases ( istop = 0 or istop <> 0 ) ; supposeC1: istop = 0 ; ::_thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ) thus R1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P0, P4, LM6G, XX3, C1; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ::_thesis: verum proof percases ( 0 <= g . istop or g . istop < 0 ) ; supposeY11: 0 <= g . istop ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y Y13: (ALGO_EXGCD (x,y)) `1_3 = 1 by C1, P0, Y11, MCART_1:def_5; (ALGO_EXGCD (x,y)) `2_3 = 0 by C1, P0, MCART_1:def_6; hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y11, P0, C1, XX3, ABSVALUE:def_1, Y13, R1; ::_thesis: verum end; supposeXX32: g . istop < 0 ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y Y13: (ALGO_EXGCD (x,y)) `1_3 = - 1 by C1, P0, XX32, MCART_1:def_5; (ALGO_EXGCD (x,y)) `2_3 = 0 by P0, C1, MCART_1:def_6; hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by P0, C1, XX3, ABSVALUE:def_1, XX32, Y13, R1; ::_thesis: verum end; end; end; end; suppose istop <> 0 ; ::_thesis: ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ) then 1 <= istop by NAT_1:14; then 1 - 1 <= istop - 1 by XREAL_1:9; then reconsider m1 = istop - 1 as Element of NAT by INT_1:3; X1: w . m1 <> 0 proof assume w . m1 = 0 ; ::_thesis: contradiction then X11: m1 in { i where i is Element of NAT : w . i = 0 } ; istop - 1 < istop - 0 by XREAL_1:15; hence contradiction by X11, P0, X0, NAT_1:def_1; ::_thesis: verum end; P5: (g . m1) gcd (w . m1) = (g . (m1 + 1)) gcd (w . (m1 + 1)) by LM3G, P0, X1, P2X; R1: (g . istop) gcd (w . istop) = (ALGO_EXGCD (x,y)) `3_3 by XX3, LM6G, P4; hence RR1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P5, X1, P2X, LM4G, P0; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y Y1: ((a . (m1 + 1)) * x) + ((b . (m1 + 1)) * y) = g . (m1 + 1) by X1, LM7G, P0; thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ::_thesis: verum proof percases ( 0 <= g . istop or g . istop < 0 ) ; supposeY11: 0 <= g . istop ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y then Y12: (ALGO_EXGCD (x,y)) `3_3 = g . istop by XX3, ABSVALUE:def_1; (ALGO_EXGCD (x,y)) `1_3 = a . istop by P0, Y11, MCART_1:def_5; hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by RR1, Y1, Y12, P0, MCART_1:def_6; ::_thesis: verum end; supposeXX32: g . istop < 0 ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y then Y12: (ALGO_EXGCD (x,y)) `3_3 = - (g . istop) by XX3, ABSVALUE:def_1; Y13: (ALGO_EXGCD (x,y)) `1_3 = - (a . istop) by P0, XX32, MCART_1:def_5; (ALGO_EXGCD (x,y)) `2_3 = - (b . istop) by P0, XX32, MCART_1:def_6; hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y1, Y12, Y13, R1, P5, X1, P2X, LM4G, P0; ::_thesis: verum end; end; end; end; end; end; definition let x, p be Element of INT ; func ALGO_INVERSE (x,p) -> Element of INT means :definverse: :: NTALGO_1:def 3 for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & it = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies it = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies it = {} ) ); existence ex b1 being Element of INT st for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) ) proof reconsider y = x mod p as Element of INT by INT_1:def_2; now__::_thesis:_ex_s_being_Element_of_INT_st_ (_(_(ALGO_EXGCD_(p,y))_`3_3_=_1_implies_(_(_(ALGO_EXGCD_(p,y))_`2_3_<_0_implies_ex_z_being_Element_of_INT_st_ (_z_=_(ALGO_EXGCD_(p,y))_`2_3_&_s_=_p_+_z_)_)_&_(_0_<=_(ALGO_EXGCD_(p,y))_`2_3_implies_s_=_(ALGO_EXGCD_(p,y))_`2_3_)_)_)_&_(_(ALGO_EXGCD_(p,y))_`3_3_<>_1_implies_s_=_{}_)_) percases ( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 ) ; supposeC1: (ALGO_EXGCD (p,y)) `3_3 = 1 ; ::_thesis: ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) now__::_thesis:_ex_s_being_Element_of_INT_st_ (_(_(ALGO_EXGCD_(p,y))_`2_3_<_0_implies_ex_z_being_Element_of_INT_st_ (_z_=_(ALGO_EXGCD_(p,y))_`2_3_&_s_=_p_+_z_)_)_&_(_0_<=_(ALGO_EXGCD_(p,y))_`2_3_implies_s_=_(ALGO_EXGCD_(p,y))_`2_3_)_&_(_(ALGO_EXGCD_(p,y))_`3_3_<>_1_implies_s_=_{}_)_) percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ; supposeC11: (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) reconsider z = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ; reconsider s = p + z as Element of INT by INT_1:def_2; ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ; hence ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by C11, C1; ::_thesis: verum end; supposeC12: 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) reconsider s = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ; thus ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by C12, C1; ::_thesis: verum end; end; end; hence ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ; ::_thesis: verum end; supposeC2: (ALGO_EXGCD (p,y)) `3_3 <> 1 ; ::_thesis: ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) reconsider s = {} as Element of INT by INT_1:def_2; ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ; hence ex s being Element of INT st ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by C2; ::_thesis: verum end; end; end; then consider s being Element of INT such that Q1: ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) ; take s ; ::_thesis: for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) thus for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ) by Q1; ::_thesis: verum end; uniqueness for b1, b2 being Element of INT st ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b2 = {} ) ) ) holds b1 = b2 proof let s1, s2 be Element of INT ; ::_thesis: ( ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) implies s1 = s2 ) assume A1: for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s1 = {} ) ) ; ::_thesis: ( ex y being Element of INT st ( y = x mod p & not ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ) or s1 = s2 ) assume A2: for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies s2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s2 = {} ) ) ; ::_thesis: s1 = s2 reconsider y = x mod p as Element of INT by INT_1:def_2; thus s1 = s2 ::_thesis: verum proof percases ( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 ) ; supposeC1: (ALGO_EXGCD (p,y)) `3_3 = 1 ; ::_thesis: s1 = s2 thus s1 = s2 ::_thesis: verum proof percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ; supposeC11: (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: s1 = s2 then C12: ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) by A1, C1; ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) by A2, C1, C11; hence s1 = s2 by C12; ::_thesis: verum end; supposeC12: 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: s1 = s2 thus s1 = (ALGO_EXGCD (p,y)) `2_3 by C12, C1, A1 .= s2 by C12, C1, A2 ; ::_thesis: verum end; end; end; end; supposeC2: (ALGO_EXGCD (p,y)) `3_3 <> 1 ; ::_thesis: s1 = s2 thus s1 = {} by A1, C2 .= s2 by A2, C2 ; ::_thesis: verum end; end; end; end; end; :: deftheorem definverse defines ALGO_INVERSE NTALGO_1:def_3_:_ for x, p, b3 being Element of INT holds ( b3 = ALGO_INVERSE (x,p) iff for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b3 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b3 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b3 = {} ) ) ); LMTh30: for x, y, p being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 holds ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p proof let x, y, p be Element of INT ; ::_thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p ) assume AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 ) ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p P3P: ( (ALGO_EXGCD (p,y)) `3_3 = p gcd y & (((ALGO_EXGCD (p,y)) `1_3) * p) + (((ALGO_EXGCD (p,y)) `2_3) * y) = p gcd y ) by Th2; reconsider s1 = ((ALGO_EXGCD (p,y)) `1_3) * p as Integer ; reconsider s2 = ((ALGO_EXGCD (p,y)) `2_3) * y as Integer ; reconsider s3 = (ALGO_EXGCD (p,y)) `2_3 as Integer ; P40C2: p mod p = 0 by INT_1:50; P4: (((ALGO_EXGCD (p,y)) `1_3) * p) mod p = ((((ALGO_EXGCD (p,y)) `1_3) mod p) * (p mod p)) mod p by NAT_D:67 .= 0 by INT_4:12, P40C2 ; reconsider I0 = 0 as Element of INT by INT_1:def_2; P6: ((((ALGO_EXGCD (p,y)) `1_3) * p) + (((ALGO_EXGCD (p,y)) `2_3) * y)) mod p = ((s1 mod p) + (s2 mod p)) mod p by NAT_D:66 .= (((ALGO_EXGCD (p,y)) `2_3) * y) mod p by LMTh3, P4 ; percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ; suppose (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p then consider z being Element of INT such that A11: ( z = (ALGO_EXGCD (p,y)) `2_3 & ALGO_INVERSE (x,p) = p + z ) by definverse, AS; thus ((ALGO_INVERSE (x,p)) * x) mod p = ((p * x) + (z * x)) mod p by A11 .= (z * x) mod p by NAT_D:61 .= ((z mod p) * (x mod p)) mod p by NAT_D:67 .= ((z mod p) * ((x mod p) mod p)) mod p by LMTh3 .= 1 mod p by P6, A11, P3P, AS, NAT_D:67 ; ::_thesis: verum end; suppose 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p hence ((ALGO_INVERSE (x,p)) * x) mod p = (((ALGO_EXGCD (p,y)) `2_3) * x) mod p by definverse, AS .= ((s3 mod p) * (x mod p)) mod p by NAT_D:67 .= ((s3 mod p) * ((x mod p) mod p)) mod p by LMTh3 .= 1 mod p by P6, P3P, AS, NAT_D:67 ; ::_thesis: verum end; end; end; theorem Th3: :: NTALGO_1:7 for x, p, y being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 holds ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p proof let x, p, y be Element of INT ; ::_thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p ) assume AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 ) ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p percases ( p = 0 or p <> 0 ) ; supposeC1: p = 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p thus ((ALGO_INVERSE (x,p)) * x) mod p = 0 by C1, INT_1:def_10 .= 1 mod p by C1, INT_1:def_10 ; ::_thesis: verum end; suppose p <> 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p hence ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p by LMTh30, AS; ::_thesis: verum end; end; end; begin definition let nlist be non empty FinSequence of [:INT,INT:]; func ALGO_CRT nlist -> Element of INT means :defALGOCRT: :: NTALGO_1:def 4 ( ( len nlist = 1 implies it = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & it = (n . (len m)) mod M ) ) ); existence ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) proof percases ( len nlist = 1 or len nlist <> 1 ) ; supposeA1: len nlist = 1 ; ::_thesis: ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) then 1 in Seg (len nlist) ; then 1 in dom nlist by FINSEQ_1:def_3; then nlist . 1 in [:INT,INT:] by FINSEQ_2:11; then (nlist . 1) `1 is Element of INT by MCART_1:10; hence ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A1; ::_thesis: verum end; supposeA2: len nlist <> 1 ; ::_thesis: ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) defpred S1[ Nat, Integer, Integer] means ex x being Element of INT st ( x = (nlist . $1) `2 & $3 = $2 * x ); reconsider i1 = 1 as Element of INT by INT_1:def_1; X1: for n being Element of NAT st 1 <= n & n < len nlist holds for z being Element of INT ex y being Element of INT st S1[n,z,y] proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S1[n,z,y] ) assume X11: ( 1 <= n & n < len nlist ) ; ::_thesis: for z being Element of INT ex y being Element of INT st S1[n,z,y] let z be Element of INT ; ::_thesis: ex y being Element of INT st S1[n,z,y] n in Seg (len nlist) by X11; then n in dom nlist by FINSEQ_1:def_3; then nlist . n in [:INT,INT:] by FINSEQ_2:11; then reconsider x = (nlist . n) `2 as Element of INT by MCART_1:10; reconsider y = z * x as Element of INT by INT_1:def_2; take y ; ::_thesis: S1[n,z,y] thus S1[n,z,y] ; ::_thesis: verum end; consider m being FinSequence of INT such that X2: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds S1[i,m . i,m . (i + 1)] ) ) from RECDEF_1:sch_4(X1); II: (len m) - 1 < (len m) - 0 by XREAL_1:15; X3: for i being Nat st 1 <= i & i <= (len m) - 1 holds ex x being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex x being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) ) assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex x being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2; i is Element of NAT by ORDINAL1:def_12; hence ex x being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) by X2, X32; ::_thesis: verum end; VV2: 1 <= len m by NAT_1:14, X2; then 1 - 1 <= (len m) - 1 by XREAL_1:9; then reconsider lm = (len m) - 1 as Element of NAT by INT_1:3; defpred S2[ Nat, Integer] means ex d, x, y being Element of INT st ( x = (nlist . $1) `2 & m . ($1 + 1) = (m . $1) * x & y = m . ($1 + 1) & d = (nlist . ($1 + 1)) `2 & $2 = ALGO_INVERSE (y,d) ); X4: for n being Nat st n in Seg lm holds ex z being Element of INT st S2[n,z] proof let n be Nat; ::_thesis: ( n in Seg lm implies ex z being Element of INT st S2[n,z] ) assume X41: n in Seg lm ; ::_thesis: ex z being Element of INT st S2[n,z] X43: ( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41; then consider x being Element of INT such that X42: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x ) by X3; reconsider y = m . (n + 1) as Element of INT by INT_1:def_2; n + 1 <= ((len m) - 1) + 1 by X43, XREAL_1:6; then ( 1 <= n + 1 & n + 1 <= len m ) by NAT_1:12; then n + 1 in Seg (len nlist) by X2; then n + 1 in dom nlist by FINSEQ_1:def_3; then nlist . (n + 1) in [:INT,INT:] by FINSEQ_2:11; then reconsider d = (nlist . (n + 1)) `2 as Element of INT by MCART_1:10; reconsider w = ALGO_INVERSE (y,d) as Element of INT ; take w ; ::_thesis: S2[n,w] thus S2[n,w] by X42; ::_thesis: verum end; consider prodi being FinSequence of INT such that X5: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds S2[k,prodi . k] ) ) from FINSEQ_1:sch_5(X4); X6: len prodi = (len nlist) - 1 by X2, FINSEQ_1:def_3, X5; X7: for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) ) assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) then i in Seg lm by FINSEQ_1:1; hence ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) by X5; ::_thesis: verum end; defpred S3[ Nat, Integer] means ex d, x, y being Element of INT st ( x = (nlist . $1) `2 & m . ($1 + 1) = (m . $1) * x & y = m . ($1 + 1) & d = (nlist . ($1 + 1)) `2 & prodi . $1 = ALGO_INVERSE (y,d) & $2 = y ); X8: for n being Nat st n in Seg lm holds ex z being Element of INT st S3[n,z] proof let n be Nat; ::_thesis: ( n in Seg lm implies ex z being Element of INT st S3[n,z] ) assume X41: n in Seg lm ; ::_thesis: ex z being Element of INT st S3[n,z] ( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41; then consider d, x, y being Element of INT such that X42: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x & y = m . (n + 1) & d = (nlist . (n + 1)) `2 & prodi . n = ALGO_INVERSE (y,d) ) by X7; reconsider w = y as Element of INT ; take w ; ::_thesis: S3[n,w] thus S3[n,w] by X42; ::_thesis: verum end; consider prodc being FinSequence of INT such that X9: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds S3[k,prodc . k] ) ) from FINSEQ_1:sch_5(X8); X10: len prodc = (len nlist) - 1 by X2, FINSEQ_1:def_3, X9; X11: for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) then i in Seg lm by FINSEQ_1:1; hence ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) by X9; ::_thesis: verum end; len nlist in Seg (len nlist) by FINSEQ_1:3; then len m in dom nlist by X2, FINSEQ_1:def_3; then nlist . (len m) in [:INT,INT:] by FINSEQ_2:11; then reconsider M0 = (nlist . (len m)) `2 as Element of INT by MCART_1:10; 1 < len m by VV2, A2, X2, XXREAL_0:1; then 1 + 1 <= len m by NAT_1:13; then 2 - 1 <= (len m) - 1 by XREAL_1:9; then VV1: lm in dom prodc by X9; prodc in INT * by FINSEQ_1:def_11; then reconsider MM = prodc . ((len m) - 1) as Element of INT by VV1, FINSEQ_1:84; reconsider M = MM * M0 as Element of INT by INT_1:def_2; defpred S4[ Nat, Integer, Integer] means ex u, u0, u1 being Element of INT st ( u0 = (nlist . ($1 + 1)) `1 & u1 = (nlist . ($1 + 1)) `2 & u = ((u0 - $2) * (prodi . $1)) mod u1 & $3 = $2 + (u * (prodc . $1)) ); reconsider i1 = 1 as Element of INT by INT_1:def_1; X12: for n being Element of NAT st 1 <= n & n < len nlist holds for z being Element of INT ex y being Element of INT st S4[n,z,y] proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S4[n,z,y] ) assume X41: ( 1 <= n & n < len nlist ) ; ::_thesis: for z being Element of INT ex y being Element of INT st S4[n,z,y] let z be Element of INT ; ::_thesis: ex y being Element of INT st S4[n,z,y] ( 1 <= n + 1 & n + 1 <= len m ) by X41, X2, NAT_1:13; then n + 1 in Seg (len nlist) by X2; then n + 1 in dom nlist by FINSEQ_1:def_3; then XX: nlist . (n + 1) in [:INT,INT:] by FINSEQ_2:11; then reconsider u0 = (nlist . (n + 1)) `1 as Element of INT by MCART_1:10; reconsider u1 = (nlist . (n + 1)) `2 as Element of INT by XX, MCART_1:10; reconsider u = ((u0 - z) * (prodi . n)) mod u1 as Element of INT by INT_1:def_2; reconsider y = z + (u * (prodc . n)) as Element of INT by INT_1:def_2; take y ; ::_thesis: S4[n,z,y] thus S4[n,z,y] ; ::_thesis: verum end; 1 in Seg (len nlist) by VV2, X2; then 1 in dom nlist by FINSEQ_1:def_3; then nlist . 1 in [:INT,INT:] by FINSEQ_2:11; then reconsider L1 = (nlist . 1) `1 as Element of INT by MCART_1:10; consider n being FinSequence of INT such that X13: ( len n = len nlist & ( n . 1 = L1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds S4[i,n . i,n . (i + 1)] ) ) from RECDEF_1:sch_4(X12); X14: for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2; i is Element of NAT by ORDINAL1:def_12; hence ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) by X13, X32; ::_thesis: verum end; reconsider s = (n . (len m)) mod M as Element of INT by INT_1:def_2; ( M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & s = (n . (len m)) mod M ) ; hence ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A2, X14, X11, X2, X13, X6, X10; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of INT st ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) holds b1 = b2 proof let s1, s2 be Element of INT ; ::_thesis: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) implies s1 = s2 ) assume A1: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) ) ; ::_thesis: ( ( len nlist = 1 & not s2 = (nlist . 1) `1 ) or ( len nlist <> 1 & ( for m, n, prodc, prodi being FinSequence of INT for M0, M being Element of INT holds ( not len m = len nlist or not len n = len nlist or not len prodc = (len nlist) - 1 or not len prodi = (len nlist) - 1 or not m . 1 = 1 or ex i being Nat st ( 1 <= i & i <= (len m) - 1 & ( for d, x, y being Element of INT holds ( not x = (nlist . i) `2 or not m . (i + 1) = (m . i) * x or not y = m . (i + 1) or not d = (nlist . (i + 1)) `2 or not prodi . i = ALGO_INVERSE (y,d) or not prodc . i = y ) ) ) or not M0 = (nlist . (len m)) `2 or not M = (prodc . ((len m) - 1)) * M0 or not n . 1 = (nlist . 1) `1 or ex i being Nat st ( 1 <= i & i <= (len m) - 1 & ( for u, u0, u1 being Element of INT holds ( not u0 = (nlist . (i + 1)) `1 or not u1 = (nlist . (i + 1)) `2 or not u = ((u0 - (n . i)) * (prodi . i)) mod u1 or not n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) ) or not s2 = (n . (len m)) mod M ) ) ) or s1 = s2 ) assume A2: ( ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) ) ; ::_thesis: s1 = s2 percases ( len nlist = 1 or len nlist <> 1 ) ; supposeC1: len nlist = 1 ; ::_thesis: s1 = s2 thus s1 = s2 by A1, A2, C1; ::_thesis: verum end; supposeC2: len nlist <> 1 ; ::_thesis: s1 = s2 consider m1, n1, prodc1, prodi1 being FinSequence of INT , M01, M1 being Element of INT such that P1: ( len m1 = len nlist & len n1 = len nlist & len prodc1 = (len nlist) - 1 & len prodi1 = (len nlist) - 1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) ) & M01 = (nlist . (len m1)) `2 & M1 = (prodc1 . ((len m1) - 1)) * M01 & n1 . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n1 . i)) * (prodi1 . i)) mod u1 & n1 . (i + 1) = (n1 . i) + (u * (prodc1 . i)) ) ) & s1 = (n1 . (len m1)) mod M1 ) by C2, A1; consider m2, n2, prodc2, prodi2 being FinSequence of INT , M02, M2 being Element of INT such that P2: ( len m2 = len nlist & len n2 = len nlist & len prodc2 = (len nlist) - 1 & len prodi2 = (len nlist) - 1 & m2 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) ) & M02 = (nlist . (len m2)) `2 & M2 = (prodc2 . ((len m2) - 1)) * M02 & n2 . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n2 . i)) * (prodi2 . i)) mod u1 & n2 . (i + 1) = (n2 . i) + (u * (prodc2 . i)) ) ) & s2 = (n2 . (len m2)) mod M2 ) by C2, A2; defpred S1[ Nat] means ( 1 <= $1 & $1 <= len m1 implies m1 . $1 = m2 . $1 ); Q50: S1[ 0 ] ; Q51: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume Q52: S1[i] ; ::_thesis: S1[i + 1] assume ( 1 <= i + 1 & i + 1 <= len m1 ) ; ::_thesis: m1 . (i + 1) = m2 . (i + 1) then Q54: ( 1 - 1 <= (i + 1) - 1 & (i + 1) - 1 <= (len m1) - 1 ) by XREAL_1:9; Q55: (len m1) - 1 <= (len m1) - 0 by XREAL_1:13; percases ( i = 0 or i <> 0 ) ; supposeC1: i = 0 ; ::_thesis: m1 . (i + 1) = m2 . (i + 1) thus m1 . (i + 1) = m2 . (i + 1) by P1, P2, C1; ::_thesis: verum end; supposeQ56P: i <> 0 ; ::_thesis: m1 . (i + 1) = m2 . (i + 1) then Q56: 1 <= i by NAT_1:14; Q57: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1, Q56, Q54; ( 1 <= i & i <= (len m2) - 1 ) by Q56P, Q54, P1, P2, NAT_1:14; then ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2; hence m1 . (i + 1) = m2 . (i + 1) by Q57, Q54, Q52, Q55, Q56P, NAT_1:14, XXREAL_0:2; ::_thesis: verum end; end; end; Q0: for k being Nat holds S1[k] from NAT_1:sch_2(Q50, Q51); QQ3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_prodc1_holds_ prodc1_._i_=_prodc2_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len prodc1 implies prodc1 . i = prodc2 . i ) assume ASX0: ( 1 <= i & i <= len prodc1 ) ; ::_thesis: prodc1 . i = prodc2 . i then X1: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1; ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2, ASX0, P1; hence prodc1 . i = prodc2 . i by X1, FINSEQ_1:14, P1, P2, Q0; ::_thesis: verum end; then Q3: prodc1 = prodc2 by FINSEQ_1:14, P1, P2; Q3A: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_prodi1_holds_ prodi1_._i_=_prodi2_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len prodi1 implies prodi1 . i = prodi2 . i ) assume ASX0: ( 1 <= i & i <= len prodi1 ) ; ::_thesis: prodi1 . i = prodi2 . i then X1: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m1 . (i + 1) = (m1 . i) * x & y = m1 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by P1; ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m2 . (i + 1) = (m2 . i) * x & y = m2 . (i + 1) & d = (nlist . (i + 1)) `2 & prodi2 . i = ALGO_INVERSE (y,d) & prodc2 . i = y ) by P2, ASX0, P1; hence prodi1 . i = prodi2 . i by X1, Q0, FINSEQ_1:14, P1, P2; ::_thesis: verum end; Q4: M1 = M2 by P2, FINSEQ_1:14, P1, QQ3; defpred S2[ Nat] means ( 1 <= $1 & $1 <= len n1 implies n1 . $1 = n2 . $1 ); Q50: S2[ 0 ] ; Q51: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume Q52: S2[k] ; ::_thesis: S2[k + 1] assume ( 1 <= k + 1 & k + 1 <= len n1 ) ; ::_thesis: n1 . (k + 1) = n2 . (k + 1) then Q54: ( 1 - 1 <= (k + 1) - 1 & (k + 1) - 1 <= (len n1) - 1 ) by XREAL_1:9; Q55: (len n1) - 1 <= (len n1) - 0 by XREAL_1:13; percases ( k = 0 or k <> 0 ) ; supposeC1: k = 0 ; ::_thesis: n1 . (k + 1) = n2 . (k + 1) thus n1 . (k + 1) = n2 . (k + 1) by P1, P2, C1; ::_thesis: verum end; supposeASQ56: k <> 0 ; ::_thesis: n1 . (k + 1) = n2 . (k + 1) then Q56: 1 <= k by NAT_1:14; Q57: ex u, u0, u1 being Element of INT st ( u0 = (nlist . (k + 1)) `1 & u1 = (nlist . (k + 1)) `2 & u = ((u0 - (n1 . k)) * (prodi1 . k)) mod u1 & n1 . (k + 1) = (n1 . k) + (u * (prodc1 . k)) ) by Q56, Q54, P1; ex u, u0, u1 being Element of INT st ( u0 = (nlist . (k + 1)) `1 & u1 = (nlist . (k + 1)) `2 & u = ((u0 - (n2 . k)) * (prodi2 . k)) mod u1 & n2 . (k + 1) = (n2 . k) + (u * (prodc2 . k)) ) by Q56, Q54, P1, P2; hence n1 . (k + 1) = n2 . (k + 1) by Q3, Q57, Q52, Q55, ASQ56, NAT_1:14, Q54, XXREAL_0:2, FINSEQ_1:14, P1, P2, Q3A; ::_thesis: verum end; end; end; for k being Nat holds S2[k] from NAT_1:sch_2(Q50, Q51); hence s1 = s2 by Q4, P1, P2, FINSEQ_1:14; ::_thesis: verum end; end; end; end; :: deftheorem defALGOCRT defines ALGO_CRT NTALGO_1:def_4_:_ for nlist being non empty FinSequence of [:INT,INT:] for b2 being Element of INT holds ( b2 = ALGO_CRT nlist iff ( ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) ) ); theorem LMLmTh4B: :: NTALGO_1:8 for a, b being Element of INT st b <> 0 holds a mod b,a are_congruent_mod b proof let a, b be Element of INT ; ::_thesis: ( b <> 0 implies a mod b,a are_congruent_mod b ) assume b <> 0 ; ::_thesis: a mod b,a are_congruent_mod b then C1: a mod b = a - ((a div b) * b) by INT_1:def_10; reconsider c = - (a div b) as Element of INT by INT_1:def_2; take c ; :: according to INT_1:def_5 ::_thesis: b * c = (a mod b) - a thus b * c = (a mod b) - a by C1; ::_thesis: verum end; theorem :: NTALGO_1:9 for a, b being Element of INT st b <> 0 holds (a mod b) gcd b = a gcd b by INT_4:14, LMLmTh4B; theorem LmTh4A: :: NTALGO_1:10 for a, b, c being Element of INT st c <> 0 & a = b mod c & b,c are_relative_prime holds a,c are_relative_prime proof let a, b, c be Element of INT ; ::_thesis: ( c <> 0 & a = b mod c & b,c are_relative_prime implies a,c are_relative_prime ) assume A1: ( c <> 0 & a = b mod c & b,c are_relative_prime ) ; ::_thesis: a,c are_relative_prime then b gcd c = 1 by INT_2:def_3; then a gcd c = 1 by A1, INT_4:14, LMLmTh4B; hence a,c are_relative_prime by INT_2:def_3; ::_thesis: verum end; LmTh4: for a, b, c being Element of INT st a = b mod c & c <> 0 holds ex d being Element of INT st a = b + (d * c) proof let a, b, c be Element of INT ; ::_thesis: ( a = b mod c & c <> 0 implies ex d being Element of INT st a = b + (d * c) ) assume ( a = b mod c & c <> 0 ) ; ::_thesis: ex d being Element of INT st a = b + (d * c) then C1: b = ((b div c) * c) + a by INT_1:59; reconsider x = - (b div c) as Element of INT by INT_1:def_2; take x ; ::_thesis: a = b + (x * c) thus a = b + (x * c) by C1; ::_thesis: verum end; LmTh5A: for b, m being FinSequence of INT st len b = len m & ( for i being Nat st i in Seg (len b) holds b . i <> 0 ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 proof let b, m be FinSequence of INT ; ::_thesis: ( len b = len m & ( for i being Nat st i in Seg (len b) holds b . i <> 0 ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 ) assume len b = len m ; ::_thesis: ( ex i being Nat st ( i in Seg (len b) & not b . i <> 0 ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 ) assume A2: ( ( for i being Nat st i in Seg (len b) holds b . i <> 0 ) & m . 1 = 1 ) ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= $1 holds m . (i + 1) = (m . i) * (b . i) ) implies m . ($1 + 1) <> 0 ); reconsider I0 = 0 as Element of NAT ; P0: S1[ 0 ] ; P1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume P11: S1[k] ; ::_thesis: S1[k + 1] assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: m . ((k + 1) + 1) <> 0 P14: k <= k + 1 by NAT_1:12; percases ( k = 0 or k <> 0 ) ; supposeP15: k = 0 ; ::_thesis: m . ((k + 1) + 1) <> 0 P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15 .= b . 1 by A2 ; ((len b) - 1) + 0 <= ((len b) - 1) + 1 by XREAL_1:7; then k + 1 <= len b by P12, XXREAL_0:2; then ( 1 <= 1 & 1 <= len b ) by XXREAL_0:2, P12; then 1 in Seg (len b) ; hence m . ((k + 1) + 1) <> 0 by P16, A2; ::_thesis: verum end; supposeP19: k <> 0 ; ::_thesis: m . ((k + 1) + 1) <> 0 P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ m_._(i_+_1)_=_(m_._i)_*_(b_._i) let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) ) assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then ( 1 <= i & i <= k + 1 ) by NAT_1:12; hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum end; thus m . ((k + 1) + 1) <> 0 ::_thesis: verum proof XX6: (k + 1) + 1 <= ((len b) - 1) + 1 by P12, XREAL_1:6; XX1: k + 1 <= (k + 1) + 1 by NAT_1:12; XX2: 1 <= k + 1 by NAT_1:12; k + 1 <= len b by XX1, XX6, XXREAL_0:2; then k + 1 in Seg (len b) by XX2; then P23: b . (k + 1) <> 0 by A2; m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12; hence m . ((k + 1) + 1) <> 0 by P23, P20, P11, P12, P14, XXREAL_0:2, NAT_1:14, P19, XCMPLX_1:6; ::_thesis: verum end; end; end; end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1); hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 ; ::_thesis: verum end; LmTh5: for b, m being FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime proof let b, m be FinSequence of INT ; ::_thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime ) assume 2 <= len b ; ::_thesis: ( ex i, j being Nat st ( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_relative_prime ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime ) assume A2: ( ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & m . 1 = 1 ) ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= $1 holds m . (i + 1) = (m . i) * (b . i) ) implies for j being Nat st $1 + 1 <= j & j <= len b holds m . ($1 + 1),b . j are_relative_prime ); reconsider I0 = 0 as Element of NAT ; P0: S1[ 0 ] ; P1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume P11: S1[k] ; ::_thesis: S1[k + 1] assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime P14: k <= k + 1 by NAT_1:12; percases ( k = 0 or k <> 0 ) ; supposeP15: k = 0 ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15 .= b . 1 by A2 ; for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime proof let j be Nat; ::_thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime ) assume XX0: ( (k + 1) + 1 <= j & j <= len b ) ; ::_thesis: m . ((k + 1) + 1),b . j are_relative_prime then XX2: ( 1 <= j & j <= len b ) by XXREAL_0:2, P15; then XX1: j in Seg (len b) by FINSEQ_1:1; ( 1 <= 1 & 1 <= len b ) by XXREAL_0:2, XX2; then XX3: 1 in Seg (len b) ; 1 <> j by XX0, P15; hence m . ((k + 1) + 1),b . j are_relative_prime by P16, A2, XX1, XX3; ::_thesis: verum end; hence for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime ; ::_thesis: verum end; supposeP19: k <> 0 ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ m_._(i_+_1)_=_(m_._i)_*_(b_._i) let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) ) assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then ( 1 <= i & i <= k + 1 ) by NAT_1:12; hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum end; thus for j being Nat st (k + 1) + 1 <= j & j <= len b holds m . ((k + 1) + 1),b . j are_relative_prime ::_thesis: verum proof let j be Nat; ::_thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime ) assume XX6: ( (k + 1) + 1 <= j & j <= len b ) ; ::_thesis: m . ((k + 1) + 1),b . j are_relative_prime k + 1 <= (k + 1) + 1 by NAT_1:12; then XX1: ( k + 1 <= j & j <= len b ) by XX6, XXREAL_0:2; then P21: m . (k + 1),b . j are_relative_prime by P20, P11, P12, P14, XXREAL_0:2, NAT_1:14, P19; XX2: 1 <= k + 1 by NAT_1:12; k + 1 <= len b by XX1, XXREAL_0:2; then XX3: k + 1 in Seg (len b) by XX2; ( 1 <= j & j <= len b ) by XX1, XX2, XXREAL_0:2; then XX4: j in Seg (len b) by FINSEQ_1:1; k + 1 < j by XX6, XXREAL_0:2, NAT_1:16; then P23: b . (k + 1),b . j are_relative_prime by A2, XX3, XX4; m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12; hence m . ((k + 1) + 1),b . j are_relative_prime by P23, P21, INT_2:26; ::_thesis: verum end; end; end; end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1); hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime ; ::_thesis: verum end; LmTh6: for b, m being FinSequence of INT st len b = len m & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 proof let b, m be FinSequence of INT ; ::_thesis: ( len b = len m & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 ) assume len b = len m ; ::_thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 ) assume A2: m . 1 = 1 ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= $1 holds m . (i + 1) = (m . i) * (b . i) ) implies for j being Nat st 1 <= j & j <= $1 holds (m . ($1 + 1)) mod (b . j) = 0 ); reconsider I0 = 0 as Element of NAT ; P0: S1[ 0 ] ; P1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume P11: S1[k] ; ::_thesis: S1[k + 1] assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 P14: k <= k + 1 by NAT_1:12; percases ( k = 0 or k <> 0 ) ; supposeP15: k = 0 ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15 .= b . 1 by A2 ; for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 proof let j be Nat; ::_thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 ) assume ( 1 <= j & j <= k + 1 ) ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0 then j = 1 by XXREAL_0:1, P15; hence (m . ((k + 1) + 1)) mod (b . j) = 0 by INT_1:50, P16; ::_thesis: verum end; hence for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 ; ::_thesis: verum end; suppose k <> 0 ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ m_._(i_+_1)_=_(m_._i)_*_(b_._i) let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) ) assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then ( 1 <= i & i <= k + 1 ) by NAT_1:12; hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum end; thus for j being Nat st 1 <= j & j <= k + 1 holds (m . ((k + 1) + 1)) mod (b . j) = 0 ::_thesis: verum proof let j be Nat; ::_thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 ) assume XX6: ( 1 <= j & j <= k + 1 ) ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0 reconsider bj = b . j as Element of INT by INT_1:def_2; percases ( j = k + 1 or j <> k + 1 ) ; supposeXX61: j = k + 1 ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0 thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by P12 .= (((m . (k + 1)) mod (b . j)) * ((b . (k + 1)) mod (b . j))) mod (b . j) by NAT_D:67 .= (((m . (k + 1)) mod (b . j)) * 0) mod (b . j) by INT_1:50, XX61 .= 0 by INT_4:12 ; ::_thesis: verum end; suppose j <> k + 1 ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0 then j < k + 1 by XX6, XXREAL_0:1; then XX1: j <= k by NAT_1:13; thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by P12 .= (((m . (k + 1)) mod (b . j)) * ((b . (k + 1)) mod (b . j))) mod (b . j) by NAT_D:67 .= (0 * ((b . (k + 1)) mod (b . j))) mod (b . j) by XX1, P20, XX6, P11, P12, P14, XXREAL_0:2 .= 0 by INT_4:12 ; ::_thesis: verum end; end; end; end; end; end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1); hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 ; ::_thesis: verum end; theorem Th4: :: NTALGO_1:11 for nlist being non empty FinSequence of [:INT,INT:] for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) holds for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) proof defpred S1[ Nat] means for nlist being non empty FinSequence of [:INT,INT:] for a, b being FinSequence of INT st len nlist = $1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) holds for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i); P0: S1[ 0 ] ; P1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume AS1: S1[n] ; ::_thesis: S1[n + 1] let nlist be non empty FinSequence of [:INT,INT:]; ::_thesis: for a, b being FinSequence of INT st len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) holds for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) let a, b be FinSequence of INT ; ::_thesis: ( len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) implies for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ) assume AS2: ( len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) ) ; ::_thesis: for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) percases ( n = 0 or n <> 0 ) ; supposeP1: n = 0 ; ::_thesis: for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) P2: 1 in Seg (len nlist) by P1, AS2; P3: ALGO_CRT nlist = (nlist . 1) `1 by defALGOCRT, P1, AS2 .= a . 1 by AS2, P2 ; thus for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by P3, TARSKI:def_1, FINSEQ_1:2, P1, AS2; ::_thesis: verum end; supposeNN1: n <> 0 ; ::_thesis: for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) then NN2: 1 <= n by NAT_1:14; P4: len nlist <> 1 by AS2, NN1; reconsider nlist1 = nlist | n as FinSequence of [:INT,INT:] ; reconsider a1 = a | n as FinSequence of INT ; reconsider b1 = b | n as FinSequence of INT ; KK: n <= n + 1 by NAT_1:11; then D02: len a1 = n by FINSEQ_1:59, AS2; D22: len nlist1 = n by KK, FINSEQ_1:59, AS2; then reconsider nlist1 = nlist1 as non empty FinSequence of [:INT,INT:] by NN1; D23: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def_3 .= Seg n by KK, FINSEQ_1:59, AS2 ; D25: len nlist1 = n by D23, FINSEQ_1:def_3; then D28: Seg (len nlist1) c= Seg (len nlist) by KK, FINSEQ_1:5, AS2; X1: ( len nlist1 = n & len a1 = len b1 & len a1 = len nlist1 ) by D02, KK, FINSEQ_1:59, AS2; X2A: for i being Nat st i in Seg (len nlist1) holds b1 . i <> 0 proof let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies b1 . i <> 0 ) assume D260: i in Seg (len nlist1) ; ::_thesis: b1 . i <> 0 then b1 . i = b . i by FUNCT_1:49, D25; hence b1 . i <> 0 by D28, D260, AS2; ::_thesis: verum end; X2: for i being Nat st i in Seg (len nlist1) holds ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) proof let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) ) assume X21: i in Seg (len nlist1) ; ::_thesis: ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) X23: (nlist1 . i) `1 = (nlist . i) `1 by X21, FUNCT_1:49, D25 .= a . i by X21, D28, AS2 .= a1 . i by X21, FUNCT_1:49, D25 ; (nlist1 . i) `2 = (nlist . i) `2 by X21, FUNCT_1:49, D25 .= b . i by X21, D28, AS2 .= b1 . i by X21, FUNCT_1:49, D25 ; hence ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) by X23; ::_thesis: verum end; X3: for i, j being Nat st i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j holds b1 . i,b1 . j are_relative_prime proof let i, j be Nat; ::_thesis: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j implies b1 . i,b1 . j are_relative_prime ) assume A1: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j ) ; ::_thesis: b1 . i,b1 . j are_relative_prime A3: b . i = b1 . i by A1, FUNCT_1:49, D25; b . j = b1 . j by A1, FUNCT_1:49, D25; hence b1 . i,b1 . j are_relative_prime by A3, A1, D28, AS2; ::_thesis: verum end; X400: for i being Nat st i in Seg (len nlist1) holds (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) proof let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) ) assume A1: i in Seg (len nlist1) ; ::_thesis: (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) then ( a1 . i = a . i & b1 . i = b . i ) by FUNCT_1:49, D25; hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by AS1, X1, X2, X3, X2A, A1; ::_thesis: verum end; consider m, l, prodc, prodi being FinSequence of INT , M0, M being Element of INT such that X5: ( len m = len nlist & len l = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & l . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (l . i)) * (prodi . i)) mod u1 & l . (i + 1) = (l . i) + (u * (prodc . i)) ) ) & ALGO_CRT nlist = (l . (len m)) mod M ) by P4, defALGOCRT; LmTh51: 1 + 1 <= n + 1 by XREAL_1:6, NN2; reconsider lb1 = (len b) - 1 as Element of NAT by AS2; LmTh54: ( 1 <= lb1 & lb1 <= lb1 ) by AS2, NAT_1:14, NN1; LmTh55: for i being Nat st 1 <= i & i <= lb1 holds m . (i + 1) = (m . i) * (b . i) proof let i be Nat; ::_thesis: ( 1 <= i & i <= lb1 implies m . (i + 1) = (m . i) * (b . i) ) assume PX0: ( 1 <= i & i <= lb1 ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then PX1: ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) by AS2, X5; i in Seg (len nlist1) by PX0, D22, AS2, FINSEQ_1:1; hence m . (i + 1) = (m . i) * (b . i) by PX1, AS2, D28; ::_thesis: verum end; LmTh56: m . (len nlist),b . (len nlist) are_relative_prime by AS2, LmTh5, LmTh51, X5, LmTh54, LmTh55; set l1 = l | n; set m1 = m | n; KK: n <= n + 1 by NAT_1:11; then PD02: len (l | n) = n by AS2, FINSEQ_1:59, X5; PD11: dom (m | n) = Seg (len (m | n)) by FINSEQ_1:def_3 .= Seg n by AS2, FINSEQ_1:59, X5, KK ; PD12: len (m | n) = n by PD11, FINSEQ_1:def_3; 1 - 1 <= n - 1 by NN2, XREAL_1:9; then n - 1 in NAT by INT_1:3; then reconsider nn1 = n - 1 as Nat ; reconsider prodi1 = prodi | nn1 as FinSequence of INT ; reconsider prodc1 = prodc | nn1 as FinSequence of INT ; XX5: n - 1 <= n - 0 by XREAL_1:10; then QD02: len prodi1 = nn1 by AS2, X5, FINSEQ_1:59; QD12: len prodc1 = nn1 by XX5, AS2, X5, FINSEQ_1:59; PD24: 1 in Seg n by NN2; PD26X: (l | n) . 1 = l . 1 by FUNCT_1:49, PD24 .= (nlist1 . 1) `1 by FUNCT_1:49, PD24, X5 ; QKK: n - 1 <= n - 0 by XREAL_1:10; PD26: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_(len_(m_|_n))_-_1_holds_ (_(m_|_n)_._i_=_m_._i_&_(l_|_n)_._i_=_l_._i_&_prodi1_._i_=_prodi_._i_&_prodc1_._i_=_prodc_._i_) let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ( (m | n) . i = m . i & (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i ) ) assume PD260X: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ( (m | n) . i = m . i & (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i ) then PD260: ( 1 <= i & i <= len (m | n) ) by PD12, QKK, XXREAL_0:2; then i in Seg (len (m | n)) by FINSEQ_1:1; hence (m | n) . i = m . i by FUNCT_1:49, PD12; ::_thesis: ( (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i ) i in Seg (len (l | n)) by FINSEQ_1:1, PD260, PD02, PD12; hence (l | n) . i = l . i by FUNCT_1:49, PD02; ::_thesis: ( prodi1 . i = prodi . i & prodc1 . i = prodc . i ) i in Seg (len prodi1) by FINSEQ_1:1, PD260X, PD12, QD02; hence prodi1 . i = prodi . i by FUNCT_1:49, QD02; ::_thesis: prodc1 . i = prodc . i i in Seg (len prodc1) by FINSEQ_1:1, PD260X, PD12, QD12; hence prodc1 . i = prodc . i by FUNCT_1:49, QD12; ::_thesis: verum end; len (m | n) in Seg (len nlist1) by D22, PD12, FINSEQ_1:3; then Z1: len (m | n) in Seg (len nlist) by D28; Z2: nlist1 . (len (m | n)) = nlist . (len (m | n)) by FUNCT_1:49, D22, PD12, FINSEQ_1:3; len (m | n) in dom nlist by FINSEQ_1:def_3, Z1; then nlist1 . (len (m | n)) in [:INT,INT:] by FINSEQ_2:11, Z2; then reconsider M01 = (nlist1 . (len (m | n))) `2 as Element of INT by MCART_1:10; reconsider M1 = (prodc1 . ((len (m | n)) - 1)) * M01 as Element of INT by INT_1:def_2; QX1: ( len (m | n) = len nlist1 & len (l | n) = len nlist1 & len prodc1 = (len nlist1) - 1 & len prodi1 = (len nlist1) - 1 & (m | n) . 1 = 1 ) by KK, FINSEQ_1:59, AS2, PD12, PD02, QD12, QD02, X5, FUNCT_1:49, PD24; QX2: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds ex d, x, y being Element of INT st ( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ex d, x, y being Element of INT st ( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) ) assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st ( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) then XQ22: (m | n) . i = m . i by PD26; XQ23: prodi1 . i = prodi . i by PD26, XQ21; XQ24: prodc1 . i = prodc . i by PD26, XQ21; XQ25: 1 <= i + 1 by NAT_1:12; i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6; then YY1: i + 1 in Seg (len (m | n)) by XQ25; then XQ27: (m | n) . (i + 1) = m . (i + 1) by FUNCT_1:49, PD12; XQ28: ( 1 <= i & i <= len (m | n) ) by XQ21, PD12, QKK, XXREAL_0:2; XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2; i in Seg (len nlist1) by PD12, D22, XQ28, FINSEQ_1:1; then XQ32: nlist1 . i = nlist . i by FUNCT_1:49, D25; nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1; hence ex d, x, y being Element of INT st ( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by XQ22, XQ23, XQ24, XQ27, XQ30, XQ32, X5; ::_thesis: verum end; QX4: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) proof let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ex u, u0, u1 being Element of INT st ( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) ) assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ex u, u0, u1 being Element of INT st ( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) then XQ22: (l | n) . i = l . i by PD26; XQ23: prodi1 . i = prodi . i by PD26, XQ21; XQ24: prodc1 . i = prodc . i by PD26, XQ21; XQ25: 1 <= i + 1 by NAT_1:12; i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6; then YY1: i + 1 in Seg (len (m | n)) by XQ25; then XQ27: (l | n) . (i + 1) = l . (i + 1) by FUNCT_1:49, PD12; XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2; nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1; hence ex u, u0, u1 being Element of INT st ( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) by XQ22, XQ23, XQ24, XQ27, XQ30, X5; ::_thesis: verum end; reconsider s = ((l | n) . (len (m | n))) mod M1 as Element of INT by INT_1:def_2; QX12: 1 <= (len m) - 1 by X5, AS2, NAT_1:14, NN1; reconsider lm1 = (len m) - 1 as Element of NAT by X5; QX13: ( 1 <= lm1 & lm1 <= (len m) - 1 ) by X5, AS2, NAT_1:14, NN1; consider d, x, y being Element of INT such that QX14: ( x = (nlist . lm1) `2 & m . (lm1 + 1) = (m . lm1) * x & y = m . (lm1 + 1) & d = (nlist . (lm1 + 1)) `2 & prodi . lm1 = ALGO_INVERSE (y,d) & prodc . lm1 = y ) by X5, AS2, NN2; consider u, u0, u1 being Element of INT such that QX15: ( u0 = (nlist . (lm1 + 1)) `1 & u1 = (nlist . (lm1 + 1)) `2 & u = ((u0 - (l . lm1)) * (prodi . lm1)) mod u1 & l . (lm1 + 1) = (l . lm1) + (u * (prodc . lm1)) ) by QX13, X5; QX43: len nlist in Seg (len nlist) by FINSEQ_1:3; QX45: M0 = b . (len nlist) by X5, AS2, QX43; then QX37B: M0 <> 0 by QX43, AS2; QX36A: (u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0)) is Element of INT by INT_1:def_2; consider r being Element of INT such that QX37: u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0) by LmTh4, X5, QX14, QX15, QX36A, QX37B; QX26A: y <> 0 by QX14, X5, AS2, LmTh5A, LmTh54, LmTh55; now__::_thesis:_ex_p,_qr_being_Element_of_INT_st_ (_ALGO_CRT_nlist_=_(((ALGO_CRT_nlist1)_-_((((l_._((len_m)_-_1))_*_(ALGO_INVERSE_(y,M0)))_*_y)_+_(p_*_y)))_+_((qr_*_M0)_*_y))_+_((u0_*_(ALGO_INVERSE_(y,M0)))_*_y)_&_ALGO_CRT_nlist1_=_(l_._((len_m)_-_1))_+_(p_*_y)_) percases ( len nlist1 = 1 or len nlist1 <> 1 ) ; supposeAA1: len nlist1 = 1 ; ::_thesis: ex p, qr being Element of INT st ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) AAA1: ALGO_CRT nlist1 = (nlist1 . 1) `1 by AA1, defALGOCRT .= (nlist . 1) `1 by FUNCT_1:49, PD24 .= l . ((len m) - 1) by AA1, AS2, X5, D23, FINSEQ_1:def_3 ; QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M by QX14, QX15, X5; reconsider p = 0 as Element of INT by INT_1:def_2; QX28: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) by AAA1; reconsider uy = u * y as Element of INT by INT_1:def_2; reconsider llm1 = l . ((len m) - 1) as Element of INT by INT_1:def_2; reconsider ly = llm1 + uy as Element of INT by INT_1:def_2; M = y * M0 by X5, QX14; then consider t being Element of INT such that QX30: ALGO_CRT nlist = ly + (t * M) by LmTh4, QX27, QX37B, QX26A, XCMPLX_1:6; reconsider qr = r + t as Element of INT by INT_1:def_2; ALGO_CRT nlist = (((ALGO_CRT nlist1) - (((llm1 * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by X5, QX14, QX37, QX30, AAA1; hence ex p, qr being Element of INT st ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) by QX28; ::_thesis: verum end; supposeAA2: len nlist1 <> 1 ; ::_thesis: ex p, qr being Element of INT st ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) then QX7: ALGO_CRT nlist1 = s by defALGOCRT, QX1, QX2, QX4, PD26X .= ((l | n) . (len (m | n))) mod ((prodc1 . ((len (m | n)) - 1)) * M01) ; QX8: (l | n) . (len (l | n)) = l . (len (l | n)) by FUNCT_1:49, NN1, PD02, FINSEQ_1:3 .= l . ((len m) - 1) by X5, AS2, FINSEQ_1:59, KK ; 2 <= len nlist1 by AA2, NAT_1:23; then 2 - 1 <= (len (m | n)) - 1 by XREAL_1:9, PD12, X1; then QX90: ( 1 <= nn1 & nn1 <= (len (m | n)) - 1 ) by PD11, FINSEQ_1:def_3; QX10: M01 = (nlist . (len (m | n))) `2 by FUNCT_1:49, D22, PD12, FINSEQ_1:3 .= (nlist . ((len m) - 1)) `2 by X5, AS2, PD11, FINSEQ_1:def_3 ; consider d1, x1, y1 being Element of INT such that QX16: ( x1 = (nlist1 . nn1) `2 & (m | n) . (nn1 + 1) = ((m | n) . nn1) * x1 & y1 = (m | n) . (nn1 + 1) & d1 = (nlist1 . (nn1 + 1)) `2 & prodi1 . nn1 = ALGO_INVERSE (y1,d1) & prodc1 . nn1 = y1 ) by QX2, QX90; QX21: len (m | n) = (len m) - 1 by X5, AS2, PD11, FINSEQ_1:def_3; then QX20: lm1 in Seg (len (m | n)) by QX12; QX24: ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01) by QX16, QX7, QX21, QX8, AS2, FINSEQ_1:59, X5, KK; QX24A: ( ALGO_CRT nlist1 is Element of INT & l . ((len m) - 1) is Element of INT & y1 * M01 is Element of INT ) by INT_1:def_2; QX26: y = y1 * x by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14; then QX26C: y1 * M01 <> 0 by X5, AS2, LmTh5A, LmTh54, LmTh55, QX10, QX14; consider p being Element of INT such that QX30: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * (y1 * M01)) by QX24, LmTh4, QX24A, QX26A, QX10, QX14, QX26; QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX15 .= ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14 ; ( ALGO_CRT nlist is Element of INT & (l . ((len m) - 1)) + (u * (y1 * x)) is Element of INT & (y1 * x) * M0 is Element of INT ) by INT_1:def_2; then consider q being Element of INT such that QX31: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) + (q * ((y1 * x) * M0)) by QX27, LmTh4, QX10, QX14, QX26C, XCMPLX_1:6, QX37B; reconsider qr = r + q as Element of INT by INT_1:def_2; ((ALGO_CRT nlist1) - (p * (y1 * M01))) + (u * (y1 * x)) = ((ALGO_CRT nlist1) - (p * (y1 * x))) + (u * (y1 * x)) by QX10, QX14 .= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by QX26, QX37 ; then ALGO_CRT nlist = ((((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)) + (q * (y * M0)) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX31, QX30 .= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) ; hence ex p, qr being Element of INT st ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) by QX30, QX26, QX10, QX14; ::_thesis: verum end; end; end; then consider p, qr being Element of INT such that QX41: ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) ; reconsider y0 = y mod M0 as Element of INT by INT_1:def_2; y0,M0 are_relative_prime by QX37B, LmTh4A, QX14, X5, QX45, LmTh56; then y0 gcd M0 = 1 by INT_2:def_3; then QX48: (ALGO_EXGCD (M0,y0)) `3_3 = 1 by Th2; QX50: ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y)) mod M0 = ((((l . ((len m) - 1)) * ((ALGO_INVERSE (y,M0)) * y)) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:66 .= (((((l . ((len m) - 1)) mod M0) * (((ALGO_INVERSE (y,M0)) * y) mod M0)) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67 .= (((((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0) + ((p * y) mod M0)) mod M0 by QX48, Th3 .= ((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67 .= (ALGO_CRT nlist1) mod M0 by QX41, NAT_D:66 ; thus for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ::_thesis: verum proof let i be Nat; ::_thesis: ( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ) assume VA0: i in Seg (len nlist) ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) then VA1: ( 1 <= i & i <= len nlist ) by FINSEQ_1:1; percases ( i = len nlist or i <> len nlist ) ; supposeVA2: i = len nlist ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) VA22: b . i <> 0 by AS2, VA0; reconsider I0 = 0 as Element of INT by INT_1:def_2; reconsider K1y = (((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y) as Element of INT by INT_1:def_2; reconsider K2y = (qr * y) * M0 as Element of INT by INT_1:def_2; reconsider K3y = u0 * ((ALGO_INVERSE (y,M0)) * y) as Element of INT by INT_1:def_2; reconsider K4y = K2y + K3y as Element of INT by INT_1:def_2; VA31: K2y mod (b . i) = (((qr * y) mod M0) * (M0 mod M0)) mod M0 by QX45, VA2, NAT_D:67 .= (((qr * y) mod M0) * I0) mod M0 by INT_1:50 .= I0 mod (b . i) by VA2, X5, AS2, QX43 ; VA30: K4y mod (b . i) = ((I0 mod (b . i)) + (K3y mod (b . i))) mod (b . i) by VA31, NAT_D:66 .= (I0 + K3y) mod (b . i) by NAT_D:66 .= ((u0 mod (b . i)) * (((ALGO_INVERSE (y,M0)) * y) mod (b . i))) mod (b . i) by NAT_D:67 .= ((u0 mod (b . i)) * (1 mod (b . i))) mod (b . i) by QX48, Th3, VA2, QX45 .= (u0 * 1) mod (b . i) by NAT_D:67 .= (a . i) mod (b . i) by VA2, QX43, X5, AS2, QX15 ; VA31: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + ((ALGO_CRT nlist1) mod (b . i))) mod (b . i) by QX50, VA2, QX45, NAT_D:66 .= ((ALGO_CRT nlist) + (ALGO_CRT nlist1)) mod (b . i) by NAT_D:66 ; VA32: ((ALGO_CRT nlist1) + K4y) mod (b . i) = (((ALGO_CRT nlist1) mod (b . i)) + (K4y mod (b . i))) mod (b . i) by NAT_D:66 .= ((ALGO_CRT nlist1) + (a . i)) mod (b . i) by NAT_D:66, VA30 ; reconsider LL = ((ALGO_CRT nlist1) + (a . i)) mod (b . i) as Element of INT by INT_1:def_2; reconsider LL1 = (ALGO_CRT nlist) + (ALGO_CRT nlist1) as Element of INT by INT_1:def_2; reconsider bi = b . i as Element of INT by INT_1:def_2; consider r being Element of INT such that VA33: LL = LL1 + (r * bi) by LmTh4, VA22, VA31, VA32, QX41; reconsider LL2 = (ALGO_CRT nlist1) + (a . i) as Element of INT by INT_1:def_2; consider s being Element of INT such that VA34: LL = LL2 + (s * bi) by LmTh4, VA22; reconsider LL3 = s - r as Element of INT by INT_1:def_2; VA36: (LL3 * (b . i)) mod (b . i) = ((LL3 mod (b . i)) * ((b . i) mod (b . i))) mod (b . i) by NAT_D:67 .= ((LL3 mod (b . i)) * I0) mod (b . i) by INT_1:50 .= I0 mod (b . i) ; thus (ALGO_CRT nlist) mod (b . i) = ((a . i) + ((s - r) * (b . i))) mod (b . i) by VA33, VA34 .= (((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i) by VA36, NAT_D:66 .= ((a . i) + I0) mod (b . i) by NAT_D:66 .= (a . i) mod (b . i) ; ::_thesis: verum end; suppose i <> len nlist ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) then i < len nlist by VA1, XXREAL_0:1; then i + 1 <= len nlist by NAT_1:13; then VA22P: (i + 1) - 1 <= (len nlist) - 1 by XREAL_1:9; then VA22: ( 1 <= i & i <= len nlist1 ) by KK, FINSEQ_1:59, AS2, FINSEQ_1:1, VA0; VA24: i in Seg (len nlist1) by FINSEQ_1:1, VA22P, AS2, X1, VA1; reconsider K1 = ((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) + p as Element of INT by INT_1:def_2; reconsider K2 = (qr * M0) + (u0 * (ALGO_INVERSE (y,M0))) as Element of INT by INT_1:def_2; reconsider I0 = 0 as Element of INT by INT_1:def_2; VA27: y mod (b . i) = 0 by X1, QX14, LmTh6, LmTh54, LmTh55, AS2, X5, VA22; reconsider K1y = K1 * y as Element of INT by INT_1:def_2; reconsider K2y = K2 * y as Element of INT by INT_1:def_2; VA29: (K1 * y) mod (b . i) = ((K1 mod (b . i)) * (y mod (b . i))) mod (b . i) by NAT_D:67 .= 0 mod (b . i) by VA27 ; VA30: (K2 * y) mod (b . i) = ((K2 mod (b . i)) * (y mod (b . i))) mod (b . i) by NAT_D:67 .= 0 mod (b . i) by VA27 ; VA31: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + (K1y mod (b . i))) mod (b . i) by NAT_D:66 .= ((ALGO_CRT nlist) + I0) mod (b . i) by NAT_D:66, VA29 .= (ALGO_CRT nlist) mod (b . i) ; ((ALGO_CRT nlist1) + K2y) mod (b . i) = (((ALGO_CRT nlist1) mod (b . i)) + (K2y mod (b . i))) mod (b . i) by NAT_D:66 .= ((ALGO_CRT nlist1) + I0) mod (b . i) by NAT_D:66, VA30 .= (ALGO_CRT nlist1) mod (b . i) ; hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by VA24, QX41, VA31, X400; ::_thesis: verum end; end; end; end; end; end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, P1); hence for nlist being non empty FinSequence of [:INT,INT:] for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) holds for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ; ::_thesis: verum end; LmTh7A: for x, y, a, b being Element of INT st x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime holds x mod (a * b) = y mod (a * b) proof let x, y, a, b be Element of INT ; ::_thesis: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime implies x mod (a * b) = y mod (a * b) ) assume AS: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime ) ; ::_thesis: x mod (a * b) = y mod (a * b) set g1 = x mod a; set g2 = x mod b; percases ( a * b = 0 or a * b <> 0 ) ; supposeC1: a * b = 0 ; ::_thesis: x mod (a * b) = y mod (a * b) thus x mod (a * b) = 0 by INT_1:def_10, C1 .= y mod (a * b) by C1, INT_1:def_10 ; ::_thesis: verum end; suppose a * b <> 0 ; ::_thesis: x mod (a * b) = y mod (a * b) then C3: ( a <> 0 & b <> 0 ) ; C5: y = ((y div a) * a) + (y mod a) by C3, INT_1:59; C6: x = ((x div b) * b) + (x mod b) by C3, INT_1:59; x - y = (((x div a) * a) + (x mod a)) - (((y div a) * a) + (y mod a)) by C3, INT_1:59, C5 .= ((x div a) - (y div a)) * a by AS ; then a divides x - y by INT_1:def_3; then C8: x,y are_congruent_mod a by INT_1:def_4; x - y = (((x div b) * b) + (x mod b)) - (((y div b) * b) + (y mod b)) by C3, INT_1:59, C6 .= ((x div b) - (y div b)) * b by AS ; then b divides x - y by INT_1:def_3; then x,y are_congruent_mod b by INT_1:def_4; then x,y are_congruent_mod a * b by AS, C8, INT_6:21; then a * b divides x - y by INT_1:def_4; then consider p being Integer such that C11: x - y = (a * b) * p by INT_1:def_3; reconsider I0 = 0 as Element of INT by INT_1:def_2; thus x mod (a * b) = (y + ((a * b) * p)) mod (a * b) by C11 .= ((y mod (a * b)) + (((a * b) * p) mod (a * b))) mod (a * b) by NAT_D:66 .= ((y mod (a * b)) + ((((a * b) mod (a * b)) * (p mod (a * b))) mod (a * b))) mod (a * b) by NAT_D:67 .= ((y mod (a * b)) + ((I0 * (p mod (a * b))) mod (a * b))) mod (a * b) by INT_1:50 .= (y + I0) mod (a * b) by NAT_D:66 .= y mod (a * b) ; ::_thesis: verum end; end; end; theorem LmTh7: :: NTALGO_1:12 for x, y being Element of INT for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) proof let x, y be Element of INT ; ::_thesis: for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) let b, m be non empty FinSequence of INT ; ::_thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds x mod (b . i) = y mod (b . i) ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) ) assume A1: 2 <= len b ; ::_thesis: ( ex i, j being Nat st ( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st ( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) ) assume A4: for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ; ::_thesis: ( ex i being Nat st ( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) ) assume A2: for i being Nat st i in Seg (len b) holds x mod (b . i) = y mod (b . i) ; ::_thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) ) assume A3: m . 1 = 1 ; ::_thesis: for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) defpred S1[ Nat] means ( 1 <= $1 & $1 <= len b & ( for i being Nat st 1 <= i & i <= $1 holds m . (i + 1) = (m . i) * (b . i) ) implies x mod (m . ($1 + 1)) = y mod (m . ($1 + 1)) ); reconsider I0 = 0 as Element of NAT ; P0: S1[ 0 ] ; P1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume P11: S1[k] ; ::_thesis: S1[k + 1] assume P12: ( 1 <= k + 1 & k + 1 <= len b & ( for i being Nat st 1 <= i & i <= k + 1 holds m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) P14: k <= k + 1 by NAT_1:12; percases ( k = 0 or k <> 0 ) ; supposeP15: k = 0 ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15 .= b . 1 by A3 ; ( 1 <= 1 & 1 <= len b ) by NAT_1:14; then P18: 1 in Seg (len b) ; thus x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by P16, P18, A2; ::_thesis: verum end; supposeP181: k <> 0 ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) (k + 1) - 1 <= (len b) - 1 by P12, XREAL_1:9; then P19: ( 1 <= k & k <= (len b) - 1 ) by P181, NAT_1:14; XX1: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_ m_._(i_+_1)_=_(m_._i)_*_(b_._i) let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) ) assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then ( 1 <= i & i <= k + 1 ) by NAT_1:12; hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum end; P22: m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12; k + 1 in Seg (len b) by P12; then P23: x mod (b . (k + 1)) = y mod (b . (k + 1)) by A2; P24: m . (k + 1),b . (k + 1) are_relative_prime by LmTh5, XX1, P19, A1, A4, A3, P12; ( m . (k + 1) is Element of INT & b . (k + 1) is Element of INT ) by INT_1:def_2; hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by P22, P23, P11, NAT_1:14, P181, P12, P14, XXREAL_0:2, XX1, P24, LmTh7A; ::_thesis: verum end; end; end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1); hence for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) ; ::_thesis: verum end; theorem LmTh8: :: NTALGO_1:13 for b being FinSequence of INT st len b = 1 holds Product b = b . 1 proof let b be FinSequence of INT ; ::_thesis: ( len b = 1 implies Product b = b . 1 ) assume len b = 1 ; ::_thesis: Product b = b . 1 then b = <*(b . 1)*> by FINSEQ_1:40; hence Product b = b . 1 by RVSUM_1:95; ::_thesis: verum end; theorem LmTh9: :: NTALGO_1:14 for b being FinSequence of INT ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) proof defpred S1[ Nat] means for b being FinSequence of INT st len b = $1 holds ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ); P0: S1[ 0 ] proof let b be FinSequence of INT ; ::_thesis: ( len b = 0 implies ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ) assume A1: len b = 0 ; ::_thesis: ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) I0: 1 in INT by INT_1:def_2; rng <*1*> = {1} by FINSEQ_1:39; then rng <*1*> c= INT by ZFMISC_1:31, I0; then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def_4; P0: len m = (len b) + 1 by A1, FINSEQ_1:40; P1: m . 1 = 1 by FINSEQ_1:40; P2: for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) by A1; b = <*> REAL by A1; hence ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P0, P1, P2, A1, RVSUM_1:94; ::_thesis: verum end; P1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A1: S1[k] ; ::_thesis: S1[k + 1] let b be FinSequence of INT ; ::_thesis: ( len b = k + 1 implies ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ) assume A2: len b = k + 1 ; ::_thesis: ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) set b1 = b | k; P2: len (b | k) = k by FINSEQ_1:59, A2, NAT_1:12; then consider m1 being non empty FinSequence of INT such that P4: ( (len (b | k)) + 1 = len m1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= len (b | k) holds m1 . (i + 1) = (m1 . i) * ((b | k) . i) ) & Product (b | k) = m1 . ((len (b | k)) + 1) ) by A1; set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>; P5Z: (Product (b | k)) * (b . (len b)) in INT by P4, INT_1:def_2; P5W: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39; then P5Q: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by ZFMISC_1:31, P5Z; P5: len (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (len m1) + (len <*((Product (b | k)) * (b . (len b)))*>) by FINSEQ_1:22 .= ((len (b | k)) + 1) + 1 by P4, FINSEQ_1:40 .= (len b) + 1 by FINSEQ_1:59, A2, NAT_1:12 ; VV2: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:31, P5W; rng m1 c= INT by FINSEQ_1:def_4; then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by P5W, VV2, P5Q, XBOOLE_1:8; then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def_4; P5B: len m1 = (len (b | k)) + 1 by P4 .= k + 1 by FINSEQ_1:59, A2, NAT_1:12 ; ( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12; then 1 in Seg (len m1) by P5B; then 1 in dom m1 by FINSEQ_1:def_3; then P8: m . 1 = 1 by P4, FINSEQ_1:def_7; P9: for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) proof let i be Nat; ::_thesis: ( 1 <= i & i <= len b implies m . (i + 1) = (m . i) * (b . i) ) assume P10: ( 1 <= i & i <= len b ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i) percases ( i = len b or i <> len b ) ; supposeP11: i = len b ; ::_thesis: m . (i + 1) = (m . i) * (b . i) (len (b | k)) + 1 in Seg (len m1) by P2, P5B, FINSEQ_1:4; then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def_3; then P13: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def_7 .= m . i by A2, FINSEQ_1:59, NAT_1:12, P11 ; 1 in Seg 1 ; then P13C: 1 in dom <*((Product (b | k)) * (b . (len b)))*> by FINSEQ_1:38; thus m . (i + 1) = <*((Product (b | k)) * (b . (len b)))*> . 1 by FINSEQ_1:def_7, P11, A2, P5B, P13C .= (m . i) * (b . i) by P13, P11, P4, FINSEQ_1:40 ; ::_thesis: verum end; suppose i <> len b ; ::_thesis: m . (i + 1) = (m . i) * (b . i) then P12D: i < len b by P10, XXREAL_0:1; then P12A: ( 1 <= i & i <= len (b | k) ) by P2, A2, NAT_1:13, P10; then P13: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by P4; i in Seg (len m1) by FINSEQ_1:1, P10, A2, P5B; then P13B: i in dom m1 by FINSEQ_1:def_3; P13E: i + 1 <= len m1 by A2, P5B, P12D, NAT_1:13; 1 <= i + 1 by NAT_1:12; then i + 1 in Seg (len m1) by P13E; then P13C: i + 1 in dom m1 by FINSEQ_1:def_3; i in Seg k by P12A, FINSEQ_1:1, P2; then P15: b . i = (b | k) . i by FUNCT_1:49; P16: m . i = m1 . i by FINSEQ_1:def_7, P13B; thus m . (i + 1) = (m . i) * (b . i) by P13, FINSEQ_1:def_7, P13C, P15, P16; ::_thesis: verum end; end; end; b | (k + 1) = (b | k) ^ <*(b . (len b))*> by INT_6:5, A2; then P17: b = (b | k) ^ <*(b . (len b))*> by FINSEQ_1:58, A2; len b in Seg (len m1) by FINSEQ_1:4, A2, P5B; then P18: len b in dom m1 by FINSEQ_1:def_3; P19: ( 1 <= len b & len b <= len b ) by A2, NAT_1:12; Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by P4, RVSUM_1:96, P17 .= (m1 . (len b)) * (b . (len b)) by A2, FINSEQ_1:59, NAT_1:12 .= (m . (len b)) * (b . (len b)) by FINSEQ_1:def_7, P18 .= m . ((len b) + 1) by P9, P19 ; hence ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P5, P8, P9; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1); hence for b being FinSequence of INT ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ; ::_thesis: verum end; theorem :: NTALGO_1:15 for nlist being non empty FinSequence of [:INT,INT:] for a, b being non empty FinSequence of INT for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds (ALGO_CRT nlist) mod y = x mod y proof let nlist be non empty FinSequence of [:INT,INT:]; ::_thesis: for a, b being non empty FinSequence of INT for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds (ALGO_CRT nlist) mod y = x mod y let a, b be non empty FinSequence of INT ; ::_thesis: for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds (ALGO_CRT nlist) mod y = x mod y let x, y be Element of INT ; ::_thesis: ( len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ) & y = Product b implies (ALGO_CRT nlist) mod y = x mod y ) assume A1: ( len a = len b & len a = len nlist ) ; ::_thesis: ( ex i being Nat st ( i in Seg (len nlist) & not b . i <> 0 ) or ex i being Nat st ( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st ( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st ( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y ) assume A2: for i being Nat st i in Seg (len nlist) holds b . i <> 0 ; ::_thesis: ( ex i being Nat st ( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st ( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st ( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y ) assume A3: for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ; ::_thesis: ( ex i, j being Nat st ( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st ( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y ) assume A4: for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ; ::_thesis: ( ex i being Nat st ( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y ) assume A5: for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ; ::_thesis: ( not y = Product b or (ALGO_CRT nlist) mod y = x mod y ) assume A6: y = Product b ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y P2: for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = x mod (b . i) proof let i be Nat; ::_thesis: ( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = x mod (b . i) ) assume P21: i in Seg (len nlist) ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = x mod (b . i) hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by Th4, A1, A2, A3, A4 .= x mod (b . i) by A5, P21 ; ::_thesis: verum end; percases ( len nlist = 1 or len nlist <> 1 ) ; supposeP3: len nlist = 1 ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y then P5: 1 in Seg (len nlist) ; thus (ALGO_CRT nlist) mod y = (ALGO_CRT nlist) mod (b . 1) by P3, A1, LmTh8, A6 .= x mod (b . 1) by P2, P5 .= x mod y by P3, A1, LmTh8, A6 ; ::_thesis: verum end; supposeP4: len nlist <> 1 ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y P5: 2 <= len nlist by P4, NAT_1:23; P6: 2 <= len b by A1, P4, NAT_1:23; consider m being non empty FinSequence of INT such that P7: ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by LmTh9; ( 1 <= len b & len b <= len b ) by P6, XXREAL_0:2; hence (ALGO_CRT nlist) mod y = x mod y by A6, P7, LmTh7, A1, A4, P2, P5; ::_thesis: verum end; end; end;