Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
From mathcomp Require Import all_ssreflect. Section Nagoya2013. Definition Sk k n := \sum_(1<=i 1. Definition Tm n := \sum_(1<=k i _. by rewrite Sk1 muln1. rewrite big_mkord. congr subn. apply eq_bigr => i _. by rewrite !exp1n !muln1. Qed. Lemma Tm2 : Tm 2 = 3^m - 3. Proof. rewrite /Tm. have ->: 3^m - 3 = 2^m - 2 + (3^m - 1 - 2^m). rewrite addnC. rewrite addnBA. rewrite subnK. by rewrite -subnDA. rewrite subn1 -ltnS prednK. by apply ltn_exp2r, ltnW. by rewrite expn_gt0. rewrite -{1}(exp1n m). rewrite ltn_exp2r //. by apply ltnW. rewrite -Tm1. rewrite [in 3^m](_ : 3 = 1+2) //. rewrite Pascal. transitivity (Tm 1 + (\sum_(1 <= k < m) 'C(m,k) * 2^k)). rewrite -big_split /=. apply eq_bigr => i _. rewrite -mulnDr. congr muln. rewrite /Sk !big_cons !big_nil. by rewrite !addn0. congr addn. transitivity ((\sum_(0 <= k < m.+1) 'C(m,k) * 2^k) - 1 - 2^m). symmetry. rewrite (@big_cat_nat _ _ _ m) //=. rewrite (@big_cat_nat _ _ _ 1) //=; last by apply ltnW. rewrite addnAC. rewrite !big_nat1. rewrite bin0 binn. rewrite !mul1n expn0. by rewrite -addnA 2!addKn. rewrite big_mkord. congr subn. congr subn. apply eq_bigr => i _. by rewrite exp1n mul1n. Qed. Theorem Tmn n : Tm n.+1 = n.+2^m - n.+2. Proof. have Hm': m > 0 by apply ltnW. elim:n => [|n IHn] /=. by apply Tm1. have ->: n.+3^m - n.+3 = n.+2^m - n.+2 + (n.+3^m - 1 - n.+2^m). rewrite addnC. rewrite addnBA. rewrite subnK. by rewrite -subnDA. rewrite subn1 -ltnS prednK. by rewrite ltn_exp2r. by rewrite expn_gt0. apply (@leq_ltn_trans (n.+1^m)). by rewrite -{1}(expn1 n.+1) leq_pexp2l. by rewrite ltn_exp2r. rewrite -IHn. rewrite [in n.+3^m](_ : n.+3 = 1+n.+2) //. rewrite Pascal. transitivity (Tm n.+1 + (\sum_(1 <= k < m) 'C(m,k) * n.+2^k)). rewrite -big_split /=. apply eq_bigr => i _. rewrite -mulnDr. congr muln. rewrite /Sk. by rewrite (@big_cat_nat _ _ _ n.+2) //= big_nat1. congr addn. transitivity ((\sum_(0 <= k < m.+1) 'C(m,k) * n.+2^k) - 1 - n.+2^m). symmetry. rewrite (@big_cat_nat _ _ _ m) //=. rewrite (@big_cat_nat _ _ _ 1) //=. rewrite addnAC. rewrite !big_nat1. rewrite bin0 binn. rewrite !mul1n expn0. by rewrite -addnA 2!addKn. rewrite big_mkord. congr subn. congr subn. apply eq_bigr => i _. by rewrite exp1n mul1n. Qed. Theorem Skp p k : p > 2 -> prime p -> 1 <= k < p.-1 -> p %| Sk k p.-1. Admitted. End Nagoya2013. Section tpp2014. Lemma lem1 a : a*a = 0 %[mod 3] \/ a*a = 1 %[mod3]. Proof. remember (a %% 3) as m. rewrite -modnMm -Heqm. destruct m => /=. by left. destruct m => /=. by right. destruct m => /=. by right. have Hm: a %% 3 >= 3. by rewrite -Heqm. by rewrite leqNgt ltn_mod in Hm. Qed.