Metamath Proof Explorer

Theorem fpprwppr

Description: A Fermat pseudoprime to the base N is aweak pseudoprime (see Wikipedia "Fermat pseudoprime", 29-May-2023, https://en.wikipedia.org/wiki/Fermat_pseudoprime . (Contributed by AV, 31-May-2023)

Ref Expression
Assertion fpprwppr ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fpprbasnn ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ )
2 fpprel ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
3 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
4 eluz4nn ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ )
5 nnm1nn0 ⊢ ( 𝑋 ∈ ℕ → ( 𝑋 − 1 ) ∈ ℕ0 )
6 4 5 syl ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑋 − 1 ) ∈ ℕ0 )
7 zexpcl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑋 − 1 ) ∈ ℕ0 ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ )
8 3 6 7 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ )
9 8 zred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℝ )
10 4 nnrpd ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℝ+ )
11 10 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑋 ∈ ℝ+ )
12 9 11 modcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ∈ ℂ )
14 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → 1 ∈ ℂ )
15 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑁 ∈ ℂ )
17 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑁 ≠ 0 )
19 13 14 16 18 mulcand ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) = ( 𝑁 · 1 ) ↔ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) )
20 oveq1 ⊢ ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) = ( 𝑁 · 1 ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) )
21 3 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑁 ∈ ℤ )
22 modmulmodr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℝ ∧ 𝑋 ∈ ℝ+ ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) mod 𝑋 ) = ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) )
23 21 9 11 22 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) mod 𝑋 ) = ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) )
24 23 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) ↔ ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) ) )
25 8 zcnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℂ )
26 16 25 mulcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) )
27 expm1t ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) )
28 27 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑋 ∈ ℕ ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) = ( 𝑁 ↑ 𝑋 ) )
29 15 4 28 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) = ( 𝑁 ↑ 𝑋 ) )
30 26 29 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) = ( 𝑁 ↑ 𝑋 ) )
31 30 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) = ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) )
32 15 mulid1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · 1 ) = 𝑁 )
33 32 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 · 1 ) = 𝑁 )
34 33 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 · 1 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) )
35 31 34 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) ↔ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
36 35 biimpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 · ( 𝑁 ↑ ( 𝑋 − 1 ) ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
37 24 36 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) mod 𝑋 ) = ( ( 𝑁 · 1 ) mod 𝑋 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
38 20 37 syl5 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑁 · ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) ) = ( 𝑁 · 1 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
39 19 38 sylbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
40 39 a1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑋 ∉ ℙ → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) )
41 40 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑋 ∉ ℙ → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) )
42 41 3impd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
43 2 42 sylbid ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
44 1 43 mpcom ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) )