Metamath Proof Explorer

Theorem 41prothprmlem2

Description: Lemma 2 for 41prothprm . (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypothesis 41prothprm.p 
|- P = ; 4 1
Assertion 41prothprmlem2 
|- ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P )

Proof

Step Hyp Ref Expression
1 41prothprm.p 
 |-  P = ; 4 1
2 1 41prothprmlem1 
 |-  ( ( P - 1 ) / 2 ) = ; 2 0
3 2 oveq2i 
 |-  ( 3 ^ ( ( P - 1 ) / 2 ) ) = ( 3 ^ ; 2 0 )
4 3 oveq1i 
 |-  ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 3 ^ ; 2 0 ) mod P )
5 5cn 
 |-  5 e. CC
6 4cn 
 |-  4 e. CC
7 5t4e20 
 |-  ( 5 x. 4 ) = ; 2 0
8 5 6 7 mulcomli 
 |-  ( 4 x. 5 ) = ; 2 0
9 8 eqcomi 
 |-  ; 2 0 = ( 4 x. 5 )
10 9 oveq2i 
 |-  ( 3 ^ ; 2 0 ) = ( 3 ^ ( 4 x. 5 ) )
11 3cn 
 |-  3 e. CC
12 4nn0 
 |-  4 e. NN0
13 5nn0 
 |-  5 e. NN0
14 expmul 
 |-  ( ( 3 e. CC /\ 4 e. NN0 /\ 5 e. NN0 ) -> ( 3 ^ ( 4 x. 5 ) ) = ( ( 3 ^ 4 ) ^ 5 ) )
15 11 12 13 14 mp3an 
 |-  ( 3 ^ ( 4 x. 5 ) ) = ( ( 3 ^ 4 ) ^ 5 )
16 10 15 eqtri 
 |-  ( 3 ^ ; 2 0 ) = ( ( 3 ^ 4 ) ^ 5 )
17 16 oveq1i 
 |-  ( ( 3 ^ ; 2 0 ) mod ; 4 1 ) = ( ( ( 3 ^ 4 ) ^ 5 ) mod ; 4 1 )
18 3z 
 |-  3 e. ZZ
19 zexpcl 
 |-  ( ( 3 e. ZZ /\ 4 e. NN0 ) -> ( 3 ^ 4 ) e. ZZ )
20 18 12 19 mp2an 
 |-  ( 3 ^ 4 ) e. ZZ
21 neg1z 
 |-  -u 1 e. ZZ
22 20 21 pm3.2i 
 |-  ( ( 3 ^ 4 ) e. ZZ /\ -u 1 e. ZZ )
23 1nn 
 |-  1 e. NN
24 12 23 decnncl 
 |-  ; 4 1 e. NN
25 nnrp 
 |-  ( ; 4 1 e. NN -> ; 4 1 e. RR+ )
26 24 25 ax-mp 
 |-  ; 4 1 e. RR+
27 13 26 pm3.2i 
 |-  ( 5 e. NN0 /\ ; 4 1 e. RR+ )
28 3exp4mod41 
 |-  ( ( 3 ^ 4 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
29 modexp 
 |-  ( ( ( ( 3 ^ 4 ) e. ZZ /\ -u 1 e. ZZ ) /\ ( 5 e. NN0 /\ ; 4 1 e. RR+ ) /\ ( ( 3 ^ 4 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 ) ) -> ( ( ( 3 ^ 4 ) ^ 5 ) mod ; 4 1 ) = ( ( -u 1 ^ 5 ) mod ; 4 1 ) )
30 22 27 28 29 mp3an 
 |-  ( ( ( 3 ^ 4 ) ^ 5 ) mod ; 4 1 ) = ( ( -u 1 ^ 5 ) mod ; 4 1 )
31 3p2e5 
 |-  ( 3 + 2 ) = 5
32 31 eqcomi 
 |-  5 = ( 3 + 2 )
33 32 oveq2i 
 |-  ( -u 1 ^ 5 ) = ( -u 1 ^ ( 3 + 2 ) )
34 2z 
 |-  2 e. ZZ
35 m1expaddsub 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( -u 1 ^ ( 3 - 2 ) ) = ( -u 1 ^ ( 3 + 2 ) ) )
36 18 34 35 mp2an 
 |-  ( -u 1 ^ ( 3 - 2 ) ) = ( -u 1 ^ ( 3 + 2 ) )
37 36 eqcomi 
 |-  ( -u 1 ^ ( 3 + 2 ) ) = ( -u 1 ^ ( 3 - 2 ) )
38 2cn 
 |-  2 e. CC
39 ax-1cn 
 |-  1 e. CC
40 2p1e3 
 |-  ( 2 + 1 ) = 3
41 11 38 39 40 subaddrii 
 |-  ( 3 - 2 ) = 1
42 41 oveq2i 
 |-  ( -u 1 ^ ( 3 - 2 ) ) = ( -u 1 ^ 1 )
43 neg1cn 
 |-  -u 1 e. CC
44 exp1 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 1 ) = -u 1 )
45 43 44 ax-mp 
 |-  ( -u 1 ^ 1 ) = -u 1
46 42 45 eqtri 
 |-  ( -u 1 ^ ( 3 - 2 ) ) = -u 1
47 33 37 46 3eqtri 
 |-  ( -u 1 ^ 5 ) = -u 1
48 47 oveq1i 
 |-  ( ( -u 1 ^ 5 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
49 17 30 48 3eqtri 
 |-  ( ( 3 ^ ; 2 0 ) mod ; 4 1 ) = ( -u 1 mod ; 4 1 )
50 1 oveq2i 
 |-  ( ( 3 ^ ; 2 0 ) mod P ) = ( ( 3 ^ ; 2 0 ) mod ; 4 1 )
51 1 oveq2i 
 |-  ( -u 1 mod P ) = ( -u 1 mod ; 4 1 )
52 49 50 51 3eqtr4i 
 |-  ( ( 3 ^ ; 2 0 ) mod P ) = ( -u 1 mod P )
53 4 52 eqtri 
 |-  ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P )