Metamath Proof Explorer

Theorem 41prothprmlem2

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

Ref Expression
Hypothesis 41prothprm.p โŠข ๐‘ƒ = 4 1
Assertion 41prothprmlem2 ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ )

Proof

Step Hyp Ref Expression
1 41prothprm.p โŠข ๐‘ƒ = 4 1
2 1 41prothprmlem1 โŠข ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) = 2 0
3 2 oveq2i โŠข ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = ( 3 โ†‘ 2 0 )
4 3 oveq1i โŠข ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( ( 3 โ†‘ 2 0 ) mod ๐‘ƒ )
5 5cn โŠข 5 โˆˆ โ„‚
6 4cn โŠข 4 โˆˆ โ„‚
7 5t4e20 โŠข ( 5 ยท 4 ) = 2 0
8 5 6 7 mulcomli โŠข ( 4 ยท 5 ) = 2 0
9 8 eqcomi โŠข 2 0 = ( 4 ยท 5 )
10 9 oveq2i โŠข ( 3 โ†‘ 2 0 ) = ( 3 โ†‘ ( 4 ยท 5 ) )
11 3cn โŠข 3 โˆˆ โ„‚
12 4nn0 โŠข 4 โˆˆ โ„•0
13 5nn0 โŠข 5 โˆˆ โ„•0
14 expmul โŠข ( ( 3 โˆˆ โ„‚ โˆง 4 โˆˆ โ„•0 โˆง 5 โˆˆ โ„•0 ) โ†’ ( 3 โ†‘ ( 4 ยท 5 ) ) = ( ( 3 โ†‘ 4 ) โ†‘ 5 ) )
15 11 12 13 14 mp3an โŠข ( 3 โ†‘ ( 4 ยท 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 โˆˆ โ„ค
19 zexpcl โŠข ( ( 3 โˆˆ โ„ค โˆง 4 โˆˆ โ„•0 ) โ†’ ( 3 โ†‘ 4 ) โˆˆ โ„ค )
20 18 12 19 mp2an โŠข ( 3 โ†‘ 4 ) โˆˆ โ„ค
21 neg1z โŠข - 1 โˆˆ โ„ค
22 20 21 pm3.2i โŠข ( ( 3 โ†‘ 4 ) โˆˆ โ„ค โˆง - 1 โˆˆ โ„ค )
23 1nn โŠข 1 โˆˆ โ„•
24 12 23 decnncl โŠข 4 1 โˆˆ โ„•
25 nnrp โŠข ( 4 1 โˆˆ โ„• โ†’ 4 1 โˆˆ โ„+ )
26 24 25 ax-mp โŠข 4 1 โˆˆ โ„+
27 13 26 pm3.2i โŠข ( 5 โˆˆ โ„•0 โˆง 4 1 โˆˆ โ„+ )
28 3exp4mod41 โŠข ( ( 3 โ†‘ 4 ) mod 4 1 ) = ( - 1 mod 4 1 )
29 modexp โŠข ( ( ( ( 3 โ†‘ 4 ) โˆˆ โ„ค โˆง - 1 โˆˆ โ„ค ) โˆง ( 5 โˆˆ โ„•0 โˆง 4 1 โˆˆ โ„+ ) โˆง ( ( 3 โ†‘ 4 ) mod 4 1 ) = ( - 1 mod 4 1 ) ) โ†’ ( ( ( 3 โ†‘ 4 ) โ†‘ 5 ) mod 4 1 ) = ( ( - 1 โ†‘ 5 ) mod 4 1 ) )
30 22 27 28 29 mp3an โŠข ( ( ( 3 โ†‘ 4 ) โ†‘ 5 ) mod 4 1 ) = ( ( - 1 โ†‘ 5 ) mod 4 1 )
31 3p2e5 โŠข ( 3 + 2 ) = 5
32 31 eqcomi โŠข 5 = ( 3 + 2 )
33 32 oveq2i โŠข ( - 1 โ†‘ 5 ) = ( - 1 โ†‘ ( 3 + 2 ) )
34 2z โŠข 2 โˆˆ โ„ค
35 m1expaddsub โŠข ( ( 3 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ( 3 โˆ’ 2 ) ) = ( - 1 โ†‘ ( 3 + 2 ) ) )
36 18 34 35 mp2an โŠข ( - 1 โ†‘ ( 3 โˆ’ 2 ) ) = ( - 1 โ†‘ ( 3 + 2 ) )
37 36 eqcomi โŠข ( - 1 โ†‘ ( 3 + 2 ) ) = ( - 1 โ†‘ ( 3 โˆ’ 2 ) )
38 2cn โŠข 2 โˆˆ โ„‚
39 ax-1cn โŠข 1 โˆˆ โ„‚
40 2p1e3 โŠข ( 2 + 1 ) = 3
41 11 38 39 40 subaddrii โŠข ( 3 โˆ’ 2 ) = 1
42 41 oveq2i โŠข ( - 1 โ†‘ ( 3 โˆ’ 2 ) ) = ( - 1 โ†‘ 1 )
43 neg1cn โŠข - 1 โˆˆ โ„‚
44 exp1 โŠข ( - 1 โˆˆ โ„‚ โ†’ ( - 1 โ†‘ 1 ) = - 1 )
45 43 44 ax-mp โŠข ( - 1 โ†‘ 1 ) = - 1
46 42 45 eqtri โŠข ( - 1 โ†‘ ( 3 โˆ’ 2 ) ) = - 1
47 33 37 46 3eqtri โŠข ( - 1 โ†‘ 5 ) = - 1
48 47 oveq1i โŠข ( ( - 1 โ†‘ 5 ) mod 4 1 ) = ( - 1 mod 4 1 )
49 17 30 48 3eqtri โŠข ( ( 3 โ†‘ 2 0 ) mod 4 1 ) = ( - 1 mod 4 1 )
50 1 oveq2i โŠข ( ( 3 โ†‘ 2 0 ) mod ๐‘ƒ ) = ( ( 3 โ†‘ 2 0 ) mod 4 1 )
51 1 oveq2i โŠข ( - 1 mod ๐‘ƒ ) = ( - 1 mod 4 1 )
52 49 50 51 3eqtr4i โŠข ( ( 3 โ†‘ 2 0 ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ )
53 4 52 eqtri โŠข ( ( 3 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ )