Theorem 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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ ) → 𝑋 ∈ ℕ )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3		nnnn0	⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℕ0 )
4		zexpcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ℤ )
5	2 3 4	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ℤ )
6	2	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ ) → 𝑁 ∈ ℤ )
7		moddvds	⊢ ( ( 𝑋 ∈ ℕ ∧ ( 𝑁 ↑ 𝑋 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ) )
8	1 5 6 7	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ) )