This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vfermltlALT

Description: Alternate proof of vfermltl , not using Euler's theorem. (Contributed by AV, 21-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion vfermltlALT 
|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = 1 )

Proof

Step Hyp Ref Expression
1 2m1e1 
 |-  ( 2 - 1 ) = 1
2 1 a1i 
 |-  ( P e. Prime -> ( 2 - 1 ) = 1 )
3 2 eqcomd 
 |-  ( P e. Prime -> 1 = ( 2 - 1 ) )
4 3 oveq2d 
 |-  ( P e. Prime -> ( P - 1 ) = ( P - ( 2 - 1 ) ) )
5 prmz 
 |-  ( P e. Prime -> P e. ZZ )
6 5 zcnd 
 |-  ( P e. Prime -> P e. CC )
7 2cnd 
 |-  ( P e. Prime -> 2 e. CC )
8 1cnd 
 |-  ( P e. Prime -> 1 e. CC )
9 6 7 8 subsubd 
 |-  ( P e. Prime -> ( P - ( 2 - 1 ) ) = ( ( P - 2 ) + 1 ) )
10 4 9 eqtrd 
 |-  ( P e. Prime -> ( P - 1 ) = ( ( P - 2 ) + 1 ) )
11 10 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 1 ) = ( ( P - 2 ) + 1 ) )
12 11 oveq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 1 ) ) = ( A ^ ( ( P - 2 ) + 1 ) ) )
13 zcn 
 |-  ( A e. ZZ -> A e. CC )
14 13 3ad2ant2 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> A e. CC )
15 prmm2nn0 
 |-  ( P e. Prime -> ( P - 2 ) e. NN0 )
16 15 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 2 ) e. NN0 )
17 14 16 expp1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( ( P - 2 ) + 1 ) ) = ( ( A ^ ( P - 2 ) ) x. A ) )
18 12 17 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 1 ) ) = ( ( A ^ ( P - 2 ) ) x. A ) )
19 18 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = ( ( ( A ^ ( P - 2 ) ) x. A ) mod P ) )
20 15 anim1i 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( P - 2 ) e. NN0 /\ A e. ZZ ) )
21 20 ancomd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A e. ZZ /\ ( P - 2 ) e. NN0 ) )
22 zexpcl 
 |-  ( ( A e. ZZ /\ ( P - 2 ) e. NN0 ) -> ( A ^ ( P - 2 ) ) e. ZZ )
23 21 22 syl 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ ( P - 2 ) ) e. ZZ )
24 23 zred 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ ( P - 2 ) ) e. RR )
25 24 3adant3 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 2 ) ) e. RR )
26 simp2 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> A e. ZZ )
27 prmnn 
 |-  ( P e. Prime -> P e. NN )
28 27 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
29 28 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. RR+ )
30 modmulmod 
 |-  ( ( ( A ^ ( P - 2 ) ) e. RR /\ A e. ZZ /\ P e. RR+ ) -> ( ( ( ( A ^ ( P - 2 ) ) mod P ) x. A ) mod P ) = ( ( ( A ^ ( P - 2 ) ) x. A ) mod P ) )
31 25 26 29 30 syl3anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( ( A ^ ( P - 2 ) ) mod P ) x. A ) mod P ) = ( ( ( A ^ ( P - 2 ) ) x. A ) mod P ) )
32 zre 
 |-  ( A e. ZZ -> A e. RR )
33 32 adantl 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> A e. RR )
34 15 adantr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P - 2 ) e. NN0 )
35 33 34 reexpcld 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( A ^ ( P - 2 ) ) e. RR )
36 28 adantr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> P e. RR+ )
37 35 36 modcld 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. RR )
38 37 recnd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ ( P - 2 ) ) mod P ) e. CC )
39 13 adantl 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> A e. CC )
40 38 39 mulcomd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) x. A ) = ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) )
41 40 3adant3 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) x. A ) = ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) )
42 41 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( ( A ^ ( P - 2 ) ) mod P ) x. A ) mod P ) = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
43 19 31 42 3eqtr2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) )
44 eqid 
 |-  ( ( A ^ ( P - 2 ) ) mod P ) = ( ( A ^ ( P - 2 ) ) mod P )
45 44 modprminv 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( ( A ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 ) )
46 45 simprd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A x. ( ( A ^ ( P - 2 ) ) mod P ) ) mod P ) = 1 )
47 43 46 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = 1 )