:: Some Remarkable Identities Involving Numbers
:: by Rafa{\l} Ziobro
::
:: Received September 5, 2014
:: Copyright (c) 2014-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, NEWTON, SQUARE_1, XCMPLX_0;
notations ABIAN, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, INT_2, ORDINAL1,
SQUARE_1, NEWTON;
constructors ABIAN, SQUARE_1, NAT_1, NAT_D, NEWTON;
registrations ABIAN, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
WSIERP_1, XCMPLX_0, ABSVALUE;
requirements REAL, NUMERALS, SUBSET, ARITHM;
expansions ABIAN, INT_1, INT_2;
theorems INT_2, NAT_1, INT_1, EULER_1, PREPOWER, NEWTON, XCMPLX_1, XREAL_1,
XXREAL_0, NAT_D, SQUARE_1, PEPIN, ABIAN, NAT_3, WSIERP_1, TAYLOR_2,
SERIES_4;
schemes NAT_1;
begin
reserve a,b,c,d,x,j,k,l,m,n for Nat,
p,q,t,z,u,v for Integer,
a1,b1,c1,d1 for Complex;
registration
let u,v be even Integer;
cluster u-v -> even;
coherence
proof
(u+1) - (v+1) is even;
hence thesis;
end;
end;
registration
let u be odd Integer;
let k;
cluster u|^k -> odd;
coherence
proof
A1: 2 divides u iff |.2.| divides |.u.| by INT_2:16;
A2: |.u.| is odd implies |.u.| |^k is odd by PEPIN:20;
|.u |^k.| = |.u.| |^k by TAYLOR_2:1;
hence thesis by A1,A2,INT_2:16;
end;
end;
registration
let k be positive Nat;
let u be even Integer;
cluster u|^k -> even;
coherence
proof
A0: 2 = |.2.|;
A2: k>0 & |.u.| is even implies (|.u.|)|^k is even by PEPIN:21;
|.u |^k.| = (|.u.|)|^k by TAYLOR_2:1;
hence thesis by A2,A0,ABIAN:def 1,INT_2:16;
end;
end;
Lm10: (a1+b1)|^2 = a1|^2 + 2*a1*b1 + b1|^2
proof
(a1+b1)|^2 = (a1+b1)^2 & a1|^2 = a1^2 & b1|^2 = b1^2 by NEWTON:81;
hence thesis by SQUARE_1:4;
end;
theorem Th1:
a1|^2 - b1|^2 = (a1-b1)*(a1+b1)
proof
a1|^2 = a1^2 & b1|^2 = b1^2 by NEWTON:81;
hence thesis by SQUARE_1:8;
end;
theorem Th2:
(2*a1+1)|^2 + (2*a1|^2 + 2*a1)|^2 = (2*a1|^2 + 2*a1 + 1)|^2
proof
((2*a1|^2) + (2*a1) +1)|^2 =
((2*a1|^2) + (2*a1) +1)*((2*a1|^2) + (2*a1) +1) by NEWTON:81
.= (2*a1|^2)*(2*a1|^2)+ (2*a1)*(2*a1) +1
+ 2*(2*a1)*(2*a1|^2) + 2*(2*a1|^2) + 2*(2*a1)
.= (2*a1|^2)|^2 + (2*a1)*(2*a1) + 1 +
2*(2*a1)*(2*a1|^2) + 2*(2*a1|^2) + 2*(2*a1) by NEWTON:81
.= (2*a1|^2)|^2 + (2*a1)|^2 + 1 + 2*(2*a1|^2)*(2*a1)
+ 2*(2*a1|^2)+ 2*(2*a1)*1 by NEWTON:81
.= ((2*a1|^2)|^2 + 2*(2*a1|^2)*(2*a1) + (2*a1)|^2)
+ ((2*2*a1|^2)+ 2*(2*a1)*1 + 1|^2)
.= ((2*a1|^2) + (2*a1))|^2 + (2*2*a1|^2+ 2*(2*a1)*1 + 1|^2) by Lm10
.= ((2*a1|^2) + (2*a1))|^2 + (2|^2*a1|^2+ 2*(2*a1)*1 + 1|^2) by NEWTON:81
.= ((2*a1|^2) + (2*a1))|^2 + ((2*a1)|^2+ 2*(2*a1)*1 + 1|^2) by NEWTON:7;
hence thesis by Lm10;
end;
theorem
a1|^2+a1*b1+b1|^2 = (3*(a1+b1)|^2 +(a1-b1)|^2)/4
proof
A1: (a1+b1)|^2 = (a1+b1)*(a1+b1) by NEWTON:81
.= a1*a1 + 2*a1*b1 + b1*b1
.= a1|^2 + 2*a1*b1 + b1*b1 by NEWTON:81
.= a1|^2 + 2*a1*b1 + b1|^2 by NEWTON:81;
(a1-b1)|^2 = (a1-b1)*(a1-b1) by NEWTON:81
.= a1*a1 - 2*a1*b1 + b1*b1
.= a1|^2 - 2*a1*b1 + b1*b1 by NEWTON:81
.= a1|^2 - 2*a1*b1 + b1|^2 by NEWTON:81;
hence thesis by A1;
end;
theorem
a is odd implies ex b st a|^2 + b|^2 = (b+1)|^2
proof
assume a is odd;
then consider k be Nat such that
A2: a = 2*k+1 by ABIAN:9;
(2*k+1)|^2 + (2*k|^2 +2*k)|^2 = ((2*k|^2 +2*k) +1)|^2 by Th2;
hence thesis by A2;
end;
theorem Th5:
((a1|^m+b1|^m)*(a1|^n-b1|^n) + (a1|^n+b1|^n)*(a1|^m-b1|^m))/2
= a1|^(m+n) - b1|^(m+n)
proof
((a1|^m+b1|^m)*(a1|^n-b1|^n) + (a1|^n+b1|^n)*(a1|^m-b1|^m))/2 =
(a1|^m*a1|^n - b1|^m*b1|^n + a1|^n*a1|^m - b1|^n*b1|^m)/2
.=(a1|^(m+n) - b1|^m*b1|^n + a1|^n*a1|^m - b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) - b1|^(m+n) + a1|^n*a1|^m - b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) - b1|^(m+n) + a1|^(m+n) - b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) - b1|^(m+n) + a1|^(n+m) - b1|^(n+m))/2 by NEWTON:8
.= a1|^(m+n)-b1|^(m+n);
hence thesis;
end;
Lm0: a|^0 + b|^0 > c|^0
proof
a|^0 = 1 & b|^0 = 1 & c|^0 = 1 by NEWTON:4;
hence thesis;
end;
theorem Th6:
a|^m + b|^m <= c|^m implies a <= c
proof
assume
A0: a|^m + b|^m <= c|^m;
m=0 implies a|^m + b|^m > c|^m by Lm0; then
A2e: 0+1 <= m by A0,NAT_1:13;
a|^m + b|^m <= c|^m + b|^m by A0,NAT_1:12;
then a|^m + b|^m -b|^m <= c|^m + b|^m- b|^m by XREAL_1:9;
hence thesis by A2e,PREPOWER:10;
end;
theorem
(a1+b1)|^(n+1) = a1|^(n+1) + b1|^(n+1) + a1*b1*c1 implies
(a1+b1)|^(n+2) = a1|^(n+2) + b1|^(n+2) + a1*b1*(a1|^n + b1|^n + c1*(a1+b1))
proof
assume (a1+b1)|^(n+1) = a1|^(n+1) + b1|^(n+1) + a1*b1*c1;
then (a1+b1)|^(n+1+1) =
(a1+b1)*(a1|^(n+1) + b1|^(n+1) + a1*b1*c1) by NEWTON:6
.= a1*a1|^(n+1) + b1*a1|^(n+1) +
a1*b1|^(n+1) + b1*b1|^(n+1) + (a1+b1)*a1*b1*c1
.= a1|^(n+1+1)+ b1*a1|^(n+1) +
a1*b1|^(n+1) + b1*b1|^(n+1) + a1*b1*(c1*(a1+b1)) by NEWTON:6
.= a1|^(n+2) + b1*(a1*a1|^n) +
a1*b1|^(n+1) + b1*b1|^(n+1) + a1*b1*c1*(a1+b1) by NEWTON:6
.= a1|^(n+2) + b1*a1*a1|^n + a1*(b1*b1|^n)
+ b1*b1|^(n+1) + a1*b1*c1*(a1+b1) by NEWTON:6
.= a1|^(n+2) + b1*a1*a1|^n + a1*b1*b1|^n
+ b1|^(n+1+1) + a1*b1*(c1*a1 + c1*b1) by NEWTON:6
.= a1|^(n+2) + b1|^(n+2) + a1*b1*(a1|^n + b1|^n + c1*(a1 + b1));
hence thesis;
end;
theorem Th8:
((a1|^m+b1|^m)*(a1|^n+b1|^n) + (a1|^n-b1|^n)*(a1|^m-b1|^m))/2
= a1|^(m+n) + b1|^(m+n)
proof
thus ((a1|^m+b1|^m)*(a1|^n+b1|^n) + (a1|^n-b1|^n)*(a1|^m-b1|^m))/2 =
(a1|^m*a1|^n + b1|^m*b1|^n + a1|^n*a1|^m + b1|^n*b1|^m)/2
.=(a1|^(m+n) + b1|^m*b1|^n + a1|^n*a1|^m + b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) + b1|^(m+n) + a1|^n*a1|^m + b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) + b1|^(m+n) + a1|^(m+n) + b1|^n*b1|^m)/2 by NEWTON:8
.=(a1|^(m+n) + b1|^(m+n) + a1|^(n+m) + b1|^(n+m))/2 by NEWTON:8
.= a1|^(m+n)+b1|^(m+n);
end;
Lm3a: a<=b implies a|^n <= b|^n
proof
per cases by NAT_1:14;
suppose A1: n = 0;
a|^0 = 1 & b|^0 = 1 by NEWTON:4;
hence thesis by A1;
end;
suppose A1: 1 <= n;
assume a <= b; then
per cases by XXREAL_0:1;
suppose a < b;
hence thesis by A1, PREPOWER:10;
end;
suppose a = b;
hence thesis;
end;
end;
end;
Lm4a: a|^n > b|^n implies a|^(n+1) > b|^(n+1)
proof
assume
A1: a|^n > b|^n;
A2: a|^(n+1) = a*a|^n & b|^(n+1)=b*b|^n by NEWTON:6;
A3: a > b by A1,Lm3a; then
A4: a*a|^n > a*b|^n by A1,XREAL_1:68;
(b|^n)*a >= (b|^n)*b by A3,XREAL_1:66;
hence thesis by A2,A4,XXREAL_0:2;
end;
Lm5c: b>0 implies a < a + b|^m
proof
assume b>0;
then b|^m > 0 by PREPOWER:6;
hence thesis by NAT_1:16;
end;
Lm5d: (a+x)|^m >= a|^m + b|^m & a>0 & b>0 implies x>0
proof
assume (a+x)|^m >= a|^m + b|^m & a>0 & b>0;
then x <> 0 by Lm5c;
hence thesis;
end;
theorem Th9:
a1|^(m+1)+b1|^(m+1) = ((a1|^m+b1|^m)*(a1+b1) + (a1-b1)*(a1|^m-b1|^m))/2
proof
thus a1|^(m+1)+b1|^(m+1)
= ((a1|^m+b1|^m)*(a1+b1) + (a1|^1-b1|^1)*(a1|^m-b1|^m))/2 by Th8
.= ((a1|^m+b1|^m)*(a1+b1) + (a1-b1)*(a1|^m-b1|^m))/2;
end;
theorem Th10:
(a-b)*(a|^m-b|^m) >= 0
proof
A0: a|^0 = 1 & b|^0 = 1 by NEWTON:4;
per cases;
suppose
A1: a|^m - b|^m >= 0;
then a|^m - b|^m + b|^m >= 0 + b|^m by XREAL_1:7;
then a >= b or m < 1 by PREPOWER:10;
then a-b >= b - b or m = 0 by XREAL_1:9,NAT_1:14;
hence thesis by A0,A1;
end;
suppose
A2: a|^m - b|^m < 0;
then a|^m - b|^m + b|^m < 0 + b|^m by XREAL_1:8;
then a - b < b - b by Lm3a,XREAL_1:9;
hence thesis by A2;
end;
end;
theorem
a|^(m+1)+b|^(m+1) >= (a|^m+b|^m)*(a+b)/2
proof
A1: a|^(m+1)+b|^(m+1)=((a|^m+b|^m)*(a+b) + (a-b)*(a|^m-b|^m))/2 by Th9
.= (a|^m+b|^m)*(a+b)/2 + (a-b)*(a|^m-b|^m)/2;
(a|^m+b|^m)*(a+b) + (a-b)*(a|^m-b|^m) >= (a|^m+b|^m)*(a+b)
by Th10,XREAL_1:31; then
((a|^m+b|^m)*(a+b) + (a-b)*(a|^m-b|^m))/2 >= ((a|^m+b|^m)*(a+b))/2
by XREAL_1:72;
hence thesis by A1;
end;
theorem
a|^m + b|^m <= c|^m implies ex x st a|^m + b|^m <= (a+x)|^m
proof
assume
A1: a|^m +b|^m <= c|^m;
then ex x st c = a + x by Th6,NAT_1:10;
hence thesis by A1;
end;
theorem Th13:
a1|^(m+1)-b1|^(m+1) = ((a1|^m+b1|^m)*(a1-b1) + (a1+b1)*(a1|^m-b1|^m))/2
proof
thus a1|^(m+1)-b1|^(m+1) =
((a1|^m+b1|^m)*(a1-b1) + (a1|^1+b1|^1)*(a1|^m-b1|^m))/2 by Th5
.= ((a1|^m+b1|^m)*(a1-b1) + (a1+b1)*(a1|^m-b1|^m))/2;
end;
Lm16: a1|^m - b1|^m = (a1-b1)*t implies
a1|^(m+1)-b1|^(m+1)=(a1-b1)*(t*(a1+b1)+a1|^m+b1|^m)/2
proof
assume a1|^m - b1|^m = (a1-b1)*t;
then a1|^(m+1)-b1|^(m+1) = ((a1|^m+b1|^m)*(a1-b1)
+ (a1+b1)*((a1-b1)*t))/2 by Th13;
hence thesis;
end;
Lm17: a1|^(m+1)-b1|^(m+1)=(a1-b1)*(t*(a1+b1)+a1|^m+b1|^m)/2 & a1+b1<>0
implies a1|^m - b1|^m = (a1-b1)*t
proof
assume
A1: a1|^(m+1)-b1|^(m+1)=(a1-b1)*(t*(a1+b1)+a1|^m+b1|^m)/2 & a1+b1<>0;
then ((a1|^m+b1|^m)*(a1-b1) + (a1+b1)*(a1|^m-b1|^m))/2 =
(a1-b1)*(t*(a1+b1)+a1|^m+b1|^m)/2 by Th13; then
(a1+b1)*(a1|^m-b1|^m) = (a1-b1)*t*(a1+b1);
hence thesis by A1,XCMPLX_1:5;
end;
theorem Th14:
a|^(m+1)-b|^(m+1)=(a-b)*(t*(a+b)+a|^m+b|^m)/2 iff
a|^m - b|^m = (a-b)*t
proof
a+b = 0 implies a|^m - b|^m = (a-b)*t
proof
assume a+b = 0; then
a = 0 & b =0;
hence thesis;
end;
hence thesis by Lm16,Lm17;
end;
theorem
(c1|^n/2+c1/2)|^2-(c1|^n/2-c1/2)|^2 = c1|^(n+1)
proof
set k = c1|^n/2+c1/2;
set l = c1|^n/2-c1/2;
k|^2 - l|^2 = k*k -l|^2 by NEWTON:81
.= k*k -l*l by NEWTON:81
.= c1*c1|^n
.= c1|^(n+1) by NEWTON:6;
hence thesis;
end;
Lm18d: n>0 & u-v is odd implies
u+v is odd & u|^n-v|^n is odd & u|^n+v|^n is odd
proof
(u is odd or u is even) & (v is odd or v is even);
hence thesis;
end;
Lm18e: u-v is even implies u+v is even & u|^n-v|^n is even
& u|^n+v|^n is even
proof
assume
A1: u-v is even;
per cases;
suppose
A2: u is even & v is even; then
(u|^n is even & v|^n is even) or n=0; then
A3a: (u|^n is even & v|^n is even) or (u|^n=1 & v|^n=1) by NEWTON:4;
then (u|^n-v|^n is even) or (u|^n-v|^n = 0);
hence thesis by A2,A3a;
end;
suppose u is odd & v is odd;
hence thesis;
end;
suppose u is odd & v is even;
hence thesis by A1;
end;
suppose u is even & v is odd;
hence thesis by A1;
end;
end;
theorem
a|^3-b|^3 = (a-b)*((a+b)*(a+b)+a|^2+b|^2)/2
proof
A1: a|^2 - b|^2 = (a-b)*(a+b) by Th1;
a|^3 - b|^3 = a|^(2+1)-b|^(2+1)
.=(a-b)*((a+b)*(a+b)+a|^2+b|^2)/2 by A1,Th14;
hence thesis;
end;
theorem Th17:
c|^m >= a|^m + b|^m & a>0 & b>0 implies
c|^(m+1) > a|^(m+1) + b|^(m+1)
proof
assume
A0: c|^m >= a|^m + b|^m & a>0 & b>0;
consider x be Nat such that
A0b: c = a + x by A0,Th6, NAT_1:10;
A1: (a+x)|^m >= a|^m + b|^m & a>0 & x>0 by A0,A0b,Lm5d;
A2a: a|^m > 0 by A0,PREPOWER:6; then
A3: (a+x)|^m > b|^m by A0,A0b,XREAL_1:39;
A4: a+x > b by A3,Lm3a;
A5: (a+x)|^m*(a+x) >= (a|^m + b|^m)*(a+x) by A0,A0b,XREAL_1:66;
A7: b|^m > 0 by A0,PREPOWER:6;
A8: a|^m*(a+x) > a|^m*a by A1,NAT_1:16,A2a,XREAL_1:68;
b|^m*(a+x) > b|^m*b by A4,A7,XREAL_1:68; then
a|^m*(a+x) + b|^m*(a+x) > a|^m*a + b|^m*b by A8,XREAL_1:8; then
A12: (a+x)|^m*(a+x) > a|^m*a + b|^m*b by A5, XXREAL_0:2;
a|^m*a = a|^(m+1) & b|^m*b = b|^(m+1) by NEWTON:6;
hence thesis by A0b,A12,NEWTON:6;
end;
theorem Th18:
c|^m >= a|^m + b|^m & a>0 & b>0 & k>0 implies
c|^(k+m) > a|^(k+m) + b|^(k+m)
proof
assume
A0: c|^m >= a|^m + b|^m & a>0 & b>0 & k>0;
then consider l such that
A0b: k = 1 + l by NAT_1:10,14;
defpred P[Nat] means c|^($1+m+1) >a|^($1+m+1)+b|^($1+m+1) & a>0 & b>0;
A1: P[0] by A0,Th17;
A2: P[x] implies P[x+1] by Th17;
for j holds P[j] from NAT_1:sch 2(A1,A2);
then c|^(l+m+1) > a|^(l+m+1) + b|^(l+m+1);
hence thesis by A0b;
end;
theorem
c|^m >= a|^m + b|^m implies
c|^(k+m) >= a|^(k+m) + b|^(k+m)
proof
assume
A0: c|^m >= a|^m + b|^m; then
A0a: m <> 0 by Lm0;
A0c: k = 0 implies thesis by A0;
per cases;
suppose
a = 0 or b = 0; then
A1: (a|^m = 0 or b|^m = 0) & (a|^(k+m) = 0 or b|^(k+m) = 0)
by A0a,NAT_1:14,NEWTON:11; then
c >= a & c >= b by A0,A0a,NAT_1:14,PREPOWER:10;
hence thesis by A1,Lm3a;
end;
suppose
a > 0 & b > 0;
hence thesis by A0,A0c,Th18;
end;
end;
Lm28:
c|^m > a|^m + b|^m & a>0 implies
c|^(m+1) > a|^(m+1) + b|^(m+1)
proof
assume
A1: c|^m > a|^m + b|^m & a>0; then
A2: m <> 0 by Lm0;
per cases;
suppose b = 0;
then b|^m = 0 & b|^(m+1) = 0 by A2,NEWTON:84;
hence thesis by A1,Lm4a;
end;
suppose b <> 0;
hence thesis by A1,Th18;
end;
end;
Lm29:
c|^m > a|^m + b|^m implies
c|^(m+1) > a|^(m+1) + b|^(m+1)
proof
assume
A1: c|^m > a|^m + b|^m; then
A2: m <> 0 by Lm0;
per cases;
suppose b = 0;
then b|^m = 0 & b|^(m+1) = 0 by A2,NEWTON:84;
hence thesis by A1,Lm4a;
end;
suppose b <> 0;
hence thesis by A1,Lm28;
end;
end;
theorem
c|^n > a|^n + b|^n implies
c|^(k+n) > a|^(k+n) + b|^(k+n)
proof
assume
AX: c|^n > a|^n + b|^n;
then n <> 0 by Lm0;
then consider m such that
AY: n = 1 + m by NAT_1:10,14;
defpred P[Nat] means c|^($1+m+1) >a|^($1+m+1)+b|^($1+m+1);
A1: P[0] by AX,AY;
A2: P[x] implies P[x+1] by Lm29;
for j holds P[j] from NAT_1:sch 2(A1,A2);
then c|^(k+m+1) > a|^(k+m+1) + b|^(k+m+1);
hence thesis by AY;
end;
theorem Th21:
a1|^(m+2) - b1|^(m+2) = (a1|^(m+1)+b1|^(m+1))*(a1-b1) + a1*b1*(a1|^m-b1|^m)
proof
(a1|^(m+1)+b1|^(m+1))*(a1-b1) + a1*b1*(a1|^m-b1|^m)
= a1|^(m+1)*a1+b1|^(m+1)*a1 -
a1|^(m+1)*b1 - b1|^(m+1)*b1 + a1*b1*(a1|^m-b1|^m)
.=a1|^(m+1+1)+b1|^(m+1)*a1 - a1|^(m+1)*b1 - b1|^(m+1)*b1
+ a1*b1*(a1|^m-b1|^m) by NEWTON:6
.=a1|^(m+2)+b1|^(m+1)*a1 - a1|^(m+1)*b1 - b1|^(m+1+1)
+ a1*b1*(a1|^m-b1|^m) by NEWTON:6
.=a1|^(m+2)+b1|^(m+1)*a1 - a1|^(m+1)*b1 -
b1|^(m+2)+ b1*(a1*a1|^m) - a1*b1*b1|^m
.=a1|^(m+2)+b1|^(m+1)*a1-a1|^(m+1)*b1 - b1|^(m+2)
+ b1*a1|^(m+1)-a1*(b1*b1|^m) by NEWTON:6
.=a1|^(m+2)+ b1|^(m+1)*a1 - b1|^(m+2) - a1*b1|^(m+1) by NEWTON:6;
hence thesis;
end;
theorem
a1|^(m+2) + b1|^(m+2) = (a1|^(m+1)-b1|^(m+1))*(a1-b1) + a1*b1*(a1|^m+b1|^m)
proof
(a1|^(m+1)-b1|^(m+1))*(a1-b1) + a1*b1*(a1|^m+b1|^m)
= a1|^(m+1)*a1-b1|^(m+1)*a1 -
a1|^(m+1)*b1 + b1|^(m+1)*b1 + a1*b1*(a1|^m+b1|^m)
.=a1|^(m+1+1) - b1|^(m+1)*a1 - a1|^(m+1)*b1 + b1|^(m+1)*b1
+ a1*b1*(a1|^m + b1|^m) by NEWTON:6
.=a1|^(m+2) - b1|^(m+1)*a1 - a1|^(m+1)*b1 + b1|^(m+1+1)
+ a1*b1*(a1|^m + b1|^m) by NEWTON:6
.=a1|^(m+2) - b1|^(m+1)*a1 - a1|^(m+1)*b1 + b1|^(m+2) +
b1*(a1*a1|^m) + a1*b1*b1|^m
.=a1|^(m+2)-b1|^(m+1)*a1-a1|^(m+1)*b1 + b1|^(m+2)
+ b1*a1|^(m+1)+a1*(b1*b1|^m) by NEWTON:6
.=a1|^(m+2)- b1|^(m+1)*a1 + b1|^(m+2) + a1*b1|^(m+1) by NEWTON:6;
hence thesis;
end;
theorem
a|^(2*m+2)-b|^(2*m+2) =
(a|^2-b|^2)*(c*(a|^2+b|^2)+a|^(2*m)+b|^(2*m))/2
iff a|^(2*m) - b|^(2*m) = (a|^2-b|^2)*c
proof
set k = a|^2; set l = b|^2;
A1: a|^(2*m)=(a|^2)|^m & b|^(2*m)=(b|^2)|^m by NEWTON:9;
A2: a|^(2*m+2) = a|^(2*(m+1))
.=(a|^2)|^(m+1) by NEWTON:9;
b|^(2*m+2) = b|^(2*(m+1))
.=(b|^2)|^(m+1) by NEWTON:9;
hence thesis by A1,A2,Th14;
end;
theorem
a1|^(2*m+3) + b1|^(2*m+3) = (a1|^(2*m+2)+b1|^(2*m+2))*(a1+b1)
- a1*b1*(a1|^(2*m+1)+b1|^(2*m+1))
proof
(a1|^(2*m+2)+b1|^(2*m+2))*(a1+b1) - a1*b1*(a1|^(2*m+1)+b1|^(2*m+1))
= a1*(a1|^(2*m+2)+b1|^(2*m+2))+b1*(a1|^(2*m+2)+b1|^(2*m+2))
- a1*b1*a1|^(2*m+1)-a1*(b1*b1|^(2*m+1))
.= a1*(a1|^(2*m+2)+b1|^(2*m+2))+b1*(a1|^(2*m+2)+b1|^(2*m+2))
- b1*(a1*a1|^(2*m+1))-a1*b1|^(2*m+1+1) by NEWTON:6
.= a1*(a1|^(2*m+2)+b1|^(2*m+2))+b1*(a1|^(2*m+2)+b1|^(2*m+2))
- b1*a1|^(2*m+1+1)-a1*b1|^(2*m+2) by NEWTON:6
.= a1*a1|^(2*m+2)+b1*b1|^(2*m+2)
.= a1|^(2*m+2+1)+b1*b1|^(2*m+2) by NEWTON:6
.=a1|^(2*m+3)+ b1|^(2*m+2+1) by NEWTON:6;
hence thesis;
end;
theorem
a1|^m - b1|^m = (a1-b1)*k implies
a1|^(m+2) - b1|^(m+2) = (a1|^(m+1)+b1|^(m+1) + a1*b1*k)*(a1-b1)
proof
assume a1|^m - b1|^m = (a1-b1)*k;
hence a1|^(m+2) - b1|^(m+2) =
(a1|^(m+1)+b1|^(m+1))*(a1-b1) + a1*b1*((a1-b1)*k) by Th21
.= (a1|^(m+1)+b1|^(m+1) + a1*b1*k)*(a1-b1);
end;
theorem
a1|^(m+2) - b1|^(m+2) = (a1|^(m+1)+b1|^(m+1) + a1*b1*k)*(a1-b1) & a1*b1<>0
implies a1|^m - b1|^m = (a1-b1)*k
proof
assume
A1: a1|^(m+2) - b1|^(m+2) =
(a1|^(m+1)+b1|^(m+1) + a1*b1*k)*(a1-b1) & a1*b1<>0; then
A5: (k*(a1-b1)*(a1*b1))/(a1*b1) = k*(a1-b1) by XCMPLX_1:89;
(a1|^(m+1)+b1|^(m+1))*(a1-b1) + a1*b1*(a1|^m-b1|^m) =
(a1|^(m+1)+b1|^(m+1))*(a1-b1) + a1*b1*k*(a1-b1) by A1,Th21;
hence thesis by A1,XCMPLX_1:89,A5;
end;
Lm56a: n>1 & b>0 & a>b implies (a|^n+b|^n)*(a-b) < a|^(n+1) - b|^(n+1)
proof
assume
A1: n > 1 & b>0 & a > b;
A2: a|^(n+1)=a*a|^n & b|^(n+1)=b*b|^n & a|^(m+1)=a*a|^m & b|^(m+1)=b*b|^m
by NEWTON:6;
consider m such that
A3: n = 1 + m by A1,NAT_1:10;
A3a: m >= 1 by A3,A1,NAT_1:13;
a|^m > b|^m by A1,A3a,PREPOWER:10; then
A3c: a|^m - b|^m > b|^m - b|^m by XREAL_1:9;
(a|^n+b|^n)*(a-b) = a|^(n+1) - b|^(n+1) + a*b|^n - b*a|^n by A2
.= a|^(n+1) - b|^(n+1) + a*(b|^(m+1)) - b*(a*a|^m) by NEWTON:6,A3
.= a|^(n+1) - b|^(n+1) + a*(b*b|^m) - b*(a*a|^m) by NEWTON:6
.= a|^(n+1) - b|^(n+1) - a*b*(a|^m - b|^m);
hence thesis by A1,A3c,XREAL_1:44;
end;
Lm57: n>0 & a>b implies (a|^n-b|^n)*(a+b) >= a|^(n+1) - b|^(n+1)
proof
assume
A1: n>0 & a > b;
A2: 0 <= a|^m - b|^m by A1,Lm3a,XREAL_1:48;
A2b: a|^(n+1)=a*a|^n & b|^(n+1)=b*b|^n & a|^(m+1)=a*a|^m & b|^(m+1)=b*b|^m
by NEWTON:6;
consider m such that
A3: n = 1 + m by A1,NAT_1:14,NAT_1:10;
A4: (a|^n-b|^n)*(a+b) = a|^(n+1) - b|^(n+1) - a*b|^n + b*a|^n by A2b
.= a|^(n+1) - b|^(n+1) - a*(b|^(m+1)) + b*(a*a|^m) by NEWTON:6,A3
.= a|^(n+1) - b|^(n+1) - a*(b*b|^m) + b*(a*a|^m) by NEWTON:6
.= a|^(n+1) - b|^(n+1) + a*b*(a|^m - b|^m);
a|^m - b|^m in NAT by A2,INT_1:3;
hence thesis by A4, XREAL_1:40;
end;
Lm57d: b>0 & a>b & (a|^n-b|^n)*(a+b) = (a|^n+b|^n)*(a-b) implies n=1
proof
assume
A0: b>0 & a>b & (a|^n - b|^n)*(a+b) = (a|^n+b|^n)*(a-b);
A1: a|^0 = 1 & b|^0 = 1 by NEWTON:4;
per cases;
suppose n=0;
then 0*(a+b) = 2*(a-b) by A0,A1;
hence thesis by A0;
end;
suppose
A20: n>0; then
A20a: n >=1 by NAT_1:14;
a|^(n+1) - b|^(n+1) <= (a|^n+b|^n)*(a-b) by A0,A20,Lm57;
then n <=1 by A0,Lm56a;
hence thesis by A20a,XXREAL_0:1;
end;
end;
theorem
b>0 & a>b implies
((a|^n-b|^n)*(a+b) = (a|^n+b|^n)*(a-b) iff n=1) by Lm57d;
theorem
n>1 & b>0 & a>b implies (a|^n-b|^n)*(a+b) > a|^(n+1) - b|^(n+1)
proof
assume
A1: n>1 & b>0 & a>b;
A2: a|^(n+1)=a*a|^n & b|^(n+1)=b*b|^n & a|^(m+1)=a*a|^m & b|^(m+1)=b*b|^m
by NEWTON:6;
consider m such that
A3: n = 1 + m by A1,NAT_1:10;
A3a: m >= 1 by A3,A1,NAT_1:13;
A3b: a|^m > b|^m by A1,A3a,PREPOWER:10;
A3c: a|^m - b|^m > b|^m - b|^m by A3b, XREAL_1:9;
(a|^n-b|^n)*(a+b) = a|^(n+1) - b|^(n+1) - a*b|^n + b*a|^n by A2
.= a|^(n+1) - b|^(n+1) - a*(b|^(m+1)) + b*(a*a|^m) by NEWTON:6,A3
.= a|^(n+1) - b|^(n+1) - a*(b*b|^m) + b*(a*a|^m) by NEWTON:6
.= a|^(n+1) - b|^(n+1) + a*b*(a|^m - b|^m);
hence thesis by A1,A3c,XREAL_1:39;
end;
theorem
n>0 & a>b implies (a|^n+b|^n)*(a-b) <= a|^(n+1) - b|^(n+1)
proof
assume
A1: n>0 & a > b; then
A2: 0 <= a|^m - b|^m by Lm3a,XREAL_1:48;
A2b: a|^(n+1)=a*a|^n & b|^(n+1)=b*b|^n & a|^(m+1)=a*a|^m & b|^(m+1)=b*b|^m
by NEWTON:6;
consider m such that
A3: n = 1 + m by A1,NAT_1:14,NAT_1:10;
A4: (a|^n+b|^n)*(a-b) = a|^(n+1) - b|^(n+1) + a*b|^n - b*a|^n by A2b
.= a|^(n+1) - b|^(n+1) + a*(b|^(m+1)) - b*(a*a|^m) by NEWTON:6,A3
.= a|^(n+1) - b|^(n+1) + a*(b*b|^m) - b*(a*a|^m) by NEWTON:6
.= a|^(n+1) - b|^(n+1) - a*b*(a|^m - b|^m);
a|^m - b|^m in NAT by A2,INT_1:3;
hence thesis by A4,XREAL_1:43;
end;
Lm18b: a-b divides a|^0-b|^0
proof
a|^0-b|^0 = 1-b|^0 by NEWTON:4 .=1-1 by NEWTON:4;
hence thesis by INT_2:12;
end;
Lm18f: n>0 & a-b divides a|^n-b|^n implies
a-b divides a|^(n+1)-b|^(n+1)
proof
assume
A1: n>0 & (a-b) divides (a|^n-b|^n);
consider q being Integer such that
A3: a|^n-b|^n=(a-b)*q by A1;
per cases;
suppose
a-b is even; then
A5: a+b is even & a|^n+b|^n is even & a|^n-b|^n is even by Lm18e; then
consider l be Integer such that
A6: (a+b)=2*l;
consider k be Integer such that
A7: (a|^n+b|^n)=2*k by A5;
a|^(n+1)-b|^(n+1) = (2*k*(a-b)+2*l*(a|^n-b|^n))/2 by Th13,A6,A7
.=k*(a-b)+l*(a|^n-b|^n)
.=k*(a-b)+l*((a-b)*q) by A3
.=(a-b)*(k+l*q);
hence thesis;
end;
suppose
A12: a-b is odd; then
A13: a+b is odd & a|^n+b|^n is odd & a|^n-b|^n is odd
& a|^(n+1)-b|^(n+1) is odd by A1,Lm18d;
q is odd by A3,A1,A12,Lm18d; then
consider m be Integer such that
A18: 2*m=((a|^n+b|^n) + (a+b)*q) by A13,ABIAN:11;
a|^(n+1)-b|^(n+1) = ((a|^n+b|^n)*(a-b) + (a+b)*((a-b)*q))/2 by Th13,A3
.= (a-b)*((a|^n+b|^n) + (a+b)*q)/2
.= (a-b)*(2*m)/2 by A18
.= (a-b)*m;
hence thesis;
end;
end;
Lm46: m > 0 implies 2*a divides a|^m + a|^m
proof
assume m > 0; then
a divides a|^m by NAT_3:3;
then 2*a divides 2*a|^m by NAT_3:1;
hence thesis;
end;
theorem Th29:
p+q divides p*u + q*v implies p+q divides p*(u+z) + q*(v+z)
proof
assume p+q divides p*u + q*v; then
consider t be Integer such that
A2: (p+q)*t = p*u + q*v;
p*(u+z) + q*(v+z) = (p+q)*(t+z) by A2;
hence thesis;
end;
theorem
p+q divides p*(t*(p+q)+z) + q*z
proof
A1: z = q*t*0+z;
p*(t*(p+q)) + q*(t*0) = p*t*(p+q) + q*t*0;
hence thesis by A1,INT_1:def 3,Th29;
end;
theorem Th31:
p+q divides u-v implies p+q divides p*(u+t) + q*(v+t)
proof
set z = u-v;
assume p+q divides u-v; then
p+q divides p*z + q*0 by INT_2:2;
then p+q divides p*(z+(v+t)) + q*(0+(v+t)) by Th29;
hence thesis;
end;
theorem Th32:
a-b divides a|^n-b|^n
proof
defpred P[Nat] means a-b divides a|^$1 -b|^$1;
A1: P[0] by Lm18b;
A2: P[x] implies P[x+1]
proof
x = 0 or x > 0;
hence thesis by Lm18f;
end;
for m holds P[m] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th33:
a|^2-b|^2 divides a|^(2*m)-b|^(2*m)
proof
a|^(2*m)=(a|^2)|^m & b|^(2*m)=(b|^2)|^m by NEWTON:9;
hence thesis by Th32;
end;
theorem Th34:
a+b divides a|^(2*m+1) + b|^(2*m+1)
proof
A2: a|^(2*m+2) - b|^(2*m+2)
= (a|^(2*m+1)+b|^(2*m+1))*(a-b) + a*b*(a|^(2*m)-b|^(2*m)) by Th21;
set n=m+1;
consider t be Integer such that
A4: a|^(2*m)-b|^(2*m) = (a|^2-b|^2)*t by Th33,INT_1:def 3;
consider z be Integer such that
A4a: a|^(2*n)-b|^(2*n) = (a|^2-b|^2)*z by Th33,INT_1:def 3;
A5: (a-b)*(a|^(2*m+1)+b|^(2*m+1))
= a|^(2*m+2) - b|^(2*m+2) - a*b*(a|^(2*m)-b|^(2*m)) by A2
.= a|^(2*n) - b|^(2*n) - a*b*((a|^2-b|^2)*t) by A4
.= (a|^2-b|^2)*(z -a*b*t) by A4a
.= (a-b)*(a+b)*(z -a*b*t) by Th1
.= (a-b)*((a+b)*(z -a*b*t));
X: 2*a = a+a;
a|^(2*m+1)+b|^(2*m+1) = (a+b)*(z-a*b*t) or a-b = 0 by A5,XCMPLX_1:5;
hence thesis by Lm46,X;
end;
Lm44: a+b divides a|^2-b|^2
proof
a|^2-b|^2 = (a+b)*(a-b) by Th1;
hence thesis;
end;
theorem
a+b divides a|^(2*m) - b|^(2*m)
proof
A1: a+b divides a|^2-b|^2 by Lm44;
a|^2-b|^2 divides a|^(2*m)-b|^(2*m) by Th33;
hence thesis by A1,INT_2:9;
end;
theorem
a+b divides a|^n - b|^n implies
a+b divides a|^(n+1) + b|^(n+1)
proof
assume a+b divides a|^n - b|^n; then
a+b divides a*(a|^n+0) + b*(b|^n+0) by Th31; then
a+b divides a|^(n+1) + b*b|^n by NEWTON:6;
hence thesis by NEWTON:6;
end;
theorem
a+b divides a|^n+b|^n or a+b divides a|^n-b|^n
proof
per cases;
suppose n is odd;
then ex k be Nat st n=2*k+1 by ABIAN:9;
hence thesis by Th34;
end;
suppose n is even;
then consider m be Nat such that
A2: n = 2*m;
A3: a+b divides a|^2 - b|^2 by Lm44;
a|^2-b|^2 divides a|^(2*m) - b|^(2*m) by Th33;
hence thesis by A2,A3,INT_2:9;
end;
end;
theorem
a>=b & c|^n - b|^n = a|^n implies (c-b) gcd (a|^n) = c-b &
(c-a) gcd b|^n = c-a
proof
assume
A1: a>=b & c|^n - b|^n = a|^n;
A1a: c|^n = b|^n + a|^n by A1; then
A1c: c - b >= a - b by Th6,XREAL_1:9;
a - b >= b - b by A1,XREAL_1:9; then
A1f: c - b in NAT by A1c,INT_1:3;
c - a >= a - a by A1a,Th6,XREAL_1:9; then
A1i: c - a in NAT by INT_1:3;
c-a divides c|^n - a|^n by Th32;
hence thesis by A1,A1i,A1f,Th32,NEWTON:49;
end;
theorem
a,b are_coprime & a+b divides a*c + b*d implies a+b divides c-d
proof
assume
A1: a,b are_coprime & a+b divides a*c + b*d;
set u = a*c; set v = -b*d;
A1a: a+b divides u - v by A1;
A2: a+b divides a*(u+0) + b*(v+0) by A1a,Th31;
consider t such that
A4: a*a*c - b*b*d = (a+b)*t by A2;
A6: (a*b)*(c-d) = (a*c-b*d-t)*(a+b) by A4;
a,a+b are_coprime & b,(a+b) are_coprime by A1,EULER_1:7; then
a*b,a+b are_coprime by WSIERP_1:6;
hence thesis by A6,INT_1:def 3,WSIERP_1:29;
end;
theorem Th40:
a*b,c*d are_coprime implies a,c are_coprime
proof
assume
A1: a*b, c*d are_coprime;
A3: a gcd c divides a*b by INT_2:2,21;
a gcd c divides c*d by INT_2:2,21;
hence a, c are_coprime by A1,A3,WSIERP_1:15,INT_2:22;
end;
Lm53: a|^(k+1),b|^(m+1) are_coprime implies a,b are_coprime
proof
a|^(k+1) = a*a|^k & b|^(m+1) = b*b|^m by NEWTON:6;
hence thesis by Th40;
end;
Lm58: a>0 & b>0 & a|^n + b|^n = c|^n implies
ex j,k,l st j|^n + k|^n = l|^n & j,k are_coprime
& a = (a gcd b)*j & b = (a gcd b)*k & c = (a gcd b)*l
proof
set x = a gcd b;
assume
A1: a>0 & b>0 & a|^n + b|^n = c|^n; then
A1b: n<>0 by Lm0;
x<>0 by A1,INT_2:5; then
A1d: x|^n>0 by PREPOWER:6;
consider j,k be Integer such that
A2: a = (a gcd b)*j & b = (a gcd b)*k & j,k are_coprime by A1,INT_2:23;
j>0 & k>0 by A1,A2; then
A2b: j in NAT & k in NAT by INT_1:3;
A3: a|^n = x|^n*j|^n by A2,NEWTON:7;
A4: b|^n = x|^n*k|^n by A2,NEWTON:7; then
c|^n = x|^n*(j|^n + k|^n) by A1,A3; then
x divides c by A1b,INT_1:def 3,WSIERP_1:26; then
consider l such that
A8: c = x*l by NAT_D:def 3;
(j|^n + k|^n)*x|^n = l|^n*x|^n by A1,A3,A4,A8,NEWTON:7; then
j|^n + k|^n = l|^n by A1d,XCMPLX_1:5;
hence thesis by A2,A2b,A8;
end;
Lm59: j|^(m+1) + k|^(m+1) = l|^(m+1) & j,k are_coprime implies
j,l are_coprime
proof
set n=m+1;
assume
A1: j|^n + k|^n = l|^n & j,k are_coprime; then
j|^n gcd k|^n = 1 by WSIERP_1:11,INT_2:def 3; then
l|^n,j|^n are_coprime by A1,EULER_1:7;
hence thesis by Lm53;
end;
theorem Th41:
a>0 & b>0 & a|^n + b|^n = c|^n implies
ex j,k,l st j|^n + k|^n = l|^n & j,k are_coprime
& j,l are_coprime & k,l are_coprime
& a = (a gcd b)*j & b = (a gcd b)*k & c = (a gcd b)*l
proof
assume
A1: a>0 & b>0 & a|^n + b|^n = c|^n;
then n <> 0 by Lm0;
then consider m such that
A3: n = 1+m by NAT_1:10,14;
consider j,k,l such that
A4: j|^(m+1) + k|^(m+1) = l|^(m+1) & j,k are_coprime
& a = (a gcd b)*j & b = (a gcd b)*k & c = (a gcd b)*l by A1,A3,Lm58;
j,l are_coprime & k,l are_coprime by A4,Lm59;
hence thesis by A3,A4;
end;
:: addenda
Lm60:
a = 1 implies a|^(n+2) + a|^(n+2) <> b|^(n+2)
proof
assume
A1: a = 1;
A5: 2+0 <= 2+n by XREAL_1:6;
assume
A2: not thesis;
2+n < 2|^(2+n) by NEWTON:86;
then b|^(2+n) > 1|^(2+n) & b|^(2+n) < 2|^(2+n) by A1,A5,A2,XXREAL_0:2;
then b > 1 & b < 1+1 by Lm3a;
hence contradiction by NAT_1:13;
end;
theorem
a>0 implies a|^(n+2) + a|^(n+2) <> b|^(n+2)
proof
assume
A1: a>0;
assume not thesis;
then consider j,k,l such that
A3: j|^(n+2) + k|^(n+2) = l|^(n+2) & j,k are_coprime
& j,l are_coprime & k,l are_coprime
& a = (a gcd a)*j & a = (a gcd a)*k & b = (a gcd a)*l by A1,Th41;
k*a = 1*a & j*a = 1*a by NAT_D:32,A3; then
k = 1 & j = 1 by A1,XCMPLX_1:5;
hence contradiction by A3,Lm60;
end;
Lm61: a1 + b1|^2 = c1|^2 implies
a1 + (b1+d1)|^2 - (c1+d1)|^2 = 2*d1*(b1-c1)
proof
assume
A1: a1 + b1|^2 = c1|^2;
a1 + (b1 + d1)|^2 - (c1+d1)|^2 =
a1 + (b1|^2 + 2*b1*d1 + d1|^2) - (c1+d1)|^2 by Lm10
.= a1 + b1|^2 + 2*b1*d1 + d1|^2 - (c1|^2 + 2*c1*d1 + d1|^2) by Lm10
.= 2*b1*d1 - 2*c1*d1 by A1;
hence thesis;
end;
theorem
x>0 & b < c & a +b|^2 = c|^2 implies a + (b+x)|^2 < (c+x)|^2
proof assume
A1: x>0 & b < c & a +b|^2 = c|^2; then
A1a: b - c < c - c by XREAL_1:9;
a + (b+x)|^2 - (c+x)|^2 = 2*x*(b-c) by A1,Lm61; then
a + (b+x)|^2 - (c+x)|^2 + (c+x)|^2 < 0+ (c+x)|^2 by A1,A1a,XREAL_1:6;
hence thesis;
end;
theorem Th44:
q < 0 & b < c & a|^2 +b|^2 = c|^2 implies
a|^2 + (b+q)|^2 > (c+q)|^2
proof assume
A1: q < 0 & b < c & a|^2 +b|^2 = c|^2; then
A1a: b - c < c - c by XREAL_1:9;
a|^2 + (b+q)|^2 - (c+q)|^2 = 2*q*(b-c) by A1,Lm61; then
a|^2 + (b+q)|^2 - (c+q)|^2 + (c+q)|^2 > 0+ (c+q)|^2 by A1,A1a,XREAL_1:6;
hence thesis;
end;
theorem
x>0 & a|^2 +b|^2 = (b+1)|^2 implies a|^2 + (b-x)|^2 > (b+1-x)|^2
proof
A0: b+1 > b+0 by XREAL_1:6;
assume
A1: x>0 & a|^2 +b|^2 = (b+1)|^2;
consider q such that
A2: q = -x;
a|^2 + (b+q)|^2 > (b+1+q)|^2 by A0,A1,A2,Th44;
hence thesis by A2;
end;
theorem Th46:
a>=1 & (a+1)|^2 + ((a+1)+x)|^2 <= ((a+1)+x+1)|^2 implies
a|^2 + (a+x)|^2 < (a+x+1)|^2
proof
A2: (a+x+1)|^2 = a|^2+x|^2+1|^2 + 2*a*x + 2*a*1 + 2*x*1 by SERIES_4:1
.= a|^2 + x|^2 + 2*a*x + 2*x + 2*a + 1;
A3: (a+x+2)|^2 = a|^2+x|^2 + 2|^2 + 2*a*x + 2*a*2 + 2*x*2 by SERIES_4:1
.= 2*a*2 + 2*x + 2*x + 2|^2 + a|^2 + 2*a*x + x|^2;
A4: (a+x)|^2 = a|^2 + 2*a*x + x|^2 by Lm10;
assume
A5: a>=1 & (a+1)|^2 + ((a+1)+x)|^2 <= ((a+1)+x+1)|^2; then
A5a: (a+1)|^2 + (a+x+1)|^2 -(a+x+2)|^2 <=
(a+x+2)|^2 -(a+x+2)|^2 by XREAL_1:9;
-((a+1)|^2 + (a+x+1)|^2 -(a+x+2)|^2) =
(a+x+2)|^2 - ((a+1)|^2 + (a+x+1)|^2)
.= a|^2 + x|^2 + 2|^2 + 2*a*x + 2*2*a + 2*x + 2*x -
((a|^2 + 2*a + 1) + (a|^2 + x|^2 + 1|^2 + 2*a*x + 2*a*1 + 2*x*1))
by Lm10,A2,A3
.= 2|^2 + 2*x - 1 - a|^2 - 1*1
.= 2*2 + 2*x - 1 -a|^2 - 1 by WSIERP_1:1; then
A6: (a|^2 + (a+x)|^2) + 0 <=
(a|^2 + (a+x)|^2) + (4 + 2*x - a|^2 - 2) by A5a,XREAL_1:6;
A7: a + 1 > 0 + 1 & a + 1 >= 1 + 1 by A5, XREAL_1:6; then
a + (a + 1) > a + (1 + 0) by XREAL_1:6; then
2*a + 1 > 1 + 1 by A7,XXREAL_0:2; then
(a|^2 + x|^2 + 2*a*x + 2*x) + (2*a + 1) >
(a|^2 + x|^2 + 2*a*x + 2*x) + 2 by XREAL_1:6;
hence thesis by A2,A4,A6,XXREAL_0:2;
end;
theorem Th47:
a>=1 & a|^2 + (a+x)|^2 >= (a+x+1)|^2 implies
(a+l+1)|^2 + (a+l+1+x)|^2 > (a+l+1+x+1)|^2
proof
assume
A1: a>=1 & a|^2 + (a+x)|^2 >= (a+x+1)|^2;
defpred P[Nat] means (a+$1+1)|^2 + ((a+$1+1)+x)|^2 > ((a+$1+1)+x+1)|^2;
A2: P[0] by A1,Th46;
A3: P[k] implies P[k+1]
proof
assume
A4: P[k];
(a+k)+1 >= 0+1 by XREAL_1:6;
hence thesis by A4,Th46;
end;
for j holds P[j] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
Lm120:
a|^2 + a|^2 > (a+1)|^2 implies a >= 3
proof
L1: (a-1)|^2 = (a+(-1))|^2
.= a|^2 + 2*a*(-1) + (-1)|^2 by Lm10
.= a|^2 + 2*a*(-1) + (-1)*(-1) by NEWTON:81;
assume
A1: a|^2 + a|^2 > (a+1)|^2; then
a|^2 > 0; then
a|^2 > 0|^2 by NEWTON:11; then
a - 1 >= 1 - 1 by NAT_1:14,XREAL_1:9; then
A2: a - 1 in NAT by INT_1:3;
(a+1)|^2 = a|^2 + 2*a*1 + 1|^2 by Lm10
.= a|^2 + 2*a + 1; then
a|^2 + a|^2 - (a|^2 + 2*a - 1) >
a|^2 + 2*a + 1 - (a|^2 + 2*a - 1) by A1,XREAL_1:9; then
(a-1)|^2 > 1|^2 by L1,XXREAL_0:2; then
(a - 1) + 1 > 1 + 1 by A2,Lm3a,XREAL_1:6; then
a >= 2 + 1 by NAT_1:13;
hence thesis;
end;
theorem
a >= 3 iff a|^2 + a|^2 > (a+1)|^2
proof
a >= 3 implies a|^2 + a|^2 > (a+1)|^2
proof
assume a >= 3; then
consider b such that
A2: a = 3 + b by NAT_1:10;
defpred P[Nat] means (3+$1)|^2 + (3+$1)|^2 > (3+$1+1)|^2;
A3: P[0]
proof
3|^2 = 3*3 & 4|^2 = 4*4 by NEWTON:81;
hence thesis;
end;
A4: P[k] implies P[k+1]
proof
assume P[k]; then
1+(2+k) >= 1+0 & (3+k)|^2 + ((3+k)+0)|^2 > ((3+k)+0+1)|^2
by XREAL_1:6; then
((3+k)+1)|^2 + ((3+k)+0+1)|^2 > ((3+k)+1+0+1)|^2 by Th47;
hence thesis;
end;
for m holds P[m] from NAT_1:sch 2(A3,A4);
hence thesis by A2;
end;
hence thesis by Lm120;
end;
theorem
2|^(3+m) + 2|^(3+m) < 3|^(3+m)
proof
A4: 2|^(2+1) + 2|^(2+1) = 2*2|^(2+1)
.= 2*(2*2|^2) by NEWTON:6 .= 2*(2*2*2) by NEWTON:81;
A5: 3|^(2+1) = 3*3|^2 by NEWTON:6 .= 3*3*3 by NEWTON:81;
A6: 2|^(3+m) = 2|^3 * 2|^m & 3|^(3+m) = 3|^3 * 3|^m by NEWTON:8;
2|^m <= 3|^m by Lm3a; then
A7: ((2|^3)+(2|^3))*(2|^m) <= ((2|^3)+(2|^3))*(3|^m) by XREAL_1:64;
3|^m > 0 by PREPOWER:6; then
((2|^3)+(2|^3))*(3|^m) < (3|^3)*(3|^m) by A4,A5,XREAL_1:68;
hence thesis by XXREAL_0:2,A6,A7;
end;