:: WSIERP_1 semantic presentation begin theorem Th1: :: WSIERP_1:1 for x being real number holds ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 ) proof let x be real number ; ::_thesis: ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 ) A1: (- x) |^ 1 = - x by NEWTON:5; A2: x = x |^ 1 by NEWTON:5; then x |^ (1 + 1) = x * x by NEWTON:8; then x |^ 2 = (- x) * (- x) .= (- x) |^ (1 + 1) by A1, NEWTON:8 ; hence ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 ) by A2, NEWTON:8; ::_thesis: verum end; theorem Th2: :: WSIERP_1:2 for x being real number for a being Nat holds ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) proof let x be real number ; ::_thesis: for a being Nat holds ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) let a be Nat; ::_thesis: ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) A1: (- x) |^ (2 * a) = ((- x) |^ 2) |^ a by NEWTON:9 .= (x |^ 2) |^ a by Th1 .= x |^ (2 * a) by NEWTON:9 ; (- x) |^ ((2 * a) + 1) = ((- x) |^ (2 * a)) * (- x) by NEWTON:6 .= - ((x |^ (2 * a)) * x) by A1 .= - (x |^ ((2 * a) + 1)) by NEWTON:6 ; hence ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) by A1; ::_thesis: verum end; theorem Th3: :: WSIERP_1:3 for x, y being real number for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds x = y proof let x, y be real number ; ::_thesis: for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds x = y let d be Nat; ::_thesis: ( x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d implies x = y ) assume that A1: x >= 0 and A2: y >= 0 and A3: d > 0 and A4: x |^ d = y |^ d ; ::_thesis: x = y A5: d >= 1 by A3, NAT_1:14; then x = d -Root (x |^ d) by A1, PREPOWER:19 .= y by A2, A4, A5, PREPOWER:19 ; hence x = y ; ::_thesis: verum end; Lm1: for x, y being real number holds ( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) ) proof let x, y be real number ; ::_thesis: ( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) ) A1: ( x >= 0 iff x + y >= 0 + y ) by XREAL_1:6; hence ( x >= 0 iff x + y >= y ) ; ::_thesis: ( ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) ) A2: ( x > 0 iff x + y > 0 + y ) by XREAL_1:6; hence ( x > 0 iff x + y > y ) ; ::_thesis: ( ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) ) thus ( x >= 0 iff y >= y - x ) by A1, XREAL_1:20; ::_thesis: ( x > 0 iff y > y - x ) thus ( x > 0 iff y > y - x ) by A2, XREAL_1:19; ::_thesis: verum end; Lm2: for x, y, z being real number st x >= 0 & y >= z holds ( x + y >= z & y >= z - x ) proof let x, y, z be real number ; ::_thesis: ( x >= 0 & y >= z implies ( x + y >= z & y >= z - x ) ) assume ( x >= 0 & y >= z ) ; ::_thesis: ( x + y >= z & y >= z - x ) then x + y >= z + 0 by XREAL_1:7; hence ( x + y >= z & y >= z - x ) by XREAL_1:20; ::_thesis: verum end; Lm3: for x, y, z being real number st ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) holds ( x + y > z & y > z - x ) proof let x, y, z be real number ; ::_thesis: ( ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) implies ( x + y > z & y > z - x ) ) assume ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) ; ::_thesis: ( x + y > z & y > z - x ) then x + y > z + 0 by XREAL_1:8; hence ( x + y > z & y > z - x ) by XREAL_1:19; ::_thesis: verum end; registration let k be Integer; let a be Nat; clusterk |^ a -> integer ; coherence k |^ a is integer proof defpred S1[ Nat] means k |^ k is Integer; A1: for a being Nat st S1[a] holds S1[a + 1] proof let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] ) assume k |^ a is Integer ; ::_thesis: S1[a + 1] then reconsider b = k |^ a as Integer ; k |^ (a + 1) = k * b by NEWTON:6; hence S1[a + 1] ; ::_thesis: verum end; A2: S1[ 0 ] by NEWTON:4; for a being Nat holds S1[a] from NAT_1:sch_2(A2, A1); hence k |^ a is integer ; ::_thesis: verum end; end; Lm4: for a being Nat ex b being Nat st ( a = 2 * b or a = (2 * b) + 1 ) proof let a be Nat; ::_thesis: ex b being Nat st ( a = 2 * b or a = (2 * b) + 1 ) set b = a div 2; set d = a mod 2; a = (2 * (a div 2)) + (a mod 2) by NAT_D:2; then ( a = (2 * (a div 2)) + 0 or a = (2 * (a div 2)) + 1 ) by NAT_1:23, NAT_D:1; hence ex b being Nat st ( a = 2 * b or a = (2 * b) + 1 ) ; ::_thesis: verum end; theorem Th4: :: WSIERP_1:4 for k, m, n being Integer st k divides m & k divides n holds k divides m + n proof let k, m, n be Integer; ::_thesis: ( k divides m & k divides n implies k divides m + n ) assume that A1: k divides m and A2: k divides n ; ::_thesis: k divides m + n consider m1 being Integer such that A3: m = k * m1 by A1, INT_1:def_3; consider n1 being Integer such that A4: n = k * n1 by A2, INT_1:def_3; m + n = k * (m1 + n1) by A3, A4; hence k divides m + n by INT_1:def_3; ::_thesis: verum end; theorem Th5: :: WSIERP_1:5 for k, m, n, m1, n1 being Integer st k divides m & k divides n holds k divides (m * m1) + (n * n1) proof let k, m, n, m1, n1 be Integer; ::_thesis: ( k divides m & k divides n implies k divides (m * m1) + (n * n1) ) assume ( k divides m & k divides n ) ; ::_thesis: k divides (m * m1) + (n * n1) then ( k divides m * m1 & k divides n * n1 ) by INT_2:2; hence k divides (m * m1) + (n * n1) by Th4; ::_thesis: verum end; theorem Th6: :: WSIERP_1:6 for m, n, k being Integer st m gcd n = 1 & k gcd n = 1 holds (m * k) gcd n = 1 proof let m, n, k be Integer; ::_thesis: ( m gcd n = 1 & k gcd n = 1 implies (m * k) gcd n = 1 ) assume ( m gcd n = 1 & k gcd n = 1 ) ; ::_thesis: (m * k) gcd n = 1 then ( m,n are_relative_prime & k,n are_relative_prime ) by INT_2:def_3; then m * k,n are_relative_prime by INT_2:26; hence (m * k) gcd n = 1 by INT_2:def_3; ::_thesis: verum end; theorem :: WSIERP_1:7 for a, b, c being Nat st a gcd b = 1 & c gcd b = 1 holds (a * c) gcd b = 1 by Th6; theorem Th8: :: WSIERP_1:8 for m being Integer holds ( 0 gcd m = abs m & 1 gcd m = 1 ) proof let m be Integer; ::_thesis: ( 0 gcd m = abs m & 1 gcd m = 1 ) A1: m gcd 1 = (abs m) gcd (abs 1) by INT_2:34 .= (abs m) gcd 1 by ABSVALUE:def_1 .= 1 by NEWTON:51 ; m gcd 0 = (abs m) gcd (abs 0) by INT_2:34 .= (abs m) gcd 0 by ABSVALUE:2 .= abs m by NEWTON:52 ; hence ( 0 gcd m = abs m & 1 gcd m = 1 ) by A1; ::_thesis: verum end; theorem Th9: :: WSIERP_1:9 for k being Integer holds 1,k are_relative_prime proof let k be Integer; ::_thesis: 1,k are_relative_prime 1 gcd k = 1 by Th8; hence 1,k are_relative_prime by INT_2:def_3; ::_thesis: verum end; theorem Th10: :: WSIERP_1:10 for a being Nat for k, l being Integer st k,l are_relative_prime holds k |^ a,l are_relative_prime proof let a be Nat; ::_thesis: for k, l being Integer st k,l are_relative_prime holds k |^ a,l are_relative_prime let k, l be Integer; ::_thesis: ( k,l are_relative_prime implies k |^ a,l are_relative_prime ) defpred S1[ Nat] means k |^ \$1,l are_relative_prime ; assume A1: k,l are_relative_prime ; ::_thesis: k |^ a,l are_relative_prime A2: for a being Nat st S1[a] holds S1[a + 1] proof let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] ) assume k |^ a,l are_relative_prime ; ::_thesis: S1[a + 1] then k * (k |^ a),l are_relative_prime by A1, INT_2:26; hence S1[a + 1] by NEWTON:6; ::_thesis: verum end; k |^ 0 = 1 by NEWTON:4; then A3: S1[ 0 ] by Th9; for a being Nat holds S1[a] from NAT_1:sch_2(A3, A2); hence k |^ a,l are_relative_prime ; ::_thesis: verum end; theorem Th11: :: WSIERP_1:11 for a, b being Nat for k, l being Integer st k,l are_relative_prime holds k |^ a,l |^ b are_relative_prime proof let a, b be Nat; ::_thesis: for k, l being Integer st k,l are_relative_prime holds k |^ a,l |^ b are_relative_prime let k, l be Integer; ::_thesis: ( k,l are_relative_prime implies k |^ a,l |^ b are_relative_prime ) assume k,l are_relative_prime ; ::_thesis: k |^ a,l |^ b are_relative_prime then k |^ a,l are_relative_prime by Th10; hence k |^ a,l |^ b are_relative_prime by Th10; ::_thesis: verum end; theorem Th12: :: WSIERP_1:12 for b, a being Nat for k, l being Integer st k gcd l = 1 holds ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) proof let b, a be Nat; ::_thesis: for k, l being Integer st k gcd l = 1 holds ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) let k, l be Integer; ::_thesis: ( k gcd l = 1 implies ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) ) assume k gcd l = 1 ; ::_thesis: ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) then k,l are_relative_prime by INT_2:def_3; then ( k,l |^ b are_relative_prime & k |^ a,l |^ b are_relative_prime ) by Th10, Th11; hence ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) by INT_2:def_3; ::_thesis: verum end; theorem :: WSIERP_1:13 for m, k being Integer holds ( abs m divides k iff m divides k ) proof let m, k be Integer; ::_thesis: ( abs m divides k iff m divides k ) A1: now__::_thesis:_(_m_divides_k_implies_abs_m_divides_k_) assume m divides k ; ::_thesis: abs m divides k then consider l being Integer such that A2: m * l = k by INT_1:def_3; now__::_thesis:_abs_m_divides_k percases ( m >= 0 or m < 0 ) ; suppose m >= 0 ; ::_thesis: abs m divides k then (abs m) * l = k by A2, ABSVALUE:def_1; hence abs m divides k by INT_1:def_3; ::_thesis: verum end; suppose m < 0 ; ::_thesis: abs m divides k then (abs m) * (- l) = (- m) * (- l) by ABSVALUE:def_1 .= k by A2 ; hence abs m divides k by INT_1:def_3; ::_thesis: verum end; end; end; hence abs m divides k ; ::_thesis: verum end; now__::_thesis:_(_abs_m_divides_k_implies_m_divides_k_) assume abs m divides k ; ::_thesis: m divides k then consider l being Integer such that A3: (abs m) * l = k by INT_1:def_3; now__::_thesis:_m_divides_k percases ( m >= 0 or m < 0 ) ; suppose m >= 0 ; ::_thesis: m divides k then m * l = k by A3, ABSVALUE:def_1; hence m divides k by INT_1:def_3; ::_thesis: verum end; suppose m < 0 ; ::_thesis: m divides k then k = (- m) * l by A3, ABSVALUE:def_1 .= m * (- l) ; hence m divides k by INT_1:def_3; ::_thesis: verum end; end; end; hence m divides k ; ::_thesis: verum end; hence ( abs m divides k iff m divides k ) by A1; ::_thesis: verum end; theorem Th14: :: WSIERP_1:14 for a, b, c being Nat st a divides b holds a |^ c divides b |^ c proof let a, b, c be Nat; ::_thesis: ( a divides b implies a |^ c divides b |^ c ) assume a divides b ; ::_thesis: a |^ c divides b |^ c then consider d being Nat such that A1: a * d = b by NAT_D:def_3; b |^ c = (a |^ c) * (d |^ c) by A1, NEWTON:7; hence a |^ c divides b |^ c by NAT_D:def_3; ::_thesis: verum end; theorem Th15: :: WSIERP_1:15 for a being Nat st a divides 1 holds a = 1 proof let a be Nat; ::_thesis: ( a divides 1 implies a = 1 ) assume A1: a divides 1 ; ::_thesis: a = 1 then a divides 1 + 1 by NAT_D:8; hence a = 1 by A1, NEWTON:39; ::_thesis: verum end; theorem :: WSIERP_1:16 for d, a, b being Nat st d divides a & a gcd b = 1 holds d gcd b = 1 by Th15, NEWTON:57; Lm5: for a, b being Nat st a <> 0 holds ( a divides b iff b / a is Element of NAT ) proof let a, b be Nat; ::_thesis: ( a <> 0 implies ( a divides b iff b / a is Element of NAT ) ) assume A1: a <> 0 ; ::_thesis: ( a divides b iff b / a is Element of NAT ) A2: now__::_thesis:_(_a_divides_b_implies_b_/_a_is_Element_of_NAT_) assume a divides b ; ::_thesis: b / a is Element of NAT then consider d being Nat such that A3: b = a * d by NAT_D:def_3; reconsider d = d as Element of NAT by ORDINAL1:def_12; b = a * d by A3; hence b / a is Element of NAT by A1, XCMPLX_1:89; ::_thesis: verum end; now__::_thesis:_(_b_/_a_is_Element_of_NAT_implies_a_divides_b_) assume b / a is Element of NAT ; ::_thesis: a divides b then reconsider d = b / a as Element of NAT ; b = a * d by A1, XCMPLX_1:87; hence a divides b by NAT_D:def_3; ::_thesis: verum end; hence ( a divides b iff b / a is Element of NAT ) by A2; ::_thesis: verum end; theorem Th17: :: WSIERP_1:17 for k, l being Integer st k <> 0 holds ( k divides l iff l / k is Integer ) proof let k, l be Integer; ::_thesis: ( k <> 0 implies ( k divides l iff l / k is Integer ) ) assume A1: k <> 0 ; ::_thesis: ( k divides l iff l / k is Integer ) A2: now__::_thesis:_(_l_/_k_is_Integer_implies_k_divides_l_) assume l / k is Integer ; ::_thesis: k divides l then reconsider m = l / k as Integer ; l = k * m by A1, XCMPLX_1:87; hence k divides l by INT_1:def_3; ::_thesis: verum end; now__::_thesis:_(_k_divides_l_implies_l_/_k_is_Integer_) assume k divides l ; ::_thesis: l / k is Integer then ex m being Integer st l = k * m by INT_1:def_3; hence l / k is Integer by A1, XCMPLX_1:89; ::_thesis: verum end; hence ( k divides l iff l / k is Integer ) by A2; ::_thesis: verum end; Lm6: for b, a being Nat for k being Integer st b <> 0 & a * k = b holds k is Element of NAT proof let b, a be Nat; ::_thesis: for k being Integer st b <> 0 & a * k = b holds k is Element of NAT let k be Integer; ::_thesis: ( b <> 0 & a * k = b implies k is Element of NAT ) assume that A1: b <> 0 and A2: a * k = b ; ::_thesis: k is Element of NAT A3: a divides b by A2, INT_1:def_3; A4: a <> 0 by A1, A2; then k = b / a by A2, XCMPLX_1:89; hence k is Element of NAT by A3, A4, Lm5; ::_thesis: verum end; Lm7: for a, b, c being Nat st a + b <= c holds ( a <= c & b <= c ) proof let a, b, c be Nat; ::_thesis: ( a + b <= c implies ( a <= c & b <= c ) ) A1: ( a <= a + b & b <= a + b ) by NAT_1:11; assume a + b <= c ; ::_thesis: ( a <= c & b <= c ) hence ( a <= c & b <= c ) by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: WSIERP_1:18 for a, b, c being Nat st a <= b - c holds ( a <= b & c <= b ) proof let a, b, c be Nat; ::_thesis: ( a <= b - c implies ( a <= b & c <= b ) ) assume a <= b - c ; ::_thesis: ( a <= b & c <= b ) then a + c <= b by XREAL_1:19; hence ( a <= b & c <= b ) by Lm7; ::_thesis: verum end; Lm8: for k, m being Integer holds ( k < m iff k <= m - 1 ) proof let k, m be Integer; ::_thesis: ( k < m iff k <= m - 1 ) A1: now__::_thesis:_(_k_<=_m_-_1_implies_k_<_m_) assume k <= m - 1 ; ::_thesis: k < m then A2: k + 1 <= m by XREAL_1:19; k < k + 1 by XREAL_1:29; hence k < m by A2, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_k_<_m_implies_k_<=_m_-_1_) assume k < m ; ::_thesis: k <= m - 1 then k + 1 <= m by INT_1:7; hence k <= m - 1 by XREAL_1:19; ::_thesis: verum end; hence ( k < m iff k <= m - 1 ) by A1; ::_thesis: verum end; Lm9: for k, m being Integer holds ( k < m + 1 iff k <= m ) proof let k, m be Integer; ::_thesis: ( k < m + 1 iff k <= m ) ( k < m + 1 iff k - 1 < m ) by XREAL_1:19; hence ( k < m + 1 iff k <= m ) by Lm8; ::_thesis: verum end; definition let D be non empty set ; let D1 be non empty Subset of D; let f1, f2 be FinSequence of D1; :: original: ^ redefine funcf1 ^ f2 -> FinSequence of D1; coherence f1 ^ f2 is FinSequence of D1 proof thus rng (f1 ^ f2) c= D1 by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; registration let fr be FinSequence of INT ; cluster Product fr -> integer ; coherence Product fr is integer proof defpred S1[ FinSequence of INT ] means Product fr is Integer; A1: now__::_thesis:_for_s_being_FinSequence_of_INT_ for_m_being_Element_of_INT_st_S1[s]_holds_ S1[s_^_<*m*>] let s be FinSequence of INT ; ::_thesis: for m being Element of INT st S1[s] holds S1[s ^ <*m*>] let m be Element of INT ; ::_thesis: ( S1[s] implies S1[s ^ <*m*>] ) reconsider k = m as Integer ; assume S1[s] ; ::_thesis: S1[s ^ <*m*>] then reconsider pis = Product s as Integer ; Product (s ^ <*m*>) = pis * k by RVSUM_1:96; hence S1[s ^ <*m*>] ; ::_thesis: verum end; A2: S1[ <*> INT] by RVSUM_1:94; for fr1 being FinSequence of INT holds S1[fr1] from FINSEQ_2:sch_2(A2, A1); hence Product fr is integer ; ::_thesis: verum end; end; definition let fp be FinSequence of NAT ; :: original: Sum redefine func Sum fp -> Element of NAT ; coherence Sum fp is Element of NAT proof defpred S1[ set ] means ex f being FinSequence of NAT st ( f = \$1 & Sum f is Element of NAT ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_a_being_Element_of_NAT_st_S1[fp]_holds_ S1[fp_^_<*a*>] let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds S1[fp ^ <*a*>] let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] ) assume S1[fp] ; ::_thesis: S1[fp ^ <*a*>] then reconsider sp = Sum fp as Element of NAT ; Sum (fp ^ <*a*>) = sp + a by RVSUM_1:74; hence S1[fp ^ <*a*>] ; ::_thesis: verum end; A2: S1[ <*> NAT] by RVSUM_1:72; for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A2, A1); then ex f being FinSequence of NAT st ( f = fp & Sum f is Element of NAT ) ; hence Sum fp is Element of NAT ; ::_thesis: verum end; end; definition let fp be FinSequence of NAT ; :: original: Product redefine func Product fp -> Element of NAT ; coherence Product fp is Element of NAT proof defpred S1[ set ] means ex f being FinSequence of NAT st ( f = \$1 & Product f is Element of NAT ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_a_being_Element_of_NAT_st_S1[fp]_holds_ S1[fp_^_<*a*>] let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds S1[fp ^ <*a*>] let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] ) assume S1[fp] ; ::_thesis: S1[fp ^ <*a*>] then reconsider sp = Product fp as Element of NAT ; Product (fp ^ <*a*>) = sp * a by RVSUM_1:96; hence S1[fp ^ <*a*>] ; ::_thesis: verum end; A2: S1[ <*> NAT] by RVSUM_1:94; for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A2, A1); then ex f being FinSequence of NAT st ( f = fp & Product f is Element of NAT ) ; hence Product fp is Element of NAT ; ::_thesis: verum end; end; Lm10: for a being Nat for fs being FinSequence st a in dom fs holds ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) proof let a be Nat; ::_thesis: for fs being FinSequence st a in dom fs holds ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) let fs be FinSequence; ::_thesis: ( a in dom fs implies ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) ) assume A1: a in dom fs ; ::_thesis: ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) then ( a >= 1 & a <= len fs ) by FINSEQ_3:25; then reconsider b = (len fs) - a, d = a - 1 as Element of NAT by INT_1:5; len fs = a + b ; then consider fs3, fs2 being FinSequence such that A2: len fs3 = a and A3: len fs2 = b and A4: fs = fs3 ^ fs2 by FINSEQ_2:22; a = d + 1 ; then consider fs1 being FinSequence, v being set such that A5: fs3 = fs1 ^ <*v*> by A2, FINSEQ_2:18; A6: (len fs1) + 1 = d + 1 by A2, A5, FINSEQ_2:16; a <> 0 by A1, FINSEQ_3:25; then a in dom fs3 by A2, CARD_1:27, FINSEQ_5:6; then fs3 . a = fs . a by A4, FINSEQ_1:def_7; then fs . a = v by A5, A6, FINSEQ_1:42; hence ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) by A3, A4, A5, A6; ::_thesis: verum end; definition let a be Nat; let fs be FinSequence; redefine func Del (fs,a) means :Def1: :: WSIERP_1:def 1 it = fs if not a in dom fs otherwise ( (len it) + 1 = len fs & ( for b being Nat holds ( ( b < a implies it . b = fs . b ) & ( b >= a implies it . b = fs . (b + 1) ) ) ) ); compatibility for b1 being set holds ( ( not a in dom fs implies ( b1 = Del (fs,a) iff b1 = fs ) ) & ( a in dom fs implies ( b1 = Del (fs,a) iff ( (len b1) + 1 = len fs & ( for b being Nat holds ( ( b < a implies b1 . b = fs . b ) & ( b >= a implies b1 . b = fs . (b + 1) ) ) ) ) ) ) ) proof let IT be FinSequence; ::_thesis: ( ( not a in dom fs implies ( IT = Del (fs,a) iff IT = fs ) ) & ( a in dom fs implies ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) ) ) thus ( not a in dom fs implies ( IT = Del (fs,a) iff IT = fs ) ) by FINSEQ_3:104; ::_thesis: ( a in dom fs implies ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) ) assume A1: a in dom fs ; ::_thesis: ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) hereby ::_thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) implies IT = Del (fs,a) ) assume A2: IT = Del (fs,a) ; ::_thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) ) ) ) then A3: ex m being Nat st ( len fs = m + 1 & len IT = m ) by A1, FINSEQ_3:104; hence (len IT) + 1 = len fs ; ::_thesis: for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) ) let b be Nat; ::_thesis: ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b1 = fs . (b1 + 1) ) ) thus ( b < a implies IT . b = fs . b ) by A2, FINSEQ_3:110; ::_thesis: ( b >= a implies IT . b1 = fs . (b1 + 1) ) assume A4: b >= a ; ::_thesis: IT . b1 = fs . (b1 + 1) percases ( b <= len IT or b > len IT ) ; suppose b <= len IT ; ::_thesis: IT . b1 = fs . (b1 + 1) hence IT . b = fs . (b + 1) by A1, A2, A3, A4, FINSEQ_3:111; ::_thesis: verum end; supposeA5: b > len IT ; ::_thesis: IT . b1 = fs . (b1 + 1) then not b in dom IT by FINSEQ_3:25; then A6: IT . b = {} by FUNCT_1:def_2; b + 1 > (len IT) + 1 by A5, XREAL_1:6; then not b + 1 in dom fs by A3, FINSEQ_3:25; hence IT . b = fs . (b + 1) by A6, FUNCT_1:def_2; ::_thesis: verum end; end; end; assume that A7: (len IT) + 1 = len fs and A8: for b being Nat holds ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ; ::_thesis: IT = Del (fs,a) A9: for k being Nat st 1 <= k & k <= len IT holds IT . k = (Del (fs,a)) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len IT implies IT . k = (Del (fs,a)) . k ) assume that 1 <= k and A10: k <= len IT ; ::_thesis: IT . k = (Del (fs,a)) . k reconsider k = k as Element of NAT by ORDINAL1:def_12; percases ( k < a or k >= a ) ; supposeA11: k < a ; ::_thesis: IT . k = (Del (fs,a)) . k then IT . k = fs . k by A8; hence IT . k = (Del (fs,a)) . k by A11, FINSEQ_3:110; ::_thesis: verum end; supposeA12: k >= a ; ::_thesis: IT . k = (Del (fs,a)) . k then IT . k = fs . (k + 1) by A8; hence IT . k = (Del (fs,a)) . k by A1, A7, A10, A12, FINSEQ_3:111; ::_thesis: verum end; end; end; ex m being Nat st ( len fs = m + 1 & len (Del (fs,a)) = m ) by A1, FINSEQ_3:104; hence IT = Del (fs,a) by A7, A9, FINSEQ_1:14; ::_thesis: verum end; correctness consistency for b1 being set holds verum; ; end; :: deftheorem Def1 defines Del WSIERP_1:def_1_:_ for a being Nat for fs being FinSequence for b3 being set holds ( ( not a in dom fs implies ( b3 = Del (fs,a) iff b3 = fs ) ) & ( a in dom fs implies ( b3 = Del (fs,a) iff ( (len b3) + 1 = len fs & ( for b being Nat holds ( ( b < a implies b3 . b = fs . b ) & ( b >= a implies b3 . b = fs . (b + 1) ) ) ) ) ) ) ); Lm11: for a being Nat for fs, fs1, fs2 being FinSequence for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 proof let a be Nat; ::_thesis: for fs, fs1, fs2 being FinSequence for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 let fs, fs1, fs2 be FinSequence; ::_thesis: for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 let v be set ; ::_thesis: ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 implies Del (fs,a) = fs1 ^ fs2 ) assume that A1: a in dom fs and A2: fs = (fs1 ^ <*v*>) ^ fs2 and A3: len fs1 = a - 1 ; ::_thesis: Del (fs,a) = fs1 ^ fs2 A4: (len (Del (fs,a))) + 1 = len fs by A1, Def1; len fs = (len (fs1 ^ <*v*>)) + (len fs2) by A2, FINSEQ_1:22 .= ((len fs1) + 1) + (len fs2) by FINSEQ_2:16 .= a + (len fs2) by A3 ; then len (Del (fs,a)) = (len fs2) + (len fs1) by A3, A4; then A5: len (fs1 ^ fs2) = len (Del (fs,a)) by FINSEQ_1:22; A6: len <*v*> = 1 by FINSEQ_1:39; A7: fs = fs1 ^ (<*v*> ^ fs2) by A2, FINSEQ_1:32; then len fs = (a - 1) + (len (<*v*> ^ fs2)) by A3, FINSEQ_1:22; then A8: len (<*v*> ^ fs2) = (len fs) - (a - 1) ; now__::_thesis:_for_e_being_Nat_st_1_<=_e_&_e_<=_len_(Del_(fs,a))_holds_ (fs1_^_fs2)_._e_=_(Del_(fs,a))_._e let e be Nat; ::_thesis: ( 1 <= e & e <= len (Del (fs,a)) implies (fs1 ^ fs2) . e = (Del (fs,a)) . e ) assume that A9: 1 <= e and A10: e <= len (Del (fs,a)) ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e now__::_thesis:_(fs1_^_fs2)_._e_=_(Del_(fs,a))_._e percases ( e < a or e >= a ) ; supposeA11: e < a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e then e <= a - 1 by Lm8; then A12: e in dom fs1 by A3, A9, FINSEQ_3:25; hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def_7 .= fs . e by A7, A12, FINSEQ_1:def_7 .= (Del (fs,a)) . e by A1, A11, Def1 ; ::_thesis: verum end; supposeA13: e >= a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e then A14: e > a - 1 by Lm8; then A15: e + 1 > a by XREAL_1:19; then (e + 1) - a > 0 by XREAL_1:50; then A16: ((e + 1) - a) + 1 > 0 + 1 by XREAL_1:6; A17: e + 1 > a - 1 by A15, XREAL_1:146, XXREAL_0:2; then (e + 1) - (a - 1) > 0 by XREAL_1:50; then reconsider f = (e + 1) - (a - 1) as Element of NAT by INT_1:3; A18: e + 1 <= len fs by A4, A10, XREAL_1:6; then A19: (e + 1) - (a - 1) <= len (<*v*> ^ fs2) by A8, XREAL_1:9; thus (fs1 ^ fs2) . e = fs2 . (e - (len fs1)) by A3, A5, A10, A14, FINSEQ_1:24 .= fs2 . (f - 1) by A3 .= (<*v*> ^ fs2) . f by A6, A16, A19, FINSEQ_1:24 .= (fs1 ^ (<*v*> ^ fs2)) . (e + 1) by A3, A7, A17, A18, FINSEQ_1:24 .= (Del (fs,a)) . e by A1, A7, A13, Def1 ; ::_thesis: verum end; end; end; hence (fs1 ^ fs2) . e = (Del (fs,a)) . e ; ::_thesis: verum end; hence Del (fs,a) = fs1 ^ fs2 by A5, FINSEQ_1:14; ::_thesis: verum end; Lm12: for a being Nat for fs being FinSequence holds dom (Del (fs,a)) c= dom fs proof let a be Nat; ::_thesis: for fs being FinSequence holds dom (Del (fs,a)) c= dom fs let fs be FinSequence; ::_thesis: dom (Del (fs,a)) c= dom fs now__::_thesis:_(_a_in_dom_fs_implies_dom_(Del_(fs,a))_c=_dom_fs_) assume A1: a in dom fs ; ::_thesis: dom (Del (fs,a)) c= dom fs dom fs = Seg (len fs) by FINSEQ_1:def_3 .= Seg ((len (Del (fs,a))) + 1) by A1, Def1 .= (Seg (len (Del (fs,a)))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:9 .= (dom (Del (fs,a))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:def_3 ; hence dom (Del (fs,a)) c= dom fs by XBOOLE_1:7; ::_thesis: verum end; hence dom (Del (fs,a)) c= dom fs by Def1; ::_thesis: verum end; definition let D be non empty set ; let a be Nat; let fs be FinSequence of D; :: original: Del redefine func Del (fs,a) -> FinSequence of D; coherence Del (fs,a) is FinSequence of D proof ( rng fs c= D & rng (Del (fs,a)) c= rng fs ) by FINSEQ_1:def_4, FINSEQ_3:106; hence rng (Del (fs,a)) c= D by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; definition let D be non empty set ; let D1 be non empty Subset of D; let a be Nat; let fs be FinSequence of D1; :: original: Del redefine func Del (fs,a) -> FinSequence of D1; coherence Del (fs,a) is FinSequence of D1 proof thus rng (Del (fs,a)) c= D1 by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; Lm13: for a being Nat for fs1, fs2 being FinSequence holds ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) proof let a be Nat; ::_thesis: for fs1, fs2 being FinSequence holds ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) let fs1, fs2 be FinSequence; ::_thesis: ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) set f = fs1 ^ fs2; A1: len (fs1 ^ fs2) = (len fs1) + (len fs2) by FINSEQ_1:22; A2: now__::_thesis:_(_a_>=_1_implies_Del_((fs1_^_fs2),((len_fs1)_+_a))_=_fs1_^_(Del_(fs2,a))_) set f2 = fs1 ^ (Del (fs2,a)); set f1 = Del ((fs1 ^ fs2),((len fs1) + a)); assume A3: a >= 1 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) now__::_thesis:_Del_((fs1_^_fs2),((len_fs1)_+_a))_=_fs1_^_(Del_(fs2,a)) percases ( a > len fs2 or a <= len fs2 ) ; supposeA4: a > len fs2 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) then A5: not a in dom fs2 by FINSEQ_3:25; (len fs1) + a > len (fs1 ^ fs2) by A1, A4, XREAL_1:6; then not (len fs1) + a in dom (fs1 ^ fs2) by FINSEQ_3:25; hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ fs2 by Def1 .= fs1 ^ (Del (fs2,a)) by A5, Def1 ; ::_thesis: verum end; supposeA6: a <= len fs2 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) then A7: a in dom fs2 by A3, FINSEQ_3:25; a - 1 >= 0 by A3, XREAL_1:48; then A8: (len fs1) + (a - 1) >= len fs1 by Lm1; A9: (len fs1) + a >= 1 by A3, NAT_1:12; (len fs1) + a <= len (fs1 ^ fs2) by A1, A6, XREAL_1:6; then A10: (len fs1) + a in dom (fs1 ^ fs2) by A9, FINSEQ_3:25; then consider g1, g2 being FinSequence such that A11: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 and A12: len g1 = ((len fs1) + a) - 1 and len g2 = (len (fs1 ^ fs2)) - ((len fs1) + a) by Lm10; A13: Del ((fs1 ^ fs2),((len fs1) + a)) = g1 ^ g2 by A10, A11, A12, Lm11; fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by A11, FINSEQ_1:32; then consider t being FinSequence such that A14: fs1 ^ t = g1 by A12, A8, FINSEQ_1:47; fs1 ^ ((t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2) = (fs1 ^ (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>)) ^ g2 by FINSEQ_1:32 .= fs1 ^ fs2 by A11, A14, FINSEQ_1:32 ; then A15: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:33; (len fs1) + (a - 1) = (len fs1) + (len t) by A12, A14, FINSEQ_1:22; then Del (fs2,a) = t ^ g2 by A7, A15, Lm11; hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) by A13, A14, FINSEQ_1:32; ::_thesis: verum end; end; end; hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ; ::_thesis: verum end; now__::_thesis:_(_a_<=_len_fs1_implies_Del_((fs1_^_fs2),a)_=_(Del_(fs1,a))_^_fs2_) set f3 = <*((fs1 ^ fs2) . a)*>; set f2 = (Del (fs1,a)) ^ fs2; set f1 = Del ((fs1 ^ fs2),a); assume A16: a <= len fs1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 len fs1 <= len (fs1 ^ fs2) by A1, NAT_1:11; then A17: a <= len (fs1 ^ fs2) by A16, XXREAL_0:2; now__::_thesis:_Del_((fs1_^_fs2),a)_=_(Del_(fs1,a))_^_fs2 percases ( a < 1 or a >= 1 ) ; supposeA18: a < 1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 then A19: not a in dom fs1 by FINSEQ_3:25; not a in dom (fs1 ^ fs2) by A18, FINSEQ_3:25; hence Del ((fs1 ^ fs2),a) = fs1 ^ fs2 by Def1 .= (Del (fs1,a)) ^ fs2 by A19, Def1 ; ::_thesis: verum end; supposeA20: a >= 1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 then A21: a in dom (fs1 ^ fs2) by A17, FINSEQ_3:25; then consider g1, g2 being FinSequence such that A22: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 and A23: len g1 = a - 1 and len g2 = (len (fs1 ^ fs2)) - a by Lm10; len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by A23, FINSEQ_2:16 .= a ; then consider t being FinSequence such that A24: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by A16, A22, FINSEQ_1:47; (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by A22, A24, FINSEQ_1:32; then A25: g2 = t ^ fs2 by FINSEQ_1:33; a in dom fs1 by A16, A20, FINSEQ_3:25; then A26: Del (fs1,a) = g1 ^ t by A23, A24, Lm11; thus Del ((fs1 ^ fs2),a) = g1 ^ g2 by A21, A22, A23, Lm11 .= (Del (fs1,a)) ^ fs2 by A26, A25, FINSEQ_1:32 ; ::_thesis: verum end; end; end; hence Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ; ::_thesis: verum end; hence ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) by A2; ::_thesis: verum end; Lm14: for fs being FinSequence for v being set holds ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) proof let fs be FinSequence; ::_thesis: for v being set holds ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) let v be set ; ::_thesis: ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) A1: len <*v*> = 1 by FINSEQ_1:39; then 1 in dom <*v*> by FINSEQ_3:25; then (len (Del (<*v*>,1))) + 1 = 1 by A1, Def1; then A2: Del (<*v*>,1) = {} ; ( 1 <= len <*v*> & {} ^ fs = fs ) by FINSEQ_1:34, FINSEQ_1:39; hence Del ((<*v*> ^ fs),1) = fs by A2, Lm13; ::_thesis: Del ((fs ^ <*v*>),((len fs) + 1)) = fs fs ^ {} = fs by FINSEQ_1:34; hence Del ((fs ^ <*v*>),((len fs) + 1)) = fs by A2, Lm13; ::_thesis: verum end; theorem :: WSIERP_1:19 for v1, v2, v3 being set holds ( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) proof let v1, v2, v3 be set ; ::_thesis: ( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) thus Del (<*v1*>,1) = Del ((<*v1*> ^ {}),1) by FINSEQ_1:34 .= {} by Lm14 ; ::_thesis: ( Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) thus Del (<*v1,v2*>,1) = <*v2*> by Lm14; ::_thesis: ( Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) len <*v1*> = 1 by FINSEQ_1:39; hence A1: Del (<*v1,v2*>,2) = Del ((<*v1*> ^ <*v2*>),((len <*v1*>) + 1)) .= <*v1*> by Lm14 ; ::_thesis: ( Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) thus Del (<*v1,v2,v3*>,1) = Del ((<*v1*> ^ <*v2,v3*>),1) by FINSEQ_1:43 .= <*v2,v3*> by Lm14 ; ::_thesis: ( Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> ) A2: len <*v1,v2*> = 2 by FINSEQ_1:44; hence Del (<*v1,v2,v3*>,2) = <*v1,v3*> by A1, Lm13; ::_thesis: Del (<*v1,v2,v3*>,3) = <*v1,v2*> (len <*v1,v2*>) + 1 = 3 by A2; hence Del (<*v1,v2,v3*>,3) = <*v1,v2*> by Lm14; ::_thesis: verum end; Lm15: for fs being FinSequence st 1 <= len fs holds ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) proof let fs be FinSequence; ::_thesis: ( 1 <= len fs implies ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) ) set fs1 = <*(fs . 1)*> ^ (Del (fs,1)); set fs2 = (Del (fs,(len fs))) ^ <*(fs . (len fs))*>; A1: len <*(fs . 1)*> = 1 by FINSEQ_1:39; assume A2: 1 <= len fs ; ::_thesis: ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) then A3: len fs in dom fs by FINSEQ_3:25; A4: 1 in dom fs by A2, FINSEQ_3:25; then A5: len fs = (len <*(fs . 1)*>) + (len (Del (fs,1))) by A1, Def1 .= len (<*(fs . 1)*> ^ (Del (fs,1))) by FINSEQ_1:22 ; for b being Nat st 1 <= b & b <= len fs holds fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b proof let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b ) assume that A6: 1 <= b and A7: b <= len fs ; ::_thesis: fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b now__::_thesis:_(<*(fs_._1)*>_^_(Del_(fs,1)))_._b_=_fs_._b percases ( b = 1 or b > 1 ) by A6, XXREAL_0:1; supposeA8: b = 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b 1 in dom <*(fs . 1)*> by A1, FINSEQ_3:25; hence (<*(fs . 1)*> ^ (Del (fs,1))) . b = <*(fs . 1)*> . 1 by A8, FINSEQ_1:def_7 .= fs . b by A8, FINSEQ_1:40 ; ::_thesis: verum end; supposeA9: b > 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b then A10: b - 1 > 0 by XREAL_1:50; then reconsider e = b - 1 as Element of NAT by INT_1:3; A11: e >= 1 by A10, NAT_1:14; thus (<*(fs . 1)*> ^ (Del (fs,1))) . b = (Del (fs,1)) . e by A1, A5, A7, A9, FINSEQ_1:24 .= fs . (e + 1) by A4, A11, Def1 .= fs . b ; ::_thesis: verum end; end; end; hence fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b ; ::_thesis: verum end; hence <*(fs . 1)*> ^ (Del (fs,1)) = fs by A5, FINSEQ_1:14; ::_thesis: fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> len <*(fs . (len fs))*> = 1 by FINSEQ_1:39; then A12: len fs = (len <*(fs . (len fs))*>) + (len (Del (fs,(len fs)))) by A3, Def1 .= len ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) by FINSEQ_1:22 ; A13: (len (Del (fs,(len fs)))) + 1 = len fs by A3, Def1; then A14: len (Del (fs,(len fs))) = (len fs) - 1 ; for b being Nat st 1 <= b & b <= len fs holds fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b proof let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b ) assume that A15: 1 <= b and A16: b <= len fs ; ::_thesis: fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b now__::_thesis:_((Del_(fs,(len_fs)))_^_<*(fs_._(len_fs))*>)_._b_=_fs_._b percases ( b = len fs or b < len fs ) by A16, XXREAL_0:1; supposeA17: b = len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b reconsider e = b - (b - 1) as Element of NAT ; thus ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = <*(fs . (len fs))*> . e by A13, A12, A17, FINSEQ_1:24, XREAL_1:146 .= fs . b by A17, FINSEQ_1:40 ; ::_thesis: verum end; supposeA18: b < len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b then b + 1 <= len fs by NAT_1:13; then b <= len (Del (fs,(len fs))) by A14, XREAL_1:19; then b in dom (Del (fs,(len fs))) by A15, FINSEQ_3:25; hence ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = (Del (fs,(len fs))) . b by FINSEQ_1:def_7 .= fs . b by A3, A18, Def1 ; ::_thesis: verum end; end; end; hence fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b ; ::_thesis: verum end; hence fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> by A12, FINSEQ_1:14; ::_thesis: verum end; Lm16: for a being Nat for ft being FinSequence of REAL st a in dom ft holds (Product (Del (ft,a))) * (ft . a) = Product ft proof let a be Nat; ::_thesis: for ft being FinSequence of REAL st a in dom ft holds (Product (Del (ft,a))) * (ft . a) = Product ft let ft be FinSequence of REAL ; ::_thesis: ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) defpred S1[ Nat] means ( \$1 in dom ft implies (ft . \$1) * (Product (Del (ft,\$1))) = Product ft ); A1: for a being Nat st S1[a] holds S1[a + 1] proof let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] ) assume S1[a] ; ::_thesis: S1[a + 1] now__::_thesis:_S1[a_+_1] percases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ; supposeA2: a = 0 ; ::_thesis: S1[a + 1] thus S1[a + 1] ::_thesis: verum proof assume a + 1 in dom ft ; ::_thesis: (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft then a + 1 <= len ft by FINSEQ_3:25; then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm15; then Product ft = (Product <*(ft . 1)*>) * (Product (Del (ft,1))) by RVSUM_1:97 .= (ft . 1) * (Product (Del (ft,1))) by RVSUM_1:95 ; hence (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft by A2; ::_thesis: verum end; end; suppose ( a > 0 & a < len ft ) ; ::_thesis: S1[a + 1] then ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13; then A3: a + 1 in dom ft by FINSEQ_3:25; then consider fs1, fs2 being FinSequence such that A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and A5: len fs1 = (a + 1) - 1 and len fs2 = (len ft) - (a + 1) by Lm10; A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm11; reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36; reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36; Product ft = (Product (fs1 ^ <*(ft . (a + 1))*>)) * (Product fs2) by A4, RVSUM_1:97 .= ((Product fs1) * (Product <*(ft . (a + 1))*>)) * (Product fs2) by RVSUM_1:97 .= ((ft . (a + 1)) * (Product fs1)) * (Product fs2) by RVSUM_1:95 .= (ft . (a + 1)) * ((Product fs1) * (Product fs2)) ; hence S1[a + 1] by A6, RVSUM_1:97; ::_thesis: verum end; suppose a >= len ft ; ::_thesis: S1[a + 1] then len ft < a + 1 by NAT_1:13; hence S1[a + 1] by FINSEQ_3:25; ::_thesis: verum end; end; end; hence S1[a + 1] ; ::_thesis: verum end; A7: S1[ 0 ] by FINSEQ_3:25; for a being Nat holds S1[a] from NAT_1:sch_2(A7, A1); hence ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; ::_thesis: verum end; theorem :: WSIERP_1:20 for a being Nat for ft being FinSequence of REAL st a in dom ft holds (Sum (Del (ft,a))) + (ft . a) = Sum ft proof let a be Nat; ::_thesis: for ft being FinSequence of REAL st a in dom ft holds (Sum (Del (ft,a))) + (ft . a) = Sum ft let ft be FinSequence of REAL ; ::_thesis: ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft ) defpred S1[ Nat] means ( \$1 in dom ft implies (ft . \$1) + (Sum (Del (ft,\$1))) = Sum ft ); A1: for a being Nat st S1[a] holds S1[a + 1] proof let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] ) assume S1[a] ; ::_thesis: S1[a + 1] now__::_thesis:_S1[a_+_1] percases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ; supposeA2: a = 0 ; ::_thesis: S1[a + 1] thus S1[a + 1] ::_thesis: verum proof assume a + 1 in dom ft ; ::_thesis: (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft then a + 1 <= len ft by FINSEQ_3:25; then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm15; then Sum ft = (Sum <*(ft . 1)*>) + (Sum (Del (ft,1))) by RVSUM_1:75 .= (ft . 1) + (Sum (Del (ft,1))) by FINSOP_1:11 ; hence (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft by A2; ::_thesis: verum end; end; suppose ( a > 0 & a < len ft ) ; ::_thesis: S1[a + 1] then ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13; then A3: a + 1 in dom ft by FINSEQ_3:25; then consider fs1, fs2 being FinSequence such that A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and A5: len fs1 = (a + 1) - 1 and len fs2 = (len ft) - (a + 1) by Lm10; A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm11; reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36; reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36; Sum ft = (Sum (fs1 ^ <*(ft . (a + 1))*>)) + (Sum fs2) by A4, RVSUM_1:75 .= ((Sum fs1) + (Sum <*(ft . (a + 1))*>)) + (Sum fs2) by RVSUM_1:75 .= ((ft . (a + 1)) + (Sum fs1)) + (Sum fs2) by FINSOP_1:11 .= (ft . (a + 1)) + ((Sum fs1) + (Sum fs2)) ; hence S1[a + 1] by A6, RVSUM_1:75; ::_thesis: verum end; suppose a >= len ft ; ::_thesis: S1[a + 1] then a + 1 > len ft by NAT_1:13; hence S1[a + 1] by FINSEQ_3:25; ::_thesis: verum end; end; end; hence S1[a + 1] ; ::_thesis: verum end; A7: S1[ 0 ] by FINSEQ_3:25; for a being Nat holds S1[a] from NAT_1:sch_2(A7, A1); hence ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft ) ; ::_thesis: verum end; theorem :: WSIERP_1:21 for a being Nat for fp being FinSequence of NAT st a in dom fp holds (Product fp) / (fp . a) is Element of NAT proof let a be Nat; ::_thesis: for fp being FinSequence of NAT st a in dom fp holds (Product fp) / (fp . a) is Element of NAT let fp be FinSequence of NAT ; ::_thesis: ( a in dom fp implies (Product fp) / (fp . a) is Element of NAT ) assume a in dom fp ; ::_thesis: (Product fp) / (fp . a) is Element of NAT then consider fs1, fs2 being FinSequence such that A1: fp = (fs1 ^ <*(fp . a)*>) ^ fs2 and len fs1 = a - 1 and len fs2 = (len fp) - a by Lm10; percases ( fp . a <> 0 or fp . a = 0 ) ; supposeA2: fp . a <> 0 ; ::_thesis: (Product fp) / (fp . a) is Element of NAT reconsider fs2 = fs2 as FinSequence of NAT by A1, FINSEQ_1:36; fs1 ^ <*(fp . a)*> is FinSequence of NAT by A1, FINSEQ_1:36; then reconsider fs1 = fs1 as FinSequence of NAT by FINSEQ_1:36; Product fp = (Product (fs1 ^ <*(fp . a)*>)) * (Product fs2) by A1, RVSUM_1:97 .= ((fp . a) * (Product fs1)) * (Product fs2) by RVSUM_1:96 .= (fp . a) * ((Product fs1) * (Product fs2)) ; hence (Product fp) / (fp . a) is Element of NAT by A2, XCMPLX_1:89; ::_thesis: verum end; supposeA3: fp . a = 0 ; ::_thesis: (Product fp) / (fp . a) is Element of NAT (Product fp) / (fp . a) = (Product fp) * ((fp . a) ") by XCMPLX_0:def_9 .= (Product fp) * 0 by A3 .= 0 ; hence (Product fp) / (fp . a) is Element of NAT ; ::_thesis: verum end; end; end; theorem Th22: :: WSIERP_1:22 for q being Rational holds numerator q, denominator q are_relative_prime proof let q be Rational; ::_thesis: numerator q, denominator q are_relative_prime set k = numerator q; set h = denominator q; reconsider a = (numerator q) gcd (denominator q) as Element of NAT by INT_2:20; a divides numerator q by INT_2:21; then A1: ex l being Integer st numerator q = a * l by INT_1:def_3; (numerator q) gcd (denominator q) divides denominator q by INT_2:21; then consider b being Nat such that A2: denominator q = a * b by NAT_D:def_3; denominator q <> 0 by RAT_1:def_3; then a <> 0 by INT_2:5; then A3: a >= 0 + 1 by NAT_1:13; reconsider b = b as Element of NAT by ORDINAL1:def_12; A4: denominator q = a * b by A2; assume not numerator q, denominator q are_relative_prime ; ::_thesis: contradiction then a <> 1 by INT_2:def_3; then a > 1 by A3, XXREAL_0:1; hence contradiction by A1, A4, RAT_1:29; ::_thesis: verum end; theorem :: WSIERP_1:23 for a being Nat for k being Integer for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds ( k = numerator q & a = denominator q ) proof let a be Nat; ::_thesis: for k being Integer for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds ( k = numerator q & a = denominator q ) let k be Integer; ::_thesis: for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds ( k = numerator q & a = denominator q ) let q be Rational; ::_thesis: ( q = k / a & a <> 0 & k,a are_relative_prime implies ( k = numerator q & a = denominator q ) ) assume that A1: ( q = k / a & a <> 0 ) and A2: k,a are_relative_prime ; ::_thesis: ( k = numerator q & a = denominator q ) a in NAT by ORDINAL1:def_12; then consider b being Element of NAT such that A3: ( k = (numerator q) * b & a = (denominator q) * b ) by A1, RAT_1:27; numerator q, denominator q are_relative_prime by Th22; then k gcd a = abs b by A3, INT_2:24; then 1 = abs b by A2, INT_2:def_3 .= b by ABSVALUE:def_1 ; hence ( k = numerator q & a = denominator q ) by A3; ::_thesis: verum end; theorem Th24: :: WSIERP_1:24 for a, b being Nat st ex q being Rational st a = q |^ b holds ex k being Integer st a = k |^ b proof let a, b be Nat; ::_thesis: ( ex q being Rational st a = q |^ b implies ex k being Integer st a = k |^ b ) given q being Rational such that A1: a = q |^ b ; ::_thesis: ex k being Integer st a = k |^ b now__::_thesis:_ex_k_being_Integer_st_a_=_k_|^_b A2: now__::_thesis:_(_b_<>_0_implies_ex_k_being_Integer_st_a_=_k_|^_b_) set d = denominator q; set k = numerator q; assume b <> 0 ; ::_thesis: ex k being Integer st a = k |^ b then consider e being Nat such that A3: e + 1 = b by NAT_1:6; denominator q <> 0 by RAT_1:def_3; then A4: (denominator q) |^ b <> 0 by CARD_4:3; (numerator q) |^ b, denominator q are_relative_prime by Th10, Th22; then A5: ((numerator q) |^ b) gcd (denominator q) = 1 by INT_2:def_3; A6: q = (numerator q) / (denominator q) by RAT_1:15; then a = ((numerator q) |^ b) / ((denominator q) |^ b) by A1, PREPOWER:8; then a * ((denominator q) |^ b) = (numerator q) |^ b by A4, XCMPLX_1:87; then (numerator q) |^ b = a * (((denominator q) |^ e) * (denominator q)) by A3, NEWTON:6 .= (a * ((denominator q) |^ e)) * (denominator q) ; then denominator q divides (numerator q) |^ b by INT_1:def_3; then ( denominator q = 1 or denominator q = - 1 ) by A5, INT_2:13, INT_2:22; hence ex k being Integer st a = k |^ b by A1, A6, INT_2:7; ::_thesis: verum end; now__::_thesis:_(_b_=_0_implies_ex_k_being_Integer_st_a_=_k_|^_b_) assume A7: b = 0 ; ::_thesis: ex k being Integer st a = k |^ b then a = 1 by A1, NEWTON:4; then a = 1 |^ 0 by NEWTON:4; hence ex k being Integer st a = k |^ b by A7; ::_thesis: verum end; hence ex k being Integer st a = k |^ b by A2; ::_thesis: verum end; hence ex k being Integer st a = k |^ b ; ::_thesis: verum end; theorem Th25: :: WSIERP_1:25 for a, d being Nat st ex q being Rational st a = q |^ d holds ex b being Nat st a = b |^ d proof let a, d be Nat; ::_thesis: ( ex q being Rational st a = q |^ d implies ex b being Nat st a = b |^ d ) assume ex q being Rational st a = q |^ d ; ::_thesis: ex b being Nat st a = b |^ d then consider k being Integer such that A1: a = k |^ d by Th24; A2: now__::_thesis:_(_a_=_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_) assume A3: a = 0 ; ::_thesis: ex b being Nat st a = b |^ d then d <> 0 by A1, NEWTON:4; then a = 0 |^ d by A3, NAT_1:14, NEWTON:11; hence ex b being Nat st a = b |^ d ; ::_thesis: verum end; A4: now__::_thesis:_(_d_<>_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_) assume d <> 0 ; ::_thesis: ex b being Nat st a = b |^ d now__::_thesis:_(_k_is_not_Element_of_NAT_implies_ex_b_being_Nat_st_a_=_b_|^_d_) consider e being Nat such that A5: ( d = 2 * e or d = (2 * e) + 1 ) by Lm4; consider c being Element of NAT such that A6: ( k = c or k = - c ) by INT_1:2; assume A7: k is not Element of NAT ; ::_thesis: ex b being Nat st a = b |^ d A8: now__::_thesis:_(_d_=_(2_*_e)_+_1_implies_ex_b_being_Nat_st_a_=_b_|^_d_) assume d = (2 * e) + 1 ; ::_thesis: ex b being Nat st a = b |^ d then - (c |^ d) = a by A1, A7, A6, Th2; hence ex b being Nat st a = b |^ d by A2; ::_thesis: verum end; now__::_thesis:_(_d_=_2_*_e_implies_ex_b_being_Nat_st_a_=_b_|^_d_) assume d = 2 * e ; ::_thesis: ex b being Nat st a = b |^ d then a = c |^ d by A1, A6, Th2; hence ex b being Nat st a = b |^ d ; ::_thesis: verum end; hence ex b being Nat st a = b |^ d by A5, A8; ::_thesis: verum end; hence ex b being Nat st a = b |^ d by A1; ::_thesis: verum end; now__::_thesis:_(_d_=_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_) assume A9: d = 0 ; ::_thesis: ex b being Nat st a = b |^ d then a = 1 by A1, NEWTON:4; then a = 1 |^ 0 by NEWTON:4; hence ex b being Nat st a = b |^ d by A9; ::_thesis: verum end; hence ex b being Nat st a = b |^ d by A4; ::_thesis: verum end; theorem :: WSIERP_1:26 for e, a, b being Nat st e > 0 & a |^ e divides b |^ e holds a divides b proof let e, a, b be Nat; ::_thesis: ( e > 0 & a |^ e divides b |^ e implies a divides b ) assume that A1: e > 0 and A2: a |^ e divides b |^ e ; ::_thesis: a divides b consider f being Nat such that A3: (a |^ e) * f = b |^ e by A2, NAT_D:def_3; A4: a in REAL by XREAL_0:def_1; A5: now__::_thesis:_(_a_<>_0_&_b_<>_0_implies_a_divides_b_) assume that A6: a <> 0 and b <> 0 ; ::_thesis: a divides b a |^ e <> 0 by A4, A6, CARD_4:3; then f = (b |^ e) / (a |^ e) by A3, XCMPLX_1:89 .= (b / a) |^ e by PREPOWER:8 ; then consider d being Nat such that A7: f = d |^ e by Th25; b |^ e = (a * d) |^ e by A3, A7, NEWTON:7; then b = a * d by A1, Th3; hence a divides b by NAT_D:def_3; ::_thesis: verum end; A8: b in REAL by XREAL_0:def_1; A9: now__::_thesis:_(_a_=_0_implies_a_divides_b_) assume A10: a = 0 ; ::_thesis: a divides b then 0 divides b |^ e by A1, A2, NAT_1:14, NEWTON:11; then ex f being Nat st 0 * f = b |^ e by NAT_D:def_3; hence a divides b by A8, A10, CARD_4:3; ::_thesis: verum end; now__::_thesis:_(_b_=_0_implies_a_divides_b_) assume b = 0 ; ::_thesis: a divides b then a * 0 = b ; hence a divides b by NAT_D:def_3; ::_thesis: verum end; hence a divides b by A9, A5; ::_thesis: verum end; theorem Th27: :: WSIERP_1:27 for a, b being Nat ex m, n being Integer st a gcd b = (a * m) + (b * n) proof let a, b be Nat; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n) A1: for c being Nat ex m, n being Integer st 0 gcd c = (0 * m) + (c * n) proof let c be Nat; ::_thesis: ex m, n being Integer st 0 gcd c = (0 * m) + (c * n) take 0 ; ::_thesis: ex n being Integer st 0 gcd c = (0 * 0) + (c * n) take 1 ; ::_thesis: 0 gcd c = (0 * 0) + (c * 1) thus 0 gcd c = (0 * 0) + (c * 1) by NEWTON:52; ::_thesis: verum end; now__::_thesis:_ex_m,_n_being_Integer_st_a_gcd_b_=_(a_*_m)_+_(b_*_n) percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; suppose a = 0 ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n) hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A1; ::_thesis: verum end; supposeA2: b = 0 ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n) then ex m, n being Integer st a gcd b = (0 * m) + (a * n) by A1; hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A2; ::_thesis: verum end; supposeA3: ( a <> 0 & b <> 0 ) ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n) defpred S1[ set ] means ex m, n being Integer st ( \$1 = (a * m) + (b * n) & \$1 <> 0 ); a + b = (a * 1) + (b * 1) ; then A4: ex c being Nat st S1[c] by A3; consider d being Nat such that A5: ( S1[d] & ( for c being Nat st S1[c] holds d <= c ) ) from NAT_1:sch_5(A4); consider e, f being Nat such that A6: a = (d * e) + f and A7: f < d by A5, NAT_1:17; consider m, n being Integer such that A8: d = (a * m) + (b * n) by A5; A9: now__::_thesis:_not_f_<>_0 assume A10: f <> 0 ; ::_thesis: contradiction f = a - (d * e) by A6 .= (a * (1 - (m * e))) + (b * (- (n * e))) by A8 ; hence contradiction by A5, A7, A10; ::_thesis: verum end; consider e, f being Nat such that A11: b = (d * e) + f and A12: f < d by A5, NAT_1:17; now__::_thesis:_not_f_<>_0 assume A13: f <> 0 ; ::_thesis: contradiction f = b - (d * e) by A11 .= (b * (1 - (n * e))) + (a * (- (m * e))) by A8 ; hence contradiction by A5, A12, A13; ::_thesis: verum end; then A14: d divides b by A11, NAT_D:def_3; d divides a by A6, A9, NAT_D:def_3; then A15: d divides a gcd b by A14, NAT_D:def_5; ( a gcd b divides a & a gcd b divides b ) by NAT_D:def_5; then a gcd b divides d by A8, Th5; hence ex m, n being Integer st a gcd b = (a * m) + (b * n) by A8, A15, NAT_D:5; ::_thesis: verum end; end; end; hence ex m, n being Integer st a gcd b = (a * m) + (b * n) ; ::_thesis: verum end; theorem Th28: :: WSIERP_1:28 for m, n being Integer ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) proof let m, n be Integer; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) m gcd n = (abs m) gcd (abs n) by INT_2:34; then consider m1, n1 being Integer such that A1: ((abs m) * m1) + ((abs n) * n1) = m gcd n by Th27; now__::_thesis:_ex_m1,_n1_being_Integer_st_m_gcd_n_=_(m_*_m1)_+_(n_*_n1) percases ( ( m >= 0 & n >= 0 ) or ( m >= 0 & n < 0 ) or ( m < 0 & n >= 0 ) or ( m < 0 & n < 0 ) ) ; suppose ( m >= 0 & n >= 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) then ( abs m = m & abs n = n ) by ABSVALUE:def_1; hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) by A1; ::_thesis: verum end; supposeA2: ( m >= 0 & n < 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) then abs n = - n by ABSVALUE:def_1; then m gcd n = (m * m1) + (n * (- n1)) by A1, A2, ABSVALUE:def_1; hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum end; supposeA3: ( m < 0 & n >= 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) then abs m = - m by ABSVALUE:def_1; then m gcd n = (m * (- m1)) + (n * n1) by A1, A3, ABSVALUE:def_1; hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum end; suppose ( m < 0 & n < 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) then ( abs m = - m & abs n = - n ) by ABSVALUE:def_1; then m gcd n = (m * (- m1)) + (n * (- n1)) by A1; hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum end; end; end; hence ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum end; theorem Th29: :: WSIERP_1:29 for m, n, k being Integer st m divides n * k & m gcd n = 1 holds m divides k proof let m, n, k be Integer; ::_thesis: ( m divides n * k & m gcd n = 1 implies m divides k ) assume that A1: m divides n * k and A2: m gcd n = 1 ; ::_thesis: m divides k consider m1, n1 being Integer such that A3: (m * m1) + (n * n1) = 1 by A2, Th28; k = ((m * m1) + (n * n1)) * k by A3 .= (m * (m1 * k)) + ((n * k) * n1) ; hence m divides k by A1, Th5; ::_thesis: verum end; theorem :: WSIERP_1:30 for a, b, c being Nat st a gcd b = 1 & a divides b * c holds a divides c by Th29; theorem Th31: :: WSIERP_1:31 for a, b being Nat st a <> 0 & b <> 0 holds ex c, d being Nat st a gcd b = (a * c) - (b * d) proof let a, b be Nat; ::_thesis: ( a <> 0 & b <> 0 implies ex c, d being Nat st a gcd b = (a * c) - (b * d) ) assume that A1: a <> 0 and A2: b <> 0 ; ::_thesis: ex c, d being Nat st a gcd b = (a * c) - (b * d) consider m, n being Integer such that A3: a gcd b = (a * m) + (b * n) by Th27; set k = [/(max ((- (m / b)),(n / a)))\] + 1; [/(max ((- (m / b)),(n / a)))\] + 1 > n / a by INT_1:32, XXREAL_0:31; then ([/(max ((- (m / b)),(n / a)))\] + 1) * a > n by A1, XREAL_1:77; then A4: (([/(max ((- (m / b)),(n / a)))\] + 1) * a) - n > 0 by XREAL_1:50; [/(max ((- (m / b)),(n / a)))\] + 1 > - (m / b) by INT_1:32, XXREAL_0:31; then [/(max ((- (m / b)),(n / a)))\] + 1 > (- m) / b by XCMPLX_1:187; then ([/(max ((- (m / b)),(n / a)))\] + 1) * b > - m by A2, XREAL_1:77; then (([/(max ((- (m / b)),(n / a)))\] + 1) * b) - (- m) > 0 by XREAL_1:50; then reconsider e = (([/(max ((- (m / b)),(n / a)))\] + 1) * b) + m, d = (([/(max ((- (m / b)),(n / a)))\] + 1) * a) - n as Element of NAT by A4, INT_1:3; (a * e) - (b * d) = ((a * m) + 0) + (b * n) ; hence ex c, d being Nat st a gcd b = (a * c) - (b * d) by A3; ::_thesis: verum end; theorem :: WSIERP_1:32 for f, g, a, b being Nat st f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g holds ex e being Nat st ( a = e |^ g & b = e |^ f ) proof let f, g, a, b be Nat; ::_thesis: ( f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g implies ex e being Nat st ( a = e |^ g & b = e |^ f ) ) assume that A1: f > 0 and A2: g > 0 and A3: f gcd g = 1 and A4: a |^ f = b |^ g ; ::_thesis: ex e being Nat st ( a = e |^ g & b = e |^ f ) A5: b in REAL by XREAL_0:def_1; A6: a in REAL by XREAL_0:def_1; now__::_thesis:_ex_e_being_Nat_st_ (_a_=_e_|^_g_&_b_=_e_|^_f_) percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; supposeA7: a = 0 ; ::_thesis: ex e being Nat st ( a = e |^ g & b = e |^ f ) then a |^ f = 0 by A1, NAT_1:14, NEWTON:11; then A8: b = 0 |^ f by A4, A5, A7, CARD_4:3; a = 0 |^ g by A2, A7, CARD_4:3; hence ex e being Nat st ( a = e |^ g & b = e |^ f ) by A8; ::_thesis: verum end; supposeA9: b = 0 ; ::_thesis: ex e being Nat st ( a = e |^ g & b = e |^ f ) then b |^ g = 0 by A2, NAT_1:14, NEWTON:11; then A10: a = 0 |^ g by A4, A6, A9, CARD_4:3; b = 0 |^ f by A1, A9, CARD_4:3; hence ex e being Nat st ( a = e |^ g & b = e |^ f ) by A10; ::_thesis: verum end; supposeA11: ( a <> 0 & b <> 0 ) ; ::_thesis: ex e being Nat st ( a = e |^ g & b = e |^ f ) consider c, d being Nat such that A12: (f * c) - (g * d) = 1 by A1, A2, A3, Th31; reconsider q = (b |^ c) / (a |^ d) as Rational ; a = a #Z 1 by PREPOWER:35 .= (a |^ (f * c)) / (a |^ (d * g)) by A11, A12, PREPOWER:43 .= ((a |^ f) |^ c) / (a |^ (d * g)) by NEWTON:9 .= ((b |^ g) |^ c) / ((a |^ d) |^ g) by A4, NEWTON:9 .= (b |^ (g * c)) / ((a |^ d) |^ g) by NEWTON:9 .= ((b |^ c) |^ g) / ((a |^ d) |^ g) by NEWTON:9 .= q |^ g by PREPOWER:8 ; then consider h being Nat such that A13: a = h |^ g by Th25; b |^ g = h |^ (f * g) by A4, A13, NEWTON:9 .= (h |^ f) |^ g by NEWTON:9 ; then b = h |^ f by A2, Th3; hence ex e being Nat st ( a = e |^ g & b = e |^ f ) by A13; ::_thesis: verum end; end; end; hence ex e being Nat st ( a = e |^ g & b = e |^ f ) ; ::_thesis: verum end; theorem Th33: :: WSIERP_1:33 for m, n, k being Integer holds ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k ) proof let m, n, k be Integer; ::_thesis: ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k ) A1: now__::_thesis:_(_m_gcd_n_divides_k_implies_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k_) assume A2: m gcd n divides k ; ::_thesis: ex x, y being Integer st (m * x) + (n * y) = k now__::_thesis:_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k consider m1, n1 being Integer such that A3: m gcd n = (m * m1) + (n * n1) by Th28; consider l being Integer such that A4: (m gcd n) * l = k by A2, INT_1:def_3; k = (m * (m1 * l)) + (n * (n1 * l)) by A4, A3; hence ex x, y being Integer st (m * x) + (n * y) = k ; ::_thesis: verum end; hence ex x, y being Integer st (m * x) + (n * y) = k ; ::_thesis: verum end; now__::_thesis:_(_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k_implies_m_gcd_n_divides_k_) given x, y being Integer such that A5: (m * x) + (n * y) = k ; ::_thesis: m gcd n divides k ( m gcd n divides m & m gcd n divides n ) by INT_2:21; hence m gcd n divides k by A5, Th5; ::_thesis: verum end; hence ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k ) by A1; ::_thesis: verum end; theorem :: WSIERP_1:34 for m, n, m1, n1, k being Integer st m <> 0 & n <> 0 & (m * m1) + (n * n1) = k holds for x, y being Integer st (m * x) + (n * y) = k holds ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) proof let m, n, m1, n1, k be Integer; ::_thesis: ( m <> 0 & n <> 0 & (m * m1) + (n * n1) = k implies for x, y being Integer st (m * x) + (n * y) = k holds ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) ) assume that A1: m <> 0 and A2: n <> 0 and A3: (m * m1) + (n * n1) = k ; ::_thesis: for x, y being Integer st (m * x) + (n * y) = k holds ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) consider m2, n2 being Integer such that A4: m = (m gcd n) * m2 and A5: n = (m gcd n) * n2 and A6: m2,n2 are_relative_prime by A1, INT_2:23; A7: m gcd n <> 0 by A1, INT_2:5; then A8: m2 = m / (m gcd n) by A4, XCMPLX_1:89; A9: n2 = n / (m gcd n) by A7, A5, XCMPLX_1:89; A10: n2 gcd m2 = 1 by A6, INT_2:def_3; let x, y be Integer; ::_thesis: ( (m * x) + (n * y) = k implies ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) ) assume (m * x) + (n * y) = k ; ::_thesis: ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) then m * (x - m1) = n * (n1 - y) by A3; then A11: m2 * (x - m1) = (n * (n1 - y)) / (m gcd n) by A8, XCMPLX_1:74 .= n2 * (n1 - y) by A9, XCMPLX_1:74 ; then n2 divides m2 * (x - m1) by INT_1:def_3; then n2 divides x - m1 by A10, Th29; then consider t being Integer such that A12: n2 * t = x - m1 by INT_1:def_3; A13: n2 <> 0 by A2, A5; then A14: t = (x - m1) / n2 by A12, XCMPLX_1:89; A15: m2 <> 0 by A1, A4; then (x - m1) / n2 = (n1 - y) / m2 by A13, A11, XCMPLX_1:94; then t * m2 = n1 - y by A15, A14, XCMPLX_1:87; then A16: y = n1 - (t * m2) ; x = m1 + (t * n2) by A12; hence ex t being Integer st ( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) by A8, A9, A16; ::_thesis: verum end; theorem :: WSIERP_1:35 for a, b, c, d being Nat st a gcd b = 1 & a * b = c |^ d holds ex e, f being Nat st ( a = e |^ d & b = f |^ d ) proof let a, b, c, d be Nat; ::_thesis: ( a gcd b = 1 & a * b = c |^ d implies ex e, f being Nat st ( a = e |^ d & b = f |^ d ) ) assume that A1: a gcd b = 1 and A2: a * b = c |^ d ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) set e = a gcd c; a gcd c divides c by NAT_D:def_5; then A3: (a gcd c) |^ d divides c |^ d by Th14; a gcd c divides a by NAT_D:def_5; then (a gcd c) gcd b = 1 by A1, Th15, NEWTON:57; then ((a gcd c) |^ d) gcd b = 1 by Th12; then (a gcd c) |^ d divides a by A2, A3, Th29; then consider g being Nat such that A4: ((a gcd c) |^ d) * g = a by NAT_D:def_3; reconsider g = g as Element of NAT by ORDINAL1:def_12; A5: now__::_thesis:_(_d_<>_0_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) A6: c in REAL by XREAL_0:def_1; assume A7: d <> 0 ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then consider d1 being Nat such that A8: d = 1 + d1 by NAT_1:10, NAT_1:14; reconsider d1 = d1 as Element of NAT by ORDINAL1:def_12; A9: d >= 1 by A7, NAT_1:14; A10: now__::_thesis:_(_a_gcd_c_<>_0_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) assume A11: a gcd c <> 0 ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then A12: ( a <> 0 or c <> 0 ) by INT_2:5; then A13: a <> 0 by A2, A6, CARD_4:3; A14: now__::_thesis:_(_c_<>_0_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) reconsider e1 = a gcd c as Real by XREAL_0:def_1; assume A15: c <> 0 ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then consider a1, c1 being Integer such that A16: a = (a gcd c) * a1 and A17: (a gcd c) * c1 = c and A18: a1,c1 are_relative_prime by INT_2:23; reconsider a1 = a1, c1 = c1 as Element of NAT by A13, A15, A16, A17, Lm6; a1 = (((a gcd c) |^ (d1 + 1)) * g) / (a gcd c) by A4, A8, A11, A16, XCMPLX_1:89 .= (((a gcd c) * ((a gcd c) |^ d1)) * g) / (a gcd c) by NEWTON:6 .= ((a gcd c) * (((a gcd c) |^ d1) * g)) / (a gcd c) .= ((a gcd c) |^ d1) * g by A11, XCMPLX_1:89 ; then A19: g divides a1 by NAT_D:def_3; a1 gcd c1 = 1 by A18, INT_2:def_3; then g gcd c1 = 1 by A19, Th15, NEWTON:57; then A20: g gcd (c1 |^ d) = 1 by Th12; A21: e1 |^ d <> 0 by A11, CARD_4:3; c1 = c / (a gcd c) by A11, A17, XCMPLX_1:89; then A22: c1 |^ d = (((a gcd c) |^ d) * (g * b)) / ((a gcd c) |^ d) by A2, A4, PREPOWER:8 .= g * b by A21, XCMPLX_1:89 ; then g divides c1 |^ d by NAT_D:def_3; then g = 1 by A20, NEWTON:49; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A4, A22; ::_thesis: verum end; now__::_thesis:_(_0_=_c_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) assume 0 = c ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then A23: b = 0 by A2, A9, A12, NEWTON:11, XCMPLX_1:6; then a = 1 by A1, NEWTON:52; then A24: a = 1 |^ d by NEWTON:10; b = 0 |^ d by A7, A23, NAT_1:14, NEWTON:11; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A24; ::_thesis: verum end; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A14; ::_thesis: verum end; now__::_thesis:_(_a_gcd_c_=_0_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) assume a gcd c = 0 ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then A25: a = 0 by INT_2:5; then b = 1 by A1, NEWTON:52; then A26: b = 1 |^ d by NEWTON:10; a = 0 |^ d by A7, A25, NAT_1:14, NEWTON:11; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A26; ::_thesis: verum end; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A10; ::_thesis: verum end; now__::_thesis:_(_d_=_0_implies_ex_e,_f_being_Nat_st_ (_a_=_e_|^_d_&_b_=_f_|^_d_)_) assume A27: d = 0 ; ::_thesis: ex e, f being Nat st ( a = e |^ d & b = f |^ d ) then A28: a * b = 1 by A2, NEWTON:4; then b divides 1 by NAT_D:def_3; then b = 1 by Th15; then A29: b = 1 |^ 0 by NEWTON:4; a divides 1 by A28, NAT_D:def_3; then a = 1 by Th15; then a = 1 |^ 0 by NEWTON:4; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A27, A29; ::_thesis: verum end; hence ex e, f being Nat st ( a = e |^ d & b = f |^ d ) by A5; ::_thesis: verum end; theorem Th36: :: WSIERP_1:36 for fp being FinSequence of NAT for d being Nat st ( for a being Nat st a in dom fp holds (fp . a) gcd d = 1 ) holds (Product fp) gcd d = 1 proof let fp be FinSequence of NAT ; ::_thesis: for d being Nat st ( for a being Nat st a in dom fp holds (fp . a) gcd d = 1 ) holds (Product fp) gcd d = 1 let d be Nat; ::_thesis: ( ( for a being Nat st a in dom fp holds (fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 ) defpred S1[ set ] means ex f being FinSequence of NAT st ( f = \$1 & ( ( for a being Nat st a in dom f holds (f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_a_being_Element_of_NAT_st_S1[fp]_holds_ S1[fp_^_<*a*>] let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds S1[fp ^ <*a*>] let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] ) assume A2: S1[fp] ; ::_thesis: S1[fp ^ <*a*>] thus S1[fp ^ <*a*>] ::_thesis: verum proof set fp1 = fp ^ <*a*>; take fp ^ <*a*> ; ::_thesis: ( fp ^ <*a*> = fp ^ <*a*> & ( ( for a being Nat st a in dom (fp ^ <*a*>) holds ((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 ) ) thus fp ^ <*a*> = fp ^ <*a*> ; ::_thesis: ( ( for a being Nat st a in dom (fp ^ <*a*>) holds ((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 ) assume A3: for b being Nat st b in dom (fp ^ <*a*>) holds ((fp ^ <*a*>) . b) gcd d = 1 ; ::_thesis: (Product (fp ^ <*a*>)) gcd d = 1 A4: dom fp c= dom (fp ^ <*a*>) by FINSEQ_1:26; A5: for b being Nat st b in dom fp holds (fp . b) gcd d = 1 proof let b be Nat; ::_thesis: ( b in dom fp implies (fp . b) gcd d = 1 ) assume A6: b in dom fp ; ::_thesis: (fp . b) gcd d = 1 then ((fp ^ <*a*>) . b) gcd d = 1 by A3, A4; hence (fp . b) gcd d = 1 by A6, FINSEQ_1:def_7; ::_thesis: verum end; len (fp ^ <*a*>) in dom (fp ^ <*a*>) by FINSEQ_5:6; then ( len (fp ^ <*a*>) = (len fp) + 1 & ((fp ^ <*a*>) . (len (fp ^ <*a*>))) gcd d = 1 ) by A3, FINSEQ_2:16; then A7: a gcd d = 1 by FINSEQ_1:42; Product (fp ^ <*a*>) = (Product fp) * a by RVSUM_1:96; hence (Product (fp ^ <*a*>)) gcd d = 1 by A2, A5, A7, Th6; ::_thesis: verum end; end; A8: S1[ <*> NAT] proof take <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds ((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) ) thus ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds ((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) ) by NEWTON:51, RVSUM_1:94; ::_thesis: verum end; for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A8, A1); then ex f being FinSequence of NAT st ( f = fp & ( ( for a being Nat st a in dom f holds (f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) ) ; hence ( ( for a being Nat st a in dom fp holds (fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 ) ; ::_thesis: verum end; theorem :: WSIERP_1:37 for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) holds for fr being FinSequence of INT st len fr = len fp holds ex fr1 being FinSequence of INT st ( len fr1 = len fp & ( for b being Nat st b in dom fp holds ((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) proof let fp be FinSequence of NAT ; ::_thesis: ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds ex fr1 being FinSequence of INT st ( len fr1 = len fp & ( for b being Nat st b in dom fp holds ((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) ) defpred S1[ FinSequence of NAT ] means for fr being FinSequence of INT st len fr = len \$1 holds ex fr1 being FinSequence of INT st ( len fr1 = len \$1 & ( for b being Nat st b in dom \$1 holds ((\$1 . b) * (fr1 . b)) + (fr . b) = ((\$1 . 1) * (fr1 . 1)) + (fr . 1) ) ); defpred S2[ FinSequence of NAT ] means for b, c being Nat st b in dom \$1 & c in dom \$1 & b <> c holds (\$1 . b) gcd (\$1 . c) = 1; defpred S3[ set ] means ex f being FinSequence of NAT st ( f = \$1 & ( len f >= 2 & S2[f] implies S1[f] ) ); A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_ for_d_being_Element_of_NAT_st_S3[fp]_holds_ S3[fp_^_<*d*>] let fp be FinSequence of NAT ; ::_thesis: for d being Element of NAT st S3[fp] holds S3[fp ^ <*d*>] let d be Element of NAT ; ::_thesis: ( S3[fp] implies S3[fp ^ <*d*>] ) assume A2: S3[fp] ; ::_thesis: S3[fp ^ <*d*>] set k = len fp; set fp1 = fp ^ <*d*>; now__::_thesis:_(_len_(fp_^_<*d*>)_>=_2_&_S2[fp_^_<*d*>]_implies_S1[fp_^_<*d*>]_) assume that A3: len (fp ^ <*d*>) >= 2 and A4: S2[fp ^ <*d*>] ; ::_thesis: S1[fp ^ <*d*>] A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16; now__::_thesis:_S1[fp_^_<*d*>] percases ( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 ) by A3, XXREAL_0:1; supposeA6: len (fp ^ <*d*>) = 2 ; ::_thesis: S1[fp ^ <*d*>] now__::_thesis:_for_fr_being_FinSequence_of_INT_st_len_fr_=_len_(fp_^_<*d*>)_holds_ ex_fr1_being_FinSequence_of_INT_st_ (_len_fr1_=_len_(fp_^_<*d*>)_&_(_for_b_being_Nat_st_b_in_dom_(fp_^_<*d*>)_holds_ (((fp_^_<*d*>)_._b)_*_(fr1_._b))_+_(fr_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr1_._1))_+_(fr_._1)_)_) let fr be FinSequence of INT ; ::_thesis: ( len fr = len (fp ^ <*d*>) implies ex fr1 being FinSequence of INT st ( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) ) ) assume len fr = len (fp ^ <*d*>) ; ::_thesis: ex fr1 being FinSequence of INT st ( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) ) ( 1 in dom (fp ^ <*d*>) & 2 in dom (fp ^ <*d*>) ) by A6, FINSEQ_3:25; then ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) = 1 by A4; then ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) divides (fr . 1) - (fr . 2) by INT_2:12; then consider m, n being Integer such that A7: (((fp ^ <*d*>) . 1) * m) + (((fp ^ <*d*>) . 2) * n) = (fr . 1) - (fr . 2) by Th33; reconsider x = - m, y = n as Element of INT by INT_1:def_2; take fr1 = <*x,y*>; ::_thesis: ( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) ) thus len fr1 = len (fp ^ <*d*>) by A6, FINSEQ_1:44; ::_thesis: for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) let b be Nat; ::_thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) assume b in dom (fp ^ <*d*>) ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) then A8: b in Seg (len (fp ^ <*d*>)) by FINSEQ_1:def_3; now__::_thesis:_(((fp_^_<*d*>)_._b)_*_(fr1_._b))_+_(fr_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr1_._1))_+_(fr_._1) percases ( b = 1 or b = 2 ) by A6, A8, FINSEQ_1:2, TARSKI:def_2; suppose b = 1 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; ::_thesis: verum end; supposeA9: b = 2 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) A10: ( fr1 . 1 = - m & fr1 . 2 = n ) by FINSEQ_1:44; (((fp ^ <*d*>) . 2) * n) - (((fp ^ <*d*>) . 1) * (- m)) = (fr . 1) - (fr . 2) by A7; hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) by A9, A10, XCMPLX_1:34; ::_thesis: verum end; end; end; hence (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; ::_thesis: verum end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; supposeA11: len (fp ^ <*d*>) > 2 ; ::_thesis: S1[fp ^ <*d*>] A12: S2[fp] proof A13: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26; let b, c be Nat; ::_thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 ) assume that A14: ( b in dom fp & c in dom fp ) and A15: b <> c ; ::_thesis: (fp . b) gcd (fp . c) = 1 ( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A14, FINSEQ_1:def_7; hence (fp . b) gcd (fp . c) = 1 by A4, A14, A15, A13; ::_thesis: verum end; A16: (len fp) + 1 > 1 + 1 by A11, FINSEQ_2:16; then A17: len fp >= 1 + 1 by NAT_1:13; now__::_thesis:_for_fr2_being_FinSequence_of_INT_st_len_fr2_=_len_(fp_^_<*d*>)_holds_ ex_fr3_being_FinSequence_of_INT_st_ (_len_fr3_=_len_(fp_^_<*d*>)_&_(_for_b_being_Nat_st_b_in_dom_(fp_^_<*d*>)_holds_ (((fp_^_<*d*>)_._b)_*_(fr3_._b))_+_(fr2_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr3_._1))_+_(fr2_._1)_)_) let fr2 be FinSequence of INT ; ::_thesis: ( len fr2 = len (fp ^ <*d*>) implies ex fr3 being FinSequence of INT st ( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) ) ) assume A18: len fr2 = len (fp ^ <*d*>) ; ::_thesis: ex fr3 being FinSequence of INT st ( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) ) then consider fr being FinSequence of INT , m being Element of INT such that A19: fr2 = fr ^ <*m*> by FINSEQ_2:19; A20: (len fp) + 1 = (len fr) + 1 by A5, A18, A19, FINSEQ_2:16; then consider fr1 being FinSequence of INT such that len fr1 = len fp and A21: for b being Nat st b in dom fp holds ((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) by A2, A16, A12, NAT_1:13; for a being Nat st a in dom fp holds (fp . a) gcd d = 1 proof let a be Nat; ::_thesis: ( a in dom fp implies (fp . a) gcd d = 1 ) A22: (len fp) + 1 in dom (fp ^ <*d*>) by A5, FINSEQ_5:6; A23: ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . ((len fp) + 1) = d ) by FINSEQ_1:26, FINSEQ_1:42; assume A24: a in dom fp ; ::_thesis: (fp . a) gcd d = 1 (len fp) + 1 > len fp by NAT_1:13; then A25: (len fp) + 1 <> a by A24, FINSEQ_3:25; (fp ^ <*d*>) . a = fp . a by A24, FINSEQ_1:def_7; hence (fp . a) gcd d = 1 by A4, A24, A23, A25, A22; ::_thesis: verum end; then (Product fp) gcd d = 1 by Th36; then (Product fp) gcd d divides ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by INT_2:12; then consider m1, n1 being Integer such that A26: ((Product fp) * m1) + (d * n1) = ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by Th33; reconsider x = - n1 as Element of INT by INT_1:def_2; deffunc H1( Nat) -> Element of REAL = ((Product (Del (fp,\$1))) * m1) + (fr1 . \$1); consider s2 being FinSequence such that A27: ( len s2 = len fp & ( for a being Nat st a in dom s2 holds s2 . a = H1(a) ) ) from FINSEQ_1:sch_2(); A28: for a being Nat st a in dom s2 holds s2 . a in INT proof let a be Nat; ::_thesis: ( a in dom s2 implies s2 . a in INT ) assume A29: a in dom s2 ; ::_thesis: s2 . a in INT reconsider a = a as Element of NAT by ORDINAL1:def_12; s2 . a = ((Product (Del (fp,a))) * m1) + (fr1 . a) by A27, A29; hence s2 . a in INT by INT_1:def_2; ::_thesis: verum end; A30: dom s2 = Seg (len fp) by A27, FINSEQ_1:def_3; reconsider s2 = s2 as FinSequence of INT by A28, FINSEQ_2:12; take fr3 = s2 ^ <*x*>; ::_thesis: ( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) ) thus len fr3 = len (fp ^ <*d*>) by A5, A27, FINSEQ_2:16; ::_thesis: for b being Nat st b in dom (fp ^ <*d*>) holds (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) let b be Nat; ::_thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) assume A31: b in dom (fp ^ <*d*>) ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) thus (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ::_thesis: verum proof A32: for c being Nat st c in Seg (len fp) holds ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c)) proof let c be Nat; ::_thesis: ( c in Seg (len fp) implies ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c)) ) assume A33: c in Seg (len fp) ; ::_thesis: ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c)) then c in dom s2 by A27, FINSEQ_1:def_3; then A34: fr3 . c = s2 . c by FINSEQ_1:def_7 .= ((Product (Del (fp,c))) * m1) + (fr1 . c) by A27, A30, A33 ; A35: c in dom fp by A33, FINSEQ_1:def_3; then fp . c = (fp ^ <*d*>) . c by FINSEQ_1:def_7; hence ((fp ^ <*d*>) . c) * (fr3 . c) = (((fp . c) * (Product (Del (fp,c)))) * m1) + ((fp . c) * (fr1 . c)) by A34 .= ((Product fp) * m1) + ((fp . c) * (fr1 . c)) by A35, Lm16 ; ::_thesis: verum end; A36: b in NAT by ORDINAL1:def_12; A37: 1 <= b by A31, FINSEQ_3:25; A38: b <= (len fp) + 1 by A5, A31, FINSEQ_3:25; now__::_thesis:_(((fp_^_<*d*>)_._b)_*_(fr3_._b))_+_(fr2_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr3_._1))_+_(fr2_._1) percases ( b <= len fp or b = (len fp) + 1 ) by A38, NAT_1:8; supposeA39: b <= len fp ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) then 1 <= len fp by A37, XXREAL_0:2; then A40: 1 in Seg (len fp) ; then 1 in dom fr by A20, FINSEQ_1:def_3; then A41: fr2 . 1 = fr . 1 by A19, FINSEQ_1:def_7; A42: b in Seg (len fp) by A37, A36, A39; then A43: b in dom fp by FINSEQ_1:def_3; b in dom fr by A20, A42, FINSEQ_1:def_3; then A44: fr2 . b = fr . b by A19, FINSEQ_1:def_7; thus (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((Product fp) * m1) + ((fp . b) * (fr1 . b))) + (fr2 . b) by A32, A42 .= ((Product fp) * m1) + (((fp . b) * (fr1 . b)) + (fr . b)) by A44 .= ((Product fp) * m1) + (((fp . 1) * (fr1 . 1)) + (fr . 1)) by A21, A43 .= (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr . 1) .= (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A32, A40, A41 ; ::_thesis: verum end; supposeA45: b = (len fp) + 1 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) then A46: (fp ^ <*d*>) . b = d by FINSEQ_1:42; A47: (fr2 . b) - (((fp . 1) * (fr1 . 1)) + (fr2 . 1)) = (d * n1) + ((Product fp) * m1) by A26, A45; 1 <= len fp by A17, XXREAL_0:2; then 1 in Seg (len fp) ; then (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) = (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr2 . 1) by A32 .= (fr2 . b) + (d * (- n1)) by A47 ; hence (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A27, A45, A46, FINSEQ_1:42; ::_thesis: verum end; end; end; hence (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ; ::_thesis: verum end; end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; end; end; hence S1[fp ^ <*d*>] ; ::_thesis: verum end; hence S3[fp ^ <*d*>] ; ::_thesis: verum end; A48: S3[ <*> NAT] proof take <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) ; ::_thesis: verum end; for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch_2(A48, A1); then ex f being FinSequence of NAT st ( f = fp & ( len f >= 2 & S2[f] implies S1[f] ) ) ; hence ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds (fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds ex fr1 being FinSequence of INT st ( len fr1 = len fp & ( for b being Nat st b in dom fp holds ((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) ) ; ::_thesis: verum end; Lm17: for k, m being Integer holds ( k divides m iff k divides abs m ) proof let k, m be Integer; ::_thesis: ( k divides m iff k divides abs m ) percases ( m >= 0 or m < 0 ) ; suppose m >= 0 ; ::_thesis: ( k divides m iff k divides abs m ) hence ( k divides m iff k divides abs m ) by ABSVALUE:def_1; ::_thesis: verum end; suppose m < 0 ; ::_thesis: ( k divides m iff k divides abs m ) then abs m = - m by ABSVALUE:def_1; hence ( k divides m iff k divides abs m ) by INT_2:10; ::_thesis: verum end; end; end; Lm18: for m, n being Integer holds (m * n) mod n = 0 proof let m, n be Integer; ::_thesis: (m * n) mod n = 0 percases ( n <> 0 or n = 0 ) ; supposeA1: n <> 0 ; ::_thesis: (m * n) mod n = 0 hence (m * n) mod n = (m * n) - (((m * n) div n) * n) by INT_1:def_10 .= (m * n) - ([\((m * n) / n)/] * n) by INT_1:def_9 .= (m * n) - ([\m/] * n) by A1, XCMPLX_1:89 .= (m * n) - (m * n) by INT_1:25 .= 0 ; ::_thesis: verum end; suppose n = 0 ; ::_thesis: (m * n) mod n = 0 hence (m * n) mod n = 0 by INT_1:def_10; ::_thesis: verum end; end; end; Lm19: for k, n, m being Integer st k mod n = m mod n holds (k - m) mod n = 0 proof let k, n, m be Integer; ::_thesis: ( k mod n = m mod n implies (k - m) mod n = 0 ) assume A1: k mod n = m mod n ; ::_thesis: (k - m) mod n = 0 percases ( n <> 0 or n = 0 ) ; supposeA2: n <> 0 ; ::_thesis: (k - m) mod n = 0 then k - ((k div n) * n) = m mod n by A1, INT_1:def_10 .= m - ((m div n) * n) by A2, INT_1:def_10 ; then k - m = n * ((k div n) - (m div n)) ; hence (k - m) mod n = 0 by Lm18; ::_thesis: verum end; suppose n = 0 ; ::_thesis: (k - m) mod n = 0 hence (k - m) mod n = 0 by INT_1:def_10; ::_thesis: verum end; end; end; Lm20: for n, m being Integer st n <> 0 & m mod n = 0 holds n divides m proof let n, m be Integer; ::_thesis: ( n <> 0 & m mod n = 0 implies n divides m ) assume ( n <> 0 & m mod n = 0 ) ; ::_thesis: n divides m then m = ((m div n) * n) + 0 by NEWTON:66 .= (m div n) * n ; hence n divides m by INT_1:def_3; ::_thesis: verum end; Lm21: for x being Integer holds ( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) ) proof let x be Integer; ::_thesis: ( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) ) hereby ::_thesis: ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) assume A1: 1 < x ; ::_thesis: ( 1 < sqrt x & sqrt x < x ) hence 1 < sqrt x by SQUARE_1:18, SQUARE_1:27; ::_thesis: sqrt x < x then sqrt x < (sqrt x) ^2 by SQUARE_1:14; hence sqrt x < x by A1, SQUARE_1:def_2; ::_thesis: verum end; hereby ::_thesis: verum assume that A2: 0 < x and A3: x < 1 ; ::_thesis: ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) thus A4: 0 < sqrt x by A2, SQUARE_1:17, SQUARE_1:27; ::_thesis: ( sqrt x < 1 & x < sqrt x ) thus sqrt x < 1 by A2, A3, SQUARE_1:18, SQUARE_1:27; ::_thesis: x < sqrt x then (sqrt x) ^2 < sqrt x by A4, SQUARE_1:13; hence x < sqrt x by A2, SQUARE_1:def_2; ::_thesis: verum end; end; theorem :: WSIERP_1:38 for a being Nat for k being Integer st a <> 0 & a gcd k = 1 holds ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) proof let a be Nat; ::_thesis: for k being Integer st a <> 0 & a gcd k = 1 holds ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) let k be Integer; ::_thesis: ( a <> 0 & a gcd k = 1 implies ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) ) assume that A1: a <> 0 and A2: a gcd k = 1 ; ::_thesis: ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) A3: a >= 1 by A1, NAT_1:14; percases ( a = 1 or a > 1 ) by A3, XXREAL_0:1; supposeA4: a = 1 ; ::_thesis: ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) take b = 1; ::_thesis: ex e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) take e = 1; ::_thesis: ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) thus ( b <> 0 & e <> 0 ) ; ::_thesis: ( b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) thus ( b <= sqrt a & e <= sqrt a ) by A4, SQUARE_1:18; ::_thesis: ( a divides (k * b) + e or a divides (k * b) - e ) thus ( a divides (k * b) + e or a divides (k * b) - e ) by A4, INT_2:12; ::_thesis: verum end; supposeA5: a > 1 ; ::_thesis: ex b, e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) A6: sqrt a > 0 by A1, SQUARE_1:25; set d = [\(sqrt a)/]; A7: [\(sqrt a)/] <= sqrt a by INT_1:def_6; sqrt a < a by A5, Lm21; then A8: [\(sqrt a)/] < a by A7, XXREAL_0:2; set d1 = [\(sqrt a)/] + 1; A9: [\(sqrt a)/] > (sqrt a) - 1 by INT_1:def_6; sqrt a > 1 by A5, SQUARE_1:18, SQUARE_1:27; then A10: (sqrt a) - 1 > 0 by XREAL_1:50; then reconsider d = [\(sqrt a)/] as Element of NAT by A9, INT_1:3; A11: d + 1 >= 1 by Lm1; then reconsider d1 = [\(sqrt a)/] + 1 as Element of NAT ; set e1 = d1 ^2 ; d1 ^2 = d1 * d1 ; then reconsider e1 = d1 ^2 as Element of NAT ; A12: (e1 - 1) / d1 = d1 - (1 / d1) by A11, XCMPLX_1:127; deffunc H1( Nat) -> Element of REAL = 1 + (((k * ((\$1 - 1) div d1)) + ((\$1 - 1) mod d1)) mod a); consider fs being FinSequence such that A13: ( len fs = e1 & ( for b being Nat st b in dom fs holds fs . b = H1(b) ) ) from FINSEQ_1:sch_2(); A14: rng fs c= Seg a proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng fs or v in Seg a ) assume v in rng fs ; ::_thesis: v in Seg a then consider b being Nat such that A15: ( b in dom fs & fs . b = v ) by FINSEQ_2:10; A16: v = 1 + (((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a) by A13, A15; then reconsider v1 = v as Integer ; A17: 0 <= ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a by NEWTON:64; then A18: 1 <= v1 by A16, Lm1; reconsider v1 = v1 as Element of NAT by A16, A17, INT_1:3; ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a < a by A1, NEWTON:65; then v1 <= a by A16, Lm9; hence v in Seg a by A18; ::_thesis: verum end; sqrt a < d1 by A9, XREAL_1:19; then (sqrt a) ^2 < e1 by A6, SQUARE_1:16; then A19: a < e1 by SQUARE_1:def_2; then A20: Seg a c= Seg e1 by FINSEQ_1:5; A21: Seg e1 = dom fs by A13, FINSEQ_1:def_3; then rng fs <> dom fs by A19, A14, FINSEQ_1:5; then not fs is one-to-one by A21, A14, A20, FINSEQ_4:59, XBOOLE_1:1; then consider v1, v2 being set such that A22: v1 in dom fs and A23: v2 in dom fs and A24: fs . v1 = fs . v2 and A25: v1 <> v2 by FUNCT_1:def_4; reconsider v1 = v1, v2 = v2 as Element of NAT by A22, A23; set x1 = (v1 - 1) div d1; set x2 = (v2 - 1) div d1; set x = ((v1 - 1) div d1) - ((v2 - 1) div d1); set y1 = (v1 - 1) mod d1; set y2 = (v2 - 1) mod d1; set y = ((v1 - 1) mod d1) - ((v2 - 1) mod d1); A26: (v1 - 1) mod d1 >= 0 by NEWTON:64; ( fs . v1 = 1 + (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod a) & fs . v2 = 1 + (((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod a) ) by A13, A22, A23; then A27: (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod a = 0 by A24, Lm19, XCMPLX_1:2; then A28: a divides ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) by A1, Lm20; 1 / d1 > 0 by A9, A10, XREAL_1:139; then A29: (e1 - 1) / d1 < d1 by A12, Lm1; A30: (v2 - 1) div d1 = [\((v2 - 1) / d1)/] by INT_1:def_9; then A31: (v2 - 1) div d1 <= (v2 - 1) / d1 by INT_1:def_6; v2 <= e1 by A13, A23, FINSEQ_3:25; then v2 - 1 <= e1 - 1 by XREAL_1:9; then (v2 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72; then (v2 - 1) / d1 < d1 by A29, XXREAL_0:2; then (v2 - 1) div d1 < d1 by A31, XXREAL_0:2; then A32: (v2 - 1) div d1 <= d by Lm9; set d2 = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)); A33: [\0/] = 0 by INT_1:25; A34: (v1 - 1) div d1 = [\((v1 - 1) / d1)/] by INT_1:def_9; then A35: (v1 - 1) div d1 <= (v1 - 1) / d1 by INT_1:def_6; 1 <= v1 by A22, FINSEQ_3:25; then v1 - 1 >= 0 by XREAL_1:48; then (v1 - 1) div d1 >= 0 by A34, A33, PRE_FF:9; then ((v2 - 1) div d1) - ((v1 - 1) div d1) <= d by A32, Lm2; then A36: - (((v2 - 1) div d1) - ((v1 - 1) div d1)) >= - d by XREAL_1:24; A37: ( ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 or ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 ) proof assume ( not ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 & not ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 ) ; ::_thesis: contradiction then v1 - 1 = (((v2 - 1) div d1) * d1) + ((v2 - 1) mod d1) by A11, NEWTON:66 .= v2 - 1 by A11, NEWTON:66 ; hence contradiction by A25; ::_thesis: verum end; v1 <= e1 by A13, A22, FINSEQ_3:25; then v1 - 1 <= e1 - 1 by XREAL_1:9; then (v1 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72; then (v1 - 1) / d1 < d1 by A29, XXREAL_0:2; then (v1 - 1) div d1 < d1 by A35, XXREAL_0:2; then A38: (v1 - 1) div d1 <= d by Lm9; A39: ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ; (v2 - 1) mod d1 < d1 by A9, A10, NEWTON:65; then ((v2 - 1) mod d1) - ((v1 - 1) mod d1) < d1 by A26, Lm3; then ((v2 - 1) mod d1) - ((v1 - 1) mod d1) <= d by Lm9; then A40: - (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) >= - d by XREAL_1:24; take b = abs (((v1 - 1) div d1) - ((v2 - 1) div d1)); ::_thesis: ex e being Nat st ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) take e = abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)); ::_thesis: ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) A41: (v2 - 1) mod d1 >= 0 by NEWTON:64; 1 <= v2 by A23, FINSEQ_3:25; then v2 - 1 >= 0 by XREAL_1:48; then (v2 - 1) div d1 >= 0 by A30, A33, PRE_FF:9; then ((v1 - 1) div d1) - ((v2 - 1) div d1) <= d by A38, Lm2; then A42: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) <= d by A36, ABSVALUE:5; then A43: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) < a by A8, XXREAL_0:2; A44: now__::_thesis:_not_((v1_-_1)_mod_d1)_-_((v2_-_1)_mod_d1)_=_0 assume A45: ((v1 - 1) mod d1) - ((v2 - 1) mod d1) = 0 ; ::_thesis: contradiction then a divides ((v1 - 1) div d1) - ((v2 - 1) div d1) by A1, A2, A27, A39, Lm20, Th29; then a divides abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) by Lm17; then abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) = 0 by A43, NAT_D:7; hence contradiction by A37, A45, ABSVALUE:2; ::_thesis: verum end; (v1 - 1) mod d1 < d1 by A9, A10, NEWTON:65; then ((v1 - 1) mod d1) - ((v2 - 1) mod d1) < d1 by A41, Lm3; then ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <= d by Lm9; then A46: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) <= d by A40, ABSVALUE:5; then A47: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) < a by A8, XXREAL_0:2; now__::_thesis:_not_((v1_-_1)_div_d1)_-_((v2_-_1)_div_d1)_=_0 assume A48: ((v1 - 1) div d1) - ((v2 - 1) div d1) = 0 ; ::_thesis: contradiction then a divides abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) by A28, Lm17; then abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) = 0 by A47, NAT_D:7; hence contradiction by A37, A48, ABSVALUE:2; ::_thesis: verum end; hence ( b <> 0 & e <> 0 ) by A44, ABSVALUE:2; ::_thesis: ( b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) thus b <= sqrt a by A7, A42, XXREAL_0:2; ::_thesis: ( e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) thus e <= sqrt a by A7, A46, XXREAL_0:2; ::_thesis: ( a divides (k * b) + e or a divides (k * b) - e ) A49: ( b = ((v1 - 1) div d1) - ((v2 - 1) div d1) or b = - (((v1 - 1) div d1) - ((v2 - 1) div d1)) ) by ABSVALUE:1; A50: ( e = ((v1 - 1) mod d1) - ((v2 - 1) mod d1) or e = - (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ) by ABSVALUE:1; - ((k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) = (k * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) ; hence ( a divides (k * b) + e or a divides (k * b) - e ) by A28, A49, A50, INT_2:10; ::_thesis: verum end; end; end; theorem :: WSIERP_1:39 for a being Nat for fs being FinSequence holds dom (Del (fs,a)) c= dom fs by Lm12; theorem :: WSIERP_1:40 for fs being FinSequence for v being set holds ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) by Lm14; begin theorem :: WSIERP_1:41 for k being Integer for n being Nat st n > 0 & k mod n <> 0 holds - (k div n) = ((- k) div n) + 1 proof let k be Integer; ::_thesis: for n being Nat st n > 0 & k mod n <> 0 holds - (k div n) = ((- k) div n) + 1 let n be Nat; ::_thesis: ( n > 0 & k mod n <> 0 implies - (k div n) = ((- k) div n) + 1 ) assume A1: n > 0 ; ::_thesis: ( not k mod n <> 0 or - (k div n) = ((- k) div n) + 1 ) assume k mod n <> 0 ; ::_thesis: - (k div n) = ((- k) div n) + 1 then not n divides k by A1, INT_1:62; then A2: k / n is not Integer by A1, Th17; thus - (k div n) = - [\(k / n)/] by INT_1:def_9 .= [\((- k) / n)/] + 1 by A2, INT_1:63 .= ((- k) div n) + 1 by INT_1:def_9 ; ::_thesis: verum end; theorem :: WSIERP_1:42 for k being Integer for n being Nat st n > 0 & k mod n = 0 holds - (k div n) = (- k) div n proof let k be Integer; ::_thesis: for n being Nat st n > 0 & k mod n = 0 holds - (k div n) = (- k) div n let n be Nat; ::_thesis: ( n > 0 & k mod n = 0 implies - (k div n) = (- k) div n ) assume A1: n > 0 ; ::_thesis: ( not k mod n = 0 or - (k div n) = (- k) div n ) assume k mod n = 0 ; ::_thesis: - (k div n) = (- k) div n then n divides k by A1, INT_1:62; then A2: k / n is Integer by A1, Th17; thus - (k div n) = - [\(k / n)/] by INT_1:def_9 .= [\((- k) / n)/] by A2, INT_1:64 .= (- k) div n by INT_1:def_9 ; ::_thesis: verum end;