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	mulridd	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 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 𝑋 ) ) ) ) )