:: Polygonal Numbers :: by Adam Grabowski :: :: Received May 19, 2013 :: Copyright (c) 2013-2018 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 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;