proposition: Theorem Pocklington: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * 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 n, prime n -> (n | N) -> n mod F1 = 1.
proof: Proof. intros N F1 R1 HF1 HR1 Neq Rec n Hn H. assert (HN: 1 < N). cut (0 < N - 1). auto with zarith. rewrite Neq. apply Z.lt_le_trans with (1* R1); auto with zarith. assert (Hn1: 1 < n). apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (H1: (F1 | n - 1)). 2: rewrite <- (Zmod_small 1 F1) by auto with zarith. 2: case H1; intros k H1'. 2: replace n with (1 + (n - 1)) by auto with zarith. 2: rewrite H1'; apply Z_mod_plus; auto with zarith. apply Zdivide_Zpower. auto with zarith. intros p i Hp Hi HiF1. case (Rec p Hp). apply Z.divide_trans with (2 := HiF1). apply Zpower_divide; auto with zarith. intros a (Ha1, (Ha2, Ha3)). assert (HNn: a ^ (N - 1) mod n = 1). apply Zdivide_mod_minus. auto with zarith. apply Z.divide_trans with (1 := H). apply Zmod_divide_minus; auto with zarith. assert (~(n | a)). intros H1; absurd (0 = 1). auto with zarith. rewrite <- HNn. apply sym_equal; apply Zdivide_mod. apply Z.divide_trans with (1 := H1); apply Zpower_divide; auto with zarith. assert (Hr: rel_prime a n). apply rel_prime_sym; apply prime_rel_prime; auto. assert (Hz: 0 < Zorder a n). apply Zorder_power_pos; auto. apply Z.divide_trans with (Zorder a n). apply prime_divide_Zpower_Zdiv with (N - 1). 1-2: auto with zarith. apply Zorder_div_power; auto with zarith. intros H1; absurd (1 < n); auto; apply Zle_not_lt; apply Zdivide_le. 1-2: auto with zarith. rewrite <- Ha3; apply Zdivide_Zgcd. 2: auto with zarith. apply Zmod_divide_minus. auto with zarith. case H1; intros t Ht; rewrite Ht. assert (Ht1: 0 <= t). apply Zmult_le_reg_r with (Zorder a n). auto with zarith. rewrite Zmult_0_l; rewrite <- Ht. apply Z.ge_le; apply Z_div_ge0. 2: auto with zarith. apply Z.lt_gt; apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. rewrite Zmult_comm. rewrite Zpower_mult by auto with zarith. rewrite Zpower_mod by auto with zarith. rewrite Zorder_power_is_1 by auto with zarith. rewrite Zpower_1_l by auto with zarith. apply Zmod_small; auto with zarith. apply Z.divide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r. apply Zorder_div; auto. Qed.
imports: ZArith Znumtheory Tactic ZCAux Zp FGroup EGroup Euler