:: INT_2 semantic presentation begin definition let a be integer number ; :: original: |. redefine func abs a -> Element of NAT ; coherence |.a.| is Element of NAT proof percases ( a >= 0 or a < 0 ) ; supposeA1: a >= 0 ; ::_thesis: |.a.| is Element of NAT then abs a = a by ABSVALUE:def_1; hence |.a.| is Element of NAT by A1, INT_1:3; ::_thesis: verum end; suppose a < 0 ; ::_thesis: |.a.| is Element of NAT then ( abs a = - a & - a > 0 ) by ABSVALUE:def_1, XREAL_1:58; hence |.a.| is Element of NAT by INT_1:3; ::_thesis: verum end; end; end; end; theorem Th1: :: INT_2:1 for a, b, c being Integer st a divides b & a divides b + c holds a divides c proof let a, b, c be Integer; ::_thesis: ( a divides b & a divides b + c implies a divides c ) given u being Integer such that A1: b = a * u ; :: according to INT_1:def_3 ::_thesis: ( not a divides b + c or a divides c ) given t being Integer such that A2: b + c = a * t ; :: according to INT_1:def_3 ::_thesis: a divides c c = a * (t - u) by A1, A2; hence a divides c by INT_1:def_3; ::_thesis: verum end; theorem Th2: :: INT_2:2 for a, b, c being Integer st a divides b holds a divides b * c proof let a, b, c be Integer; ::_thesis: ( a divides b implies a divides b * c ) assume a divides b ; ::_thesis: a divides b * c then consider l being Integer such that A1: b = a * l by INT_1:def_3; (a * l) * c = a * (l * c) ; hence a divides b * c by A1, INT_1:def_3; ::_thesis: verum end; theorem Th3: :: INT_2:3 for a being Integer holds ( 0 divides a iff a = 0 ) proof let a be Integer; ::_thesis: ( 0 divides a iff a = 0 ) ( 0 divides a implies a = 0 ) proof assume 0 divides a ; ::_thesis: a = 0 then ex b being Integer st a = 0 * b by INT_1:def_3; hence a = 0 ; ::_thesis: verum end; hence ( 0 divides a iff a = 0 ) ; ::_thesis: verum end; Lm1: for a being Integer holds ( a divides - a & - a divides a ) proof let a be Integer; ::_thesis: ( a divides - a & - a divides a ) - a = a * (- 1) ; hence a divides - a by INT_1:def_3; ::_thesis: - a divides a a = (- a) * (- 1) ; hence - a divides a by INT_1:def_3; ::_thesis: verum end; Lm2: for a, b, c being Integer st a divides b & b divides c holds a divides c proof let a, b, c be Integer; ::_thesis: ( a divides b & b divides c implies a divides c ) assume that A1: a divides b and A2: b divides c ; ::_thesis: a divides c consider k being Integer such that A3: b = a * k by A1, INT_1:def_3; consider l being Integer such that A4: c = b * l by A2, INT_1:def_3; c = a * (k * l) by A3, A4; hence a divides c by INT_1:def_3; ::_thesis: verum end; Lm3: for a, b being Integer holds ( a divides b iff a divides - b ) proof let a, b be Integer; ::_thesis: ( a divides b iff a divides - b ) thus ( a divides b implies a divides - b ) ::_thesis: ( a divides - b implies a divides b ) proof assume A1: a divides b ; ::_thesis: a divides - b b divides - b by Lm1; hence a divides - b by A1, Lm2; ::_thesis: verum end; assume A2: a divides - b ; ::_thesis: a divides b - b divides b by Lm1; hence a divides b by A2, Lm2; ::_thesis: verum end; Lm4: for a, b being Integer holds ( a divides b iff - a divides b ) proof let a, b be Integer; ::_thesis: ( a divides b iff - a divides b ) thus ( a divides b implies - a divides b ) ::_thesis: ( - a divides b implies a divides b ) proof assume A1: a divides b ; ::_thesis: - a divides b - a divides a by Lm1; hence - a divides b by A1, Lm2; ::_thesis: verum end; assume A2: - a divides b ; ::_thesis: a divides b a divides - a by Lm1; hence a divides b by A2, Lm2; ::_thesis: verum end; Lm5: for a being Integer holds ( a divides 0 & 1 divides a & - 1 divides a ) proof let a be Integer; ::_thesis: ( a divides 0 & 1 divides a & - 1 divides a ) 0 = a * 0 ; hence a divides 0 by INT_1:def_3; ::_thesis: ( 1 divides a & - 1 divides a ) a = 1 * a ; hence 1 divides a by INT_1:def_3; ::_thesis: - 1 divides a a = (- 1) * (- a) ; hence - 1 divides a by INT_1:def_3; ::_thesis: verum end; Lm6: for a, b, c being Integer st a divides b & a divides c holds a divides b mod c proof let a, b, c be Integer; ::_thesis: ( a divides b & a divides c implies a divides b mod c ) assume that A1: a divides b and A2: a divides c ; ::_thesis: a divides b mod c A3: now__::_thesis:_(_c_<>_0_implies_a_divides_b_mod_c_) assume c <> 0 ; ::_thesis: a divides b mod c then A4: b = (c * (b div c)) + (b mod c) by INT_1:59; a divides c * (b div c) by A2, Th2; hence a divides b mod c by A1, A4, Th1; ::_thesis: verum end; now__::_thesis:_(_c_=_0_implies_a_divides_b_mod_c_) assume c = 0 ; ::_thesis: a divides b mod c then b mod c = 0 by INT_1:def_10; hence a divides b mod c by Lm5; ::_thesis: verum end; hence a divides b mod c by A3; ::_thesis: verum end; Lm7: for k, l being Nat holds ( k divides l iff ex t being Nat st l = k * t ) proof let k, l be Nat; ::_thesis: ( k divides l iff ex t being Nat st l = k * t ) hereby ::_thesis: ( ex t being Nat st l = k * t implies k divides l ) assume A1: k divides l ; ::_thesis: ex t being Nat st l = k * t thus ex t being Nat st l = k * t ::_thesis: verum proof A2: k >= 0 by NAT_1:2; consider t being Integer such that A3: l = k * t by A1, INT_1:def_3; percases ( 0 < l or l = 0 ) by NAT_1:3; suppose 0 < l ; ::_thesis: ex t being Nat st l = k * t then 0 <= t by A3, A2, XREAL_1:131; then reconsider t = t as Element of NAT by INT_1:3; take t ; ::_thesis: l = k * t thus l = k * t by A3; ::_thesis: verum end; supposeA4: l = 0 ; ::_thesis: ex t being Nat st l = k * t take 0 ; ::_thesis: l = k * 0 thus l = k * 0 by A4; ::_thesis: verum end; end; end; end; assume ex t being Nat st l = k * t ; ::_thesis: k divides l hence k divides l by INT_1:def_3; ::_thesis: verum end; Lm8: for i, j being Nat st i divides j & j divides i holds i = j proof let i, j be Nat; ::_thesis: ( i divides j & j divides i implies i = j ) assume i divides j ; ::_thesis: ( not j divides i or i = j ) then consider a being Integer such that A1: j = i * a by INT_1:def_3; assume j divides i ; ::_thesis: i = j then consider b being Integer such that A2: i = j * b by INT_1:def_3; ( i <> 0 implies i = j ) proof A3: i >= 0 by NAT_1:2; assume A4: i <> 0 ; ::_thesis: i = j 1 * i = i * (a * b) by A1, A2; then a * b = 1 by A4, XCMPLX_1:5; then ( i = j * 1 or i = j * (- 1) ) by A2, INT_1:9; hence i = j by A4, A3; ::_thesis: verum end; hence i = j by A1; ::_thesis: verum end; definition let a, b be Integer; funca lcm b -> Nat means :Def1: :: INT_2:def 1 ( a divides it & b divides it & ( for m being Integer st a divides m & b divides m holds it divides m ) ); existence ex b1 being Nat st ( a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds b1 divides m ) ) proof percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; supposeA1: ( a = 0 or b = 0 ) ; ::_thesis: ex b1 being Nat st ( a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds b1 divides m ) ) take 0 ; ::_thesis: ( a divides 0 & b divides 0 & ( for m being Integer st a divides m & b divides m holds 0 divides m ) ) thus ( a divides 0 & b divides 0 ) by Lm5; ::_thesis: for m being Integer st a divides m & b divides m holds 0 divides m thus for m being Integer st a divides m & b divides m holds 0 divides m by A1; ::_thesis: verum end; supposeA2: ( a <> 0 & b <> 0 ) ; ::_thesis: ex b1 being Nat st ( a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds b1 divides m ) ) defpred S1[ Nat] means ( a divides \$1 & b divides \$1 & \$1 <> 0 ); a * b in INT by INT_1:def_2; then consider k being Element of NAT such that A3: ( a * b = k or a * b = - k ) by INT_1:def_1; b divides a * b by INT_1:def_3; then A4: b divides k by A3, Lm3; a divides a * b by INT_1:def_3; then A5: a divides k by A3, Lm3; k <> 0 by A2, A3, XCMPLX_1:6; then A6: ex k being Nat st S1[k] by A5, A4; consider k being Nat such that A7: S1[k] and A8: for n being Nat st S1[n] holds k <= n from NAT_1:sch_5(A6); take k ; ::_thesis: ( a divides k & b divides k & ( for m being Integer st a divides m & b divides m holds k divides m ) ) thus ( a divides k & b divides k ) by A7; ::_thesis: for m being Integer st a divides m & b divides m holds k divides m let m be Integer; ::_thesis: ( a divides m & b divides m implies k divides m ) m in INT by INT_1:def_2; then consider n being Element of NAT such that A9: ( m = n or m = - n ) by INT_1:def_1; assume that A10: a divides m and A11: b divides m ; ::_thesis: k divides m b divides n by A9, A11, Lm3; then A12: b divides n mod k by A7, Lm6; A13: k > 0 by A7, NAT_1:3; then n mod k in NAT by INT_1:3, INT_1:57; then reconsider i = n mod k as Nat ; assume A14: not k divides m ; ::_thesis: contradiction A15: now__::_thesis:_not_i_=_0 assume i = 0 ; ::_thesis: contradiction then n - ((n div k) * k) = 0 by A7, INT_1:def_10; then k divides n by INT_1:def_3; hence contradiction by A9, A14, Lm3; ::_thesis: verum end; a divides n by A9, A10, Lm3; then a divides n mod k by A7, Lm6; then k divides n by A8, A13, A12, A15, INT_1:58; hence contradiction by A9, A14, Lm3; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Nat st a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds b1 divides m ) & a divides b2 & b divides b2 & ( for m being Integer st a divides m & b divides m holds b2 divides m ) holds b1 = b2 proof let IT1, IT2 be Nat; ::_thesis: ( a divides IT1 & b divides IT1 & ( for m being Integer st a divides m & b divides m holds IT1 divides m ) & a divides IT2 & b divides IT2 & ( for m being Integer st a divides m & b divides m holds IT2 divides m ) implies IT1 = IT2 ) assume ( a divides IT1 & b divides IT1 & ( for m being Integer st a divides m & b divides m holds IT1 divides m ) & a divides IT2 & b divides IT2 & ( for m being Integer st a divides m & b divides m holds IT2 divides m ) ) ; ::_thesis: IT1 = IT2 then ( IT1 divides IT2 & IT2 divides IT1 ) ; hence IT1 = IT2 by Lm8; ::_thesis: verum end; commutativity for b1 being Nat for a, b being Integer st a divides b1 & b divides b1 & ( for m being Integer st a divides m & b divides m holds b1 divides m ) holds ( b divides b1 & a divides b1 & ( for m being Integer st b divides m & a divides m holds b1 divides m ) ) ; end; :: deftheorem Def1 defines lcm INT_2:def_1_:_ for a, b being Integer for b3 being Nat holds ( b3 = a lcm b iff ( a divides b3 & b divides b3 & ( for m being Integer st a divides m & b divides m holds b3 divides m ) ) ); theorem Th4: :: INT_2:4 for a, b being Integer holds ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) proof let a, b be Integer; ::_thesis: ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) A1: ( b = 0 implies a lcm b = 0 ) proof assume b = 0 ; ::_thesis: a lcm b = 0 then 0 divides a lcm b by Def1; hence a lcm b = 0 by Th3; ::_thesis: verum end; A2: ( not a lcm b = 0 or a = 0 or b = 0 ) proof A3: ( b divides b implies b divides b * a ) by Th2; assume A4: a lcm b = 0 ; ::_thesis: ( a = 0 or b = 0 ) ( a divides a implies a divides a * b ) by Th2; then 0 divides a * b by A4, A3, Def1; then a * b = 0 by Th3; hence ( a = 0 or b = 0 ) by XCMPLX_1:6; ::_thesis: verum end; ( a = 0 implies a lcm b = 0 ) proof assume a = 0 ; ::_thesis: a lcm b = 0 then 0 divides a lcm b by Def1; hence a lcm b = 0 by Th3; ::_thesis: verum end; hence ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) by A1, A2; ::_thesis: verum end; Lm9: for j, i being Nat st 0 < j & i divides j holds i <= j proof let j, i be Nat; ::_thesis: ( 0 < j & i divides j implies i <= j ) assume that A1: 0 < j and A2: i divides j ; ::_thesis: i <= j consider l being Nat such that A3: j = i * l by A2, Lm7; l <> 0 by A1, A3; then consider k being Nat such that A4: l = k + 1 by NAT_1:6; i * (k + 1) = i + (i * k) ; hence i <= j by A3, A4, NAT_1:11; ::_thesis: verum end; definition let a, b be Integer; funca gcd b -> Nat means :Def2: :: INT_2:def 2 ( it divides a & it divides b & ( for m being Integer st m divides a & m divides b holds m divides it ) ); existence ex b1 being Nat st ( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) ) proof percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; supposeA1: a = 0 ; ::_thesis: ex b1 being Nat st ( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) ) b in INT by INT_1:def_2; then consider k being Element of NAT such that A2: ( b = k or b = - k ) by INT_1:def_1; take k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds m divides k ) ) thus ( k divides a & k divides b ) by A1, A2, Lm4, Lm5; ::_thesis: for m being Integer st m divides a & m divides b holds m divides k let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k ) assume that m divides a and A3: m divides b ; ::_thesis: m divides k thus m divides k by A2, A3, Lm3; ::_thesis: verum end; supposeA4: b = 0 ; ::_thesis: ex b1 being Nat st ( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) ) a in INT by INT_1:def_2; then consider k being Element of NAT such that A5: ( a = k or a = - k ) by INT_1:def_1; take k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds m divides k ) ) thus ( k divides a & k divides b ) by A4, A5, Lm4, Lm5; ::_thesis: for m being Integer st m divides a & m divides b holds m divides k let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k ) assume that A6: m divides a and m divides b ; ::_thesis: m divides k thus m divides k by A5, A6, Lm3; ::_thesis: verum end; supposeA7: ( a <> 0 & b <> 0 ) ; ::_thesis: ex b1 being Nat st ( b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) ) defpred S1[ Nat] means ( \$1 divides a & \$1 divides b & \$1 <> 0 ); A8: a divides a * b by INT_1:def_3; a * b in INT by INT_1:def_2; then consider k being Element of NAT such that A9: ( a * b = k or a * b = - k ) by INT_1:def_1; k <> 0 by A7, A9, XCMPLX_1:6; then A10: k > 0 by NAT_1:3; A11: for i being Nat st S1[i] holds i <= k proof let i be Nat; ::_thesis: ( S1[i] implies i <= k ) assume S1[i] ; ::_thesis: i <= k then i divides a * b by A8, Lm2; then i divides k by A9, Lm3; hence i <= k by A10, Lm9; ::_thesis: verum end; ( 1 divides a & 1 divides b ) by Lm5; then A12: ex k being Nat st S1[k] ; consider k being Nat such that A13: S1[k] and A14: for n being Nat st S1[n] holds n <= k from NAT_1:sch_6(A11, A12); take k ; ::_thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds m divides k ) ) thus ( k divides a & k divides b ) by A13; ::_thesis: for m being Integer st m divides a & m divides b holds m divides k let m be Integer; ::_thesis: ( m divides a & m divides b implies m divides k ) assume that A15: m divides a and A16: m divides b ; ::_thesis: m divides k m in INT by INT_1:def_2; then consider n being Element of NAT such that A17: ( m = n or m = - n ) by INT_1:def_1; set i = n lcm k; A18: k divides n lcm k by Def1; A19: now__::_thesis:_not_n_lcm_k_=_0 assume n lcm k = 0 ; ::_thesis: contradiction then ( n = 0 or k = 0 ) by Th4; hence contradiction by A7, A13, A17, A15, Th3; ::_thesis: verum end; then 0 < n lcm k by NAT_1:3; then A20: k <= n lcm k by A18, Lm9; n divides b by A17, A16, Lm4; then A21: n lcm k divides b by A13, Def1; n divides a by A17, A15, Lm4; then n lcm k divides a by A13, Def1; then k >= n lcm k by A14, A21, A19; then k = n lcm k by A20, XXREAL_0:1; then A22: n divides k by Def1; assume not m divides k ; ::_thesis: contradiction hence contradiction by A17, A22, Lm4; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Nat st b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) & b2 divides a & b2 divides b & ( for m being Integer st m divides a & m divides b holds m divides b2 ) holds b1 = b2 proof let IT1, IT2 be Nat; ::_thesis: ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds m divides IT2 ) implies IT1 = IT2 ) assume ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds m divides IT2 ) ) ; ::_thesis: IT1 = IT2 then ( IT1 divides IT2 & IT2 divides IT1 ) ; hence IT1 = IT2 by Lm8; ::_thesis: verum end; commutativity for b1 being Nat for a, b being Integer st b1 divides a & b1 divides b & ( for m being Integer st m divides a & m divides b holds m divides b1 ) holds ( b1 divides b & b1 divides a & ( for m being Integer st m divides b & m divides a holds m divides b1 ) ) ; end; :: deftheorem Def2 defines gcd INT_2:def_2_:_ for a, b being Integer for b3 being Nat holds ( b3 = a gcd b iff ( b3 divides a & b3 divides b & ( for m being Integer st m divides a & m divides b holds m divides b3 ) ) ); theorem Th5: :: INT_2:5 for a, b being Integer holds ( ( a = 0 & b = 0 ) iff a gcd b = 0 ) proof let a, b be Integer; ::_thesis: ( ( a = 0 & b = 0 ) iff a gcd b = 0 ) 0 divides 0 gcd 0 by Def2; hence ( a = 0 & b = 0 implies a gcd b = 0 ) by Th3; ::_thesis: ( a gcd b = 0 implies ( a = 0 & b = 0 ) ) assume a gcd b = 0 ; ::_thesis: ( a = 0 & b = 0 ) then ( 0 divides a & 0 divides b ) by Def2; hence ( a = 0 & b = 0 ) by Th3; ::_thesis: verum end; theorem Th6: :: INT_2:6 for n being Nat holds ( - n is Element of NAT iff n = 0 ) proof let n be Nat; ::_thesis: ( - n is Element of NAT iff n = 0 ) thus ( - n is Element of NAT implies n = 0 ) ::_thesis: ( n = 0 implies - n is Element of NAT ) proof assume - n is Element of NAT ; ::_thesis: n = 0 then ( - n >= 0 & n + (- n) >= 0 + n ) by NAT_1:2; hence n = 0 ; ::_thesis: verum end; thus ( n = 0 implies - n is Element of NAT ) ; ::_thesis: verum end; registration let n be non zero Nat; cluster - n -> non natural ; coherence not - n is natural proof - n is not Element of NAT by Th6; hence not - n is natural by ORDINAL1:def_12; ::_thesis: verum end; end; theorem :: INT_2:7 - 1 is not Element of NAT ; theorem :: INT_2:8 for a being Integer holds ( a divides - a & - a divides a ) by Lm1; theorem :: INT_2:9 for a, b, c being Integer st a divides b & b divides c holds a divides c by Lm2; theorem Th10: :: INT_2:10 for a, b being Integer holds ( ( a divides b implies a divides - b ) & ( a divides - b implies a divides b ) & ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) ) proof let a, b be Integer; ::_thesis: ( ( a divides b implies a divides - b ) & ( a divides - b implies a divides b ) & ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) ) A1: ( a divides b implies a divides - b ) proof assume A2: a divides b ; ::_thesis: a divides - b b divides - b by Lm1; hence a divides - b by A2, Lm2; ::_thesis: verum end; A3: ( a divides - b implies a divides b ) proof assume A4: a divides - b ; ::_thesis: a divides b - b divides b by Lm1; hence a divides b by A4, Lm2; ::_thesis: verum end; hence ( a divides b iff a divides - b ) by A1; ::_thesis: ( ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) ) A5: ( - a divides b implies a divides b ) proof assume A6: - a divides b ; ::_thesis: a divides b a divides - a by Lm1; hence a divides b by A6, Lm2; ::_thesis: verum end; A7: ( - a divides - b implies a divides b ) proof assume A8: - a divides - b ; ::_thesis: a divides b - b divides b by Lm1; hence a divides b by A5, A8, Lm2; ::_thesis: verum end; A9: ( a divides b implies - a divides b ) proof assume A10: a divides b ; ::_thesis: - a divides b - a divides a by Lm1; hence - a divides b by A10, Lm2; ::_thesis: verum end; hence ( a divides b iff - a divides b ) by A5; ::_thesis: ( ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) ) ( a divides b implies - a divides - b ) proof assume A11: a divides b ; ::_thesis: - a divides - b - a divides a by Lm1; hence - a divides - b by A1, A11, Lm2; ::_thesis: verum end; hence ( a divides b iff - a divides - b ) by A7; ::_thesis: ( a divides - b iff - a divides b ) thus ( a divides - b iff - a divides b ) by A1, A3, A9, A5; ::_thesis: verum end; theorem :: INT_2:11 for a, b being Integer st a divides b & b divides a & not a = b holds a = - b proof let a, b be Integer; ::_thesis: ( a divides b & b divides a & not a = b implies a = - b ) assume that A1: a divides b and A2: b divides a ; ::_thesis: ( a = b or a = - b ) consider a1 being Integer such that A3: b = a * a1 by A1, INT_1:def_3; consider b1 being Integer such that A4: a = b * b1 by A2, INT_1:def_3; ( not a <> 0 or a = b or a = - b ) proof assume A5: a <> 0 ; ::_thesis: ( a = b or a = - b ) 1 * a = a * (a1 * b1) by A3, A4; then a1 * b1 = 1 by A5, XCMPLX_1:5; then ( a = b * 1 or a = b * (- 1) ) by A4, INT_1:9; hence ( a = b or a = - b ) ; ::_thesis: verum end; hence ( a = b or a = - b ) by A1, Th3; ::_thesis: verum end; theorem :: INT_2:12 for a being Integer holds ( a divides 0 & 1 divides a & - 1 divides a ) by Lm5; theorem Th13: :: INT_2:13 for a being Integer holds ( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 ) proof let a be Integer; ::_thesis: ( ( not a divides 1 & not a divides - 1 ) or a = 1 or a = - 1 ) A1: ( not a divides 1 or a = 1 or a = - 1 ) proof assume a divides 1 ; ::_thesis: ( a = 1 or a = - 1 ) then ex b being Integer st 1 = a * b by INT_1:def_3; hence ( a = 1 or a = - 1 ) by INT_1:9; ::_thesis: verum end; A2: ( not a divides - 1 or a = 1 or a = - 1 ) proof assume a divides - 1 ; ::_thesis: ( a = 1 or a = - 1 ) then ex b being Integer st - 1 = a * b by INT_1:def_3; hence ( a = 1 or a = - 1 ) by INT_1:10; ::_thesis: verum end; assume ( a divides 1 or a divides - 1 ) ; ::_thesis: ( a = 1 or a = - 1 ) hence ( a = 1 or a = - 1 ) by A1, A2; ::_thesis: verum end; theorem :: INT_2:14 for a being Integer st ( a = 1 or a = - 1 ) holds ( a divides 1 & a divides - 1 ) by Lm5; theorem :: INT_2:15 for a, b, c being Integer holds ( a,b are_congruent_mod c iff c divides a - b ) proof let a, b, c be Integer; ::_thesis: ( a,b are_congruent_mod c iff c divides a - b ) thus ( a,b are_congruent_mod c implies c divides a - b ) ::_thesis: ( c divides a - b implies a,b are_congruent_mod c ) proof assume a,b are_congruent_mod c ; ::_thesis: c divides a - b then ex d being Integer st a - b = c * d by INT_1:def_5; hence c divides a - b by INT_1:def_3; ::_thesis: verum end; assume c divides a - b ; ::_thesis: a,b are_congruent_mod c then ex d being Integer st a - b = c * d by INT_1:def_3; hence a,b are_congruent_mod c by INT_1:def_5; ::_thesis: verum end; theorem :: INT_2:16 for a, b being Integer holds ( a divides b iff abs a divides abs b ) proof let a, b be Integer; ::_thesis: ( a divides b iff abs a divides abs b ) thus ( a divides b implies abs a divides abs b ) ::_thesis: ( abs a divides abs b implies a divides b ) proof assume a divides b ; ::_thesis: abs a divides abs b then consider c being Integer such that A1: b = a * c by INT_1:def_3; abs b = (abs a) * (abs c) by A1, COMPLEX1:65; hence abs a divides abs b by INT_1:def_3; ::_thesis: verum end; assume abs a divides abs b ; ::_thesis: a divides b then consider m being Integer such that A2: abs b = (abs a) * m by INT_1:def_3; A3: ( a >= 0 implies a divides b ) proof assume a >= 0 ; ::_thesis: a divides b then A4: abs b = a * m by A2, ABSVALUE:def_1; percases ( b < 0 or b >= 0 ) ; suppose b < 0 ; ::_thesis: a divides b then - b = a * m by A4, ABSVALUE:def_1; then b = a * (- m) ; hence a divides b by INT_1:def_3; ::_thesis: verum end; suppose b >= 0 ; ::_thesis: a divides b then b = a * m by A4, ABSVALUE:def_1; hence a divides b by INT_1:def_3; ::_thesis: verum end; end; end; ( a < 0 implies a divides b ) proof assume a < 0 ; ::_thesis: a divides b then A5: abs b = (- a) * m by A2, ABSVALUE:def_1; percases ( b < 0 or b >= 0 ) ; suppose b < 0 ; ::_thesis: a divides b then - b = - (a * m) by A5, ABSVALUE:def_1; hence a divides b by INT_1:def_3; ::_thesis: verum end; suppose b >= 0 ; ::_thesis: a divides b then b = a * (- m) by A5, ABSVALUE:def_1; hence a divides b by INT_1:def_3; ::_thesis: verum end; end; end; hence a divides b by A3; ::_thesis: verum end; theorem :: INT_2:17 for a, b being Integer holds a lcm b is Element of NAT by ORDINAL1:def_12; theorem :: INT_2:18 for a, b being Integer holds a divides a lcm b by Def1; theorem :: INT_2:19 for a, b, c being Integer st a divides c & b divides c holds a lcm b divides c by Def1; theorem :: INT_2:20 for a, b being Integer holds a gcd b is Element of NAT by ORDINAL1:def_12; theorem Th21: :: INT_2:21 for a, b being Integer holds a gcd b divides a by Def2; theorem :: INT_2:22 for a, b, c being Integer st c divides a & c divides b holds c divides a gcd b by Def2; definition let a, b be Integer; preda,b are_relative_prime means :Def3: :: INT_2:def 3 a gcd b = 1; symmetry for a, b being Integer st a gcd b = 1 holds b gcd a = 1 ; end; :: deftheorem Def3 defines are_relative_prime INT_2:def_3_:_ for a, b being Integer holds ( a,b are_relative_prime iff a gcd b = 1 ); theorem :: INT_2:23 for a, b being Integer st ( a <> 0 or b <> 0 ) holds ex a1, b1 being Integer st ( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) proof let a, b be Integer; ::_thesis: ( ( a <> 0 or b <> 0 ) implies ex a1, b1 being Integer st ( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) ) assume ( a <> 0 or b <> 0 ) ; ::_thesis: ex a1, b1 being Integer st ( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) then A1: a gcd b <> 0 by Th5; a gcd b divides a by Def2; then consider a1 being Integer such that A2: a = (a gcd b) * a1 by INT_1:def_3; a gcd b divides b by Def2; then consider b1 being Integer such that A3: b = (a gcd b) * b1 by INT_1:def_3; a1 gcd b1 divides b1 by Def2; then consider b2 being Integer such that A4: b1 = (a1 gcd b1) * b2 by INT_1:def_3; b = ((a gcd b) * (a1 gcd b1)) * b2 by A3, A4; then A5: (a gcd b) * (a1 gcd b1) divides b by INT_1:def_3; a1 gcd b1 divides a1 by Def2; then consider a2 being Integer such that A6: a1 = (a1 gcd b1) * a2 by INT_1:def_3; a = ((a gcd b) * (a1 gcd b1)) * a2 by A2, A6; then (a gcd b) * (a1 gcd b1) divides a by INT_1:def_3; then (a gcd b) * (a1 gcd b1) divides a gcd b by A5, Def2; then consider c being Integer such that A7: a gcd b = ((a gcd b) * (a1 gcd b1)) * c by INT_1:def_3; (a gcd b) * 1 = (a gcd b) * ((a1 gcd b1) * c) by A7; then 1 = (a1 gcd b1) * c by A1, XCMPLX_1:5; then ( a1 gcd b1 = 1 or a1 gcd b1 = - 1 ) by INT_1:9; then a1,b1 are_relative_prime by Def3; hence ex a1, b1 being Integer st ( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_relative_prime ) by A2, A3; ::_thesis: verum end; theorem Th24: :: INT_2:24 for a, b, c being Integer st a,b are_relative_prime holds ( (c * a) gcd (c * b) = abs c & (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) proof let a, b, c be Integer; ::_thesis: ( a,b are_relative_prime implies ( (c * a) gcd (c * b) = abs c & (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) ) assume a,b are_relative_prime ; ::_thesis: ( (c * a) gcd (c * b) = abs c & (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) then A1: a gcd b = 1 by Def3; thus A2: (c * a) gcd (c * b) = abs c ::_thesis: ( (c * a) gcd (b * c) = abs c & (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) proof (c * a) gcd (c * b) divides c * b by Def2; then consider l being Integer such that A3: c * b = ((c * a) gcd (c * b)) * l by INT_1:def_3; (c * a) gcd (c * b) divides c * a by Def2; then consider k being Integer such that A4: c * a = ((c * a) gcd (c * b)) * k by INT_1:def_3; ( c divides c * a & c divides c * b ) by Th2; then c divides (c * a) gcd (c * b) by Def2; then consider d being Integer such that A5: (c * a) gcd (c * b) = c * d by INT_1:def_3; A6: c * b = c * (d * l) by A5, A3; A7: c * a = c * (d * k) by A5, A4; A8: ( c <> 0 implies (c * a) gcd (c * b) = abs c ) proof assume A9: c <> 0 ; ::_thesis: (c * a) gcd (c * b) = abs c then b = d * l by A6, XCMPLX_1:5; then A10: d divides b by INT_1:def_3; a = d * k by A7, A9, XCMPLX_1:5; then d divides a by INT_1:def_3; then d divides 1 by A1, A10, Def2; then ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = c * (- 1) ) by A5, Th13; then ( (c * a) gcd (c * b) = c * 1 or (c * a) gcd (c * b) = (- c) * 1 ) ; then A11: abs ((c * a) gcd (c * b)) = abs c by COMPLEX1:52; (c * a) gcd (c * b) >= 0 by NAT_1:2; hence (c * a) gcd (c * b) = abs c by A11, ABSVALUE:def_1; ::_thesis: verum end; (0 * a) gcd (0 * b) = 0 by Th5 .= abs 0 by ABSVALUE:2 ; hence (c * a) gcd (c * b) = abs c by A8; ::_thesis: verum end; hence (c * a) gcd (b * c) = abs c ; ::_thesis: ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) thus ( (a * c) gcd (c * b) = abs c & (a * c) gcd (b * c) = abs c ) by A2; ::_thesis: verum end; theorem Th25: :: INT_2:25 for c, a, b being Integer st c divides a * b & a,c are_relative_prime holds c divides b proof let c, a, b be Integer; ::_thesis: ( c divides a * b & a,c are_relative_prime implies c divides b ) assume that A1: c divides a * b and A2: a,c are_relative_prime ; ::_thesis: c divides b c divides c * b by Th2; then A3: c divides (a * b) gcd (c * b) by A1, Def2; A4: (a * b) gcd (c * b) = abs b by A2, Th24; ( b < 0 implies c divides b ) proof assume b < 0 ; ::_thesis: c divides b then c divides - b by A4, A3, ABSVALUE:def_1; hence c divides b by Th10; ::_thesis: verum end; hence c divides b by A4, A3, ABSVALUE:def_1; ::_thesis: verum end; theorem :: INT_2:26 for a, c, b being Integer st a,c are_relative_prime & b,c are_relative_prime holds a * b,c are_relative_prime proof let a, c, b be Integer; ::_thesis: ( a,c are_relative_prime & b,c are_relative_prime implies a * b,c are_relative_prime ) assume that A1: a,c are_relative_prime and A2: b,c are_relative_prime ; ::_thesis: a * b,c are_relative_prime A3: a gcd c = 1 by A1, Def3; A4: ((a * b) gcd c) gcd a divides a by Def2; A5: (a * b) gcd c divides c by Def2; ((a * b) gcd c) gcd a divides (a * b) gcd c by Def2; then ((a * b) gcd c) gcd a divides c by A5, Lm2; then ((a * b) gcd c) gcd a divides 1 by A3, A4, Def2; then ( ((a * b) gcd c) gcd a = 1 or ((a * b) gcd c) gcd a = - 1 ) by Th13; then a,(a * b) gcd c are_relative_prime by Def3; then A6: (a * b) gcd c divides b by Th21, Th25; b gcd c = 1 by A2, Def3; then (a * b) gcd c divides 1 by A5, A6, Def2; then ( (a * b) gcd c = 1 or (a * b) gcd c = - 1 ) by Th13; hence a * b,c are_relative_prime by Def3; ::_thesis: verum end; definition let p be Nat; attrp is prime means :Def4: :: INT_2:def 4 ( p > 1 & ( for n being Nat holds ( not n divides p or n = 1 or n = p ) ) ); end; :: deftheorem Def4 defines prime INT_2:def_4_:_ for p being Nat holds ( p is prime iff ( p > 1 & ( for n being Nat holds ( not n divides p or n = 1 or n = p ) ) ) ); theorem Th27: :: INT_2:27 for b, a being Integer st 0 < b & a divides b holds a <= b proof let b, a be Integer; ::_thesis: ( 0 < b & a divides b implies a <= b ) assume A1: 0 < b ; ::_thesis: ( not a divides b or a <= b ) assume a divides b ; ::_thesis: a <= b then consider c being Integer such that A2: b = a * c by INT_1:def_3; percases ( a <= 0 or a > 0 ) ; suppose a <= 0 ; ::_thesis: a <= b hence a <= b by A1, XXREAL_0:2; ::_thesis: verum end; supposeA3: a > 0 ; ::_thesis: a <= b then c > 0 by A1, A2, XREAL_1:131; then c >= 0 + 1 by INT_1:7; hence a <= b by A2, A3, XREAL_1:151; ::_thesis: verum end; end; end; theorem Th28: :: INT_2:28 2 is prime proof thus 2 > 1 ; :: according to INT_2:def_4 ::_thesis: for n being Nat holds ( not n divides 2 or n = 1 or n = 2 ) let n be Nat; ::_thesis: ( not n divides 2 or n = 1 or n = 2 ) assume A1: n divides 2 ; ::_thesis: ( n = 1 or n = 2 ) then n <= 2 by Th27; then ( n = 0 or n = 1 or n = 2 ) by NAT_1:26; hence ( n = 1 or n = 2 ) by A1, Th3; ::_thesis: verum end; theorem Th29: :: INT_2:29 not 4 is prime proof ex n being Nat st ( n divides 4 & n <> 1 & n <> 4 ) proof take 2 ; ::_thesis: ( 2 divides 4 & 2 <> 1 & 2 <> 4 ) 4 = 2 * 2 ; hence ( 2 divides 4 & 2 <> 1 & 2 <> 4 ) by INT_1:def_3; ::_thesis: verum end; hence not 4 is prime by Def4; ::_thesis: verum end; registration cluster ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer prime for set ; existence ex b1 being Nat st b1 is prime by Th28; cluster ext-real non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer non prime for set ; existence ex b1 being Nat st ( not b1 is zero & not b1 is prime ) by Th29; end; theorem :: INT_2:30 for p, q being Nat st p is prime & q is prime & not p,q are_relative_prime holds p = q proof let p, q be Nat; ::_thesis: ( p is prime & q is prime & not p,q are_relative_prime implies p = q ) assume that A1: p is prime and A2: q is prime ; ::_thesis: ( p,q are_relative_prime or p = q ) A3: p gcd q divides q by Def2; assume not p,q are_relative_prime ; ::_thesis: p = q then A4: p gcd q <> 1 by Def3; p gcd q divides p by Def2; then p gcd q = p by A1, A4, Def4; hence p = q by A2, A4, A3, Def4; ::_thesis: verum end; theorem :: INT_2:31 for l being Nat st l >= 2 holds ex p being Element of NAT st ( p is prime & p divides l ) proof let l be Nat; ::_thesis: ( l >= 2 implies ex p being Element of NAT st ( p is prime & p divides l ) ) defpred S1[ Nat] means ex p being Nat st ( p is prime & p divides \$1 ); A1: for k being Nat st k >= 2 & ( for n being Nat st n >= 2 & n < k holds S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( k >= 2 & ( for n being Nat st n >= 2 & n < k holds S1[n] ) implies S1[k] ) assume A2: k >= 2 ; ::_thesis: ( ex n being Nat st ( n >= 2 & n < k & not S1[n] ) or S1[k] ) assume A3: for n being Nat st n >= 2 & n < k holds ex p being Nat st ( p is prime & p divides n ) ; ::_thesis: S1[k] A4: (k + 1) - 1 > (1 + 1) - 1 by A2, NAT_1:13; ( not k is prime implies ex p being Element of NAT st ( p is prime & p divides k ) ) proof assume not k is prime ; ::_thesis: ex p being Element of NAT st ( p is prime & p divides k ) then consider m being Nat such that A5: m divides k and A6: m <> 1 and A7: m <> k by A4, Def4; m <> 0 by A5, A7, Th3; then m > 0 by NAT_1:3; then m >= 0 + 1 by NAT_1:13; then m > 1 by A6, XXREAL_0:1; then A8: m >= 1 + 1 by NAT_1:13; k > 0 by A2, XXREAL_0:2; then m <= k by A5, Th27; then m < k by A7, XXREAL_0:1; then consider p1 being Nat such that A9: ( p1 is prime & p1 divides m ) by A3, A8; reconsider p1 = p1 as Element of NAT by ORDINAL1:def_12; take p1 ; ::_thesis: ( p1 is prime & p1 divides k ) thus ( p1 is prime & p1 divides k ) by A5, A9, Lm2; ::_thesis: verum end; hence S1[k] ; ::_thesis: verum end; A10: for k being Nat st k >= 2 holds S1[k] from NAT_1:sch_9(A1); assume l >= 2 ; ::_thesis: ex p being Element of NAT st ( p is prime & p divides l ) then consider p being Nat such that A11: ( p is prime & p divides l ) by A10; reconsider p = p as Element of NAT by ORDINAL1:def_12; take p ; ::_thesis: ( p is prime & p divides l ) thus ( p is prime & p divides l ) by A11; ::_thesis: verum end; begin theorem :: INT_2:32 for i, j being Integer st i >= 0 & j >= 0 holds ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) proof let i, j be Integer; ::_thesis: ( i >= 0 & j >= 0 implies ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) ) assume that A1: i >= 0 and A2: j >= 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) percases ( j > 0 or j = 0 ) by A2, XXREAL_0:1; supposeA3: j > 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) i = abs i by A1, ABSVALUE:def_1; hence ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A3, ABSVALUE:def_1; ::_thesis: verum end; supposeA4: j = 0 ; ::_thesis: ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) abs 0 = 0 by ABSVALUE:def_1; then ( (abs i) mod (abs 0) = 0 & (abs i) div (abs 0) = 0 ) by INT_1:48, INT_1:def_10; hence ( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j ) by A4, INT_1:48, INT_1:def_10; ::_thesis: verum end; end; end; theorem :: INT_2:33 for a, b being Integer holds a lcm b = (abs a) lcm (abs b) proof let a, b be Integer; ::_thesis: a lcm b = (abs a) lcm (abs b) A1: ( abs b = b or abs b = - b ) by ABSVALUE:1; A2: ( abs a = a or abs a = - a ) by ABSVALUE:1; A3: now__::_thesis:_for_m_being_Integer_st_abs_a_divides_m_&_abs_b_divides_m_holds_ a_lcm_b_divides_m let m be Integer; ::_thesis: ( abs a divides m & abs b divides m implies a lcm b divides m ) assume ( abs a divides m & abs b divides m ) ; ::_thesis: a lcm b divides m then ( a divides m & b divides m ) by A2, A1, Th10; hence a lcm b divides m by Def1; ::_thesis: verum end; b divides a lcm b by Def1; then A4: abs b divides a lcm b by A1, Th10; a divides a lcm b by Def1; then abs a divides a lcm b by A2, Th10; hence a lcm b = (abs a) lcm (abs b) by A4, A3, Def1; ::_thesis: verum end; theorem :: INT_2:34 for a, b being Integer holds a gcd b = (abs a) gcd (abs b) proof let a, b be Integer; ::_thesis: a gcd b = (abs a) gcd (abs b) A1: ( abs b = b or abs b = - b ) by ABSVALUE:1; A2: ( abs a = a or abs a = - a ) by ABSVALUE:1; A3: now__::_thesis:_for_m_being_Integer_st_m_divides_abs_a_&_m_divides_abs_b_holds_ m_divides_a_gcd_b let m be Integer; ::_thesis: ( m divides abs a & m divides abs b implies m divides a gcd b ) assume ( m divides abs a & m divides abs b ) ; ::_thesis: m divides a gcd b then ( m divides a & m divides b ) by A2, A1, Th10; hence m divides a gcd b by Def2; ::_thesis: verum end; a gcd b divides b by Def2; then A4: a gcd b divides abs b by A1, Th10; a gcd b divides a by Def2; then a gcd b divides abs a by A2, Th10; hence a gcd b = (abs a) gcd (abs b) by A4, A3, Def2; ::_thesis: verum end;