Metamath Proof Explorer

Theorem 41prothprm

Description: 41 is aProth prime. (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypothesis 41prothprm.p 
|- P = ; 4 1
Assertion 41prothprm 
|- ( P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) /\ P e. Prime )

Proof

Step Hyp Ref Expression
1 41prothprm.p 
 |-  P = ; 4 1
2 1 41prothprmlem2 
 |-  ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P )
3 dfdec10 
 |-  ; 4 1 = ( ( ; 1 0 x. 4 ) + 1 )
4 4t2e8 
 |-  ( 4 x. 2 ) = 8
5 4cn 
 |-  4 e. CC
6 2cn 
 |-  2 e. CC
7 5 6 mulcomi 
 |-  ( 4 x. 2 ) = ( 2 x. 4 )
8 4 7 eqtr3i 
 |-  8 = ( 2 x. 4 )
9 8 oveq2i 
 |-  ( 5 x. 8 ) = ( 5 x. ( 2 x. 4 ) )
10 5cn 
 |-  5 e. CC
11 10 6 5 mulassi 
 |-  ( ( 5 x. 2 ) x. 4 ) = ( 5 x. ( 2 x. 4 ) )
12 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
13 12 oveq1i 
 |-  ( ( 5 x. 2 ) x. 4 ) = ( ; 1 0 x. 4 )
14 9 11 13 3eqtr2i 
 |-  ( 5 x. 8 ) = ( ; 1 0 x. 4 )
15 cu2 
 |-  ( 2 ^ 3 ) = 8
16 15 eqcomi 
 |-  8 = ( 2 ^ 3 )
17 16 oveq2i 
 |-  ( 5 x. 8 ) = ( 5 x. ( 2 ^ 3 ) )
18 14 17 eqtr3i 
 |-  ( ; 1 0 x. 4 ) = ( 5 x. ( 2 ^ 3 ) )
19 18 oveq1i 
 |-  ( ( ; 1 0 x. 4 ) + 1 ) = ( ( 5 x. ( 2 ^ 3 ) ) + 1 )
20 1 3 19 3eqtri 
 |-  P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 )
21 simpr 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) )
22 3nn 
 |-  3 e. NN
23 22 a1i 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> 3 e. NN )
24 5nn 
 |-  5 e. NN
25 24 a1i 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> 5 e. NN )
26 5lt8 
 |-  5 < 8
27 26 15 breqtrri 
 |-  5 < ( 2 ^ 3 )
28 27 a1i 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> 5 < ( 2 ^ 3 ) )
29 3z 
 |-  3 e. ZZ
30 29 a1i 
 |-  ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> 3 e. ZZ )
31 oveq1 
 |-  ( x = 3 -> ( x ^ ( ( P - 1 ) / 2 ) ) = ( 3 ^ ( ( P - 1 ) / 2 ) ) )
32 31 oveq1d 
 |-  ( x = 3 -> ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) )
33 32 eqeq1d 
 |-  ( x = 3 -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) <-> ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) )
34 33 adantl 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ x = 3 ) -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) <-> ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) )
35 id 
 |-  ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
36 30 34 35 rspcedvd 
 |-  ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
37 36 adantr 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
38 23 25 21 28 37 proththd 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> P e. Prime )
39 21 38 jca 
 |-  ( ( ( ( 3 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) /\ P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) ) -> ( P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) /\ P e. Prime ) )
40 2 20 39 mp2an 
 |-  ( P = ( ( 5 x. ( 2 ^ 3 ) ) + 1 ) /\ P e. Prime )