proposition: Theorem PocklingtonExtraCorollary: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 -> (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Z.gcd (a ^ ((N - 1)/ p) - 1) N = 1) -> let s := (R1 / (2 * F1)) in let r := (R1 mod (2 * F1)) in N < 2 * F1 * F1 * F1 -> (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
proof: Proof. intros N F1 R1 H1 H2 H3 OF1 ER1 H4 s r H5 H6. apply PocklingtonExtra with (6 := H4) (R1 := R1) (m := 1); auto with zarith. apply Z.lt_le_trans with (1 := H5). match goal with |- ?X <= ?K * ((?Y + ?Z) + ?T) => rewrite <- (Zplus_0_l X); replace (K * ((Y + Z) + T)) with ((F1 * (Z + T) + Y + Z + T) + X);[idtac | ring] end. apply Zplus_le_compat_r. case (Zle_lt_or_eq 0 r); unfold r. case (Z_mod_lt R1 (2 * F1)); auto with zarith. intros HH; repeat ((rewrite <- (Zplus_0_r 0); apply Zplus_le_compat)); auto with zarith. intros HH; contradict ER1; apply Zeven_not_Zodd. rewrite (Z_div_mod_eq_full R1 (2 * F1)). rewrite <- HH; rewrite Zplus_0_r. rewrite <- Zmult_assoc; apply Zeven_2p. Qed.
imports: ZArith Znumtheory Tactic ZCAux Zp FGroup EGroup Euler