dfwppr

Description: Alternate definition of aweak pseudoprime X , which fulfils ( N ^ X ) == N (modulo X ), see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime , 29-May-2023. (Contributed by AV, 31-May-2023)

		Ref	Expression
	Assertion	dfwppr	$⊢ (N \in ℕ \land X \in ℕ) \to (N^{X} \mod X = N \mod X \leftrightarrow X ∥ (N^{X} - N))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (N \in ℕ \land X \in ℕ) \to X \in ℕ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3		nnnn0	$⊢ X \in ℕ \to X \in ℕ_{0}$
4		zexpcl	$⊢ (N \in ℤ \land X \in ℕ_{0}) \to N^{X} \in ℤ$
5	2 3 4	syl2an	$⊢ (N \in ℕ \land X \in ℕ) \to N^{X} \in ℤ$
6	2	adantr	$⊢ (N \in ℕ \land X \in ℕ) \to N \in ℤ$
7		moddvds	$⊢ (X \in ℕ \land N^{X} \in ℤ \land N \in ℤ) \to (N^{X} \mod X = N \mod X \leftrightarrow X ∥ (N^{X} - N))$
8	1 5 6 7	syl3anc	$⊢ (N \in ℕ \land X \in ℕ) \to (N^{X} \mod X = N \mod X \leftrightarrow X ∥ (N^{X} - N))$

Metamath Proof Explorer

Theorem dfwppr

Proof