proposition: Theorem PocklingtonExtra: 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) -> forall m, 1 <= m -> (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) -> let s := (R1 / (2 * F1)) in let r := (R1 mod (2 * F1)) in N < (m * F1 + 1) * (2 * F1 * F1 + (r - m) * F1 + 1) -> (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
proof: Proof. intros N F1 R1 H1 H2 H3 OF1 ER1 H4 m H5 H6 s r H7 H8. case (prime_dec N). auto. intros H9. assert (HN: 1 < N). cut (0 < N - 1). auto with zarith. rewrite H3. apply Z.lt_le_trans with (1* R1); auto with zarith. case Zdivide_div_prime_le_square with N. 1-2: auto. intros X (Hx1, (Hx2, Hx3)). assert (Hx0: 1 < X). apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. pose (c := (X / F1)). assert(Hc1: 0 <= c). apply Z.ge_le; unfold c; apply Z_div_ge0; auto with zarith. assert (Hc2: X = c * F1 + 1). rewrite (Z_div_mod_eq_full X F1). eq_tac. rewrite (Zmult_comm F1); auto. apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith. case Zle_lt_or_eq with (1 := Hc1); clear Hc1; intros Hc1. 2: contradict Hx0; rewrite Hc2; try rewrite <- Hc1; auto with zarith. case (Zle_or_lt m c); intros Hc3. 2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5. 2: case (H6 c); auto with zarith; rewrite <- Hc2; auto. 2: contradict Hc3; rewrite <- H5; auto with zarith. pose (d := ((N / X) / F1)). assert(Hd0: 0 <= N / X) by (apply Z_div_pos; auto with zarith). assert(Hd1: 0 <= d). apply Z.ge_le; unfold d; repeat apply Z_div_ge0; auto with zarith. assert (Hd2: N / X = d * F1 + 1). rewrite (Z_div_mod_eq_full (N / X) F1). eq_tac. rewrite (Zmult_comm F1); auto. apply PocklingtonCorollary2 with (R1 := R1) (4 := H4). 1-4: auto with zarith. exists X. apply Zdivide_Zdiv_eq; auto with zarith. case Zle_lt_or_eq with (1 := Hd0); clear Hd0; intros Hd0. 2: contradict HN; rewrite (Zdivide_Zdiv_eq X N) by auto with zarith. 2: rewrite <- Hd0; auto with zarith. case (Zle_lt_or_eq 1 (N / X)); auto with zarith; clear Hd0; intros Hd0. 2: contradict H9; rewrite (Zdivide_Zdiv_eq X N) by auto with zarith. 2: rewrite <- Hd0; rewrite Zmult_1_r; auto with zarith. case Zle_lt_or_eq with (1 := Hd1); clear Hd1; intros Hd1. 2: contradict Hd0; rewrite Hd2; try rewrite <- Hd1; auto with zarith. case (Zle_or_lt m d); intros Hd3. 2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5. 2: case (H6 d); auto with zarith; rewrite <- Hd2; auto. 2: exists X. 2: apply Zdivide_Zdiv_eq; auto with zarith. 2: contradict Hd3; rewrite <- H5; auto with zarith. assert (L5: N = (c * F1 + 1) * (d * F1 + 1)). rewrite <- Hc2; rewrite <- Hd2; apply Zdivide_Zdiv_eq; auto with zarith. assert (L6: R1 = c * d * F1 + c + d). apply trans_equal with ((N - 1) / F1). rewrite H3; rewrite Zmult_comm; apply sym_equal; apply Z_div_mult; auto with zarith. rewrite L5. match goal with |- (?X / ?Y = ?Z) => replace X with (Z * Y) end; try ring; apply Z_div_mult; auto with zarith. assert (L6_1: Zodd (c + d)). case (Zeven_odd_dec (c + d)); auto; intros O1. contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto. apply Zeven_mult_Zeven_r; auto. assert (L6_2: Zeven (c * d)). case (Zeven_odd_dec c); intros HH1. apply Zeven_mult_Zeven_l; auto. case (Zeven_odd_dec d); intros HH2. apply Zeven_mult_Zeven_r; auto. contradict L6_1; apply Zeven_not_Zodd; apply Zodd_plus_Zodd; auto. assert ((c + d) mod (2 * F1) = r). rewrite <- Z_mod_plus with (b := Z.div2 (c * d)) by auto with zarith. match goal with |- ?X mod _ = _ => replace X with R1 end; auto. rewrite L6; pattern (c * d) at 1. rewrite Zeven_div2 with (1 := L6_2); ring. assert (L9: c + d - r < 2 * F1). apply Zplus_lt_reg_r with (r - m). apply Zmult_lt_reg_r with (F1). auto with zarith. apply Zplus_lt_reg_r with 1. match goal with |- ?X < ?Y => replace Y with (2 * F1 * F1 + (r - m) * F1 + 1); try ring; replace X with ((((c + d) - m) * F1) + 1); try ring end. apply Zmult_lt_reg_r with (m * F1 + 1). apply Z.lt_trans with (m * F1 + 0). 2: auto with zarith. rewrite Zplus_0_r; apply Zmult_lt_O_compat; auto with zarith. repeat rewrite (fun x => Zmult_comm x (m * F1 + 1)). apply Z.le_lt_trans with (2 := H7). rewrite L5. match goal with |- ?X <= ?Y => replace X with ((m * (c + d) - m * m ) * F1 * F1 + (c + d) * F1 + 1); try ring; replace Y with ((c * d) * F1 * F1 + (c + d) * F1 + 1); try ring end. repeat apply Zplus_le_compat_r. repeat (apply Zmult_le_compat_r; [ | auto with zarith ]). assert (tmp: forall p q, 0 <= p - q -> q <= p) by auto with zarith; apply tmp. match goal with |- _ <= ?X => replace X with ((c - m) * (d - m)); try ring; auto with zarith end. assert (L10: c + d = r). apply Zmod_closeby_eq with (2 * F1). 1, 3-4: auto with zarith. unfold r; apply Z_mod_lt; auto with zarith. assert (L11: 2 * s = c * d). apply Zmult_reg_r with F1. auto with zarith. apply trans_equal with (R1 - (c + d)). rewrite L10; rewrite (Z_div_mod_eq_full R1 (2 * F1)). unfold s, r; ring. rewrite L6; ring. case H8; intro H10. absurd (0 < c * d). auto with zarith. apply Zmult_lt_O_compat; auto with zarith. case H10; exists (c - d). rewrite <- L10. replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring. Qed.
imports: ZArith Znumtheory Tactic ZCAux Zp FGroup EGroup Euler