:: Polygonal Numbers
:: by Adam Grabowski
::
:: Received May 19, 2013
:: Copyright (c) 2013-2016 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 ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2,
INT_1, SQUARE_1, SEQ_1, NUMPOLY1, REALSET1, SERIES_1, POWER, SEQ_2,
ASYMPT_1, FUNCT_7, CARD_1, EUCLID_3, GR_CY_3, ABIAN, TOPGEN_1, FINSET_1,
TARSKI, PYTHTRIP, EC_PF_2, NEWTON, XXREAL_0, ORDINAL4, XBOOLE_0, REAL_1,
INT_2, NAT_1, XREAL_0, CARD_3, XCMPLX_0, ORDINAL1, SUBSET_1, ZFMISC_1,
NUMBERS;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
VALUED_1, ZFMISC_1, SQUARE_1, INT_1, INT_2, XREAL_0, FUNCT_1, FINSET_1,
FINSEQ_1, FUNCOP_1, NEWTON, NAT_D, SEQ_1, SEQ_2, FINSEQ_2, RVSUM_1,
SERIES_1, POWER, ABIAN, PYTHTRIP, PEPIN, GR_CY_3, NAT_5, EC_PF_2;
constructors SEQ_1, COMSEQ_2, GR_CY_3, NAT_5, ABIAN, EC_PF_2, MOEBIUS1,
RVSUM_1, SERIES_1, SEQ_2, REAL_1, PEPIN, POLYEQ_3, RELSET_1, NAT_D,
PYTHTRIP, FINSET_1;
registrations RELSET_1, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1,
RVSUM_1, XXREAL_0, NAT_2, NEWTON, SEQ_1, XCMPLX_0, NUMBERS, SEQ_2, POWER,
ABIAN, PYTHTRIP, SQUARE_1, ORDINAL1, XBOOLE_0, FUNCT_2, VALUED_0,
VALUED_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
begin :: Preliminaries
scheme :: NUMPOLY1:sch 1
LNatRealSeq {F(set) -> Real}:
(ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2);
theorem :: NUMPOLY1:1
for n, a being non zero Nat holds
1 <= a * n;
registration let n be Integer;
cluster n * (n - 1) -> even;
cluster n * (n + 1) -> even;
end;
theorem :: NUMPOLY1:2
for n being even Integer holds
n / 2 is Integer;
registration let n be even Nat;
cluster n / 2 -> natural;
end;
registration let n be odd Nat;
cluster n - 1 -> natural;
end;
registration let n be odd Nat;
cluster n - 1 -> even;
end;
reserve n,s for Nat;
theorem :: NUMPOLY1:3
n mod 5 = 0 or ... or n mod 5 = 4;
theorem :: NUMPOLY1:4 ::: NTALGO_1:8, 9 should be improved
for k be Nat st k <> 0 holds n, n mod k are_congruent_mod k;
theorem :: NUMPOLY1:5
n, 0 are_congruent_mod 5 or ... or n, 4 are_congruent_mod 5;
theorem :: NUMPOLY1:6
not n * n + n, 4 are_congruent_mod 5;
theorem :: NUMPOLY1:7
not n * n + n, 3 are_congruent_mod 5;
theorem :: NUMPOLY1:8
n mod 10 = 0 or ... or n mod 10 = 9;
theorem :: NUMPOLY1:9
n, 0 are_congruent_mod 10 or ... or n, 9 are_congruent_mod 10;
registration
cluster non trivial -> 2_or_greater for Nat;
cluster 2_or_greater -> non trivial for Nat;
end;
registration
cluster 4_or_greater -> 3_or_greater non zero for Nat;
end;
registration
cluster 4_or_greater -> non trivial for Nat;
end;
registration
cluster 4_or_greater for Nat;
cluster 3_or_greater for Nat;
end;
begin :: Triangular Numbers
definition let n be Nat;
func Triangle n -> Real equals
:: NUMPOLY1:def 1
Sum idseq n;
end;
definition let n be object;
attr n is triangular means
:: NUMPOLY1:def 2
ex k being Nat st n = Triangle k;
end;
registration let n be zero number;
cluster Triangle n -> zero;
end;
theorem :: NUMPOLY1:10
Triangle (n + 1) = (Triangle n) + (n + 1);
theorem :: NUMPOLY1:11
Triangle 1 = 1;
theorem :: NUMPOLY1:12
Triangle 2 = 3;
theorem :: NUMPOLY1:13
Triangle 3 = 6;
theorem :: NUMPOLY1:14
Triangle 4 = 10;
theorem :: NUMPOLY1:15
Triangle 5 = 15;
theorem :: NUMPOLY1:16
Triangle 6 = 21;
theorem :: NUMPOLY1:17
Triangle 7 = 28;
theorem :: NUMPOLY1:18
Triangle 8 = 36;
theorem :: NUMPOLY1:19
Triangle n = n * (n + 1) / 2;
theorem :: NUMPOLY1:20
Triangle n >= 0;
registration let n be Nat;
cluster Triangle n -> non negative;
end;
registration let n be non zero Nat;
cluster Triangle n -> positive;
end;
registration let n be Nat;
cluster Triangle n -> natural;
end;
theorem :: NUMPOLY1:21
Triangle (n -' 1) = n * (n - 1) / 2;
registration
cluster triangular -> natural for number;
end;
registration
cluster triangular non zero for number;
end;
theorem :: NUMPOLY1:22
for n being triangular number holds
not n, 7 are_congruent_mod 10;
theorem :: NUMPOLY1:23
for n being triangular number holds
not n, 9 are_congruent_mod 10;
theorem :: NUMPOLY1:24
for n being triangular number holds
not n, 2 are_congruent_mod 10;
theorem :: NUMPOLY1:25
for n being triangular number holds
not n, 4 are_congruent_mod 10;
theorem :: NUMPOLY1:26
for n being triangular number holds
n, 0 are_congruent_mod 10 or
n, 1 are_congruent_mod 10 or
n, 3 are_congruent_mod 10 or
n, 5 are_congruent_mod 10 or
n, 6 are_congruent_mod 10 or
n, 8 are_congruent_mod 10;
begin :: Polygonal Numbers
definition let s, n be natural Number;
func Polygon (s,n) -> Integer equals
:: NUMPOLY1:def 3
(n ^2 * (s - 2) - n * (s - 4)) / 2;
end;
theorem :: NUMPOLY1:27
s >= 2 implies Polygon (s,n) is natural;
theorem :: NUMPOLY1:28
Polygon (s,n) = (n * (s - 2) * (n - 1)) / 2 + n;
definition let s be Nat;
let x be object;
attr x is s-gonal means
:: NUMPOLY1:def 4
ex n being Nat st x = Polygon (s,n);
end;
definition let x be object;
attr x is polygonal means
:: NUMPOLY1:def 5
ex s being Nat st x is s-gonal;
end;
theorem :: NUMPOLY1:29
Polygon (s,1) = 1;
theorem :: NUMPOLY1:30
Polygon (s,2) = s;
registration let s be Nat;
cluster s-gonal for number;
end;
registration let s be non zero Nat;
cluster non zero s-gonal for number;
end;
registration let s be Nat;
cluster s-gonal -> real for number;
end;
registration let s be non trivial Nat;
cluster s-gonal -> natural for number;
end;
theorem :: NUMPOLY1:31
Polygon (s,n + 1) - Polygon (s,n) = (s - 2) * n + 1;
definition let s be Nat, x be s-gonal number;
func IndexPoly (s,x) -> Real equals
:: NUMPOLY1:def 6
(sqrt (((8 * s - 16) * x) + (s - 4) ^2) + s - 4) / (2 * s - 4);
end;
theorem :: NUMPOLY1:32
for s being non zero Nat, x be non zero s-gonal number
st x = Polygon (s,n) holds
((8*s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2;
theorem :: NUMPOLY1:33
for s being non zero Nat, x be non zero s-gonal number st s >= 4 holds
((8*s - 16) * x) + (s - 4) ^2 is square;
theorem :: NUMPOLY1:34
for s being non zero Nat,
x being non zero s-gonal number st s >= 4 holds
IndexPoly (s,x) in NAT;
theorem :: NUMPOLY1:35
for s being non trivial Nat,
x being s-gonal number holds
0 <= ((8 * s - 16) * x) + (s - 4) ^2;
theorem :: NUMPOLY1:36
for n being odd Nat st s >= 2 holds
n divides Polygon (s,n);
begin :: Centered Polygonal Numbers
::$N Centered polygonal number
definition let s, n be Nat;
func CenterPolygon (s,n) -> Integer equals
:: NUMPOLY1:def 7
(s * n) / 2 * (n - 1) + 1;
end;
registration let s be Nat;
let n be non zero Nat;
cluster CenterPolygon (s,n) -> natural;
end;
theorem :: NUMPOLY1:37
CenterPolygon (0,n) = 1;
theorem :: NUMPOLY1:38
CenterPolygon (s,0) = 1;
theorem :: NUMPOLY1:39
CenterPolygon (s,n) = s * (Triangle (n -' 1)) + 1;
begin :: On the Connection between Triangular and Other Polygonal Numbers
theorem :: NUMPOLY1:40
Triangle n = Polygon (3, n);
theorem :: NUMPOLY1:41
for n being odd Nat holds
n divides Triangle n;
theorem :: NUMPOLY1:42
Triangle n <= Triangle (n + 1);
theorem :: NUMPOLY1:43
for k being Nat st k <= n holds
Triangle k <= Triangle n;
theorem :: NUMPOLY1:44
n <= Triangle n;
theorem :: NUMPOLY1:45
for n being non trivial Nat holds
n < Triangle n;
theorem :: NUMPOLY1:46
n <> 2 implies Triangle n is non prime;
registration let n be 3_or_greater Nat;
cluster Triangle n -> non prime;
end;
registration
cluster triangular -> non prime for 4_or_greater Nat;
end;
registration let s be 4_or_greater non zero Nat,
x be non zero s-gonal number;
cluster IndexPoly (s,x) -> natural;
end;
theorem :: NUMPOLY1:47
for s being 4_or_greater Nat,
x being non zero s-gonal number st s <> 2 holds
Polygon (s, IndexPoly (s,x)) = x;
theorem :: NUMPOLY1:48
36 is square triangular;
registration let n be Nat;
cluster Polygon (3,n) -> natural;
end;
registration let n be Nat;
cluster Polygon (3,n) -> triangular;
end;
theorem :: NUMPOLY1:49
Polygon (s,n) = (s - 2) * Triangle (n -' 1) + n;
theorem :: NUMPOLY1:50
Polygon (s,n) = (s - 3) * Triangle (n -' 1) + Triangle n;
theorem :: NUMPOLY1:51
Polygon (0,n) = n * (2 - n);
theorem :: NUMPOLY1:52
Polygon (1,n) = n * (3 - n) / 2;
theorem :: NUMPOLY1:53
Polygon (2,n) = n;
registration let s be non trivial Nat, n be Nat;
cluster Polygon (s,n) -> natural;
end;
registration let n be Nat;
cluster Polygon (4,n) -> square;
end;
registration
cluster 3-gonal -> triangular for Nat;
cluster triangular -> 3-gonal for Nat;
cluster 4-gonal -> square for Nat;
cluster square -> 4-gonal for Nat;
end;
theorem :: NUMPOLY1:54
Triangle (n -' 1) + Triangle (n) = n^2;
theorem :: NUMPOLY1:55
Triangle (n) + Triangle (n + 1) = (n + 1) ^2;
registration let n be Nat;
cluster Triangle n + Triangle (n + 1) -> square;
end;
theorem :: NUMPOLY1:56
for n being non trivial Nat holds
(1 / 3) * Triangle (3 * n -' 1) = n * (3 * n - 1) / 2;
theorem :: NUMPOLY1:57
for n being non zero Nat holds
Triangle (2 * n -' 1) = n * (4 * n - 2) / 2;
definition let n, k be Nat;
func NPower (n, k) -> FinSequence of REAL means
:: NUMPOLY1:def 8
dom it = Seg k &
for i being Nat st i in dom it holds
it.i = i |^ n;
end;
theorem :: NUMPOLY1:58
for k being Nat holds
NPower (n,k+1) = NPower (n,k) ^ <*(k+1) |^ n*>;
registration
let n be Nat;
reduce Sum NPower (n, 0) to 0;
end;
theorem :: NUMPOLY1:59
(Triangle n) |^ 2 = Sum NPower (3, n);
theorem :: NUMPOLY1:60
for n being non trivial Nat holds
Triangle n + Triangle (n -' 1) * Triangle (n + 1) = (Triangle n) |^ 2;
theorem :: NUMPOLY1:61
(Triangle n) |^ 2 + (Triangle (n + 1)) |^ 2 = Triangle ((n + 1) |^ 2);
theorem :: NUMPOLY1:62
(Triangle (n + 1)) |^ 2 - (Triangle n) |^ 2 = (n + 1) |^ 3;
theorem :: NUMPOLY1:63
for n being non zero Nat holds
3 * (Triangle n) + (Triangle (n -' 1)) = Triangle (2 * n);
theorem :: NUMPOLY1:64
3 * (Triangle n) + Triangle (n + 1) = Triangle (2 * n + 1);
theorem :: NUMPOLY1:65
for n being non zero Nat holds
Triangle (n -' 1) + 6 * (Triangle n) + Triangle (n + 1) =
8 * (Triangle n) + 1;
theorem :: NUMPOLY1:66
for n being non zero Nat holds
Triangle n + Triangle (n -' 1) = (1 + 2 * n - 1) * n / 2;
theorem :: NUMPOLY1:67
1 + 9 * Triangle n = Triangle (3 * n + 1);
theorem :: NUMPOLY1:68
for m being Nat holds
Triangle (n + m) = Triangle n + Triangle m + n * m;
theorem :: NUMPOLY1:69
for n,m being non trivial Nat holds
(Triangle n) * (Triangle m) +
(Triangle (n -' 1)) * (Triangle (m -' 1)) =
Triangle (n * m);
begin :: Sets of Polygonal Numbers
definition let s be Nat;
func PolygonalNumbers s -> set equals
:: NUMPOLY1:def 9
the set of all Polygon (s,n) where n is Nat;
end;
definition let s be non trivial Nat;
redefine func PolygonalNumbers s -> Subset of NAT;
end;
definition
func TriangularNumbers -> Subset of NAT equals
:: NUMPOLY1:def 10
PolygonalNumbers 3;
func SquareNumbers -> Subset of NAT equals
:: NUMPOLY1:def 11
PolygonalNumbers 4;
end;
registration let s be non trivial Nat;
cluster PolygonalNumbers s -> non empty;
end;
registration
cluster TriangularNumbers -> non empty;
cluster SquareNumbers -> non empty;
end;
registration
cluster -> triangular for Element of TriangularNumbers;
cluster -> square for Element of SquareNumbers;
end;
theorem :: NUMPOLY1:70
for x being number holds
x in TriangularNumbers iff x is triangular;
theorem :: NUMPOLY1:71
for x being number holds
x in SquareNumbers iff x is square;
begin :: Some Well-known Properties
theorem :: NUMPOLY1:72
(n + 1) choose 2 = n * (n + 1) / 2;
theorem :: NUMPOLY1:73
Triangle n = (n + 1) choose 2;
theorem :: NUMPOLY1:74
for n being non zero Nat st n is even perfect holds
n is triangular;
registration let n be non zero Nat;
cluster Mersenne n -> non zero;
end;
definition let n be number;
attr n is mersenne means
:: NUMPOLY1:def 12
ex p being Nat st n = Mersenne p;
end;
registration
cluster mersenne for Prime;
cluster non prime for Nat;
end;
registration
cluster mersenne non prime for Nat;
end;
registration
cluster -> non zero for Prime;
end;
registration let n be mersenne Prime;
cluster Triangle n -> perfect;
end;
registration
cluster even perfect -> triangular for non zero Nat;
end;
theorem :: NUMPOLY1:75
8 * (Triangle n) + 1 = (2 * n + 1) ^2;
theorem :: NUMPOLY1:76
n is triangular implies 8 * n + 1 is square;
theorem :: NUMPOLY1:77
n is triangular implies 9 * n + 1 is triangular;
theorem :: NUMPOLY1:78
Triangle n is triangular square implies
Triangle (4 * n * (n + 1)) is triangular square;
registration
cluster TriangularNumbers -> infinite;
cluster SquareNumbers -> infinite;
end;
registration
cluster triangular square non zero for Nat;
end;
theorem :: NUMPOLY1:79
0 is triangular square;
registration
cluster zero -> triangular square for number;
end;
theorem :: NUMPOLY1:80
1 is triangular square;
::$N Square triangular number
theorem :: NUMPOLY1:81
36 is triangular square;
theorem :: NUMPOLY1:82
1225 is triangular square;
registration let n be triangular Nat;
cluster 9 * n + 1 -> triangular;
end;
registration let n be triangular Nat;
cluster 8 * n + 1 -> square;
end;
begin :: Reciprocals of Triangular Numbers
registration
let a be Real;
reduce lim seq_const a to a;
end;
definition
func ReciTriangRS -> Real_Sequence means
:: NUMPOLY1:def 13
for i being Nat holds
it.i = 1 / Triangle i;
end;
registration
reduce ReciTriangRS.0 to 0;
end;
theorem :: NUMPOLY1:83
1 / (Triangle n) = 2 / (n * (n + 1));
theorem :: NUMPOLY1:84
Partial_Sums ReciTriangRS.n = 2 - 2 / (n + 1);
definition
func SumsReciTriang -> Real_Sequence means
:: NUMPOLY1:def 14
for n being Nat holds it.n = 2 - 2 / (n + 1);
let a, b be Real;
func geo-seq (a,b) -> Real_Sequence means
:: NUMPOLY1:def 15
for n being Nat holds it.n = a / (n + b);
end;
theorem :: NUMPOLY1:85
for a, b being Real st b > 0 holds
geo-seq (a,b) is convergent & lim geo-seq (a,b) = 0;
theorem :: NUMPOLY1:86
SumsReciTriang = seq_const 2 + - geo-seq (2,1);
theorem :: NUMPOLY1:87
SumsReciTriang is convergent & lim SumsReciTriang = 2;
theorem :: NUMPOLY1:88
Partial_Sums ReciTriangRS = SumsReciTriang;
::$N Reciprocals of triangular numbers
theorem :: NUMPOLY1:89
Sum ReciTriangRS = 2;