∀ p a, prime p ⇒ ¬(p | a) ⇒ (a ^ (p-1)) ≡ 1 [p]

Theorem congruent_exp_pred_SO : forall (p:nat.nat), forall (a:nat.nat), (primes.prime p) -> (connectives.Not (primes.divides p a)) -> cong.congruent (exp.exp a (nat.pred p)) (nat.S nat.O) p.

theorem congruent_exp_pred_SO : \forall (p:nat). \forall (a:nat). ((prime) p) -> ((Not) ((divides) p a)) -> (congruent) ((exp) a ((pred) p)) ((S) (O) ) p.

theorem congruent_exp_pred_SO : forall (p:nat.nat) , forall (a:nat.nat) , (((primes.prime) ) (p)) -> (((connectives.Not) ) ((((primes.divides) ) (p)) (a))) -> ((((cong.congruent) ) ((((exp.exp) ) (a)) (((nat.pred_) ) (p)))) (((nat.S) ) ((nat.O) ))) (p).

congruent_exp_pred_SO : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(a:nat_sttfa_th.sttfa_nat):(primes_sttfa_th.prime(p) => (connectives_sttfa_th.sttfa_Not(primes_sttfa_th.sttfa_divides(p)(a)) => cong_sttfa_th.congruent(exp_sttfa_th.sttfa_exp(a)(nat_sttfa_th.pred(p)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(p)))))

Printing for OpenTheory is not working at the moment.