Metamath Proof Explorer

Theorem 41prothprm

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

Ref Expression
Hypothesis 41prothprm.p โŠข ๐‘ƒ = 4 1
Assertion 41prothprm ( ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) โˆง ๐‘ƒ โˆˆ โ„™ )

Proof

Step Hyp Ref Expression
1 41prothprm.p โŠข ๐‘ƒ = 4 1
2 1 41prothprmlem2 โŠข ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ )
3 dfdec10 โŠข 4 1 = ( ( 1 0 ยท 4 ) + 1 )
4 4t2e8 โŠข ( 4 ยท 2 ) = 8
5 4cn โŠข 4 โˆˆ โ„‚
6 2cn โŠข 2 โˆˆ โ„‚
7 5 6 mulcomi โŠข ( 4 ยท 2 ) = ( 2 ยท 4 )
8 4 7 eqtr3i โŠข 8 = ( 2 ยท 4 )
9 8 oveq2i โŠข ( 5 ยท 8 ) = ( 5 ยท ( 2 ยท 4 ) )
10 5cn โŠข 5 โˆˆ โ„‚
11 10 6 5 mulassi โŠข ( ( 5 ยท 2 ) ยท 4 ) = ( 5 ยท ( 2 ยท 4 ) )
12 5t2e10 โŠข ( 5 ยท 2 ) = 1 0
13 12 oveq1i โŠข ( ( 5 ยท 2 ) ยท 4 ) = ( 1 0 ยท 4 )
14 9 11 13 3eqtr2i โŠข ( 5 ยท 8 ) = ( 1 0 ยท 4 )
15 cu2 โŠข ( 2 โ†‘ 3 ) = 8
16 15 eqcomi โŠข 8 = ( 2 โ†‘ 3 )
17 16 oveq2i โŠข ( 5 ยท 8 ) = ( 5 ยท ( 2 โ†‘ 3 ) )
18 14 17 eqtr3i โŠข ( 1 0 ยท 4 ) = ( 5 ยท ( 2 โ†‘ 3 ) )
19 18 oveq1i โŠข ( ( 1 0 ยท 4 ) + 1 ) = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 )
20 1 3 19 3eqtri โŠข ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 )
21 simpr โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) )
22 3nn โŠข 3 โˆˆ โ„•
23 22 a1i โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ 3 โˆˆ โ„• )
24 5nn โŠข 5 โˆˆ โ„•
25 24 a1i โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ 5 โˆˆ โ„• )
26 5lt8 โŠข 5 < 8
27 26 15 breqtrri โŠข 5 < ( 2 โ†‘ 3 )
28 27 a1i โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ 5 < ( 2 โ†‘ 3 ) )
29 3z โŠข 3 โˆˆ โ„ค
30 29 a1i โŠข ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ 3 โˆˆ โ„ค )
31 oveq1 โŠข ( ๐‘ฅ = 3 โ†’ ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
32 31 oveq1d โŠข ( ๐‘ฅ = 3 โ†’ ( ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) )
33 32 eqeq1d โŠข ( ๐‘ฅ = 3 โ†’ ( ( ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†” ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
34 33 adantl โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ฅ = 3 ) โ†’ ( ( ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†” ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
35 id โŠข ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
36 30 34 35 rspcedvd โŠข ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ค ( ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
37 36 adantr โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ค ( ( ๐‘ฅ โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
38 23 25 21 28 37 proththd โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ ๐‘ƒ โˆˆ โ„™ )
39 21 38 jca โŠข ( ( ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โˆง ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) ) โ†’ ( ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) โˆง ๐‘ƒ โˆˆ โ„™ ) )
40 2 20 39 mp2an โŠข ( ๐‘ƒ = ( ( 5 ยท ( 2 โ†‘ 3 ) ) + 1 ) โˆง ๐‘ƒ โˆˆ โ„™ )