wsierp_1.miz
begin
reserve x,y,z for
Real,
a,b,c,d,e,f,g,h for
Nat,
k,l,m,n,m1,n1,m2,n2 for
Integer,
q for
Rational;
theorem ::
WSIERP_1:1
Th1: (x
|^ 2)
= (x
* x) & ((
- x)
|^ 2)
= (x
|^ 2)
proof
A1: ((
- x)
|^ 1)
= (
- x);
A2: x
= (x
|^ 1);
then (x
|^ (1
+ 1))
= (x
* x) by
NEWTON: 8;
then (x
|^ 2)
= ((
- x)
* (
- x))
.= ((
- x)
|^ (1
+ 1)) by
A1,
NEWTON: 8;
hence thesis by
A2,
NEWTON: 8;
end;
theorem ::
WSIERP_1:2
Th2: for a be
Nat holds ((
- x)
|^ (2
* a))
= (x
|^ (2
* a)) & ((
- x)
|^ ((2
* a)
+ 1))
= (
- (x
|^ ((2
* a)
+ 1)))
proof
let a be
Nat;
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 thesis by
A1;
end;
theorem ::
WSIERP_1:3
Th3: x
>=
0 & y
>=
0 & d
>
0 & (x
|^ d)
= (y
|^ d) implies x
= y
proof
assume that
A1: x
>=
0 and
A2: y
>=
0 and
A3: d
>
0 and
A4: (x
|^ d)
= (y
|^ d);
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 thesis;
end;
Lm1: (x
>=
0 iff (x
+ y)
>= y) & (x
>
0 iff (x
+ y)
> y) & (x
>=
0 iff y
>= (y
- x)) & (x
>
0 iff y
> (y
- x))
proof
A1: x
>=
0 iff (x
+ y)
>= (
0 qua
Nat
+ y) by
XREAL_1: 6;
hence x
>=
0 iff (x
+ y)
>= y;
A2: x
>
0 iff (x
+ y)
> (
0 qua
Nat
+ y) by
XREAL_1: 6;
hence x
>
0 iff (x
+ y)
> y;
thus x
>=
0 iff y
>= (y
- x) by
A1,
XREAL_1: 20;
thus thesis by
A2,
XREAL_1: 19;
end;
Lm2: x
>=
0 & y
>= z implies (x
+ y)
>= z & y
>= (z
- x)
proof
assume x
>=
0 & y
>= z;
then (x
+ y)
>= (z
+
0 qua
Nat) by
XREAL_1: 7;
hence thesis by
XREAL_1: 20;
end;
Lm3: (x
>=
0 & y
> z or x
>
0 & y
>= z) implies (x
+ y)
> z & y
> (z
- x)
proof
assume x
>=
0 & y
> z or x
>
0 & y
>= z;
then (x
+ y)
> (z
+
0 qua
Nat) by
XREAL_1: 8;
hence thesis by
XREAL_1: 19;
end;
registration
let k be
Integer, a be
natural
Number;
cluster (k
|^ a) ->
integer;
coherence
proof
A1: a is
Nat by
TARSKI: 1;
defpred
Q[
Nat] means (k
|^ $1) is
Integer;
A2: for a st
Q[a] holds
Q[(a
+ 1)]
proof
let a;
assume (k
|^ a) is
Integer;
then
reconsider b = (k
|^ a) as
Integer;
(k
|^ (a
+ 1))
= (k
* b) by
NEWTON: 6;
hence thesis;
end;
A3:
Q[
0 ] by
NEWTON: 4;
for a holds
Q[a] from
NAT_1:sch 2(
A3,
A2);
hence thesis by
A1;
end;
end
Lm4: for a holds ex b st a
= (2
* b) or a
= ((2
* b)
+ 1)
proof
let a;
set b = (a
div 2), d = (a
mod 2);
a
= ((2
* b)
+ d) by
NAT_D: 2;
then a
= ((2
* b)
+
0 qua
Nat) or a
= ((2
* b)
+ 1) by
NAT_1: 23,
NAT_D: 1;
hence thesis;
end;
theorem ::
WSIERP_1:4
Th4: k
divides m & k
divides n implies k
divides (m
+ n)
proof
assume that
A1: k
divides m and
A2: k
divides n;
consider m1 such that
A3: m
= (k
* m1) by
A1;
consider n1 such that
A4: n
= (k
* n1) by
A2;
(m
+ n)
= (k
* (m1
+ n1)) by
A3,
A4;
hence thesis;
end;
theorem ::
WSIERP_1:5
Th5: k
divides m & k
divides n implies k
divides ((m
* m1)
+ (n
* n1))
proof
assume k
divides m & k
divides n;
then k
divides (m
* m1) & k
divides (n
* n1) by
INT_2: 2;
hence thesis by
Th4;
end;
theorem ::
WSIERP_1:6
Th6: (m
gcd n)
= 1 & (k
gcd n)
= 1 implies ((m
* k)
gcd n)
= 1
proof
assume (m
gcd n)
= 1 & (k
gcd n)
= 1;
then (m,n)
are_coprime & (k,n)
are_coprime by
INT_2:def 3;
then ((m
* k),n)
are_coprime by
INT_2: 26;
hence thesis by
INT_2:def 3;
end;
theorem ::
WSIERP_1:7
(a
gcd b)
= 1 & (c
gcd b)
= 1 implies ((a
* c)
gcd b)
= 1 by
Th6;
theorem ::
WSIERP_1:8
Th8: (
0
gcd m)
=
|.m.| & (1
gcd m)
= 1
proof
A1: (m
gcd 1)
= (
|.m.|
gcd
|.1.|) by
INT_2: 34
.= (
|.m.|
gcd 1) by
ABSVALUE:def 1
.= 1 by
NEWTON: 51;
(m
gcd
0 )
= (
|.m.|
gcd
|.
0 qua
Nat.|) by
INT_2: 34
.= (
|.m.|
gcd
0 ) by
ABSVALUE: 2
.=
|.m.| by
NEWTON: 52;
hence thesis by
A1;
end;
theorem ::
WSIERP_1:9
Th9: (1,k)
are_coprime
proof
(1
gcd k)
= 1 by
Th8;
hence thesis by
INT_2:def 3;
end;
theorem ::
WSIERP_1:10
Th10: (k,l)
are_coprime implies ((k
|^ a),l)
are_coprime
proof
defpred
P[
Nat] means ((k
|^ $1),l)
are_coprime ;
assume
A1: (k,l)
are_coprime ;
A2: for a st
P[a] holds
P[(a
+ 1)]
proof
let a;
assume ((k
|^ a),l)
are_coprime ;
then ((k
* (k
|^ a)),l)
are_coprime by
A1,
INT_2: 26;
hence thesis by
NEWTON: 6;
end;
(k
|^
0 )
= 1 by
NEWTON: 4;
then
A3:
P[
0 ] by
Th9;
for a holds
P[a] from
NAT_1:sch 2(
A3,
A2);
hence thesis;
end;
theorem ::
WSIERP_1:11
Th11: (k,l)
are_coprime implies ((k
|^ a),(l
|^ b))
are_coprime
proof
assume (k,l)
are_coprime ;
then ((k
|^ a),l)
are_coprime by
Th10;
hence thesis by
Th10;
end;
theorem ::
WSIERP_1:12
Th12: (k
gcd l)
= 1 implies (k
gcd (l
|^ b))
= 1 & ((k
|^ a)
gcd (l
|^ b))
= 1
proof
assume (k
gcd l)
= 1;
then (k,l)
are_coprime by
INT_2:def 3;
then (k,(l
|^ b))
are_coprime & ((k
|^ a),(l
|^ b))
are_coprime by
Th10,
Th11;
hence thesis by
INT_2:def 3;
end;
theorem ::
WSIERP_1:13
|.m.|
divides k iff m
divides k
proof
A1:
now
assume m
divides k;
then
consider l such that
A2: (m
* l)
= k;
now
per cases ;
suppose m
>=
0 ;
then (
|.m.|
* l)
= k by
A2,
ABSVALUE:def 1;
hence
|.m.|
divides k;
end;
suppose m
<
0 ;
then (
|.m.|
* (
- l))
= ((
- m)
* (
- l)) by
ABSVALUE:def 1
.= k by
A2;
hence
|.m.|
divides k;
end;
end;
hence
|.m.|
divides k;
end;
now
assume
|.m.|
divides k;
then
consider l such that
A3: (
|.m.|
* l)
= k;
now
per cases ;
suppose m
>=
0 ;
then (m
* l)
= k by
A3,
ABSVALUE:def 1;
hence m
divides k;
end;
suppose m
<
0 ;
then k
= ((
- m)
* l) by
A3,
ABSVALUE:def 1
.= (m
* (
- l));
hence m
divides k;
end;
end;
hence m
divides k;
end;
hence thesis by
A1;
end;
theorem ::
WSIERP_1:14
Th14: a
divides b implies (a
|^ c)
divides (b
|^ c)
proof
assume a
divides b;
then
consider d be
Nat such that
A1: (a
* d)
= b by
NAT_D:def 3;
(b
|^ c)
= ((a
|^ c)
* (d
|^ c)) by
A1,
NEWTON: 7;
hence thesis;
end;
theorem ::
WSIERP_1:15
Th15: a
divides 1 implies a
= 1
proof
assume
A1: a
divides 1;
then a
divides (1
+ 1) by
NAT_D: 8;
hence thesis by
A1,
NEWTON: 39;
end;
theorem ::
WSIERP_1:16
d
divides a & (a
gcd b)
= 1 implies (d
gcd b)
= 1 by
Th15,
NEWTON: 57;
Lm5: a
<>
0 implies (a
divides b iff (b
/ a) is
Element of
NAT )
proof
assume
A1: a
<>
0 ;
A2:
now
assume a
divides b;
then
consider d be
Nat such that
A3: b
= (a
* d) by
NAT_D:def 3;
reconsider 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;
end;
now
assume (b
/ a) is
Element of
NAT ;
then
reconsider d = (b
/ a) as
Element of
NAT ;
b
= (a
* d) by
A1,
XCMPLX_1: 87;
hence a
divides b;
end;
hence thesis by
A2;
end;
theorem ::
WSIERP_1:17
Th17: k
<>
0 implies (k
divides l iff (l
/ k) is
Integer)
proof
assume
A1: k
<>
0 ;
hence k
divides l implies (l
/ k) is
Integer by
XCMPLX_1: 89;
assume (l
/ k) is
Integer;
then
reconsider m = (l
/ k) as
Integer;
l
= (k
* m) by
A1,
XCMPLX_1: 87;
hence k
divides l;
end;
Lm6: b
<>
0 & (a
* k)
= b implies k is
Element of
NAT
proof
assume that
A1: b
<>
0 and
A2: (a
* k)
= b;
A3: a
divides b qua
Integer by
A2;
A4: a
<>
0 by
A1,
A2;
then k
= (b
/ a) by
A2,
XCMPLX_1: 89;
hence thesis by
A3,
A4,
Lm5;
end;
Lm7: (a
+ b)
<= c implies a
<= c & b
<= c
proof
A1: a
<= (a
+ b) & b
<= (a
+ b) by
NAT_1: 11;
assume (a
+ b)
<= c;
hence thesis by
A1,
XXREAL_0: 2;
end;
theorem ::
WSIERP_1:18
a
<= (b
- c) implies a
<= b & c
<= b
proof
assume a
<= (b
- c);
then (a
+ c)
<= b by
XREAL_1: 19;
hence thesis by
Lm7;
end;
Lm8: k
< m iff k
<= (m
- 1)
proof
A1:
now
assume k
<= (m
- 1);
then
A2: (k
+ 1)
<= m by
XREAL_1: 19;
k
< (k
+ 1) by
XREAL_1: 29;
hence k
< m by
A2,
XXREAL_0: 2;
end;
now
assume k
< m;
then (k
+ 1)
<= m by
INT_1: 7;
hence k
<= (m
- 1) by
XREAL_1: 19;
end;
hence thesis by
A1;
end;
Lm9: k
< (m
+ 1) iff k
<= m
proof
k
< (m
+ 1) iff (k
- 1)
< m by
XREAL_1: 19;
hence thesis by
Lm8;
end;
reserve fs,fs1,fs2,fs3 for
FinSequence;
reserve D for non
empty
set,
v,v1,v2,v3 for
object,
fp for
FinSequence of
NAT ,
fr,fr1,fr2 for
FinSequence of
INT ,
ft for
FinSequence of
REAL ;
registration
let fr;
cluster (
Product fr) ->
integer;
coherence
proof
defpred
P[
FinSequence of
INT ] means (
Product $1) is
Integer;
A1:
now
let s be
FinSequence of
INT , m be
Element of
INT ;
reconsider k = m as
Integer;
assume
P[s];
then
reconsider pis = (
Product s) as
Integer;
(
Product (s
^
<*m*>))
= (pis
* k) by
RVSUM_1: 96;
hence
P[(s
^
<*m*>)];
end;
A2:
P[(
<*>
INT )] by
RVSUM_1: 94;
for fr1 holds
P[fr1] from
FINSEQ_2:sch 2(
A2,
A1);
hence thesis;
end;
end
definition
let fp;
:: original:
Sum
redefine
func
Sum (fp) ->
Element of
NAT ;
coherence
proof
defpred
P[
FinSequence of
NAT ] means (
Sum $1) is
Element of
NAT ;
A1:
now
let fp;
let a be
Element of
NAT ;
assume
P[fp];
then
reconsider sp = (
Sum fp) as
Element of
NAT ;
(
Sum (fp
^
<*a*>))
= (sp
+ a) by
RVSUM_1: 74;
hence
P[(fp
^
<*a*>)];
end;
A2:
P[(
<*>
NAT )] by
RVSUM_1: 72;
for fp holds
P[fp] from
FINSEQ_2:sch 2(
A2,
A1);
hence thesis;
end;
end
definition
let fp;
:: original:
Product
redefine
func
Product fp ->
Element of
NAT ;
coherence
proof
defpred
P[
FinSequence of
NAT ] means (
Product $1) is
Element of
NAT ;
A1:
now
let fp;
let a be
Element of
NAT ;
assume
P[fp];
then
reconsider sp = (
Product fp) as
Element of
NAT ;
(
Product (fp
^
<*a*>))
= (sp
* a) by
RVSUM_1: 96;
hence
P[(fp
^
<*a*>)];
end;
A2:
P[(
<*>
NAT )] by
RVSUM_1: 94;
for fp holds
P[fp] from
FINSEQ_2:sch 2(
A2,
A1);
hence thesis;
end;
end
Lm10: a
in (
dom fs) implies ex fs1, fs2 st fs
= ((fs1
^
<*(fs
. a)*>)
^ fs2) & (
len fs1)
= (a
- 1) & (
len fs2)
= ((
len fs)
- a)
proof
assume
A1: a
in (
dom fs);
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 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, v 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 thesis by
A3,
A4,
A5,
A6;
end;
definition
let a be
Nat, fs;
:: original:
Del
redefine
::
WSIERP_1:def1
func
Del (fs,a) means
:
Def1: it
= fs if not a
in (
dom fs)
otherwise ((
len it )
+ 1)
= (
len fs) & for b holds (b
< a implies (it
. b)
= (fs
. b)) & (b
>= a implies (it
. b)
= (fs
. (b
+ 1)));
compatibility
proof
let IT be
FinSequence;
thus not a
in (
dom fs) implies (IT
= (
Del (fs,a)) iff IT
= fs) by
FINSEQ_3: 104;
assume
A1: a
in (
dom fs);
hereby
assume
A2: IT
= (
Del (fs,a));
then
A3: ex m be
Nat st (
len fs)
= (m
+ 1) & (
len IT)
= m by
A1,
FINSEQ_3: 104;
hence ((
len IT)
+ 1)
= (
len fs);
let b;
thus b
< a implies (IT
. b)
= (fs
. b) by
A2,
FINSEQ_3: 110;
assume
A4: b
>= a;
per cases ;
suppose b
<= (
len IT);
hence (IT
. b)
= (fs
. (b
+ 1)) by
A1,
A2,
A3,
A4,
FINSEQ_3: 111;
end;
suppose
A5: b
> (
len IT);
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;
end;
end;
assume that
A7: ((
len IT)
+ 1)
= (
len fs) and
A8: for b holds (b
< a implies (IT
. b)
= (fs
. b)) & (b
>= a implies (IT
. b)
= (fs
. (b
+ 1)));
A9: for k be
Nat st 1
<= k & k
<= (
len IT) holds (IT
. k)
= ((
Del (fs,a))
. k)
proof
let k be
Nat;
assume that 1
<= k and
A10: k
<= (
len IT);
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
per cases ;
suppose
A11: k
< a;
then (IT
. k)
= (fs
. k) by
A8;
hence thesis by
A11,
FINSEQ_3: 110;
end;
suppose
A12: k
>= a;
then (IT
. k)
= (fs
. (k
+ 1)) by
A8;
hence thesis by
A1,
A7,
A10,
A12,
FINSEQ_3: 111;
end;
end;
ex m be
Nat st (
len fs)
= (m
+ 1) & (
len (
Del (fs,a)))
= m by
A1,
FINSEQ_3: 104;
hence thesis by
A7,
A9;
end;
correctness ;
end
Lm11: a
in (
dom fs) & fs
= ((fs1
^
<*v*>)
^ fs2) & (
len fs1)
= (a
- 1) implies (
Del (fs,a))
= (fs1
^ fs2)
proof
assume that
A1: a
in (
dom fs) and
A2: fs
= ((fs1
^
<*v*>)
^ fs2) and
A3: (
len fs1)
= (a
- 1);
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
let e be
Nat;
assume that
A9: 1
<= e and
A10: e
<= (
len (
Del (fs,a)));
now
per cases ;
suppose
A11: e
< a;
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;
end;
suppose
A13: e
>= a;
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 qua
Nat
+ 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;
end;
end;
hence ((fs1
^ fs2)
. e)
= ((
Del (fs,a))
. e);
end;
hence thesis by
A5;
end;
Lm12: (
dom (
Del (fs,a)))
c= (
dom fs)
proof
now
assume
A1: a
in (
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 thesis by
XBOOLE_1: 7;
end;
hence thesis by
Def1;
end;
definition
let D;
let a be
Nat;
let fs be
FinSequence of D;
:: original:
Del
redefine
func
Del (fs,a) ->
FinSequence of D ;
coherence
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;
end;
end
definition
let D;
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
proof
thus (
rng (
Del (fs,a)))
c= D1 by
FINSEQ_1:def 4;
end;
end
Lm13: (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
set f = (fs1
^ fs2);
A1: (
len f)
= ((
len fs1)
+ (
len fs2)) by
FINSEQ_1: 22;
A2:
now
set f2 = (fs1
^ (
Del (fs2,a)));
set f1 = (
Del (f,((
len fs1)
+ a)));
assume
A3: a
>= 1;
now
per cases ;
suppose
A4: a
> (
len fs2);
then
A5: not a
in (
dom fs2) by
FINSEQ_3: 25;
((
len fs1)
+ a)
> (
len f) by
A1,
A4,
XREAL_1: 6;
then not ((
len fs1)
+ a)
in (
dom f) by
FINSEQ_3: 25;
hence f1
= (fs1
^ fs2) by
Def1
.= f2 by
A5,
Def1;
end;
suppose
A6: a
<= (
len fs2);
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 f) by
A1,
A6,
XREAL_1: 6;
then
A10: ((
len fs1)
+ a)
in (
dom f) by
A9,
FINSEQ_3: 25;
then
consider g1,g2 be
FinSequence such that
A11: f
= ((g1
^
<*(f
. ((
len fs1)
+ a))*>)
^ g2) and
A12: (
len g1)
= (((
len fs1)
+ a)
- 1) and (
len g2)
= ((
len f)
- ((
len fs1)
+ a)) by
Lm10;
A13: f1
= (g1
^ g2) by
A10,
A11,
A12,
Lm11;
f
= (g1
^ (
<*(f
. ((
len fs1)
+ a))*>
^ g2)) by
A11,
FINSEQ_1: 32;
then
consider t be
FinSequence such that
A14: (fs1
^ t)
= g1 by
A12,
A8,
FINSEQ_1: 47;
(fs1
^ ((t
^
<*(f
. ((
len fs1)
+ a))*>)
^ g2))
= ((fs1
^ (t
^
<*(f
. ((
len fs1)
+ a))*>))
^ g2) by
FINSEQ_1: 32
.= f by
A11,
A14,
FINSEQ_1: 32;
then
A15: fs2
= ((t
^
<*(f
. ((
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 f1
= f2 by
A13,
A14,
FINSEQ_1: 32;
end;
end;
hence f1
= f2;
end;
now
set f3 =
<*(f
. a)*>;
set f2 = ((
Del (fs1,a))
^ fs2);
set f1 = (
Del (f,a));
assume
A16: a
<= (
len fs1);
(
len fs1)
<= (
len f) by
A1,
NAT_1: 11;
then
A17: a
<= (
len f) by
A16,
XXREAL_0: 2;
now
per cases ;
suppose
A18: a
< 1;
then
A19: not a
in (
dom fs1) by
FINSEQ_3: 25;
not a
in (
dom f) by
A18,
FINSEQ_3: 25;
hence f1
= f by
Def1
.= f2 by
A19,
Def1;
end;
suppose
A20: a
>= 1;
then
A21: a
in (
dom f) by
A17,
FINSEQ_3: 25;
then
consider g1,g2 be
FinSequence such that
A22: f
= ((g1
^ f3)
^ g2) and
A23: (
len g1)
= (a
- 1) and (
len g2)
= ((
len f)
- a) by
Lm10;
(
len (g1
^ f3))
= ((a
- 1)
+ 1) by
A23,
FINSEQ_2: 16
.= a;
then
consider t be
FinSequence such that
A24: fs1
= ((g1
^ f3)
^ t) by
A16,
A22,
FINSEQ_1: 47;
((g1
^ f3)
^ g2)
= ((g1
^ f3)
^ (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 f1
= (g1
^ g2) by
A21,
A22,
A23,
Lm11
.= f2 by
A26,
A25,
FINSEQ_1: 32;
end;
end;
hence f1
= f2;
end;
hence thesis by
A2;
end;
Lm14: (
Del ((
<*v*>
^ fs),1))
= fs & (
Del ((fs
^
<*v*>),((
len fs)
+ 1)))
= fs
proof
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;
(fs
^
{} )
= fs by
FINSEQ_1: 34;
hence thesis by
A2,
Lm13;
end;
theorem ::
WSIERP_1:19
(
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
thus (
Del (
<*v1*>,1))
= (
Del ((
<*v1*>
^
{} ),1)) by
FINSEQ_1: 34
.=
{} by
Lm14;
thus (
Del (
<*v1, v2*>,1))
=
<*v2*> by
Lm14;
(
len
<*v1*>)
= 1 by
FINSEQ_1: 39;
hence
A1: (
Del (
<*v1, v2*>,2))
= (
Del ((
<*v1*>
^
<*v2*>),((
len
<*v1*>)
+ 1)))
.=
<*v1*> by
Lm14;
thus (
Del (
<*v1, v2, v3*>,1))
= (
Del ((
<*v1*>
^
<*v2, v3*>),1)) by
FINSEQ_1: 43
.=
<*v2, v3*> by
Lm14;
A2: (
len
<*v1, v2*>)
= 2 by
FINSEQ_1: 44;
hence (
Del (
<*v1, v2, v3*>,2))
=
<*v1, v3*> by
A1,
Lm13;
((
len
<*v1, v2*>)
+ 1)
= 3 by
A2;
hence thesis by
Lm14;
end;
Lm15: 1
<= (
len fs) implies fs
= (
<*(fs
. 1)*>
^ (
Del (fs,1))) & fs
= ((
Del (fs,(
len fs)))
^
<*(fs
. (
len fs))*>)
proof
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);
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 fs1) by
FINSEQ_1: 22;
for b be
Nat st 1
<= b & b
<= (
len fs) holds (fs
. b)
= (fs1
. b)
proof
let b be
Nat;
assume that
A6: 1
<= b and
A7: b
<= (
len fs);
now
per cases by
A6,
XXREAL_0: 1;
suppose
A8: b
= 1;
1
in (
dom
<*(fs
. 1)*>) by
A1,
FINSEQ_3: 25;
hence (fs1
. b)
= (
<*(fs
. 1)*>
. 1) by
A8,
FINSEQ_1:def 7
.= (fs
. b) by
A8,
FINSEQ_1: 40;
end;
suppose
A9: b
> 1;
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 (fs1
. b)
= ((
Del (fs,1))
. e) by
A1,
A5,
A7,
A9,
FINSEQ_1: 24
.= (fs
. (e
+ 1)) by
A4,
A11,
Def1
.= (fs
. b);
end;
end;
hence thesis;
end;
hence fs1
= fs by
A5;
(
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 fs2) 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 be
Nat st 1
<= b & b
<= (
len fs) holds (fs
. b)
= (fs2
. b)
proof
let b be
Nat;
assume that
A15: 1
<= b and
A16: b
<= (
len fs);
now
per cases by
A16,
XXREAL_0: 1;
suppose
A17: b
= (
len fs);
reconsider e = (b
- (b
- 1)) as
Element of
NAT ;
thus (fs2
. b)
= (
<*(fs
. (
len fs))*>
. e) by
A13,
A12,
A17,
FINSEQ_1: 24,
XREAL_1: 146
.= (fs
. b) by
A17,
FINSEQ_1: 40;
end;
suppose
A18: b
< (
len fs);
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 (fs2
. b)
= ((
Del (fs,(
len fs)))
. b) by
FINSEQ_1:def 7
.= (fs
. b) by
A3,
A18,
Def1;
end;
end;
hence thesis;
end;
hence thesis by
A12;
end;
Lm16: a
in (
dom ft) implies ((
Product (
Del (ft,a)))
* (ft
. a))
= (
Product ft)
proof
defpred
P[
Nat] means $1
in (
dom ft) implies ((ft
. $1)
* (
Product (
Del (ft,$1))))
= (
Product ft);
A1: for a st
P[a] holds
P[(a
+ 1)]
proof
let a such that
P[a];
now
per cases ;
suppose
A2: a
=
0 ;
thus
P[(a
+ 1)]
proof
assume (a
+ 1)
in (
dom 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))));
hence thesis by
A2;
end;
end;
suppose a
>
0 & a
< (
len ft);
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 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 as
FinSequence of
REAL by
A4,
FINSEQ_1: 36;
reconsider 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))
.= ((ft
. (a
+ 1))
* ((
Product fs1)
* (
Product fs2)));
hence thesis by
A6,
RVSUM_1: 97;
end;
suppose a
>= (
len ft);
then (
len ft)
< (a
+ 1) by
NAT_1: 13;
hence thesis by
FINSEQ_3: 25;
end;
end;
hence thesis;
end;
A7:
P[
0 ] by
FINSEQ_3: 25;
for a holds
P[a] from
NAT_1:sch 2(
A7,
A1);
hence thesis;
end;
theorem ::
WSIERP_1:20
a
in (
dom ft) implies ((
Sum (
Del (ft,a)))
+ (ft
. a))
= (
Sum ft)
proof
defpred
P[
Nat] means $1
in (
dom ft) implies ((ft
. $1)
+ (
Sum (
Del (ft,$1))))
= (
Sum ft);
A1: for a st
P[a] holds
P[(a
+ 1)]
proof
let a such that
P[a];
now
per cases ;
suppose
A2: a
=
0 ;
thus
P[(a
+ 1)]
proof
reconsider ft1 = (ft
. 1) as
Element of
REAL by
XREAL_0:def 1;
assume (a
+ 1)
in (
dom ft);
then (a
+ 1)
<= (
len ft) by
FINSEQ_3: 25;
then (
<*(ft
. 1)*>
^ (
Del (ft,1)))
= ft by
A2,
Lm15;
then (
Sum ft)
= ((
Sum
<*ft1*>)
+ (
Sum (
Del (ft,1)))) by
RVSUM_1: 75
.= ((ft
. 1)
+ (
Sum (
Del (ft,1)))) by
FINSOP_1: 11;
hence thesis by
A2;
end;
end;
suppose a
>
0 & a
< (
len ft);
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 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;
reconsider fta1 = (ft
. (a
+ 1)) as
Element of
REAL by
XREAL_0:def 1;
A6: (
Del (ft,(a
+ 1)))
= (fs1
^ fs2) by
A3,
A4,
A5,
Lm11;
reconsider fs2 as
FinSequence of
REAL by
A4,
FINSEQ_1: 36;
reconsider 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
<*fta1*>))
+ (
Sum fs2)) by
RVSUM_1: 75
.= ((fta1
+ (
Sum fs1))
+ (
Sum fs2)) by
FINSOP_1: 11
.= ((ft
. (a
+ 1))
+ ((
Sum fs1)
+ (
Sum fs2)));
hence thesis by
A6,
RVSUM_1: 75;
end;
suppose a
>= (
len ft);
then (a
+ 1)
> (
len ft) by
NAT_1: 13;
hence thesis by
FINSEQ_3: 25;
end;
end;
hence thesis;
end;
A7:
P[
0 ] by
FINSEQ_3: 25;
for a holds
P[a] from
NAT_1:sch 2(
A7,
A1);
hence thesis;
end;
theorem ::
WSIERP_1:21
a
in (
dom fp) implies ((
Product fp)
/ (fp
. a)) is
Element of
NAT
proof
assume a
in (
dom fp);
then
consider fs1, fs2 such that
A1: fp
= ((fs1
^
<*(fp
. a)*>)
^ fs2) and (
len fs1)
= (a
- 1) and (
len fs2)
= ((
len fp)
- a) by
Lm10;
per cases ;
suppose
A2: (fp
. a)
<>
0 ;
reconsider 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 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 thesis by
A2,
XCMPLX_1: 89;
end;
suppose
A3: (fp
. a)
=
0 ;
((
Product fp)
/ (fp
. a))
= ((
Product fp)
* ((fp
. a)
" )) by
XCMPLX_0:def 9
.= ((
Product fp)
*
0 qua
Nat) by
A3
.=
0 ;
hence thesis;
end;
end;
theorem ::
WSIERP_1:22
Th22: ((
numerator q),(
denominator q))
are_coprime
proof
set k = (
numerator q);
set h = (
denominator q);
reconsider a = (k
gcd h) as
Element of
NAT by
INT_2: 20;
a
divides k by
INT_2: 21;
then
A1: ex l st k
= (a
* l);
(k
gcd h)
divides h by
INT_2: 21;
then
consider b be
Nat such that
A2: h
= (a
* b) by
NAT_D:def 3;
a
<>
0 by
INT_2: 5;
then
A3: a
>= (
0 qua
Nat
+ 1) by
NAT_1: 13;
reconsider b as
Element of
NAT by
ORDINAL1:def 12;
A4: h
= (a
* b) by
A2;
assume not (k,h)
are_coprime ;
then a
<> 1 by
INT_2:def 3;
then a
> 1 by
A3,
XXREAL_0: 1;
hence contradiction by
A1,
A4,
RAT_1: 29;
end;
theorem ::
WSIERP_1:23
q
= (k
/ a) & a
<>
0 & (k,a)
are_coprime implies k
= (
numerator q) & a
= (
denominator q)
proof
assume that
A1: q
= (k
/ a) & a
<>
0 and
A2: (k,a)
are_coprime ;
consider b be
Nat such that
A3: k
= ((
numerator q)
* b) & a
= ((
denominator q)
* b) by
A1,
RAT_1: 27;
((
numerator q),(
denominator q))
are_coprime by
Th22;
then (k
gcd a)
=
|.b.| by
A3,
INT_2: 24;
then 1
=
|.b.| by
A2,
INT_2:def 3
.= b by
ABSVALUE:def 1;
hence thesis by
A3;
end;
theorem ::
WSIERP_1:24
Th24: (ex q st a
= (q
|^ b)) implies ex k st a
= (k
|^ b)
proof
given q such that
A1: a
= (q
|^ b);
now
A2:
now
set d = (
denominator q);
set k = (
numerator q);
assume b
<>
0 ;
then
consider e be
Nat such that
A3: (e
+ 1)
= b by
NAT_1: 6;
A4: (d
|^ b)
<>
0 by
CARD_4: 3;
((k
|^ b),d)
are_coprime by
Th10,
Th22;
then
A5: ((k
|^ b)
gcd d)
= 1 by
INT_2:def 3;
A6: q
= (k
/ d) by
RAT_1: 15;
then a
= ((k
|^ b)
/ (d
|^ b)) by
A1,
PREPOWER: 8;
then (a
* (d
|^ b))
= (k
|^ b) by
A4,
XCMPLX_1: 87;
then (k
|^ b)
= (a
* ((d
|^ e)
* d)) by
A3,
NEWTON: 6
.= ((a
* (d
|^ e))
* d);
then d
divides (k
|^ b);
then d
= 1 or d
= (
- 1) by
A5,
INT_2: 13,
INT_2: 22;
hence thesis by
A1,
A6;
end;
now
assume
A7: b
=
0 ;
then a
= 1 by
A1,
NEWTON: 4;
then a
= (1
|^
0 );
hence thesis by
A7;
end;
hence thesis by
A2;
end;
hence thesis;
end;
theorem ::
WSIERP_1:25
Th25: (ex q st a
= (q
|^ d)) implies ex b st a
= (b
|^ d)
proof
assume ex q st a
= (q
|^ d);
then
consider k such that
A1: a
= (k
|^ d) by
Th24;
A2:
now
assume
A3: a
=
0 ;
then d
<>
0 by
A1,
NEWTON: 4;
then a
= (
0
|^ d) by
A3,
NAT_1: 14,
NEWTON: 11;
hence thesis;
end;
per cases ;
suppose d
<>
0 ;
now
consider e such that
A4: d
= (2
* e) or d
= ((2
* e)
+ 1) by
Lm4;
consider c be
Nat such that
A5: k
= c or k
= (
- c) by
INT_1: 2;
assume
A6: not k is
Nat;
A7:
now
assume d
= ((2
* e)
+ 1);
then (
- (c
|^ d))
= a by
A1,
A6,
A5,
Th2;
hence thesis by
A2;
end;
now
assume d
= (2
* e);
then a
= (c
|^ d) by
A1,
A5,
Th2;
hence thesis;
end;
hence thesis by
A4,
A7;
end;
hence thesis by
A1;
end;
suppose
A8: d
=
0 ;
then a
= 1 by
A1,
NEWTON: 4;
then a
= (1
|^
0 );
hence thesis by
A8;
end;
end;
theorem ::
WSIERP_1:26
e
>
0 & (a
|^ e)
divides (b
|^ e) implies a
divides b
proof
assume that
A1: e
>
0 and
A2: (a
|^ e)
divides (b
|^ e);
consider f be
Nat such that
A3: ((a
|^ e)
* f)
= (b
|^ e) by
A2,
NAT_D:def 3;
A4:
now
assume that
A5: a
<>
0 and b
<>
0 ;
(a
|^ e)
<>
0 by
A5,
CARD_4: 3;
then f
= ((b
|^ e)
/ (a
|^ e)) by
A3,
XCMPLX_1: 89
.= ((b
/ a)
|^ e) by
PREPOWER: 8;
then
consider d such that
A6: f
= (d
|^ e) by
Th25;
(b
|^ e)
= ((a
* d)
|^ e) by
A3,
A6,
NEWTON: 7;
then b
= (a
* d) by
A1,
Th3;
hence thesis;
end;
A7:
now
assume
A8: a
=
0 ;
then
0
divides (b
|^ e) by
A1,
A2,
NAT_1: 14,
NEWTON: 11;
then ex f be
Nat st (
0
* f)
= (b
|^ e) by
NAT_D:def 3;
hence thesis by
A8,
CARD_4: 3;
end;
now
assume b
=
0 ;
then (a
*
0 qua
Nat)
= b;
hence thesis;
end;
hence thesis by
A7,
A4;
end;
theorem ::
WSIERP_1:27
Th27: ex m, n st (a
gcd b)
= ((a
* m)
+ (b
* n))
proof
A1: ex m, n st (
0
gcd c)
= ((
0
* m)
+ (c
* n))
proof
take
0 , 1;
thus thesis by
NEWTON: 52;
end;
now
per cases ;
suppose a
=
0 ;
hence thesis by
A1;
end;
suppose
A2: b
=
0 ;
then ex m, n st (a
gcd b)
= ((
0
* m)
+ (a
* n)) by
A1;
hence thesis by
A2;
end;
suppose
A3: a
<>
0 & b
<>
0 ;
defpred
P[
set] means ex m, n st $1
= ((a
* m)
+ (b
* n)) & $1
<>
0 ;
(a
+ b)
= ((a
* 1)
+ (b
* 1));
then
A4: ex c be
Nat st
P[c] by
A3;
consider d be
Nat such that
A5:
P[d] & for c be
Nat st
P[c] holds d
<= c from
NAT_1:sch 5(
A4);
consider e,f be
Nat such that
A6: a
= ((d
* e)
+ f) and
A7: f
< d by
A5,
NAT_1: 17;
consider m, n such that
A8: d
= ((a
* m)
+ (b
* n)) by
A5;
A9:
now
assume
A10: f
<>
0 ;
f
= (a
- (d
* e)) by
A6
.= ((a
* (1
- (m
* e)))
+ (b
* (
- (n
* e)))) by
A8;
hence contradiction by
A5,
A7,
A10;
end;
consider e,f be
Nat such that
A11: b
= ((d
* e)
+ f) and
A12: f
< d by
A5,
NAT_1: 17;
now
assume
A13: f
<>
0 ;
f
= (b
- (d
* e)) by
A11
.= ((b
* (1
- (n
* e)))
+ (a
* (
- (m
* e)))) by
A8;
hence contradiction by
A5,
A12,
A13;
end;
then
A14: d
divides b by
A11;
d
divides a by
A6,
A9;
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 qua
Integer by
A8,
Th5;
hence thesis by
A8,
A15,
NAT_D: 5;
end;
end;
hence thesis;
end;
theorem ::
WSIERP_1:28
Th28: ex m1, n1 st (m
gcd n)
= ((m
* m1)
+ (n
* n1))
proof
(m
gcd n)
= (
|.m.|
gcd
|.n.|) by
INT_2: 34;
then
consider m1, n1 such that
A1: ((
|.m.|
* m1)
+ (
|.n.|
* n1))
= (m
gcd n) by
Th27;
now
per cases ;
suppose m
>=
0 & n
>=
0 ;
then
|.m.|
= m &
|.n.|
= n by
ABSVALUE:def 1;
hence thesis by
A1;
end;
suppose
A2: m
>=
0 & n
<
0 ;
then
|.n.|
= (
- n) by
ABSVALUE:def 1;
then (m
gcd n)
= ((m
* m1)
+ (n
* (
- n1))) by
A1,
A2,
ABSVALUE:def 1;
hence thesis;
end;
suppose
A3: m
<
0 & n
>=
0 ;
then
|.m.|
= (
- m) by
ABSVALUE:def 1;
then (m
gcd n)
= ((m
* (
- m1))
+ (n
* n1)) by
A1,
A3,
ABSVALUE:def 1;
hence thesis;
end;
suppose m
<
0 & n
<
0 ;
then
|.m.|
= (
- m) &
|.n.|
= (
- n) by
ABSVALUE:def 1;
then (m
gcd n)
= ((m
* (
- m1))
+ (n
* (
- n1))) by
A1;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
WSIERP_1:29
Th29: m
divides (n
* k) & (m
gcd n)
= 1 implies m
divides k
proof
assume that
A1: m
divides (n
* k) and
A2: (m
gcd n)
= 1;
consider m1, n1 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 thesis by
A1,
Th5;
end;
theorem ::
WSIERP_1:30
for a,b,c be
Nat holds (a
gcd b)
= 1 & a
divides (b
* c) implies a
divides c by
Th29;
theorem ::
WSIERP_1:31
Th31: a
<>
0 & b
<>
0 implies ex c, d st (a
gcd b)
= ((a
* c)
- (b
* d))
proof
assume that
A1: a
<>
0 and
A2: b
<>
0 ;
consider m, n such that
A3: (a
gcd b)
= ((a
* m)
+ (b
* n)) by
Th27;
set k = (
[/(
max ((
- (m
/ b)),(n
/ a)))\]
+ 1);
k
> (n
/ a) by
INT_1: 32,
XXREAL_0: 31;
then (k
* a)
> n by
A1,
XREAL_1: 77;
then
A4: ((k
* a)
- n)
>
0 by
XREAL_1: 50;
k
> (
- (m
/ b)) by
INT_1: 32,
XXREAL_0: 31;
then k
> ((
- m)
/ b) by
XCMPLX_1: 187;
then (k
* b)
> (
- m) by
A2,
XREAL_1: 77;
then ((k
* b)
- (
- m))
>
0 by
XREAL_1: 50;
then
reconsider e = ((k
* b)
+ m), d = ((k
* a)
- n) as
Element of
NAT by
A4,
INT_1: 3;
((a
* e)
- (b
* d))
= (((a
* m)
+
0 qua
Nat)
+ (b
* n));
hence thesis by
A3;
end;
theorem ::
WSIERP_1:32
f
>
0 & g
>
0 & (f
gcd g)
= 1 & (a
|^ f)
= (b
|^ g) implies ex e st a
= (e
|^ g) & b
= (e
|^ f)
proof
assume that
A1: f
>
0 and
A2: g
>
0 and
A3: (f
gcd g)
= 1 and
A4: (a
|^ f)
= (b
|^ g);
now
per cases ;
suppose
A5: a
=
0 ;
then (a
|^ f)
=
0 by
A1,
NAT_1: 14,
NEWTON: 11;
then
A6: b
= (
0
|^ f) by
A4,
A5,
CARD_4: 3;
a
= (
0
|^ g) by
A2,
A5,
CARD_4: 3;
hence thesis by
A6;
end;
suppose
A7: b
=
0 ;
then (b
|^ g)
=
0 by
A2,
NAT_1: 14,
NEWTON: 11;
then
A8: a
= (
0
|^ g) by
A4,
A7,
CARD_4: 3;
b
= (
0
|^ f) by
A1,
A7,
CARD_4: 3;
hence thesis by
A8;
end;
suppose
A9: a
<>
0 & b
<>
0 ;
consider c, d such that
A10: ((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
A9,
A10,
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 such that
A11: a
= (h
|^ g) by
Th25;
(b
|^ g)
= (h
|^ (f
* g)) by
A4,
A11,
NEWTON: 9
.= ((h
|^ f)
|^ g) by
NEWTON: 9;
then b
= (h
|^ f) by
A2,
Th3;
hence thesis by
A11;
end;
end;
hence thesis;
end;
reserve x,y,t for
Integer;
theorem ::
WSIERP_1:33
Th33: (ex x, y st ((m
* x)
+ (n
* y))
= k) iff (m
gcd n)
divides k
proof
A1:
now
assume
A2: (m
gcd n)
divides k;
now
consider m1, n1 such that
A3: (m
gcd n)
= ((m
* m1)
+ (n
* n1)) by
Th28;
consider l such that
A4: ((m
gcd n)
* l)
= k by
A2;
k
= ((m
* (m1
* l))
+ (n
* (n1
* l))) by
A4,
A3;
hence ex x, y st ((m
* x)
+ (n
* y))
= k;
end;
hence ex x, y st ((m
* x)
+ (n
* y))
= k;
end;
now
given x, y such that
A5: ((m
* x)
+ (n
* y))
= k;
(m
gcd n)
divides m & (m
gcd n)
divides n by
INT_2: 21;
hence (m
gcd n)
divides k by
A5,
Th5;
end;
hence thesis by
A1;
end;
theorem ::
WSIERP_1:34
m
<>
0 & n
<>
0 & ((m
* m1)
+ (n
* n1))
= k implies for x, y st ((m
* x)
+ (n
* y))
= k holds ex t st x
= (m1
+ (t
* (n
/ (m
gcd n)))) & y
= (n1
- (t
* (m
/ (m
gcd n))))
proof
assume that
A1: m
<>
0 and
A2: n
<>
0 and
A3: ((m
* m1)
+ (n
* n1))
= k;
consider m2, n2 such that
A4: m
= ((m
gcd n)
* m2) and
A5: n
= ((m
gcd n)
* n2) and
A6: (m2,n2)
are_coprime 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;
assume ((m
* x)
+ (n
* y))
= k;
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));
then n2
divides (x
- m1) by
A10,
Th29;
then
consider t such that
A12: (n2
* t)
= (x
- m1);
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 thesis by
A8,
A9,
A16;
end;
theorem ::
WSIERP_1:35
(a
gcd b)
= 1 & (a
* b)
= (c
|^ d) implies ex e, f st a
= (e
|^ d) & b
= (f
|^ d)
proof
assume that
A1: (a
gcd b)
= 1 and
A2: (a
* b)
= (c
|^ d);
set e = (a
gcd c);
e
divides c by
NAT_D:def 5;
then
A3: (e
|^ d)
divides (c
|^ d) by
Th14;
e
divides a by
NAT_D:def 5;
then (e
gcd b)
= 1 by
A1,
Th15,
NEWTON: 57;
then ((e
|^ d)
gcd b)
= 1 by
Th12;
then (e
|^ d)
divides a by
A2,
A3,
Th29;
then
consider g be
Nat such that
A4: ((e
|^ d)
* g)
= a by
NAT_D:def 3;
reconsider g as
Element of
NAT by
ORDINAL1:def 12;
A5:
now
assume
A6: d
<>
0 ;
then
consider d1 be
Nat such that
A7: d
= (1
+ d1) by
NAT_1: 10,
NAT_1: 14;
reconsider d1 as
Element of
NAT by
ORDINAL1:def 12;
A8: d
>= 1 by
A6,
NAT_1: 14;
A9:
now
assume
A10: e
<>
0 ;
then
A11: a
<>
0 or c
<>
0 by
INT_2: 5;
then
A12: a
<>
0 by
A2,
CARD_4: 3;
A13:
now
reconsider e1 = e as
Real;
assume
A14: c
<>
0 ;
then
consider a1,c1 be
Integer such that
A15: a
= (e
* a1) and
A16: (e
* c1)
= c and
A17: (a1,c1 qua
Integer)
are_coprime by
INT_2: 23;
reconsider a1, c1 as
Element of
NAT by
A12,
A14,
A15,
A16,
Lm6;
a1
= (((e
|^ (d1
+ 1))
* g)
/ e) by
A4,
A7,
A10,
A15,
XCMPLX_1: 89
.= (((e
* (e
|^ d1))
* g)
/ e) by
NEWTON: 6
.= ((e
* ((e
|^ d1)
* g))
/ e)
.= ((e
|^ d1)
* g) by
A10,
XCMPLX_1: 89;
then
A18: g
divides a1;
(a1
gcd c1)
= 1 by
A17,
INT_2:def 3;
then (g
gcd c1)
= 1 by
A18,
Th15,
NEWTON: 57;
then
A19: (g
gcd (c1
|^ d))
= 1 by
Th12;
A20: (e1
|^ d)
<>
0 by
A10,
CARD_4: 3;
c1
= (c
/ e) by
A10,
A16,
XCMPLX_1: 89;
then
A21: (c1
|^ d)
= (((e
|^ d)
* (g
* b))
/ (e
|^ d)) by
A2,
A4,
PREPOWER: 8
.= (g
* b) by
A20,
XCMPLX_1: 89;
then g
divides (c1
|^ d);
then g
= 1 by
A19,
NEWTON: 49;
hence thesis by
A4,
A21;
end;
now
assume
0
= c;
then
A22: b
=
0 by
A2,
A8,
A11,
NEWTON: 11,
XCMPLX_1: 6;
then a
= 1 by
A1,
NEWTON: 52;
then
A23: a
= (1
|^ d);
b
= (
0
|^ d) by
A6,
A22,
NAT_1: 14,
NEWTON: 11;
hence thesis by
A23;
end;
hence thesis by
A13;
end;
now
assume e
=
0 ;
then
A24: a
=
0 by
INT_2: 5;
then b
= 1 by
A1,
NEWTON: 52;
then
A25: b
= (1
|^ d);
a
= (
0
|^ d) by
A6,
A24,
NAT_1: 14,
NEWTON: 11;
hence thesis by
A25;
end;
hence thesis by
A9;
end;
now
assume
A26: d
=
0 ;
then
A27: (a
* b)
= 1 by
A2,
NEWTON: 4;
then b
divides 1;
then b
= 1 by
Th15;
then
A28: b
= (1
|^
0 );
a
divides 1 by
A27;
then a
= 1 by
Th15;
then a
= (1
|^
0 );
hence thesis by
A26,
A28;
end;
hence thesis by
A5;
end;
::$Notion-Name
theorem ::
WSIERP_1:36
Th36: for d holds (for a st a
in (
dom fp) holds ((fp
. a)
gcd d)
= 1) implies ((
Product fp)
gcd d)
= 1
proof
let d;
defpred
TH[
set] means ex f be
FinSequence of
NAT st f
= $1 & ((for a st a
in (
dom f) holds ((f
. a)
gcd d)
= 1) implies ((
Product f)
gcd d)
= 1);
A1:
now
let fp;
let a be
Element of
NAT such that
A2:
TH[fp];
thus
TH[(fp
^
<*a*>)]
proof
set fp1 = (fp
^
<*a*>);
take fp1;
thus fp1
= (fp
^
<*a*>);
assume
A3: for b st b
in (
dom fp1) holds ((fp1
. b)
gcd d)
= 1;
A4: (
dom fp)
c= (
dom fp1) by
FINSEQ_1: 26;
A5: for b st b
in (
dom fp) holds ((fp
. b)
gcd d)
= 1
proof
let b;
assume
A6: b
in (
dom fp);
then ((fp1
. b)
gcd d)
= 1 by
A3,
A4;
hence thesis by
A6,
FINSEQ_1:def 7;
end;
(
len fp1)
in (
dom fp1) by
FINSEQ_5: 6;
then (
len fp1)
= ((
len fp)
+ 1) & ((fp1
. (
len fp1))
gcd d)
= 1 by
A3,
FINSEQ_2: 16;
then
A7: (a
gcd d)
= 1 by
FINSEQ_1: 42;
(
Product fp1)
= ((
Product fp)
* a) by
RVSUM_1: 96;
hence thesis by
A2,
A5,
A7,
Th6;
end;
end;
A8:
TH[(
<*>
NAT )]
proof
take (
<*>
NAT );
thus thesis by
NEWTON: 51,
RVSUM_1: 94;
end;
for fp holds
TH[fp] from
FINSEQ_2:sch 2(
A8,
A1);
then ex f be
FinSequence of
NAT st f
= fp & ((for a st a
in (
dom f) holds ((f
. a)
gcd d)
= 1) implies ((
Product f)
gcd d)
= 1);
hence thesis;
end;
theorem ::
WSIERP_1:37
(
len fp)
>= 2 & (for b, c st b
in (
dom fp) & c
in (
dom fp) & b
<> c holds ((fp
. b)
gcd (fp
. c))
= 1) implies for fr st (
len fr)
= (
len fp) holds ex fr1 st ((
len fr1)
= (
len fp) & for b st b
in (
dom fp) holds (((fp
. b)
* (fr1
. b))
+ (fr
. b))
= (((fp
. 1)
* (fr1
. 1))
+ (fr
. 1)))
proof
defpred
CC[
FinSequence of
NAT ] means for fr st (
len fr)
= (
len $1) holds ex fr1 st ((
len fr1)
= (
len $1) & for b st b
in (
dom $1) holds ((($1
. b)
* (fr1
. b))
+ (fr
. b))
= ((($1
. 1)
* (fr1
. 1))
+ (fr
. 1)));
defpred
RP[
FinSequence of
NAT ] means for b, c st b
in (
dom $1) & c
in (
dom $1) & b
<> c holds (($1
. b)
gcd ($1
. c))
= 1;
defpred
TH[
set] means ex f be
FinSequence of
NAT st f
= $1 & (((
len f)
>= 2 &
RP[f]) implies
CC[f]);
A1:
now
let fp;
let d be
Element of
NAT such that
A2:
TH[fp];
set k = (
len fp);
set fp1 = (fp
^
<*d*>);
now
assume that
A3: (
len fp1)
>= 2 and
A4:
RP[fp1];
A5: (
len fp1)
= (k
+ 1) by
FINSEQ_2: 16;
now
per cases by
A3,
XXREAL_0: 1;
suppose
A6: (
len fp1)
= 2;
now
let fr such that (
len fr)
= (
len fp1);
1
in (
dom fp1) & 2
in (
dom fp1) by
A6,
FINSEQ_3: 25;
then ((fp1
. 1)
gcd (fp1
. 2))
= 1 by
A4;
then ((fp1
. 1)
gcd (fp1
. 2))
divides ((fr
. 1)
- (fr
. 2)) by
INT_2: 12;
then
consider m, n such that
A7: (((fp1
. 1)
* m)
+ ((fp1
. 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*>;
thus (
len fr1)
= (
len fp1) by
A6,
FINSEQ_1: 44;
let b;
assume b
in (
dom fp1);
then
A8: b
in (
Seg (
len fp1)) by
FINSEQ_1:def 3;
now
per cases by
A6,
A8,
FINSEQ_1: 2,
TARSKI:def 2;
suppose b
= 1;
hence (((fp1
. b)
* (fr1
. b))
+ (fr
. b))
= (((fp1
. 1)
* (fr1
. 1))
+ (fr
. 1));
end;
suppose
A9: b
= 2;
A10: (fr1
. 1)
= (
- m) & (fr1
. 2)
= n by
FINSEQ_1: 44;
(((fp1
. 2)
* n)
- ((fp1
. 1)
* (
- m)))
= ((fr
. 1)
- (fr
. 2)) by
A7;
hence (((fp1
. b)
* (fr1
. b))
+ (fr
. b))
= (((fp1
. 1)
* (fr1
. 1))
+ (fr
. 1)) by
A9,
A10,
XCMPLX_1: 34;
end;
end;
hence (((fp1
. b)
* (fr1
. b))
+ (fr
. b))
= (((fp1
. 1)
* (fr1
. 1))
+ (fr
. 1));
end;
hence
CC[fp1];
end;
suppose
A11: (
len fp1)
> 2;
A12:
RP[fp]
proof
A13: (
dom fp)
c= (
dom fp1) by
FINSEQ_1: 26;
let b, c such that
A14: b
in (
dom fp) & c
in (
dom fp) and
A15: b
<> c;
(fp1
. b)
= (fp
. b) & (fp1
. c)
= (fp
. c) by
A14,
FINSEQ_1:def 7;
hence thesis by
A4,
A14,
A15,
A13;
end;
A16: (k
+ 1)
> (1
+ 1) by
A11,
FINSEQ_2: 16;
then
A17: k
>= (1
+ 1) by
NAT_1: 13;
now
let fr2;
assume
A18: (
len fr2)
= (
len fp1);
then
consider fr be
FinSequence of
INT , m be
Element of
INT such that
A19: fr2
= (fr
^
<*m*>) by
FINSEQ_2: 19;
A20: (k
+ 1)
= ((
len fr)
+ 1) by
A5,
A18,
A19,
FINSEQ_2: 16;
then
consider fr1 such that (
len fr1)
= k and
A21: for b 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;
a
in (
dom fp) implies ((fp
. a)
gcd d)
= 1
proof
A22: ((
len fp)
+ 1)
in (
dom fp1) by
A5,
FINSEQ_5: 6;
A23: (
dom fp)
c= (
dom fp1) & (fp1
. ((
len fp)
+ 1))
= d by
FINSEQ_1: 26,
FINSEQ_1: 42;
assume
A24: a
in (
dom fp);
((
len fp)
+ 1)
> (
len fp) by
NAT_1: 13;
then
A25: ((
len fp)
+ 1)
<> a by
A24,
FINSEQ_3: 25;
(fp1
. a)
= (fp
. a) by
A24,
FINSEQ_1:def 7;
hence thesis by
A4,
A24,
A23,
A25,
A22;
end;
then ((
Product fp)
gcd d)
= 1 by
Th36;
then ((
Product fp)
gcd d)
divides (((fr2
. (k
+ 1))
- ((fp
. 1)
* (fr1
. 1)))
- (fr2
. 1)) by
INT_2: 12;
then
consider m1, n1 such that
A26: (((
Product fp)
* m1)
+ (d
* n1))
= (((fr2
. (k
+ 1))
- ((fp
. 1)
* (fr1
. 1)))
- (fr2
. 1)) by
Th33;
reconsider x = (
- n1) as
Element of
INT by
INT_1:def 2;
deffunc
F(
Nat) = (((
Product (
Del (fp,$1)))
* m1)
+ (fr1
. $1));
consider s2 be
FinSequence such that
A27: (
len s2)
= k & for a be
Nat st a
in (
dom s2) holds (s2
. a)
=
F(a) from
FINSEQ_1:sch 2;
A28: for a be
Nat st a
in (
dom s2) holds (s2
. a)
in
INT
proof
let a be
Nat;
assume
A29: a
in (
dom s2);
reconsider a as
Element of
NAT by
ORDINAL1:def 12;
(s2
. a)
= (((
Product (
Del (fp,a)))
* m1)
+ (fr1
. a)) by
A27,
A29;
hence thesis by
INT_1:def 2;
end;
A30: (
dom s2)
= (
Seg k) by
A27,
FINSEQ_1:def 3;
reconsider s2 as
FinSequence of
INT by
A28,
FINSEQ_2: 12;
take fr3 = (s2
^
<*x*>);
thus (
len fr3)
= (
len fp1) by
A5,
A27,
FINSEQ_2: 16;
let b such that
A31: b
in (
dom fp1);
thus (((fp1
. b)
* (fr3
. b))
+ (fr2
. b))
= (((fp1
. 1)
* (fr3
. 1))
+ (fr2
. 1))
proof
A32: c
in (
Seg k) implies ((fp1
. c)
* (fr3
. c))
= (((
Product fp)
* m1)
+ ((fp
. c)
* (fr1
. c)))
proof
assume
A33: c
in (
Seg k);
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;
for n be
Nat st n
in (
dom fp) holds (fp
. n)
in
REAL by
XREAL_0:def 1;
then
A35: fp is
FinSequence of
REAL by
FINSEQ_2: 12;
A36: c
in (
dom fp) by
A33,
FINSEQ_1:def 3;
then (fp
. c)
= (fp1
. c) by
FINSEQ_1:def 7;
hence ((fp1
. c)
* (fr3
. c))
= ((((fp
. c)
* (
Product (
Del (fp,c))))
* m1)
+ ((fp
. c)
* (fr1
. c))) by
A34
.= (((
Product fp)
* m1)
+ ((fp
. c)
* (fr1
. c))) by
A36,
Lm16,
A35;
end;
A37: 1
<= b by
A31,
FINSEQ_3: 25;
A38: b
<= (k
+ 1) by
A5,
A31,
FINSEQ_3: 25;
now
per cases by
A38,
NAT_1: 8;
suppose
A39: b
<= k;
then 1
<= k by
A37,
XXREAL_0: 2;
then
A40: 1
in (
Seg k);
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 k) by
A37,
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 (((fp1
. 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))
.= (((fp1
. 1)
* (fr3
. 1))
+ (fr2
. 1)) by
A32,
A40,
A41;
end;
suppose
A45: b
= (k
+ 1);
then
A46: (fp1
. b)
= d by
FINSEQ_1: 42;
A47: ((fr2
. b)
- (((fp
. 1)
* (fr1
. 1))
+ (fr2
. 1)))
= ((d
* n1)
+ ((
Product fp)
* m1)) by
A26,
A45;
1
<= k by
A17,
XXREAL_0: 2;
then 1
in (
Seg k);
then (((fp1
. 1)
* (fr3
. 1))
+ (fr2
. 1))
= ((((
Product fp)
* m1)
+ ((fp
. 1)
* (fr1
. 1)))
+ (fr2
. 1)) by
A32
.= ((fr2
. b)
+ (d
* (
- n1))) by
A47;
hence thesis by
A27,
A45,
A46,
FINSEQ_1: 42;
end;
end;
hence thesis;
end;
end;
hence
CC[fp1];
end;
end;
hence
CC[fp1];
end;
hence
TH[fp1];
end;
A48:
TH[(
<*>
NAT )]
proof
take (
<*>
NAT );
thus thesis;
end;
for fp holds
TH[fp] from
FINSEQ_2:sch 2(
A48,
A1);
then ex f be
FinSequence of
NAT st f
= fp & (((
len f)
>= 2 &
RP[f]) implies
CC[f]);
hence thesis;
end;
Lm17: k
divides m iff k
divides
|.m.|
proof
per cases ;
suppose m
>=
0 ;
hence thesis by
ABSVALUE:def 1;
end;
suppose m
<
0 ;
then
|.m.|
= (
- m) by
ABSVALUE:def 1;
hence thesis by
INT_2: 10;
end;
end;
Lm18: ((m
* n)
mod n)
=
0
proof
per cases ;
suppose
A1: 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 ;
end;
suppose n
=
0 ;
hence thesis by
INT_1:def 10;
end;
end;
Lm19: (k
mod n)
= (m
mod n) implies ((k
- m)
mod n)
=
0
proof
assume
A1: (k
mod n)
= (m
mod n);
per cases ;
suppose
A2: 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 thesis by
Lm18;
end;
suppose n
=
0 ;
hence thesis by
INT_1:def 10;
end;
end;
Lm20: n
<>
0 & (m
mod n)
=
0 implies n
divides m
proof
assume n
<>
0 & (m
mod n)
=
0 ;
then m
= (((m
div n)
* n)
+
0 qua
Nat) by
NEWTON: 66
.= ((m
div n)
* n);
hence thesis;
end;
Lm21: (1
< x implies 1
< (
sqrt x) & (
sqrt x)
< x) & (
0
< x & x
< 1 implies
0
< (
sqrt x) & (
sqrt x)
< 1 & x
< (
sqrt x))
proof
hereby
assume
A1: 1
< x;
hence 1
< (
sqrt x) by
SQUARE_1: 18,
SQUARE_1: 27;
then (
sqrt x)
< ((
sqrt x)
^2 ) by
SQUARE_1: 14;
hence (
sqrt x)
< x by
A1,
SQUARE_1:def 2;
end;
hereby
assume that
A2:
0
< x and
A3: x
< 1;
thus
A4:
0
< (
sqrt x) by
A2,
SQUARE_1: 17,
SQUARE_1: 27;
thus (
sqrt x)
< 1 by
A2,
A3,
SQUARE_1: 18,
SQUARE_1: 27;
then ((
sqrt x)
^2 )
< (
sqrt x) by
A4,
SQUARE_1: 13;
hence x
< (
sqrt x) by
A2,
SQUARE_1:def 2;
end;
end;
::$Notion-Name
theorem ::
WSIERP_1:38
a
<>
0 & (a
gcd k)
= 1 implies ex b, e st
0
<> b &
0
<> e & b
<= (
sqrt a) & e
<= (
sqrt a) & (a
divides ((k
* b)
+ e) or a
divides ((k
* b)
- e))
proof
assume that
A1: a
<>
0 and
A2: (a
gcd k)
= 1;
A3: a
>= 1 by
A1,
NAT_1: 14;
per cases by
A3,
XXREAL_0: 1;
suppose
A4: a
= 1;
take b = 1, e = 1;
thus b
<>
0 & e
<>
0 ;
thus b
<= (
sqrt a) & e
<= (
sqrt a) by
A4,
SQUARE_1: 18;
thus a
divides ((k
* b)
+ e) or a
divides ((k
* b)
- e) by
A4,
INT_2: 12;
end;
suppose
A5: a
> 1;
A6: (
sqrt a)
>
0 by
A1,
SQUARE_1: 25;
set d =
[\(
sqrt a)/];
A7: d
<= (
sqrt a) by
INT_1:def 6;
(
sqrt a)
< a by
A5,
Lm21;
then
A8: d
< a by
A7,
XXREAL_0: 2;
set d1 = (d
+ 1);
A9: d
> ((
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 as
Element of
NAT by
A9,
INT_1: 3;
A11: (d
+ 1)
>= 1 by
Lm1;
then
reconsider d1 as
Element of
NAT ;
set e1 = (d1
^2 );
e1
= (d1
* d1);
then
reconsider e1 as
Element of
NAT ;
A12: ((e1
- 1)
/ d1)
= (d1
- (1
/ d1)) by
A11,
XCMPLX_1: 127;
deffunc
F(
Nat) = (1
+ (((k
* (($1
- 1)
div d1))
+ (($1
- 1)
mod d1))
mod a));
consider fs such that
A13: (
len fs)
= e1 & for b be
Nat st b
in (
dom fs) holds (fs
. b)
=
F(b) from
FINSEQ_1:sch 2;
A14: (
rng fs)
c= (
Seg a)
proof
let v be
object;
assume v
in (
rng fs);
then
consider b be
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 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 thesis by
A18;
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 be
object 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, v2 as
Element of
NAT by
A22,
A23;
set x1 = ((v1
- 1)
div d1), x2 = ((v2
- 1)
div d1), x = (x1
- x2);
set y1 = ((v1
- 1)
mod d1), y2 = ((v2
- 1)
mod d1), y = (y1
- y2);
A26: y1
>=
0 by
NEWTON: 64;
(fs
. v1)
= (1
+ (((k
* x1)
+ y1)
mod a)) & (fs
. v2)
= (1
+ (((k
* x2)
+ y2)
mod a)) by
A13,
A22,
A23;
then
A27: ((((k
* x1)
+ y1)
- ((k
* x2)
+ y2))
mod a)
=
0 by
A24,
Lm19,
XCMPLX_1: 2;
then
A28: a
divides (((k
* x1)
+ y1)
- ((k
* x2)
+ y2)) by
A1,
Lm20;
(1
/ d1)
>
0 by
A9,
A10,
XREAL_1: 139;
then
A29: ((e1
- 1)
/ d1)
< d1 by
A12,
Lm1;
A30: x2
=
[\((v2
- 1)
/ d1)/] by
INT_1:def 9;
then
A31: x2
<= ((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 x2
< d1 by
A31,
XXREAL_0: 2;
then
A32: x2
<= d by
Lm9;
set d2 = ((k
* x)
+ y);
A33:
[\
0 /]
=
0 by
INT_1: 25;
A34: x1
=
[\((v1
- 1)
/ d1)/] by
INT_1:def 9;
then
A35: x1
<= ((v1
- 1)
/ d1) by
INT_1:def 6;
1
<= v1 by
A22,
FINSEQ_3: 25;
then (v1
- 1)
>=
0 by
XREAL_1: 48;
then x1
>=
0 by
A34,
A33,
PRE_FF: 9;
then (x2
- x1)
<= d by
A32,
Lm2;
then
A36: (
- (x2
- x1))
>= (
- d) by
XREAL_1: 24;
A37: x
<>
0 or y
<>
0
proof
assume not thesis;
then (v1
- 1)
= ((x2
* d1)
+ y2) by
A11,
NEWTON: 66
.= (v2
- 1) by
A11,
NEWTON: 66;
hence contradiction by
A25;
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 x1
< d1 by
A35,
XXREAL_0: 2;
then
A38: x1
<= d by
Lm9;
A39: (((k
* x1)
+ y1)
- ((k
* x2)
+ y2))
= ((k
* x)
+ y);
y2
< d1 by
A9,
A10,
NEWTON: 65;
then (y2
- y1)
< d1 by
A26,
Lm3;
then (y2
- y1)
<= d by
Lm9;
then
A40: (
- (y2
- y1))
>= (
- d) by
XREAL_1: 24;
take b =
|.x.|, e =
|.y.|;
A41: y2
>=
0 by
NEWTON: 64;
1
<= v2 by
A23,
FINSEQ_3: 25;
then (v2
- 1)
>=
0 by
XREAL_1: 48;
then x2
>=
0 by
A30,
A33,
PRE_FF: 9;
then x
<= d by
A38,
Lm2;
then
A42:
|.x.|
<= d by
A36,
ABSVALUE: 5;
then
A43:
|.x.|
< a by
A8,
XXREAL_0: 2;
A44:
now
assume
A45: y
=
0 ;
then a
divides x by
A1,
A2,
A27,
A39,
Lm20,
Th29;
then a
divides
|.x.| by
Lm17;
then
|.x.|
=
0 by
A43,
NAT_D: 7;
hence contradiction by
A37,
A45,
ABSVALUE: 2;
end;
y1
< d1 by
A9,
A10,
NEWTON: 65;
then y
< d1 by
A41,
Lm3;
then y
<= d by
Lm9;
then
A46:
|.y.|
<= d by
A40,
ABSVALUE: 5;
then
A47:
|.y.|
< a by
A8,
XXREAL_0: 2;
now
assume
A48: x
=
0 ;
then a
divides
|.y.| by
A28,
Lm17;
then
|.y.|
=
0 by
A47,
NAT_D: 7;
hence contradiction by
A37,
A48,
ABSVALUE: 2;
end;
hence b
<>
0 & e
<>
0 by
A44,
ABSVALUE: 2;
thus b
<= (
sqrt a) by
A7,
A42,
XXREAL_0: 2;
thus e
<= (
sqrt a) by
A7,
A46,
XXREAL_0: 2;
A49: b
= x or b
= (
- x) by
ABSVALUE: 1;
A50: e
= y or e
= (
- y) by
ABSVALUE: 1;
(
- d2)
= ((k
* (
- x))
+ (
- y));
hence thesis by
A28,
A49,
A50,
INT_2: 10;
end;
end;
theorem ::
WSIERP_1:39
(
dom (
Del (fs,a)))
c= (
dom fs) by
Lm12;
theorem ::
WSIERP_1:40
(
Del ((
<*v*>
^ fs),1))
= fs & (
Del ((fs
^
<*v*>),((
len fs)
+ 1)))
= fs by
Lm14;
begin
reserve n for
Nat;
theorem ::
WSIERP_1:41
n
>
0 & (k
mod n)
<>
0 implies (
- (k
div n))
= (((
- k)
div n)
+ 1)
proof
assume
A1: n
>
0 ;
assume (k
mod n)
<>
0 ;
then not n qua
Integer
divides k by
A1,
INT_1: 62;
then
A2: not (k
/ n) is
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;
end;
theorem ::
WSIERP_1:42
(k
mod n)
=
0 implies (
- (k
div n))
= ((
- k)
div n)
proof
assume
A1: (k
mod n)
=
0 ;
per cases ;
suppose
A2: n
>
0 ;
then n qua
Integer
divides k by
A1,
INT_1: 62;
then
A3: (k
/ n) is
Integer by
A2,
Th17;
thus (
- (k
div n))
= (
-
[\(k
/ n)/]) by
INT_1:def 9
.=
[\((
- k)
/ n)/] by
A3,
INT_1: 64
.= ((
- k)
div n) by
INT_1:def 9;
end;
suppose
A4: n
=
0 ;
(k
div
0 )
=
0 & ((
- k)
div
0 )
=
0 by
INT_1: 48;
hence thesis by
A4;
end;
end;
reserve i1,i2,i3 for
Integer;
Lm4: i1
divides i2 & i1
divides i3 implies i1
divides (i2
- i3)
proof
assume that
A1: i1
divides i2 and
A2: i1
divides i3;
consider i4 be
Integer such that
A3: i2
= (i1
* i4) by
A1;
consider i5 be
Integer such that
A4: i3
= (i1
* i5) by
A2;
(i2
- i3)
= (i1
* (i4
- i5)) by
A3,
A4;
hence thesis;
end;
theorem ::
WSIERP_1:43
(i1,i2)
are_congruent_mod i3 implies (i1
gcd i3)
= (i2
gcd i3)
proof
set d = (i2
gcd i3);
reconsider d as
Nat;
assume (i1,i2)
are_congruent_mod i3;
then i3
divides (i1
- i2);
then
consider i be
Integer such that
A1: (i1
- i2)
= (i3
* i);
A2: d
= (
|.i2.|
gcd
|.i3.|) by
INT_2: 34;
then d
divides
|.i2.| by
NAT_D:def 5;
then
|.d.|
divides
|.i2.| by
ABSVALUE:def 1;
then
A3: d
divides i2 by
INT_2: 16;
A4: i2
= (i1
- (i3
* i)) by
A1;
A5: for n be
Nat st n
divides
|.i1.| & n
divides
|.i3.| holds n
divides d
proof
let n be
Nat;
assume that
A6: n
divides
|.i1.| and
A7: n
divides
|.i3.|;
|.n.|
divides
|.i3.| by
A7,
ABSVALUE:def 1;
then n
divides i3 by
INT_2: 16;
then
A8: n
divides (i3
* i) by
INT_2: 2;
|.n.|
divides
|.i1.| by
A6,
ABSVALUE:def 1;
then n
divides i1 by
INT_2: 16;
then n
divides i2 by
A4,
A8,
Lm4;
then
|.n.|
divides
|.i2.| by
INT_2: 16;
then n
divides
|.i2.| by
ABSVALUE:def 1;
hence thesis by
A2,
A7,
NAT_D:def 5;
end;
A9: d
divides
|.i3.| by
A2,
NAT_D:def 5;
then
|.d.|
divides
|.i3.| by
ABSVALUE:def 1;
then d
divides i3 by
INT_2: 16;
then
A10: d
divides (i3
* i) by
INT_2: 2;
i1
= ((i3
* i)
+ i2) by
A1;
then
|.d.|
= d & d
divides i1 by
A3,
A10,
ABSVALUE:def 1,
Th4;
then d
divides
|.i1.| by
INT_2: 16;
then (
|.i1.|
gcd
|.i3.|)
= d by
A9,
A5,
NAT_D:def 5;
hence thesis by
INT_2: 34;
end;