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 
|- ( X e. ( FPPr ` N ) -> ( ( N ^ X ) mod X ) = ( N mod X ) )

Proof

Step Hyp Ref Expression
1 fpprbasnn 
 |-  ( X e. ( FPPr ` N ) -> N e. NN )
2 fpprel 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
3 nnz 
 |-  ( N e. NN -> N e. ZZ )
4 eluz4nn 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. NN )
5 nnm1nn0 
 |-  ( X e. NN -> ( X - 1 ) e. NN0 )
6 4 5 syl 
 |-  ( X e. ( ZZ>= ` 4 ) -> ( X - 1 ) e. NN0 )
7 zexpcl 
 |-  ( ( N e. ZZ /\ ( X - 1 ) e. NN0 ) -> ( N ^ ( X - 1 ) ) e. ZZ )
8 3 6 7 syl2an 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N ^ ( X - 1 ) ) e. ZZ )
9 8 zred 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N ^ ( X - 1 ) ) e. RR )
10 4 nnrpd 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. RR+ )
11 10 adantl 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> X e. RR+ )
12 9 11 modcld 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N ^ ( X - 1 ) ) mod X ) e. RR )
13 12 recnd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N ^ ( X - 1 ) ) mod X ) e. CC )
14 1cnd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> 1 e. CC )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 15 adantr 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> N e. CC )
17 nnne0 
 |-  ( N e. NN -> N =/= 0 )
18 17 adantr 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> N =/= 0 )
19 13 14 16 18 mulcand 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) = ( N x. 1 ) <-> ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) )
20 oveq1 
 |-  ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) = ( N x. 1 ) -> ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) mod X ) = ( ( N x. 1 ) mod X ) )
21 3 adantr 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> N e. ZZ )
22 modmulmodr 
 |-  ( ( N e. ZZ /\ ( N ^ ( X - 1 ) ) e. RR /\ X e. RR+ ) -> ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) mod X ) = ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) )
23 21 9 11 22 syl3anc 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) mod X ) = ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) )
24 23 eqeq1d 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) mod X ) = ( ( N x. 1 ) mod X ) <-> ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) = ( ( N x. 1 ) mod X ) ) )
25 8 zcnd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N ^ ( X - 1 ) ) e. CC )
26 16 25 mulcomd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N x. ( N ^ ( X - 1 ) ) ) = ( ( N ^ ( X - 1 ) ) x. N ) )
27 expm1t 
 |-  ( ( N e. CC /\ X e. NN ) -> ( N ^ X ) = ( ( N ^ ( X - 1 ) ) x. N ) )
28 27 eqcomd 
 |-  ( ( N e. CC /\ X e. NN ) -> ( ( N ^ ( X - 1 ) ) x. N ) = ( N ^ X ) )
29 15 4 28 syl2an 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N ^ ( X - 1 ) ) x. N ) = ( N ^ X ) )
30 26 29 eqtrd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N x. ( N ^ ( X - 1 ) ) ) = ( N ^ X ) )
31 30 oveq1d 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) = ( ( N ^ X ) mod X ) )
32 15 mulid1d 
 |-  ( N e. NN -> ( N x. 1 ) = N )
33 32 adantr 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( N x. 1 ) = N )
34 33 oveq1d 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N x. 1 ) mod X ) = ( N mod X ) )
35 31 34 eqeq12d 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) = ( ( N x. 1 ) mod X ) <-> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
36 35 biimpd 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( ( N x. ( N ^ ( X - 1 ) ) ) mod X ) = ( ( N x. 1 ) mod X ) -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
37 24 36 sylbid 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) mod X ) = ( ( N x. 1 ) mod X ) -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
38 20 37 syl5 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( N x. ( ( N ^ ( X - 1 ) ) mod X ) ) = ( N x. 1 ) -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
39 19 38 sylbird 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( ( ( N ^ ( X - 1 ) ) mod X ) = 1 -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
40 39 a1d 
 |-  ( ( N e. NN /\ X e. ( ZZ>= ` 4 ) ) -> ( X e/ Prime -> ( ( ( N ^ ( X - 1 ) ) mod X ) = 1 -> ( ( N ^ X ) mod X ) = ( N mod X ) ) ) )
41 40 ex 
 |-  ( N e. NN -> ( X e. ( ZZ>= ` 4 ) -> ( X e/ Prime -> ( ( ( N ^ ( X - 1 ) ) mod X ) = 1 -> ( ( N ^ X ) mod X ) = ( N mod X ) ) ) ) )
42 41 3impd 
 |-  ( N e. NN -> ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
43 2 42 sylbid 
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) -> ( ( N ^ X ) mod X ) = ( N mod X ) ) )
44 1 43 mpcom 
 |-  ( X e. ( FPPr ` N ) -> ( ( N ^ X ) mod X ) = ( N mod X ) )