:: Parity as a Property of Integers
:: by Rafa{\l} Ziobro
::
:: Received June 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ABIAN, NUMBERS, NAT_1, INT_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1,
INT_2, COMPLEX1, RELAT_1, PYTHTRIP, SQUARE_1, REAL_1, XCMPLX_0, ORDINAL1,
NEWTON, POWER, NEWTON05, SUBSET_1, NAT_3, ZFMISC_1;
notations TARSKI, XBOOLE_0, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0,
CARD_1, RELAT_1, FUNCT_1, POWER, INT_1, INT_2, NAT_1, NEWTON, ABIAN,
ABSVALUE, RVSUM_1, FINSEQ_1, FINSEQ_3, TREES_4, IRRAT_1, COMPLEX1,
NEWTON03, PYTHTRIP, SQUARE_1, SUBSET_1, PARTFUN1, ZFMISC_1, NAT_D;
constructors SQUARE_1, NAT_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1, EULER_1,
SEQ_1, RECDEF_1, CLASSES1, BINOP_2, RELSET_1, NUMBERS, COMPLEX1, POWER,
INT_1, PREPOWER, ABIAN, NEWTON02, NEWTON03, PYTHTRIP, ORDINAL1, PEPIN,
ABSVALUE, NAT_3, MOEBIUS1, XCMPLX_0, REAL_1;
registrations ABIAN, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
XCMPLX_0, WSIERP_1, NAT_6, PYTHTRIP, NEWTON01, NEWTON02, NEWTON03,
COMPLEX1, ABSVALUE, REAL_3, FOMODEL0, NAT_5;
requirements REAL, NUMERALS, SUBSET, ARITHM;
expansions INT_1, INT_2, NEWTON03, ABIAN, ORDINAL1;
theorems INT_2, NAT_1, ABSVALUE, INT_1, PREPOWER, NEWTON, XCMPLX_1, GR_CY_3,
XREAL_1, XXREAL_0, NAT_D, WSIERP_1, COMPLEX1, POWER, INT_4, INT_6,
TAYLOR_2, PEPIN, INT_5, PYTHTRIP, ABIAN, NEWTON02, NEWTON03, PRE_FF,
NAT_2, SQUARE_1, NEWTON04;
schemes NAT_1;
begin
registration
let a be Integer;
cluster a mod a -> zero;
coherence by INT_1:50;
cluster a mod 2 -> natural;
coherence;
end;
registration
let a,b be Integer;
reduce (a*b) gcd |.a.| to |.a.|;
reducibility
proof
|.a.| in NAT by INT_1:3; then
reconsider k = |.a.| as Nat;
(a*b) gcd |.a.| = |.a*b.| gcd |.|.a.|.| by INT_2:34
.= (0 + |.a.|*|.b.|) gcd |.a.| by COMPLEX1:65
.= 0 gcd k by NEWTON02:5;
hence thesis;
end;
end;
registration
let a be odd Nat;
cluster a mod 2 -> non zero;
coherence
proof
not 2 divides a;
hence thesis by INT_1:62;
end;
end;
registration
let a be even Integer;
cluster a mod 2 -> zero;
coherence
proof
2 divides a by ABIAN:def 1;
hence thesis;
end;
reduce (a+1) mod 2 to 1;
reducibility
proof
reconsider b = a/2 as Integer;
(2*b+1) mod 2 = 1 mod 2 by NAT_D:61;
hence thesis by NAT_D:14;
end;
end;
registration
let a,b be Real;
cluster max (a,b) - min (a,b) -> non negative;
coherence
proof
max (a,b) >= a & a >= min (a,b) by XXREAL_0:17,XXREAL_0:25; then
max (a,b) >= min (a,b) by XXREAL_0:2; then
max (a,b) - min (a,b) >= max (a,b) - max (a,b) by XREAL_1:10;
hence thesis;
end;
end;
registration
let a be Nat,b be non zero Nat;
reduce a mod (a+b) to a;
reducibility
proof
a+b > a+0 by XREAL_1:6;
hence thesis by NAT_D:63;
end;
cluster a div (a+b) -> zero;
coherence
proof
a+b > a+0 by XREAL_1:6;
hence thesis by NAT_D:27;
end;
end;
registration
let a be non trivial Nat;
cluster a |-count 1 -> zero;
coherence
proof
not a divides 1 by NAT_D:7,NEWTON03:def 1;
hence thesis by NEWTON03:77;
end;
cluster a |-count (-1) -> zero;
coherence
proof
a <> 1 by NAT_2:def 1; then
not a divides (-1) by INT_2:13;
hence thesis by NEWTON03:77;
end;
end;
registration
let a be non trivial Nat, b be Nat;
reduce a |-count a|^b to b;
reducibility
proof
a|-count (a|^b*1) = b + (a|-count 1) by NEWTON03:105;
hence thesis;
end;
reduce a |-count -a|^b to b;
reducibility
proof
a|-count (a|^b*(-1)) = b + (a|-count (-1)) by NEWTON03:105;
hence thesis;
end;
end;
theorem Th1:
for a,b be Integer holds a divides b implies b/a is integer
proof
let a,b be Integer;
a = 0 or thesis by WSIERP_1:17;
hence thesis;
end;
registration
cluster non zero even for Integer;
existence
proof
take 2;
thus thesis;
end;
cluster non zero trivial -> odd for Nat;
coherence
proof
2*0+1 is odd;
hence thesis by NAT_2:def 1;
end;
end;
registration
cluster non trivial odd for Nat;
existence
proof
3 is non trivial & 2*1+1 is odd;
hence thesis;
end;
end;
registration
let a be Integer, b be even Integer;
cluster a lcm b -> even;
coherence
proof
2 divides b & b divides a lcm b by INT_2:def 1,ABIAN:def 1;
hence thesis;
end;
end;
registration
let a,b be odd Integer;
cluster a lcm b -> odd;
coherence
proof
a divides a*b & b divides a*b; then
(a lcm b) divides a*b by INT_2:19;
hence thesis;
end;
end;
:: min, max, absolute value
registration
let a,b be Integer;
cluster (a+b)/(a gcd b) -> integer;
coherence
proof
(a gcd b) divides a & (a gcd b) divides b by INT_2:def 2;
hence thesis by Th1,WSIERP_1:4;
end;
cluster (a-b)/(a gcd b) -> integer;
coherence
proof
reconsider c = -b as Integer;
(a+c)/(a gcd c) is Integer;
hence thesis by NEWTON02:1;
end;
end;
theorem ABS:
for a,b be Real holds |.a + b.| = |.a.| + |.b.| or |.a - b.| = |.a.| + |. b.|
proof
let a,b be Real;
per cases;
suppose (a >= 0 & b >= 0) or (a <= 0 & b <= 0); then
a*b >= 0;
hence thesis by ABSVALUE:11;
end;
suppose (a > 0 & b < 0) or (a < 0 & b > 0); then
a*(-b) >= 0; then
|.a + - b.| = |.a.|+ |.-b.| by ABSVALUE:11;
hence thesis by COMPLEX1:52;
end;
end;
theorem ABS1:
for a,b be Real holds
|.|.a.| - |.b.|.| = |.a + b.| or |.|.a.| - |. b.|.| = |.a - b.|
proof
let a,b be Real;
per cases;
suppose
A1: a >= 0;
per cases;
suppose b >= 0; then
|.a.| = a & |.b.| = b by A1,ABSVALUE:def 1;
hence thesis;
end;
suppose b < 0; then
|.a.| = a & |.b.| = -b by A1,ABSVALUE:def 1;
hence thesis;
end;
end;
suppose
A1: a < 0;
per cases;
suppose b >= 0; then
|.a.| = -a & |.b.| = b by A1,ABSVALUE:def 1; then
|.|.a.| - |.b.|.| = |.-(a + b).|;
hence thesis by COMPLEX1:52;
end;
suppose b < 0; then
|.a.| = -a & |.b.| = -b by A1,ABSVALUE:def 1; then
|.|.a.| - |.b.|.| =|.-(a - b).|;
hence thesis by COMPLEX1:52;
end;
end;
end;
theorem LmABS:
for a,b be Real holds
|.|.a.| - |.b.|.| = |.a + b.| iff |.a - b.| = |.a.| + |.b.|
proof
let a,b be Real;
per cases;
suppose
B1: a >= 0;
per cases;
suppose b >= 0; then
|.a.| = a & |.b.| = b by B1,ABSVALUE:def 1;
hence thesis;
end;
suppose b < 0; then
|.a.| = a & |.b.| = -b by B1,ABSVALUE:def 1;
hence thesis;
end;
end;
suppose
B1: a < 0;
per cases;
suppose b >= 0; then
C1: |.a.| = -a & |.b.| = b by B1,ABSVALUE:def 1; then
C2: |.|.a.| - |.b.|.| = |.-(a + b).|;
|.a - b.| = |.-(|.a.|+|.b.|).| by C1
.= |.|.a.| + |.b.|.| by COMPLEX1:52;
hence thesis by C2,COMPLEX1:52;
end;
suppose b < 0; then
C1: |.a.| = -a & |.b.| = -b by B1,ABSVALUE:def 1; then
C2: |.|.a.| - |.b.|.| =|.-(a - b).|;
|.a + b.| = |.-(|.a.|+|.b.|).| by C1
.= |.|.a.| + |.b.|.| by COMPLEX1:52;
hence thesis by COMPLEX1:52,C2;
end;
end;
end;
theorem LABS:
for a,b be Real holds
|.a + b.| = |.a.| + |.b.| iff |.a - b.| = |.|.a.| - |.b.|.|
proof
let a,b be Real;
reconsider c = -b as Real;
|.|.a.| - |.c.|.| = |.a + c.| iff |.a - c.| = |.a.| + |.c.| by LmABS;
hence thesis by COMPLEX1:52;
end;
theorem
for a,b be non zero Real holds
(|.|.a.| - |.b.|.| = |.a + b.| & |.a - b.| = |.a.| + |. b.|)
iff not (|.|.a.| - |.b.|.| = |.a - b.| & |.a + b.| = |.a.| + |. b.|)
proof
let a,b be non zero Real;
A1: |.|.a.| - |.b.|.| = |.a + b.| iff |.a - b.| = |.a.| + |.b.| by LmABS;
A2: |.|.a.| - |.b.|.| = |.a - b.| iff |.a + b.| = |.a.| + |.b.|
proof
reconsider c = -b as non zero Real;
|.|.a.| - |.c.|.| = |.a + c.| iff |.a - c.| = |.a.| + |.c.| by LmABS;
hence thesis by COMPLEX1:52;
end;
|.a + b.| = |.a.| + |.b.| iff not |.a - b.| = |.a.| + |.b.|
proof
(|.a.| - |.b.|) + 0 < (|.a.| - |.b.|) + 2*|.b.| &
(|.b.| - |.a.|) + 0 < (|.b.| - |.a.|) + 2*|.a.|
by XREAL_1:6; then
B0: |.a.| + |.b.| > |.a.| - |.b.| & |.a.| + |.b.| > -(|.a.| - |.b.|);
per cases by ABS;
suppose |.a + b.| = |.a.| + |.b.|;
hence thesis by A2,B0,ABSVALUE:1;
end;
suppose |.a - b.| = |.a.| + |. b.|;
hence thesis by A1,B0,ABSVALUE:1;
end;
end;
hence thesis by LmABS,A2;
end;
theorem
for a,b be positive Real, n be Nat holds
min (a|^n,b|^n) = (min (a,b))|^n
proof
let a,b be positive Real, n be Nat;
per cases;
suppose
A1: a >= b; then
min (a,b) = b by XXREAL_0:def 9;
hence thesis by A1,NEWTON02:41,XXREAL_0:def 9;
end;
suppose
A1: b >= a; then
min (a,b) = a by XXREAL_0:def 9;
hence thesis by A1,NEWTON02:41,XXREAL_0:def 9;
end;
end;
theorem
for a,b be positive Real, n be Nat holds
max (a|^n,b|^n) = (max (a,b))|^n
proof
let a,b be positive Real, n be Nat;
per cases;
suppose
A1: a >= b; then
max (a,b) = a by XXREAL_0:def 10;
hence thesis by A1,NEWTON02:41,XXREAL_0:def 10;
end;
suppose
A1: b >= a; then
max (a,b) = b by XXREAL_0:def 10;
hence thesis by A1,NEWTON02:41,XXREAL_0:def 10;
end;
end;
theorem MIN1:
for a be non zero Nat,m,n be Nat holds
min (a|^n,a|^m) = a|^(min (n,m))
proof
let a be non zero Nat,m,n be Nat;
per cases;
suppose
A1: m >= n; then
A2: min(m,n) = n by XXREAL_0:def 9;
a|^n divides a|^m by A1,NEWTON:89; then
a|^m >= a|^n by NAT_D:7;
hence thesis by A2,XXREAL_0:def 9;
end;
suppose
A1: n >= m; then
A2: min(m,n) = m by XXREAL_0:def 9;
a|^m divides a|^n by A1,NEWTON:89; then
a|^n >= a|^m by NAT_D:7;
hence thesis by A2,XXREAL_0:def 9;
end;
end;
theorem
for a be non zero Nat,m,n be Nat holds
max (a|^n,a|^m) = a|^(max (n,m))
proof
let a be non zero Nat,m,n be Nat;
per cases;
suppose
A1: m <= n; then
A2: max(m,n) = n by XXREAL_0:def 10;
a|^m divides a|^n by A1,NEWTON:89; then
a|^m <= a|^n by NAT_D:7;
hence thesis by A2,XXREAL_0:def 10;
end;
suppose
A1: m >= n; then
A2: max(m,n) = m by XXREAL_0:def 10;
a|^n divides a|^m by A1,NEWTON:89; then
a|^m >= a|^n by NAT_D:7;
hence thesis by A2,XXREAL_0:def 10;
end;
end;
:: modular arithmetic
theorem AMB:
for a,b be Nat holds a mod b <= a
proof
let a,b be Nat;
per cases;
suppose b = 0;
hence thesis;
end;
suppose b <> 0; then
reconsider b as non zero Nat;
(a div b)*b + (a mod b) >= 0 + (a mod b) by XREAL_1:6;
hence thesis by NAT_D:2;
end;
end;
theorem
for a be Nat, b,c be non zero Nat holds
(a mod c) + (b mod c) >= (a+b) mod c
proof
let a be Nat ,b,c be non zero Nat;
((a mod c)+(b mod c)) mod c <= (a mod c)+(b mod c) by AMB;
hence thesis by NAT_D:66;
end;
theorem
for a be Nat, b,c be non zero Nat holds
(a mod c) * (b mod c) >= (a*b) mod c
proof
let a be Nat ,b,c be non zero Nat;
((a mod c)*(b mod c)) mod c <= (a mod c)*(b mod c) by AMB;
hence thesis by NAT_D:67;
end;
theorem
for a be Nat, b,n be non zero Nat holds
(a mod b)|^n >= a|^n mod b
proof
let a be Nat, b,n be non zero Nat;
reconsider m = n-1 as Nat;
A1: (a mod b)*(a mod b)|^m = (a mod b)|^(m+1) by NEWTON:6;
((a mod b)*(a mod b)|^m) mod b <= (a mod b)*(a mod b)|^m by AMB;
hence thesis by A1,GR_CY_3:30;
end;
theorem
for a be Nat, b,n be non zero Nat holds
a mod b = 1 implies a|^n mod b = 1
proof
let a be Nat, b,n be non zero Nat;
assume a mod b = 1; then
1 = ((a mod b)|^n) mod b;
hence thesis by GR_CY_3:30;
end;
theorem for a,b be Nat, c be non zero Nat holds
(a mod c)*(b mod c) < c iff (a*b) mod c = (a mod c)*(b mod c)
proof
let a,b be Nat, c be non zero Nat;
(a mod c)*(b mod c) < c implies (a*b) mod c = (a mod c)*(b mod c)
proof
assume (a mod c)*(b mod c) < c; then
((a mod c)*(b mod c)) mod c = (a mod c)*(b mod c) by NAT_D:24;
hence thesis by NAT_D:67;
end;
hence thesis by INT_1:58;
end;
theorem for a,b,c be Nat holds
(a mod c)*(b mod c) = c implies a*b mod c = 0
proof
let a,b,c be Nat;
assume (a mod c)*(b mod c) = c; then
c mod c = ((a mod c)*(b mod c)) mod c;
hence thesis by NAT_D:67;
end;
theorem
for a,b be Nat,c be non zero Nat holds
(a mod c)*(b mod c) >= c implies a mod c > 1
proof
let a,b be Nat,c be non zero Nat;
assume
A1: (a mod c)*(b mod c) >= c;
a mod c > 1 or (a mod c)*(b mod c) <= 1*(b mod c) by XREAL_1:64; then
(a mod c) > 1 or (b mod c) >= c by A1,XXREAL_0:2;
hence thesis by INT_1:58;
end;
theorem MAB:
for a,b be Integer, c be non zero Nat holds
((a+b) mod c = b mod c implies a mod c = 0) &
((a+b) mod c <> b mod c implies a mod c > 0)
proof
let a,b be Integer, c be non zero Nat;
L1: (a+b) mod c = b mod c implies a mod c = 0
proof
assume (a+b) mod c = b mod c; then
0 = ((a+b) mod c - (b mod c)) mod c
.= (a+b - b) mod c by INT_6:7;
hence thesis;
end;
(a+b) mod c = ((a mod c) + (b mod c)) mod c by NAT_D:66; then
a mod c = 0 implies (a+b) mod c = b mod c;
hence thesis by L1;
end;
theorem
for a be Nat, b,c be non zero Nat holds
(a*b) mod c = b implies (a*(b gcd c)) mod c = b gcd c
proof
let a be Nat, b,c be non zero Nat;
assume
A1: (a*b) mod c = b;
reconsider a as non zero Nat by A1;
consider k,l be Integer such that
A4: b = (b gcd c)*k & c = (b gcd c)*l & k,l are_coprime by INT_2:23;
k >= 0 by A4; then
k in NAT by INT_1:3; then
reconsider k as non zero Nat by A4;
l >= 0 by A4; then
l in NAT by INT_1:3; then
reconsider l as non zero Nat by A4;
A5: (a*k) mod l = ((b gcd c)*((a*k) mod l))/(b gcd c) by XCMPLX_1:89
.= ((a*k*(b gcd c)) mod (l*(b gcd c)))/(b gcd c) by INT_4:20
.= k by A1,A4,XCMPLX_1:89; then
A6: k mod l = k;
l > k & k >= 1 by A5,INT_1:58,NAT_1:14; then
l > 1 by XXREAL_0:2; then
1 = a mod l by A4,A5,A6,PEPIN:11; then
(b gcd c)*1 = (a*(b gcd c)) mod c by A4,INT_4:20;
hence thesis;
end;
theorem for a,b be Integer holds a,b are_congruent_mod a gcd b
proof
let a,b be Integer;
(a gcd b) divides a & (a gcd b) divides b by INT_2:def 2;
hence thesis by INT_5:1;
end;
theorem N0319:
for k,l be odd square Integer holds (k-l) mod 8 = 0
proof
let k,l be odd square Integer;
reconsider k,l as odd Element of NAT by INT_1:3;
8 divides k - l by NEWTON03:19;
hence thesis;
end;
theorem
for k,l be odd square Integer holds (k+l) mod 8 = 2
proof
let k,l be odd square Integer;
1|^2 is square & 2*0+1 is odd & 1 is integer; then
A1: (k - 1) mod 8 = 0 & (l - 1) mod 8 = 0 by N0319;
(k+l) mod 8 = ((k-1)+((l-1)+2)) mod 8
.= (((k-1) mod 8) + (((l-1)+2) mod 8)) mod 8 by NAT_D:66
.= (((l-1) mod 8) + (2 mod 8)) mod 8 by NAT_D:66,A1
.= 2 mod (2+6) by A1
.= 2;
hence thesis;
end;
:: Two definitions of parity, denoted by small and capital letters are introduced.
:: Both are defined according to a typical "even/odd" distinction, not the
:: property itself (therefore 1 has non zero "parity"/"Parity").
:: "Parity" denoted by a capital letter results in the largest power of 2
:: which divides certain number (or zero if no such number could be given)
:: At the same time "parity" denoted by a small letter refers only to the
:: divisibility by 2 (therefore 2 has zero "parity", which could be misleading).
:: Although "oddness" could be used here instead of "parity", it would not
:: be compatible with "Parity" (moreover "even oddness" is also confusing),
definition
let a be Integer;
func parity a -> trivial Nat equals
a mod 2;
coherence
proof
a mod 2 = 0 or a mod 2 = 1 by NAT_1:23,INT_1:58;
hence thesis by NAT_2:def 1;
end;
end;
definition
let a be Integer;
redefine func parity a -> trivial Nat equals :: redefines parity (NEWTON05, definition)
2 - (a gcd 2);
coherence;
compatibility
proof
per cases;
suppose A1: a is odd;
then a mod 2 <> 0 by INT_1:62;
hence thesis by A1,PRE_FF:6;
end;
suppose a is even;
hence thesis by INT_1:62;
end;
end;
end;
registration
let a be even Integer;
cluster parity a -> zero;
coherence;
end;
registration
let a be odd Integer;
cluster parity a -> non zero;
coherence
proof a is odd;
hence thesis;
end;
end;
definition
let a be Integer;
func Parity a -> Nat equals
:Def1:
0 if a = 0 otherwise 2|^(2|-count a);
coherence;
consistency;
end;
registration
let a be non zero Integer;
cluster Parity a -> non zero;
coherence
proof
Parity a = 2|^(2|-count a) by Def1;
hence thesis;
end;
end;
registration
let a be non zero even Integer;
cluster Parity a -> non trivial;
coherence
proof
2 is non trivial & 2 divides a by ABIAN:def 1; then
2|-count a >= 1 by NAT_1:14,NEWTON03:89; then
2|^(2|-count a) >= 2|^1 & 1+1 > 1+0 by PREPOWER:12; then
2|^(2|-count a) > 1 by XXREAL_0:2;
hence thesis by Def1;
end;
cluster Parity a -> even;
coherence
proof
2 is non trivial & 2 divides a by ABIAN:def 1; then
2|-count a >= 1 by NAT_1:14,NEWTON03:89; then
2|^1 divides 2|^(2|-count a) by NEWTON:89;
hence thesis by Def1;
end;
end;
registration
let a be even Integer;
cluster Parity a -> even;
coherence
proof
(a = 0 or a is non zero even Integer) & Parity 0 is even by Def1;
hence thesis;
end;
cluster Parity (a+1) -> odd;
coherence
proof
2|-count (a+1) = 0; then
Parity (a+1) = 1*2|^0 by Def1;
hence thesis;
end;
end;
registration
let a be odd Integer;
cluster Parity a -> trivial;
coherence
proof
2|-count a = 0; then
Parity a = 1*2|^0 by Def1;
hence thesis;
end;
end;
reconsider dwa = 2 as prime Nat by INT_2:28;
registration
let n be Nat;
reduce Parity (2|^n) to 2|^n;
reducibility
proof
Parity (dwa|^n) = dwa|^(dwa|-count (dwa|^n)) by Def1;
hence thesis;
end;
end;
registration
reduce Parity 1 to 1;
reducibility
proof
Parity (2*0 + 1) = 1 by NAT_2:def 1;
hence thesis;
end;
reduce Parity 2 to 2;
reducibility
proof
Parity 2|^1 = 2|^1;
hence thesis;
end;
end;
theorem Th3:
for a be Integer holds Parity a divides a
proof
let a be Integer;
per cases;
suppose a = 0;
hence thesis by Def1;
end;
suppose
A1: a <> 0;
|.2.| > 1; then
2|^(2|-count a) divides a by A1,NEWTON03:def 7;
hence thesis by A1,Def1;
end;
end;
theorem ILP: for a,b be Integer holds Parity (a*b) = (Parity a)*(Parity b)
proof
let a,b be Integer;
per cases;
suppose a = 0 or b = 0; then
(Parity a = 0 or Parity b = 0) & Parity (a*b) = 0 by Def1;
hence thesis;
end;
suppose
B1: a <> 0 & b <> 0; then
B2: Parity b = 2|^(2|-count b) & Parity a = 2|^(2|-count a) by Def1;
Parity (a*b) = 2|^(2|-count (a*b)) by B1,Def1
.= 2|^((2|-count a) + (2|-count b)) by B1,NEWTON03:57,INT_2:28
.= (2|^(2|-count a)) * (2|^(2|-count b)) by NEWTON:8;
hence thesis by B2;
end;
end;
definition
let a be Integer;
func Oddity a -> Integer equals
a/Parity a;
coherence by Th1,Th3;
end;
theorem ADI:
for a be non zero Integer holds a/(Parity a) = a div (Parity a)
proof
let a be non zero Integer;
(Parity a) > 0 & Parity a divides a by Th3; then
A1: a mod (Parity a) = 0;
a/(Parity a) = ((a div (Parity a))*(Parity a) +
(a mod (Parity a)))/(Parity a) by INT_1:59
.= ((a div (Parity a))*(Parity a))/(Parity a) by A1;
hence thesis by XCMPLX_1:89;
end;
registration
let a be Integer;
reduce (Parity a)*(Oddity a) to a;
reducibility
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0;
hence thesis by XCMPLX_1:87;
end;
end;
reduce Parity (Parity a) to Parity a;
reducibility
proof
per cases;
suppose a is zero;
hence thesis by Def1;
end;
suppose not a is zero; then
reconsider a as non zero Integer;
2|^(2|-count a) = Parity (2|^(2|-count a))
.= Parity (Parity a) by Def1;
hence thesis by Def1;
end;
end;
reduce Oddity (Oddity a) to Oddity a;
reducibility
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose a <> 0; then
reconsider a as non zero Integer;
(Oddity a)*(Parity a)
= (Parity (Oddity a)*(Oddity (Oddity a)))*(Parity (Parity a))
.= (Oddity (Oddity a))*((Parity (Oddity a))*((Parity (Parity a))))
.= Oddity (Oddity a) * Parity ((Oddity a)*(Parity a)) by ILP
.= Oddity (Oddity a)* (Parity a);
hence thesis by XCMPLX_1:5;
end;
end;
cluster Parity (Oddity a) -> trivial;
coherence
proof
per cases;
suppose a is zero;
hence thesis by Def1;
end;
suppose a is non zero; then
reconsider a as non zero Integer;
Oddity (Oddity a) = Oddity a &
(Oddity(Oddity a))*(Parity(Oddity a)) = Oddity a;
hence thesis by XCMPLX_1:7;
end;
end;
cluster a + Parity a -> even;
coherence
proof
a is odd or a is even;
hence thesis;
end;
cluster a - Parity a -> even;
coherence
proof
a is odd or a is even;
hence thesis;
end;
cluster a/(Parity a) -> integer;
coherence by Th1,Th3;
end;
theorem OPA:
for a be non zero Integer holds Oddity (Parity a) = 1
proof
let a be non zero Integer;
Parity (Parity a) = Parity a &
(Parity(Parity a))*(Oddity(Parity a)) = Parity a;
hence thesis by XCMPLX_1:7;
end;
theorem ILO:
for a,b be Integer holds Oddity (a*b) = (Oddity a)*(Oddity b)
proof
let a,b be Integer;
per cases;
suppose a = 0 or b = 0;
hence thesis;
end;
suppose a <> 0 & b <> 0; then
reconsider a,b as non zero Integer;
(Oddity a)*(Oddity b)*Parity (a*b)
= (Oddity a)*(Oddity b)*((Parity a)*(Parity b)) by ILP
.= ((Oddity a)*(Parity a))*((Oddity b)*(Parity b))
.= Oddity (a*b)*Parity (a*b);
hence thesis by XCMPLX_1:5;
end;
end;
registration
let a be non zero Integer;
cluster a/(Parity a) -> odd;
coherence
proof
Parity a = 2|^(2 |-count a) by Def1;
hence thesis;
end;
cluster a div (Parity a) -> odd;
coherence
proof
a/(Parity a) is odd;
hence thesis by ADI;
end;
end;
theorem Th4:
for a,b be Integer holds
Parity a divides Parity b or Parity b divides Parity a
proof
let a,b be Integer;
per cases;
suppose
a = 0 or b = 0; then
Parity a = 0 or Parity b = 0 by Def1;
hence thesis by INT_2:12;
end;
suppose
B1: a <> 0 & b <> 0; then
reconsider a as non zero Integer;
reconsider b as non zero Integer by B1;
B2: Parity a = 2|^(2|-count a) & Parity b = 2|^(2|-count b) by Def1;
per cases;
suppose 2|-count a >= 2|-count b;
hence thesis by B2,NEWTON:89;
end;
suppose 2|-count b >= 2|-count a;
hence thesis by B2,NEWTON:89;
end;
end;
end;
theorem PEPIN31: for a,b be non zero Integer holds
Parity a divides Parity b iff Parity b >= Parity a
proof
let a,b be non zero Integer;
A1: Parity a = 2|^(2|-count a) & Parity b = 2|^(2|-count b) by Def1;
Parity b >= Parity a implies Parity a divides Parity b
proof
assume Parity b >= Parity a; then
2|-count b >= 2|-count a by A1,PEPIN:66;
hence thesis by A1,NEWTON:89;
end;
hence thesis by NAT_D:7;
end;
theorem P2P:
for a,b be non zero Integer st Parity a > Parity b holds
2*(Parity b) divides Parity a
proof
let a,b be non zero Integer such that
A1: Parity a > Parity b;
A2: Parity a = 2|^(2|-count a) & Parity b = 2|^(2|-count b) by Def1; then
2|-count a > 2|-count b by A1,PREPOWER:93; then
2|-count a >= (2|-count b) + 1 by NAT_1:13; then
2|^((2|-count b) + 1) divides 2|^(2|-count a) by NEWTON:89;
hence thesis by A2,NEWTON:6;
end;
theorem PM:
for a be Integer holds Parity a = Parity (-a)
proof
let a be Integer;
per cases;
suppose a <> 0; then
reconsider a as non zero Integer;
B1: 2 is non trivial Nat by NAT_2:def 1;
Parity (-a) = 2|^(2|-count (a*(-1))) by Def1
.= 2|^((2|-count a)+(2|-count (-1))) by NEWTON03:57,INT_2:28
.= 2|^((2|-count a)+0) by B1;
hence thesis by Def1;
end;
suppose a = 0;
hence thesis;
end;
end;
theorem PMP:
for a be Integer holds Parity a = Parity |.a.|
proof
let a be Integer;
per cases by ABSVALUE:1;
suppose |.a.| = a;
hence thesis;
end;
suppose |.a.| = -a;
hence thesis by PM;
end;
end;
theorem
for a be Integer holds Parity a <= |.a.|
proof
let a be Integer;
per cases;
suppose a = 0;
hence thesis by Def1;
end;
suppose
a <> 0; then
Parity |.a.| <= |.a.| by Th3,NAT_D:7;
hence thesis by PMP;
end;
end;
theorem PYTHTRIP10:
for a,b be Integer st a,b are_coprime holds a is odd or b is odd
proof
let a,b be Integer such that
A1: a,b are_coprime;
assume not thesis; then
a gcd b is even;
hence contradiction by A1;
end;
theorem MPO:
for a,b be odd Integer st |.a.| <> |.b.| holds
min (Parity(a-b),Parity(a+b)) = 2
proof
let a,b be odd Integer such that
A1: |.a.| <> |.b.|;
A0: |.a.| in NAT & |.b.| in NAT by INT_1:3; then
reconsider k = |.a.| as odd Nat;
reconsider l = |.b.| as odd Nat by A0;
k-l <> 0 & k+l <> 0 by A1; then
A2: Parity(k-l) = 2|^(2|-count (k-l)) &
Parity(k+l) = 2|^(2|-count (k+l)) by Def1;
A3: Parity (k-l) = Parity |.k-l.| &
Parity (a+b) = Parity |.a+b.| &
Parity (a-b) = Parity |.a-b.| by PMP;
min (2|-count (k-l), 2|-count (k+l)) = 1 by A1,NEWTON03:82; then
A4: min (Parity (k-l),Parity (k+l)) = 2|^1 by A2,MIN1;
per cases by ABS;
suppose
|.a + b.| = |.a.| + |.b.|; then
|.a -(-b).| = |.a.| + |.-b.| by COMPLEX1:52; then
|.a -(-b).| = (|.a.|+|.-b.|) & |.a + (-b).| = |.|.a.|-|.-b.|.|
by LmABS; then
Parity |.a + b.| = Parity(|.a.|+|.b.|) &
Parity|.a - b.| = Parity|.|.a.|-|.b.|.| by COMPLEX1:52;
hence thesis by A4,A3;
end;
suppose
|.a - b.| = |.a.| + |. b.|;
hence thesis by A4,A3,LmABS;
end;
end;
theorem ODP:
for a,b be odd Integer holds min (Parity(a-b),Parity(a+b)) <= 2
proof
let a,b be odd Integer;
A0: |.a.| in NAT & |.b.| in NAT by INT_1:3; then
reconsider k = |.a.| as odd Nat;
reconsider l = |.b.| as odd Nat by A0;
per cases;
suppose
k = l; then
Parity |.|.a.| - |.b.|.| = 0 by Def1; then
Parity |.a-b.| = 0 or Parity |.a+b.| = 0 by ABS1; then
Parity (a-b) = 0 or Parity (a+b) = 0 by PMP;
hence thesis by XXREAL_0:def 9;
end;
suppose
k <> l;
hence thesis by MPO;
end;
end;
theorem
for a,b be Integer st a,b are_coprime holds min
(Parity(a-b),Parity(a+b)) <= 2
proof
let a,b be Integer such that
A1: a,b are_coprime;
per cases;
suppose
B1: a is even; then
b is odd by A1,PYTHTRIP10; then
Parity (a + b) = 1 & Parity (a - b) = 1 by B1,NAT_2:def 1;
hence thesis;
end;
suppose
B1: b is even; then
a is odd by A1,PYTHTRIP10; then
Parity (a + b) = 1 & Parity (a - b) = 1 by B1,NAT_2:def 1;
hence thesis;
end;
suppose a is odd & b is odd;
hence thesis by ODP;
end;
end;
theorem CCM:
for a,b be non zero Integer, c be non trivial Nat holds
c|-count (a gcd b) = min (c|-count a, c|-count b)
proof
let a,b be non zero Integer, c be non trivial Nat;
A1: |.c.| > 1 by NEWTON03:def 1; then
A3: c|^(c|-count a) divides a &
not c|^((c|-count a) +1) divides a by NEWTON03:def 7;
A4: c|^(c|-count b) divides b &
not c|^((c|-count b) +1) divides b by A1,NEWTON03:def 7;
A5: |.c|^((c|-count b)+1).| in NAT & |.a.| in NAT &
|.b.| in NAT by INT_1:3;
per cases;
suppose
B1: c|-count a >= c|-count b; then
B2: min(c|-count a,c|-count b ) = c|-count b by XXREAL_0:def 9;
c|^(c|-count b) divides c|^(c|-count a) by B1,NEWTON:89; then
c|^(c|-count b) divides a by A3,INT_2:9; then
B3: c|^(c|-count b) divides (a gcd b) by A4,INT_2:def 2;
not |.c|^((c|-count b)+1).| divides |.b.| by A4,INT_2:16; then
not |.c|^((c|-count b)+1).| divides (|.a.| gcd |.b.|)
by A5,NEWTON:50;then
not c|^((c|-count b)+1) divides (a gcd b) by INT_2:34;
hence thesis by A1,B2,B3,NEWTON03:def 7;
end;
suppose
B1: c|-count b > c|-count a; then
B2: min(c|-count b,c|-count a ) = c|-count a by XXREAL_0:def 9;
c|^(c|-count a) divides c|^(c|-count b) by B1,NEWTON:89; then
c|^(c|-count a) divides b by A4,INT_2:9; then
B3: c|^(c|-count a) divides (a gcd b) by A3,INT_2:def 2;
not |.c|^((c|-count a)+1).| divides |.a.| by A3,INT_2:16; then
not |.c|^((c|-count a)+1).| divides (|.a.| gcd |.b.|)
by A5,NEWTON:50;then
not c|^((c|-count a)+1) divides (a gcd b) by INT_2:34;
hence thesis by A1,B2,B3,NEWTON03:def 7;
end;
end;
theorem PGC:
for a,b be non zero Integer holds
Parity (a gcd b) = min (Parity a,Parity b)
proof
let a,b be non zero Integer;
reconsider c = a gcd b as non zero Nat;
A1: Parity c = 2|^(2|-count (a gcd b)) & Parity b = 2|^(2|-count b)
& Parity a = 2|^(2|-count a) by Def1;
2 is non trivial; then
2|^(2|-count (a gcd b)) = 2|^(min (2|-count a, 2|-count b)) by CCM
.= min (2|^(2|-count a), 2|^(2|-count b)) by MIN1;
hence thesis by A1;
end;
theorem PGG:
for a,b be Integer holds (Parity a) gcd (Parity b) = Parity (a gcd b)
proof
let a,b be Integer;
|.a.| in NAT by INT_1:3; then
reconsider k = |.a.| as Nat;
|.b.| in NAT by INT_1:3; then
reconsider l = |.b.| as Nat;
per cases;
suppose
A1: a = 0; then
Parity a = 0 by Def1; then
(Parity a) gcd (Parity b) = Parity (k gcd l) by A1,PMP;
hence thesis by INT_2:34;
end;
suppose
A1: b = 0; then
Parity b = 0 by Def1; then
(Parity a) gcd (Parity b) = Parity (k gcd l) by A1,PMP;
hence thesis by INT_2:34;
end;
suppose
A0: a <> 0 & b <> 0;
reconsider a as non zero Integer by A0;
reconsider b as non zero Integer by A0;
per cases by Th4;
suppose
B1: (Parity a) divides (Parity b); then
B2: Parity a <= Parity b by NAT_D:7;
(Parity a) gcd (Parity b) = |.Parity a.| by B1
.= min (Parity a,Parity b) by B2,XXREAL_0:def 9
.= Parity (a gcd b) by PGC;
hence thesis;
end;
suppose
B1: (Parity b) divides (Parity a); then
B2: Parity a >= Parity b by NAT_D:7;
(Parity a) gcd (Parity b) = |.Parity b.| by B1
.= min (Parity a,Parity b) by B2,XXREAL_0:def 9
.= Parity (a gcd b) by PGC;
hence thesis;
end;
end;
end;
theorem
for a be Nat holds Parity (2*a) = 2*(Parity a)
proof
let a be Nat;
Parity (2*a) = (Parity 2)*(Parity a) by ILP;
hence thesis;
end;
theorem PLG:
for a,b be Integer holds (Parity a) lcm (Parity b) = Parity (a lcm b)
proof
let a,b be Integer;
|.a.| in NAT by INT_1:3; then
reconsider k = |.a.| as Nat;
|.b.| in NAT by INT_1:3; then
reconsider l = |.b.| as Nat;
per cases;
suppose
A1: a = 0 or b = 0; then
Parity a = 0 or Parity b = 0 by Def1;
hence thesis by A1;
end;
suppose
A0: a <> 0 & b <> 0;
reconsider a as non zero Integer by A0;
reconsider b as non zero Integer by A0;
((Parity a) lcm (Parity b))*((Parity a) gcd (Parity b))
= (Parity a)*(Parity b) by NAT_D:29
.= Parity (a*b) by ILP
.= Parity |.a*b.| by PMP
.= Parity (k*l) by COMPLEX1:65
.= Parity ((k gcd l)*(k lcm l)) by NAT_D:29
.= (Parity (k gcd l)) * (Parity (k lcm l)) by ILP
.= (Parity (a gcd b)) * (Parity (k lcm l)) by INT_2:34
.= (Parity (a gcd b)) *(Parity (a lcm b)) by INT_2:33
.= ((Parity a) gcd (Parity b))*(Parity (a lcm b)) by PGG;
hence thesis by XCMPLX_1:5;
end;
end;
theorem
for a,b be non zero Integer holds Parity (a lcm b) = max (Parity a,Parity b)
proof
let a,b be non zero Integer;
min(Parity a,Parity b)*max(Parity a,Parity b) = (Parity a)*(Parity b)
by NEWTON04:18
.= ((Parity a) gcd (Parity b))*((Parity a) lcm (Parity b)) by NAT_D:29
.= (Parity (a gcd b))*((Parity a) lcm (Parity b)) by PGG
.= min (Parity a,Parity b)*((Parity a) lcm (Parity b)) by PGC
.= min (Parity a,Parity b)*(Parity (a lcm b)) by PLG;
hence thesis by XCMPLX_1:5;
end;
theorem
for a,b be Integer holds
Parity (a + b) = Parity(a gcd b)*Parity ((a+b)/(a gcd b))
proof
let a,b be Integer;
per cases;
suppose
a = 0 & b = 0; then
Parity (a gcd b) = 0 & Parity (a+b) = 0 by Def1;
hence thesis;
end;
suppose
A1: a <> 0 or b <> 0;
Parity (((a+b)/(a gcd b))*(a gcd b))
= Parity ((a+b)/(a gcd b)) * Parity(a gcd b) by ILP;
hence thesis by A1,XCMPLX_1:87;
end;
end;
theorem PAN:
for a be Integer, n be Nat holds Parity (a|^n) = (Parity a)|^n
proof
let a be Integer, n be Nat;
defpred P[Nat] means Parity (a|^$1) = (Parity a)|^$1;
A1: P[0]
proof
Parity (1*a|^0) = 1*(Parity a)|^0;
hence thesis;
end;
A2: for k be Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
B1: Parity (a|^k) = (Parity a)|^k;
Parity a|^(k+1) = Parity (a*a|^k) by NEWTON:6
.= (Parity a)*(Parity a)|^k by B1,ILP;
hence thesis by NEWTON:6;
end;
for x be Nat holds P[x] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem for a,b be non zero Integer, n be Nat holds
min (Parity (a|^n),Parity (b|^n)) = (min (Parity a,Parity b))|^n
proof
let a,b be non zero Integer, n be Nat;
min (Parity (a|^n),Parity (b|^n)) = Parity ((a|^n) gcd (b|^n)) by PGC
.= Parity ((a gcd b)|^n) by NEWTON03:4
.= (Parity (a gcd b))|^n by PAN;
hence thesis by PGC;
end;
registration
let a be odd Integer;
identify Parity a with parity a;
correctness
proof
thus Parity a = 1 by NAT_2:def 1
.= parity a by NAT_2:def 1;
end;
identify parity a with Parity a;
correctness;
reduce a|^(parity a) to a;
reducibility
proof
a|^(parity a) = a|^1 by NAT_2:def 1;
hence thesis;
end;
end;
registration
let a be even Integer;
cluster a|^(parity a) -> trivial non zero;
coherence
proof
a|^(parity a) = 1*a|^0;
hence thesis by NAT_2:def 1;
end;
end;
registration
let a be Integer;
reduce parity (parity a) to parity a;
reducibility;
reduce Parity (parity a) to parity a;
reducibility
proof
per cases;
suppose a is odd;
hence thesis;
end;
suppose a is even;
hence thesis by Def1;
end;
end;
end;
theorem PIP:
for a be Integer holds
(a is even iff parity a is even) & (parity a is even iff Parity a is even)
proof
let a be Integer;
per cases;
suppose
a is even;
hence thesis;
end;
suppose
a is odd;
hence thesis;
end;
end;
registration
let a be Integer;
cluster parity a + Parity a -> even;
coherence
proof
Parity a is even iff parity a is even by PIP;
hence thesis;
end;
cluster Parity a - parity a -> even;
coherence
proof
Parity a is even iff parity a is even by PIP;
hence thesis;
end;
cluster Parity a - parity a -> natural;
coherence
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0; then
Parity a >= 1 & parity a <= 1 by NAT_1:14,NEWTON03:def 1; then
Parity a - parity a >= 1 - 1 by XREAL_1:13;
hence thesis;
end;
end;
cluster a + parity a -> even;
coherence
proof
a is even iff parity a is even;
hence thesis;
end;
cluster a - parity a -> even;
coherence
proof
a is odd iff parity a is odd;
hence thesis;
end;
end;
:: Some obvious theorems on parity
theorem
for a be Integer holds parity (Parity a) = parity a
proof
let a be Integer;
per cases;
suppose
A1: a is even; then
Parity a is even;
hence thesis by A1;
end;
suppose
A1: a is odd; then
Parity a is odd;
hence thesis by A1;
end;
end;
theorem P1: for a be Integer holds parity a = parity (-a)
proof
let a be Integer;
per cases;
suppose
A1: a is even;
0 is even; then
0 - a is even by A1;
hence thesis by A1;
end;
suppose
A1: a is odd; then
-a is odd;
hence thesis by A1;
end;
end;
theorem PMI:
for a,b be Integer holds parity (a-b) = |.(parity a) - (parity b).|
proof
let a,b be Integer;
per cases;
suppose
A1: a is even;
per cases;
suppose b is even; then
parity (a - b) = 0 & |.(parity a) - (parity b).| = 0 by A1;
hence thesis;
end;
suppose
B1: b is odd; then
B2: a - b is odd by A1;
|.(parity a) - (parity b).| = --1 by A1,B1
.= parity (a - b) by B2;
hence thesis;
end;
end;
suppose
A1: a is odd;
per cases;
suppose b is odd; then
parity (a - b) = 0 & |.(parity a) - (parity b).| = 0 by A1;
hence thesis;
end;
suppose
B1: b is even; then
a - b is odd by A1;
hence thesis by A1,B1;
end;
end;
end;
theorem
for a,b be Integer holds parity (a+b) = parity ((parity a)+(parity b))
by NAT_D:66;
theorem PPM: for a,b be Integer holds parity (a+b) = parity (a-b)
proof
let a,b be Integer;
parity (a+b) = parity (parity(a)+parity(b)) by NAT_D:66
.= parity (parity(a) + parity(-b)) by P1
.= parity (a + -b) by NAT_D:66;
hence thesis;
end;
theorem ABP:
for a,b be Integer holds parity (a+b) = |.(parity a) - (parity b).|
proof
let a,b be Integer;
thus parity (a+b) = parity (a-b) by PPM
.= |.(parity a) - (parity b).| by PMI;
end;
theorem
for a,b be Nat holds
(parity (a+b) = parity b implies parity a = 0) &
(parity (a+b) <> parity b implies parity a = 1)
proof
let a,b be Nat;
((a+b) mod 2 = b mod 2 implies a mod 2 = 0) &
((a+b) mod 2 <> b mod 2 implies a mod 2 <> 0) by MAB;
hence thesis by NAT_2:def 1;
end;
theorem for a,b be Integer holds
parity (a+b) = (parity a) + (parity b) - 2*(parity a)*(parity b) &
parity a - parity b = parity (a+b) - 2*(parity (a+b))*(parity b) &
parity a - parity b = 2*(parity a)*parity (a+b) - parity (a+b)
proof
let a,b be Integer;
per cases;
suppose a is even & b is even; then
parity a = 0 & parity b = 0 & parity (a+b) = 0;
hence thesis;
end;
suppose
a is odd & b is odd; then
parity a = 1 & parity b = 1 & parity (a+b) = 0;
hence thesis;
end;
suppose
A1: a is even & b is odd; then
a + b is odd;
hence thesis by A1;
end;
suppose
A1: a is odd & b is even; then
a + b is odd;
hence thesis by A1;
end;
end;
theorem EVP:
for a,b be Integer holds (a+b) is even iff parity a = parity b
proof
let a,b be Integer;
thus (a+b) is even implies parity a = parity b
proof
assume (a+b) is even; then
0 = parity (a+b)
.= |.(parity a)-(parity b).| by ABP; then
(parity a) - (parity b) = 0;
hence thesis;
end;
assume parity a = parity b; then
0 = |.(parity a) - (parity b).|
.= parity (a+b) by ABP;
hence thesis;
end;
theorem for a,b be Integer holds parity (a*b) = (parity a)*(parity b)
proof
let a,b be Integer;
per cases;
suppose a is even; then
parity a = 0 & parity (a*b) = 0;
hence thesis;
end;
suppose a is odd; then
parity a = 1 & (b is even iff a*b is even);
hence thesis;
end;
end;
theorem for a,b be Integer holds parity (a lcm b) = parity (a*b)
proof
let a,b be Integer;
per cases;
suppose
A1: a*b is odd; then
a is odd & b is odd; then
a lcm b is odd;
hence thesis by A1;
end;
suppose
A1: a*b is even;
then a is even or b is even; then
a lcm b is even;
hence thesis by A1;
end;
end;
theorem for a,b be Integer holds parity (a gcd b) = max (parity a, parity b)
proof
let a,b be Integer;
per cases;
suppose
A1: a is odd; then
a gcd b is odd;
hence thesis by A1,XXREAL_0:def 10,NEWTON03:def 1;
end;
suppose
A1: a is even;
per cases;
suppose
B1: b is odd; then
(a gcd b) is odd;
hence thesis by B1,A1,XXREAL_0:def 10;
end;
suppose
B1: b is even; then
(a gcd b) is even by A1;
hence thesis by B1,A1;
end;
end;
end;
theorem for a,b be Integer holds parity (a*b) = min (parity a, parity b)
proof
let a,b be Integer;
min (parity a,parity b) = parity a or
min (parity a,parity b) = parity b by XXREAL_0:def 9; then
per cases by NAT_2:def 1;
suppose
B1: min(parity a, parity b) = 0; then
a is even or b is even;
hence thesis by B1;
end;
suppose
B1: min (parity a, parity b) = 1; then
a is odd & b is odd by XXREAL_0:def 9; then
a*b is odd;
hence thesis by B1;
end;
end;
theorem for a be Integer, n be non zero Nat holds parity (a|^n) = parity a
proof
let a be Integer, n be non zero Nat;
per cases;
suppose
A1: a is even; then
a|^n is even;
hence thesis by A1;
end;
suppose
A1: a is odd; then
a|^n is odd;
hence thesis by A1;
end;
end;
PAP:
for a,b be non zero Integer holds
Parity a > Parity b implies Parity (a+b) = Parity b
proof
let a,b be non zero Integer;
assume
A1: Parity a > Parity b; then
A1a: not (Parity a) divides (Parity b) by NAT_D:7;
A2: |.2.| > 1;
a <> -b by A1,PM; then
A3: a+b <> 0;
reconsider k = 2|-count a as Nat;
reconsider l = 2|-count b as Nat;
A2a: Parity a = 2|^k & Parity b = 2|^l by Def1; then
A2b: k > l by A1a,PEPIN:31; then
2|^l divides Parity a & Parity a divides a & Parity b divides b
by PEPIN:31,A2a,Th3; then
2|^l divides a & 2|^l divides b by Def1,INT_2:9; then
A4: 2|^l divides a+b by WSIERP_1:4;
not 2|^(l+1) divides (a+b)
proof
l+1 <= k by A2b,NAT_1:13; then
B1: 2|^(l+1) divides 2|^k by PEPIN:31;
2|^k divides a by A2,NEWTON03:def 7; then
B2: 2|^(l+1) divides a by INT_2:9,B1;
not 2|^(l+1) divides b by A2,NEWTON03:def 7;
hence thesis by INT_2:1,B2;
end; then
2|-count (a+b) = l by A2,A3,A4,NEWTON03:def 7; then
Parity (a+b) = 2|^l by A3,Def1;
hence thesis by Def1;
end;
theorem LEQ:
for a,b be non zero Integer holds
Parity (a+b) >= (Parity a)+(Parity b) implies
Parity a = Parity b
proof
let a,b be non zero Integer;
assume
A1: Parity (a+b) >= (Parity a)+(Parity b);
(Parity a) + (Parity b) > (Parity b) + 0 &
(Parity a) + (Parity b) > (Parity a) + 0 by XREAL_1:6; then
Parity a <= Parity b & Parity b <= Parity a by A1,PAP;
hence thesis by XXREAL_0:1;
end;
theorem
for a,b be Integer holds Parity (a+b) > (Parity a)+(Parity b) implies
Parity a = Parity b
proof
let a,b be Integer;
per cases;
suppose a is zero; then
Parity (a+b) = Parity b & Parity a = 0 by Def1;
hence thesis;
end;
suppose b is zero; then
Parity (a+b) = Parity a & Parity b = 0 by Def1;
hence thesis;
end;
suppose not a is zero & not b is zero;
hence thesis by LEQ;
end;
end;
theorem
for a,b be odd Integer, m be odd Nat holds
Parity (a|^m + b|^m) = Parity (a + b)
proof
let a,b be odd Integer, m be odd Nat;
per cases;
suppose
A1: a + b = 0; then
a = -b; then
a|^m = -(b|^m) by POWER:2;
hence thesis by A1;
end;
suppose
A1: a + b <> 0; then
a <> -b; then
a|^m <> (-b)|^m by NEWTON03:13; then
a|^m <> -(b|^m) by POWER:2; then
a|^m + b|^m <> 0; then
Parity (a|^m + b|^m) = 2|^(2|-count (a|^m + b|^m)) &
Parity (a+b) = 2|^(2|-count (a + b)) by A1,Def1;
hence thesis by NEWTON03:81;
end;
end;
theorem for a,b be odd Integer, m be even Nat holds
Parity (a|^m + b|^m) = 2
proof
let a,b be odd Integer, m be even Nat;
reconsider n = m/2 as Nat;
A1: (a|^n)|^2 = a|^(2*n) & (b|^n)|^2 = b|^(2*n) by NEWTON:9;
2|^(2|-count ((a|^n)|^2+(b|^n)|^2)) = 2|^1 by NEWTON03:74;
hence thesis by A1,Def1;
end;
theorem PEQ:
for a,b be non zero Integer st a + b <> 0 holds
Parity a = Parity b implies Parity (a+b) >= (Parity a) + (Parity b)
proof
let a,b be non zero Integer such that
A0: a+b <> 0;
reconsider k = 2|-count a as Nat;
assume
A1: Parity a = Parity b;
reconsider l = a/(Parity a)+ b/(Parity b) as even Integer;
A2: l*(Parity a) = a/(Parity a)*(Parity a) + b/(Parity b)*(Parity b) by A1
.= a/(Parity a)*(Parity a) + b by XCMPLX_1:87
.= a + b by XCMPLX_1:87;
A3: 2*(Parity a) = 2*2|^k by Def1 .= 2|^(k+1) by NEWTON:6;
2 divides l by ABIAN:def 1; then
2 is non trivial & 2|^(k+1) divides (a+b) by NEWTON03:5,A2,A3; then
2|-count (a+b) >= k+1 by A0,NEWTON03:59; then
2|^(k+1) divides 2|^(2|-count (a+b)) by PEPIN:31; then
2|^(k+1) divides Parity (a+b) by A0,Def1;
hence thesis by A0,A1,A3,NAT_D:7;
end;
theorem
for a,b be non zero Integer holds
Parity (a+b) = Parity b iff Parity a > Parity b
proof
let a,b be non zero Integer;
thus Parity (a+b) = Parity b implies Parity a > Parity b
proof
assume
A1: Parity (a+b) = Parity b;then
A2: Parity (a+b) + 0 < (Parity a) + (Parity b) by XREAL_1:6;
per cases by XXREAL_0:1;
suppose Parity a = Parity b;
hence thesis by A1,A2,Def1,PEQ;
end;
suppose Parity b > Parity a;
hence thesis by A1,PAP;
end;
suppose Parity b < Parity a;
hence thesis;
end;
end;
thus thesis by PAP;
end;
theorem
for a,b be non zero Nat holds Parity (a+b) < (Parity a)+(Parity b) implies
Parity (a+b) = min (Parity a, Parity b)
proof
let a,b be non zero Nat;
assume Parity (a+b) < (Parity a)+(Parity b); then
Parity a <> Parity b by PEQ; then
per cases by XXREAL_0:1;
suppose
B1: Parity a > Parity b; then
Parity (a+b) = Parity b by PAP;
hence thesis by B1,XXREAL_0:def 9;
end;
suppose
B1: Parity a < Parity b; then
Parity (a+b) = Parity a by PAP;
hence thesis by B1,XXREAL_0:def 9;
end;
end;
theorem
for a,b be non zero Integer st a + b <> 0 holds
Parity (a+b) = Parity a implies Parity a < Parity b
proof
let a,b be non zero Integer such that
A0: a + b <> 0;
assume
A1: Parity (a+b) = Parity a;
(Parity a)+(Parity b) > Parity a + 0 by XREAL_1:6; then
Parity a <> Parity b by A0,A1,PEQ; then
Parity a > Parity b or Parity a < Parity b by XXREAL_0:1;
hence thesis by PAP,A1;
end;
theorem PGP:
for a be Integer holds
Parity(a + Parity a) = (Parity ((Oddity a) + 1)) * (Parity a) &
Parity(a - Parity a) = (Parity ((Oddity a) - 1)) * (Parity a)
proof
let a be Integer;
per cases;
suppose a is non zero; then
reconsider a as non zero Integer;
A1: Parity(a - Parity a) = Parity((Oddity a)*Parity a - 1*Parity a)
.= Parity (((Oddity a) - 1) * Parity a)
.= (Parity ((Oddity a) - 1)) * Parity (Parity a) by ILP
.= (Parity ((Oddity a) - 1)) * (Parity a);
Parity(a + Parity a) = Parity ((Oddity a)*(Parity a) + Parity a)
.= Parity (((Oddity a) + 1) * (Parity a))
.= (Parity ((Oddity a) + 1)) * Parity (Parity a) by ILP
.= (Parity ((Oddity a) + 1)) * (Parity a);
hence thesis by A1;
end;
suppose a is zero; then
Parity (a + Parity a) = Parity 0 & Parity a = 0 by Def1;
hence thesis;
end;
end;
theorem ADA: for a be Integer holds 2*(Parity a) divides Parity (a + Parity a)
& 2*(Parity a) divides Parity (a - Parity a)
proof
let a be Integer;
per cases;
suppose
a is zero; then
Parity a = 0 by Def1;
hence thesis;
end;
suppose not a is zero; then
reconsider a as non zero Integer;
2 divides Parity ((Oddity a) + 1) & 2 divides Parity ((Oddity a) - 1)
by ABIAN:def 1; then
2*(Parity a) divides (Parity a)*Parity ((Oddity a) + 1) &
2*(Parity a) divides (Parity a)*Parity ((Oddity a) - 1) by NEWTON03:5;
hence thesis by PGP;
end;
end;
theorem
for a,b be Integer st Parity a = Parity b holds
Parity (a+b) = Parity ((a+Parity a) + (b-Parity b));
theorem
for a be Nat holds Parity (a + Parity a) >= 2*Parity a
proof
let a be Nat;
per cases;
suppose
a = 0; then
Parity a = 0 by Def1;
hence thesis;
end;
suppose a <> 0;
hence thesis by ADA,NAT_D:7;
end;
end;
theorem
for a be Nat holds Parity (a - Parity a) >= 2*Parity a or a = Parity a
proof
let a be Nat;
per cases;
suppose a = Parity a;
hence thesis;
end;
suppose
A0: a <> Parity a; then
reconsider a as non zero Nat by Def1;
A1: Parity(a - Parity a) = (Parity ((Oddity a) - 1)) * (Parity a)
by PGP;
a = (Oddity a)*(Parity a); then
A2: (Oddity a) - 1 <> 0 by A0;
Parity ((Oddity a)-1) <> 1;
hence thesis by A1,A2,XREAL_1:64,NAT_1:23;
end;
end;
theorem PSD:
for a,b be odd Integer holds Parity (a+b) <> Parity (a-b)
proof
let a,b be odd Integer;
per cases;
suppose
B1: a+b is zero; then
Parity (a-b) = Parity (2*a)
.= (Parity 2)*(Parity a) by ILP;
hence thesis by B1,Def1;
end;
suppose
B1: a-b is zero; then
Parity (a+b) = Parity (2*a)
.= (Parity 2)*Parity a by ILP;
hence thesis by B1,Def1;
end;
suppose
B0: a+b <> 0 & a-b <> 0; then
B1: 2|^(2|-count (a+b)) = Parity (a+b) &
2|^(2|-count (a-b)) = Parity (a-b) by Def1;
2*2 = 2|^2 by NEWTON:81; then
B2: 2|^2 divides (a+b) iff not 2|^2 divides (a-b) by NEWTON03:73;
2 is non trivial; then
2|-count (a+b) >= 2 iff 2|-count (a-b) < 2 by B0,B2,NEWTON03:59; then
per cases by XXREAL_0:1;
suppose
2|-count (a+b) > 2|-count (a-b);
hence thesis by B1,PEPIN:66;
end;
suppose
2|-count (a+b) < 2|-count (a-b);
hence thesis by B1,PEPIN:66;
end;
end;
end;
theorem
for a,b be odd Integer holds Parity (a+1) = Parity (b-1) implies a <> b
proof
let a,b be odd Integer;
1 is odd;
hence thesis by PSD;
end;
theorem PMG:
for a be odd Nat, b be non trivial odd Nat holds
Parity (a+b) = min(Parity (a+1), Parity (b-1)) or
Parity (a+b) >= 2*Parity (a+1)
proof
let a be odd Nat, b be non trivial odd Nat;
per cases by XXREAL_0:1;
suppose
A1: Parity (a+1) = Parity (b-1); then
Parity ((a+1)+(b-1)) >= Parity (a+1) + Parity (b-1) by PEQ;
hence thesis by A1;
end;
suppose
B1: Parity (a+1) > Parity (b-1); then
Parity ((a+1)+(b-1)) = Parity (b-1) by PAP;
hence thesis by B1,XXREAL_0:def 9;
end;
suppose
B1: Parity (a+1) < Parity (b-1); then
Parity ((a+1)+(b-1)) = Parity (a+1) by PAP;
hence thesis by B1,XXREAL_0:def 9;
end;
end;
theorem
for a,b be non zero Integer holds Parity a > Parity b implies
a div (Parity b) is even
proof
let a,b be non zero Integer;
assume Parity a > Parity b; then
A0: 2*(Parity b) divides Parity a by P2P;
Parity a divides a by Th3; then
2*(Parity b) divides a by INT_2:9,A0; then
consider c be Integer such that
A1: a = 2*(Parity b)*c;
(0 + (2*c)*(Parity b)) div (Parity b) = (0 div (Parity b)) + 2*c;
hence thesis by A1;
end;
theorem
for a,b be non zero Integer holds
Parity a > Parity b iff (Parity a) div (Parity b) is non zero even
proof
let a,b be non zero Integer;
thus Parity a > Parity b implies (Parity a) div (Parity b) is non zero even
proof
assume Parity a > Parity b; then
2*(Parity b) divides Parity a by P2P; then
consider c be Integer such that
A1: Parity a = 2*(Parity b)*c;
(0 + (2*c)*(Parity b)) div (Parity b) = (0 div (Parity b)) + 2*c;
hence thesis by A1;
end;
assume (Parity a) div (Parity b) is non zero even; then
B1: (Parity b)*((Parity a) div Parity b) >= 2*Parity b
by NAT_D:7,NEWTON02:2;
B2: 2*(Parity b) > 1*(Parity b) by XREAL_1:68;
(Parity b)*((Parity a) div Parity b) + ((Parity a) mod Parity b) >=
(Parity b)*((Parity a) div Parity b) + 0 by XREAL_1:6; then
Parity a >= (Parity b)*((Parity a) div Parity b) + 0 by INT_1:59; then
Parity a >= 2*(Parity b) by B1,XXREAL_0:2;
hence thesis by B2,XXREAL_0:2;
end;
theorem
for a be odd Nat holds Parity (a-1) = 2 * Parity(a div 2)
proof
let a be odd Nat;
a = (a div 2)*2 + (a mod 2) by INT_1:59
.= (a div 2)*2 + 1 by NAT_D:12; then
Parity (a-1) = (Parity (a div 2))*Parity 2 by ILP;
hence thesis;
end;
theorem MPA:
for a,b be non zero Integer holds min(Parity a,Parity b) divides a &
min (Parity a,Parity b) divides b
proof
let a,b be non zero Integer;
min (Parity a,Parity b) = Parity a or min (Parity a,Parity b) = Parity b
by XXREAL_0:def 9; then
A1: min (Parity a,Parity b) divides Parity a &
min (Parity a,Parity b) divides Parity b by XXREAL_0:def 9,PEPIN31;
Parity a divides a & Parity b divides b by Th3;
hence thesis by A1,INT_2:9;
end;
registration
let a,b be non zero Integer;
cluster (a+b)/min(Parity a,Parity b) -> integer;
coherence
proof
min (Parity a,Parity b) divides a &
min (Parity a,Parity b) divides b by MPA;
hence thesis by Th1,WSIERP_1:4;
end;
end;
registration
let p be non square Integer;
let n be odd Nat;
cluster p|^n -> non square;
coherence
proof
per cases;
suppose p >= 0; then
p in NAT by INT_1:3;
hence thesis;
end;
suppose p < 0;
hence thesis;
end;
end;
end;
registration
let a be Integer;
let n be even Nat;
cluster a|^n -> square;
coherence
proof
reconsider k = |.a.| as Element of NAT by INT_1:3;
k|^n = |.a|^n.| by TAYLOR_2:1;
hence thesis;
end;
end;
registration
let p be prime Nat;
let a be non zero square Integer;
cluster p|-count a -> even;
coherence
proof
reconsider a as non zero square Element of NAT by INT_1:3;
|.p.| > 1 by NEWTON03:def 1; then
p|^(p|-count a) divides a by NEWTON03:def 7; then
consider k be Nat such that
A0: a = p|^(p|-count a)*k by NAT_D:def 3;
not p divides k by A0,NEWTON03:76; then
not k gcd p = p by INT_2:def 2; then
k,p are_coprime by PEPIN:2; then
A1: k,p|^(p|-count a) are_coprime by WSIERP_1:10;
assume
A2: not thesis;
A3: not 2-root (p|^(p|-count a)) in NAT
proof
assume not thesis; then
(2-root (p|^(p|-count a)))|^2 is square Nat;
hence contradiction by A2;
end;
not ex c be Nat st k*(p|^(p|-count a)) = c^2
proof
assume not thesis; then
consider c be Nat such that
B1: c^2 = k*(p|^(p|-count a));
k*(p|^(p|-count a)) = c|^2 by B1,NEWTON:81;
hence contradiction by NEWTON03:14,A1,A3;
end;
hence contradiction by A0,PYTHTRIP:def 3;
end;
end;
registration
let a be odd Integer;
cluster 2*a -> non square;
coherence
proof
per cases;
suppose a >= 0; then
a in NAT by INT_1:3; then
reconsider a as odd Nat;
A1: a,2 are_coprime by NEWTON03:def 5;
not (2-root 2)|^2 is square by INT_2:28; then
A2: not 2-root 2 in NAT;
not ex c be Nat st 2*a = c^2
proof
assume not thesis; then
consider c be Nat such that
B1: 2*a = c^2;
2*a = c|^2 by B1,NEWTON:81;
hence contradiction by A1,A2,NEWTON03:14;
end;
hence thesis by PYTHTRIP:def 3;
end;
suppose a < 0;
hence thesis;
end;
end;
end;
registration
let a be square Integer;
cluster Parity a -> square;
coherence
proof
per cases;
suppose a = 0;
hence thesis by Def1;
end;
suppose a <> 0; then
reconsider a as non zero Integer;
Parity a = 2|^(dwa|-count a) by Def1;
hence thesis;
end;
end;
cluster Oddity a -> square;
coherence
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0; then
reconsider a as non zero Integer;
a = (Parity a)*(Oddity a);
hence thesis;
end;
end;
end;
registration
let a be non zero square Integer;
cluster 2|-count a -> even;
coherence by INT_2:28;
end;
theorem MMD:
for a,b be non negative Real holds
max(a,b) - min(a,b) = |.a - b.|
proof
let a,b be non negative Real;
per cases;
suppose a >= b; then
max (a,b) = a & min (a,b) = b by XXREAL_0:def 9,def 10;
hence thesis;
end;
suppose a < b; then
max (a,b) = b & min (a,b) = a by XXREAL_0:def 9,def 10; then
|.max (a,b) - min (a,b).| = |.-(b - a).| by COMPLEX1:52;
hence thesis;
end;
end;
theorem A4I:
for a be even Integer st not 4 divides a holds a is non square
proof
let a be even Integer such that
A1: not 4 divides a;
not 2 divides a/2
proof
assume not thesis; then
2*2 divides (a/2)*2 by NEWTON02:2;
hence contradiction by A1;
end; then
reconsider b = a/2 as odd Integer by ABIAN:def 1;
2*b is non square;
hence thesis;
end;
theorem for a,b be odd Integer holds a-b is square implies not a + b is square
proof
let a,b be odd Integer;
assume a-b is square; then
consider c be Nat such that
A1: c^2 = a - b by PYTHTRIP:def 3;
reconsider c as even Nat by A1;
A2: |.a.| in NAT & |.b.| in NAT by INT_1:3; then
reconsider k = max (|.a.|,|.b.|) as odd Nat by XXREAL_0:def 10;
reconsider l = min (|.a.|,|.b.|) as odd Nat by A2, XXREAL_0:def 9;
A3: |.a.| + |.b.| = k + l by NEWTON03:41;
2 divides c by ABIAN:def 1; then
2*2 divides c*c by NEWTON02:2; then
A5: 2*2 divides c^2 by SQUARE_1:def 1;
per cases by ABS;
suppose
B1: |.a + b.| = |.a.| + |.b.|; then
B2: |.a - b.| = |.|.a.| - |.b.|.| by LABS
.= k - l by MMD;
not 4 divides k|^1 + l|^1 by A1,A5,B2,NEWTON03:20;
hence thesis by B1,A3,A4I;
end;
suppose
B1: |.a - b.| = |.a.| + |.b.|; then
B2: |.a + b.| = |.|.a.| - |.b.|.| by LmABS
.= k - l by MMD;
4 divides k|^1 + l|^1 by B1,A1,NEWTON03:41,A5; then
not 4 divides k - l by NEWTON03:20;
hence thesis by B2,A4I;
end;
end;
theorem
for a,b be non zero Integer holds
Parity (a+b) = (min (Parity a,Parity b))*
Parity ((a+b)/min(Parity a,Parity b))
proof
let a,b be non zero Integer;
A1: min (Parity a,Parity b) = Parity a or
min (Parity a,Parity b) = Parity b by XXREAL_0:def 9;
min (Parity a,Parity b) divides (Parity a)
by A1,XXREAL_0:def 9,PEPIN31; then
consider c be Nat such that
A2: Parity a = min (Parity a,Parity b)*c by NAT_D:def 3;
min (Parity a,Parity b) divides (Parity b)
by A1,XXREAL_0:def 9,PEPIN31; then
consider d be Nat such that
A3: Parity b = min (Parity a,Parity b)*d by NAT_D:def 3;
(Parity a)/min (Parity a,Parity b) = c &
(Parity b)/min (Parity a,Parity b) = d by A2,A3,XCMPLX_1:89; then
A4: (Oddity a)*c = a/min (Parity a,Parity b) &
(Oddity b)*d = b/min (Parity a,Parity b) by XCMPLX_1:98;
a + b = (Oddity a)*(min(Parity a,Parity b)*c) +
(Oddity b)*(min(Parity a,Parity b)*d) by A2,A3
.= min(Parity a,Parity b)*((Oddity a)*c + (Oddity b)*d); then
Parity (a+b)
= Parity (min(Parity a,Parity b))*Parity((Oddity a)*c + (Oddity b)*d)
by ILP
.= min (Parity a, Parity b) * Parity((Oddity a)*c + (Oddity b)*d) by A1;
hence thesis by A4,XCMPLX_1:62;
end;
theorem OPC:
for a,b be non zero Integer holds
Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1
proof
let a,b be non zero Integer;
(Oddity b) gcd 2 = 1 by NEWTON03:def 5; then
(Oddity b) gcd (2|^(2|-count a)) = 1 by WSIERP_1:12;
hence thesis by Def1;
end;
theorem OMO:
for a be Integer holds |.Oddity a.| = Oddity |.a.|
proof
let a be Integer;
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0; then
reconsider a as non zero Integer;
|.Oddity a.|*|.Parity a.| = |.(Oddity a)*(Parity a).| by COMPLEX1:65
.= (Oddity |.a.|)*(Parity |.a.|)
.= (Oddity |.a.|)*|.Parity a.| by PMP;
hence thesis by XCMPLX_1:5;
end;
end;
theorem
for a,b be Integer holds (Oddity a) gcd (Oddity b) = Oddity (a gcd b)
proof
let a,b be Integer;
per cases;
suppose
A1: a <> 0 & b <> 0; then
reconsider a as non zero Integer;
reconsider b as non zero Integer by A1;
A2: Parity((Oddity a) gcd (Oddity b)) = 1 gcd 1 by NAT_2:def 1;
Oddity (a gcd b) = Oddity (((Parity a)*(Oddity a)) gcd
((Parity b)*(Oddity b)))
.= Oddity ((((Parity a) gcd ((Parity b)*(Oddity b))))*(((Oddity a) gcd
((Parity b)*(Oddity b))))) by OPC,NEWTON03:35
.= Oddity ((((Parity a) gcd (Parity b)))*((Parity a) gcd (Oddity b))*
(((Oddity a) gcd ((Parity b)*(Oddity b))))) by OPC,NEWTON03:35
.= Oddity ((((Parity a) gcd (Parity b)))*1*
(((Oddity a) gcd ((Parity b)*(Oddity b))))) by OPC
.= Oddity ((((Parity a) gcd (Parity b)))*
(((Oddity a) gcd (Parity b))* ((Oddity a) gcd (Oddity b))))
by OPC,NEWTON03:35
.= Oddity ((((Parity a) gcd (Parity b)))*(1* ((Oddity a)
gcd (Oddity b)))) by OPC
.= (Oddity ((Parity a) gcd (Parity b)))*(Oddity ((Oddity a)
gcd (Oddity b))) by ILO
.= Oddity (Parity (a gcd b))*Oddity ((Oddity a) gcd (Oddity b)) by PGG
.= 1*Oddity ((Oddity a) gcd (Oddity b)) by OPA;
hence thesis by A2;
end;
suppose a = 0; then
Oddity (a gcd b) = Oddity |.b.| &
(Oddity a) gcd (Oddity b) = |.Oddity b.| by INT_2:12,NEWTON02:3;
hence thesis by OMO;
end;
suppose b = 0; then
Oddity (a gcd b) = Oddity |.a.| &
(Oddity a) gcd (Oddity b) = |.Oddity a.| by INT_2:12,NEWTON02:3;
hence thesis by OMO;
end;
end;
theorem
for a,b be non zero Integer holds
a gcd b = ((Parity a) gcd (Parity b))*((Oddity a) gcd (Oddity b))
proof
let a,b be non zero Integer;
a gcd b = ((Parity a)*(Oddity a)) gcd b
.= ((Parity a) gcd (Parity b)*(Oddity b))* ((Oddity a) gcd b)
by NEWTON03:35,OPC
.= ((Parity a) gcd (Parity b))*((Parity a) gcd (Oddity b))*
((Oddity a) gcd b) by NEWTON03:35,OPC
.= ((Parity a) gcd (Parity b))*1*((Oddity a) gcd b) by OPC
.= ((Parity a) gcd (Parity b))*((Oddity a) gcd ((Parity b)*(Oddity b)))
.= ((Parity a) gcd (Parity b))*(((Oddity a) gcd ((Parity b)))*((Oddity a)
gcd(Oddity b))) by NEWTON03:35,OPC
.= ((Parity a) gcd (Parity b))*(1*((Oddity a) gcd (Oddity b))) by OPC;
hence thesis;
end;
theorem
for a be odd Nat holds Parity (a+1) = 2 iff parity (a div 2) = 0
proof
let a be odd Nat;
a >= 1 by NAT_1:14; then
per cases by XXREAL_0:1;
suppose
B0: a = 1;
parity (1 div (1+1)) = parity 0;
hence thesis by B0;
end;
suppose a > 1; then
reconsider a as non trivial odd Nat by NAT_2:def 1;
reconsider l = 2*0+1 as odd Nat;
L1: Parity (a+1) = 2 implies parity (a div 2) = 0
proof
assume
A1: Parity (a+1) = 2; then
per cases by PMG;
suppose
2 = min (Parity (l+1),Parity (a-1)); then
Parity (a-1) > 2 by A1,PSD,XXREAL_0:def 9; then
2|^(2|-count (a-1)) > 2|^1 by Def1; then
2|-count (a-1) > 1 by PREPOWER:93; then
2|-count (a-1) >= 1+1 by NAT_1:13; then
2|^2 divides (a-1) by NEWTON03:59; then
2*2 divides (a-1) by NEWTON:81; then
((a-1) div 4) * 4 = a-1
.= (a div 2)*2 + (a mod 2) -1 by INT_1:59
.= (a div 2)*2 +1 -1 by NAT_D:12; then
((a-1) div 4)*2 = a div 2;
hence thesis;
end;
suppose 2 >= 2*Parity (l+1);
hence thesis;
end;
end;
parity (a div 2) = 0 implies Parity (a+1) = 2
proof
assume parity (a div 2) = 0; then
reconsider k = (a div 2) as even Nat;
a + 1 = (a div 2)*2 + (a mod 2) + 1 by INT_1:59
.= (a div 2)*2 + 1 + 1 by NAT_D:12
.= 2*(k + 1); then
Parity (a+1) = (Parity 2)*(Parity (k+1)) by ILP
.= 2*1;
hence thesis;
end;
hence thesis by L1;
end;
end;
theorem for a be even Integer holds a div 2 = (a+1) div 2
proof
let a be even Integer;
((a+1) div 2)*2 + ((a+1) mod 2) = a + 1 by INT_1:59
.= (a div 2)*2 + (a mod 2) + 1 by INT_1:59
.= (a div 2)*2 + ((a+1) mod 2);
hence thesis;
end;
theorem SAB:
for a,b be Integer holds
a + b = 2*((a div 2) + (b div 2)) + (parity a) + (parity b)
proof
let a,b be Integer;
a = (a div 2)*2 + (a mod 2) & b = (b div 2)*2 + (b mod 2) by INT_1:59;
hence thesis;
end;
theorem SPA: for a,b be odd Integer holds
Parity (a+b) = 2*Parity ((a div 2) + (b div 2) + 1)
proof
let a,b be odd Integer;
parity a = 1 & parity b = 1 by NAT_2:def 1; then
Parity (a + b) = Parity ( 2*((a div 2) + (b div 2)) + 1 + 1) by SAB
.= Parity (2*((a div 2) + (b div 2) + 1))
.= (Parity 2)*Parity ((a div 2) + (b div 2) + 1) by ILP;
hence thesis;
end;
theorem PPD:
for a,b be odd Integer holds
Parity (a+b) = 2 iff parity (a div 2) = parity (b div 2)
proof
let a,b be odd Integer;
thus Parity (a+b) = 2 implies parity (a div 2) = parity (b div 2)
proof
assume Parity (a+b) = 2; then
2*(Parity (((a div 2) + (b div 2) + 1))) = 2*1 by SPA; then
(a div 2) + (b div 2) is even;
hence thesis by EVP;
end;
assume parity (a div 2) = parity (b div 2); then
a div 2 is odd iff b div 2 is odd; then
2*(Parity (((a div 2) + (b div 2)) + 1)) = 2*1 by NAT_2:def 1;
hence thesis by SPA;
end;
theorem PSU:
for a,b be non zero Integer holds Parity (a+b) = ((Parity a)+(Parity b)) iff
(Parity a = Parity b) & parity ((Oddity a) div 2) = parity ((Oddity b) div 2)
proof
let a,b be non zero Integer;
thus Parity (a+b) = ((Parity a)+(Parity b)) implies
(Parity a = Parity b) &
parity ((Oddity a) div 2) = parity ((Oddity b) div 2)
proof
assume
A1: Parity (a+b) = ((Parity a) + (Parity b)); then
A2: Parity a = Parity b by LEQ; then
2*Parity a = Parity ((Parity a)*(Oddity a) + (Parity b)*(Oddity b)) by A1
.= Parity ((Parity a)*((Oddity a)+ (Oddity b))) by A2
.= (Parity (Parity a))*(Parity((Oddity a) + (Oddity b))) by ILP
.= (Parity a)*Parity ((Oddity a)+(Oddity b));
hence thesis by A1,LEQ,PPD,XCMPLX_1:5;
end;
assume
A1: (Parity a = Parity b) &
parity ((Oddity a) div 2) = parity ((Oddity b) div 2);
Parity (a+b) = Parity ((Parity a)*(Oddity a)+(Parity b)*(Oddity b))
.= Parity ((Parity a)*((Oddity a)+ (Oddity b))) by A1
.= (Parity(Parity a))*(Parity ((Oddity a)+(Oddity b))) by ILP
.= 2*(Parity a) by A1,PPD;
hence thesis by A1;
end;
theorem for a,b be non zero Integer st
a+b <> 0 & Parity a = Parity b &
parity ((Oddity a) div 2) <> parity ((Oddity b) div 2) holds
Parity (a+b) > (Parity a)+(Parity b)
proof
let a,b be non zero Integer such that
A1: a + b <> 0 & Parity a = Parity b &
parity ((Oddity a) div 2) <> parity ((Oddity b) div 2);
A2: Parity (a+b) >= Parity a + Parity b by A1,PEQ;
Parity (a+b) <> Parity a + Parity b by A1,PSU;
hence thesis by A2,XXREAL_0:1;
end;
registration
let a be Nat;
cluster Oddity a -> natural;
coherence
proof
a/Parity a is non negative;
thus thesis;
end;
end;