proposition: Theorem PepinTest: forall n, let Fn := FermatNumber n in (3 ^ ((Fn - 1) / 2) + 1) mod Fn = 0 -> prime Fn.
proof: Proof. intros n Fn H. assert (Hn: 1 < Fn). unfold Fn; apply Fermat_pos. apply PocklingtonCorollary1 with (F1 := 2^(2^(Z_of_nat n))) (R1 := 1). 2: auto with zarith. 2: unfold Fn, FermatNumber; auto with zarith. apply Z.lt_le_trans with (2 ^ 1). rewrite Zpower_1_r; auto with zarith. apply Zpower_le_monotone. 2: split. 1-2: auto with zarith. rewrite <- (Zpower_0_r 2); apply Zpower_le_monotone; try split; auto with zarith. unfold Fn, FermatNumber. assert (H1: 2 <= 2 ^ 2 ^ Z_of_nat n). pattern 2 at 1; rewrite <- (Zpower_1_r 2) by auto with zarith. apply Zpower_le_monotone; split. auto with zarith. rewrite <- (Zpower_0_r 2); apply Zpower_le_monotone; try split; auto with zarith. apply Z.lt_le_trans with (2 * 2 ^2 ^Z_of_nat n). assert (tmp: forall p, 2 * p = p + p); auto with zarith. apply Zmult_le_compat_r; auto with zarith. assert (Hd: (2 | Fn - 1)). exists (2 ^ (2^(Z_of_nat n) - 1)). pattern 2 at 3; rewrite <- (Zpower_1_r 2). rewrite <- Zpower_exp. 3: auto with zarith. assert (tmp: forall p, p = (p - 1) +1) by auto with zarith; rewrite <- tmp. unfold Fn, FermatNumber; ring. assert (0 < 2 ^ Z_of_nat n); auto with zarith. intros p Hp Hp1; exists 3; split. auto with zarith. split. rewrite (Zdivide_Zdiv_eq 2 (Fn -1)) by auto with zarith. rewrite Zmult_comm. rewrite Zpower_mult. 3: auto with zarith. rewrite Zpower_mod by auto with zarith. assert (tmp: forall p, p = (p + 1) -1) by auto with zarith; rewrite (fun x => (tmp (3 ^ x))). rewrite Zminus_mod by auto with zarith. rewrite H. rewrite (Zmod_small 1) by auto with zarith. rewrite <- Zpower_mod by auto with zarith. rewrite Zmod_small. auto with zarith. simpl; unfold Zpower_pos; simpl; auto with zarith. apply Z_div_pos; auto with zarith. apply Zis_gcd_gcd. auto with zarith. apply Zis_gcd_intro. 1-2: auto with zarith. intros x HD1 HD2. assert (Hd1: p = 2). apply prime_div_Zpower_prime with (4 := Hp1). 1-2: auto with zarith. apply prime_2. assert (Hd2: (x | 2)). replace 2 with ((3 ^ ((Fn - 1) / 2) + 1) - (3 ^ ((Fn - 1) / 2) - 1)) by auto with zarith. apply Zdivide_minus_l; auto. apply Z.divide_trans with (1 := HD2). apply Zmod_divide; auto with zarith. rewrite <- Hd1; auto. replace 1 with (Fn - (Fn - 1)) by auto with zarith. apply Zdivide_minus_l; auto. apply Z.divide_trans with (1 := Hd2); auto. Qed.
imports: ZArith ZCAux Pocklington