Metamath Proof Explorer

Theorem fpprwpprb

Description: An integer X which is coprime with an integer N is a Fermat pseudoprime to the base N iff it is a weak pseudoprime to the base N . (Contributed by AV, 2-Jun-2023)

Ref Expression
Assertion fpprwpprb ( ( 𝑋 gcd 𝑁 ) = 1 → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fpprbasnn ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ )
2 fpprel ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
3 3simpa ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) )
4 3 a1i ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ) )
5 2 4 sylbid ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ) )
6 1 5 mpcom ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) )
7 fpprwppr ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) )
8 1 7 jca ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) )
9 6 8 jca ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) )
10 simprll ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → 𝑋 ∈ ( ℤ≥ ‘ 4 ) )
11 simprlr ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → 𝑋 ∉ ℙ )
12 eluz4nn ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ )
13 12 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ ℕ )
14 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
15 12 nnnn0d ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ0 )
16 zexpcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ℤ )
17 14 15 16 syl2anr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) ∈ ℤ )
18 14 adantl ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
19 moddvds ⊢ ( ( 𝑋 ∈ ℕ ∧ ( 𝑁 ↑ 𝑋 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ) )
20 13 17 18 19 syl3anc ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ) )
21 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
22 expm1t ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑋 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) )
23 21 12 22 syl2anr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ 𝑋 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) )
24 23 oveq1d ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) = ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) − 𝑁 ) )
25 nnm1nn0 ⊢ ( 𝑋 ∈ ℕ → ( 𝑋 − 1 ) ∈ ℕ0 )
26 12 25 syl ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑋 − 1 ) ∈ ℕ0 )
27 zexpcl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑋 − 1 ) ∈ ℕ0 ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ )
28 14 26 27 syl2anr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ )
29 28 zcnd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℂ )
30 21 adantl ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
31 29 30 mulsubfacd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) · 𝑁 ) − 𝑁 ) = ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) )
32 24 31 eqtrd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) = ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) )
33 32 breq2d ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) ↔ 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) ) )
34 1zzd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℤ )
35 28 34 zsubcld ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ∈ ℤ )
36 dvdsmulgcd ⊢ ( ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) ↔ 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) ) )
37 35 18 36 syl2anc ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) ↔ 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) ) )
38 eluzelz ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℤ )
39 gcdcom ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑋 gcd 𝑁 ) = ( 𝑁 gcd 𝑋 ) )
40 38 14 39 syl2an ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 gcd 𝑁 ) = ( 𝑁 gcd 𝑋 ) )
41 40 eqeq1d ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑋 gcd 𝑁 ) = 1 ↔ ( 𝑁 gcd 𝑋 ) = 1 ) )
42 41 biimpd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑋 gcd 𝑁 ) = 1 → ( 𝑁 gcd 𝑋 ) = 1 ) )
43 42 imp ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( 𝑁 gcd 𝑋 ) = 1 )
44 43 oveq2d ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) = ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 1 ) )
45 35 zcnd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ∈ ℂ )
46 45 mulid1d ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 1 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) )
47 46 adantr ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 1 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) )
48 44 47 eqtrd ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) )
49 48 breq2d ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) ↔ 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) )
50 49 biimpd ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 gcd 𝑁 ) = 1 ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) )
51 50 ex ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑋 gcd 𝑁 ) = 1 → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
52 51 com23 ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · ( 𝑁 gcd 𝑋 ) ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
53 37 52 sylbid ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∥ ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) · 𝑁 ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
54 33 53 sylbid ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑋 ∥ ( ( 𝑁 ↑ 𝑋 ) − 𝑁 ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
55 20 54 sylbid ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
56 55 expimpd ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
57 56 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) → ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) ) )
58 57 imp ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → ( ( 𝑋 gcd 𝑁 ) = 1 → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) )
59 58 impcom ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) )
60 eluz4eluz2 ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
61 60 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
62 61 adantr ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
63 14 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) → 𝑁 ∈ ℤ )
64 26 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) → ( 𝑋 − 1 ) ∈ ℕ0 )
65 63 64 27 syl2anr ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ )
66 62 65 jca ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ ) )
67 66 adantl ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ ) )
68 modm1div ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ↑ ( 𝑋 − 1 ) ) ∈ ℤ ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ↔ 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) )
69 67 68 syl ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → ( ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ↔ 𝑋 ∥ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) − 1 ) ) )
70 59 69 mpbird ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 )
71 2 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
72 71 adantl ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
73 72 adantl ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
74 10 11 70 73 mpbir3and ⊢ ( ( ( 𝑋 gcd 𝑁 ) = 1 ∧ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) → 𝑋 ∈ ( FPPr ‘ 𝑁 ) )
75 74 ex ⊢ ( ( 𝑋 gcd 𝑁 ) = 1 → ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) → 𝑋 ∈ ( FPPr ‘ 𝑁 ) ) )
76 9 75 impbid2 ⊢ ( ( 𝑋 gcd 𝑁 ) = 1 → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ) ∧ ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 ↑ 𝑋 ) mod 𝑋 ) = ( 𝑁 mod 𝑋 ) ) ) ) )