Metamath Proof Explorer

Theorem m1lgs

Description: The first supplement to the law of quadratic reciprocity. Negative one is a square mod an odd prime P iff P == 1 (mod 4 ). See first case of theorem 9.4 in ApostolNT p. 181. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion m1lgs ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( - 1 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 4 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 neg1z โŠข - 1 โˆˆ โ„ค
2 oddprm โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„• )
3 2 nnnn0d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„•0 )
4 zexpcl โŠข ( ( - 1 โˆˆ โ„ค โˆง ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โˆˆ โ„ค )
5 1 3 4 sylancr โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โˆˆ โ„ค )
6 5 peano2zd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) โˆˆ โ„ค )
7 eldifi โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„™ )
8 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
9 7 8 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„• )
10 6 9 zmodcld โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆˆ โ„•0 )
11 10 nn0cnd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆˆ โ„‚ )
12 1cnd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 1 โˆˆ โ„‚ )
13 11 12 12 subaddd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆ’ 1 ) = 1 โ†” ( 1 + 1 ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) ) )
14 2re โŠข 2 โˆˆ โ„
15 14 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 2 โˆˆ โ„ )
16 9 nnrpd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„+ )
17 0le2 โŠข 0 โ‰ค 2
18 17 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 0 โ‰ค 2 )
19 oddprmgt2 โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 2 < ๐‘ƒ )
20 modid โŠข ( ( ( 2 โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( 0 โ‰ค 2 โˆง 2 < ๐‘ƒ ) ) โ†’ ( 2 mod ๐‘ƒ ) = 2 )
21 15 16 18 19 20 syl22anc โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 2 mod ๐‘ƒ ) = 2 )
22 df-2 โŠข 2 = ( 1 + 1 )
23 21 22 eqtrdi โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 2 mod ๐‘ƒ ) = ( 1 + 1 ) )
24 23 eqeq1d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โ†” ( 1 + 1 ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) ) )
25 eldifsni โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โ‰  2 )
26 25 neneqd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ยฌ ๐‘ƒ = 2 )
27 prmuz2 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
28 7 27 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
29 2prm โŠข 2 โˆˆ โ„™
30 dvdsprm โŠข ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง 2 โˆˆ โ„™ ) โ†’ ( ๐‘ƒ โˆฅ 2 โ†” ๐‘ƒ = 2 ) )
31 28 29 30 sylancl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ๐‘ƒ โˆฅ 2 โ†” ๐‘ƒ = 2 ) )
32 26 31 mtbird โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ยฌ ๐‘ƒ โˆฅ 2 )
33 32 adantr โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ยฌ ๐‘ƒ โˆฅ 2 )
34 1cnd โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ 1 โˆˆ โ„‚ )
35 2 adantr โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„• )
36 simpr โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) )
37 oexpneg โŠข ( ( 1 โˆˆ โ„‚ โˆง ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„• โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = - ( 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
38 34 35 36 37 syl3anc โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = - ( 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
39 35 nnzd โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„ค )
40 1exp โŠข ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„ค โ†’ ( 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = 1 )
41 39 40 syl โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = 1 )
42 41 negeqd โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ - ( 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = - 1 )
43 38 42 eqtrd โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = - 1 )
44 43 oveq1d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) = ( - 1 + 1 ) )
45 ax-1cn โŠข 1 โˆˆ โ„‚
46 neg1cn โŠข - 1 โˆˆ โ„‚
47 1pneg1e0 โŠข ( 1 + - 1 ) = 0
48 45 46 47 addcomli โŠข ( - 1 + 1 ) = 0
49 44 48 eqtrdi โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) = 0 )
50 49 oveq2d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) = ( 2 โˆ’ 0 ) )
51 2cn โŠข 2 โˆˆ โ„‚
52 51 subid1i โŠข ( 2 โˆ’ 0 ) = 2
53 50 52 eqtrdi โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) = 2 )
54 53 breq2d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ( ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) โ†” ๐‘ƒ โˆฅ 2 ) )
55 33 54 mtbird โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) )
56 55 ex โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ยฌ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โ†’ ยฌ ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) ) )
57 56 con4d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) โ†’ 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
58 2z โŠข 2 โˆˆ โ„ค
59 58 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 2 โˆˆ โ„ค )
60 moddvds โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง 2 โˆˆ โ„ค โˆง ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) โˆˆ โ„ค ) โ†’ ( ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โ†” ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) ) )
61 9 59 6 60 syl3anc โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โ†” ๐‘ƒ โˆฅ ( 2 โˆ’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) ) ) )
62 4z โŠข 4 โˆˆ โ„ค
63 4ne0 โŠข 4 โ‰  0
64 nnm1nn0 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
65 9 64 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
66 65 nn0zd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ค )
67 dvdsval2 โŠข ( ( 4 โˆˆ โ„ค โˆง 4 โ‰  0 โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ค ) โ†’ ( 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” ( ( ๐‘ƒ โˆ’ 1 ) / 4 ) โˆˆ โ„ค ) )
68 62 63 66 67 mp3an12i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” ( ( ๐‘ƒ โˆ’ 1 ) / 4 ) โˆˆ โ„ค ) )
69 65 nn0cnd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ )
70 51 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 2 โˆˆ โ„‚ )
71 2ne0 โŠข 2 โ‰  0
72 71 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 2 โ‰  0 )
73 69 70 70 72 72 divdiv1d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) = ( ( ๐‘ƒ โˆ’ 1 ) / ( 2 ยท 2 ) ) )
74 2t2e4 โŠข ( 2 ยท 2 ) = 4
75 74 oveq2i โŠข ( ( ๐‘ƒ โˆ’ 1 ) / ( 2 ยท 2 ) ) = ( ( ๐‘ƒ โˆ’ 1 ) / 4 )
76 73 75 eqtrdi โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) = ( ( ๐‘ƒ โˆ’ 1 ) / 4 ) )
77 76 eleq1d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค โ†” ( ( ๐‘ƒ โˆ’ 1 ) / 4 ) โˆˆ โ„ค ) )
78 68 77 bitr4d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค ) )
79 2 nnzd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„ค )
80 dvdsval2 โŠข ( ( 2 โˆˆ โ„ค โˆง 2 โ‰  0 โˆง ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„ค ) โ†’ ( 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โ†” ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค ) )
81 58 71 79 80 mp3an12i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โ†” ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค ) )
82 78 81 bitr4d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” 2 โˆฅ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
83 57 61 82 3imtr4d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โ†’ 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
84 46 a1i โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ - 1 โˆˆ โ„‚ )
85 neg1ne0 โŠข - 1 โ‰  0
86 85 a1i โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ - 1 โ‰  0 )
87 58 a1i โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ 2 โˆˆ โ„ค )
88 78 biimpa โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค )
89 expmulz โŠข ( ( ( - 1 โˆˆ โ„‚ โˆง - 1 โ‰  0 ) โˆง ( 2 โˆˆ โ„ค โˆง ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค ) ) โ†’ ( - 1 โ†‘ ( 2 ยท ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) ) = ( ( - 1 โ†‘ 2 ) โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) )
90 84 86 87 88 89 syl22anc โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( - 1 โ†‘ ( 2 ยท ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) ) = ( ( - 1 โ†‘ 2 ) โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) )
91 2 nncnd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆˆ โ„‚ )
92 91 70 72 divcan2d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 2 ยท ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) )
93 92 adantr โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( 2 ยท ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) )
94 93 oveq2d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( - 1 โ†‘ ( 2 ยท ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) ) = ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) )
95 neg1sqe1 โŠข ( - 1 โ†‘ 2 ) = 1
96 95 oveq1i โŠข ( ( - 1 โ†‘ 2 ) โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = ( 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) )
97 1exp โŠข ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) โˆˆ โ„ค โ†’ ( 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = 1 )
98 88 97 syl โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = 1 )
99 96 98 eqtrid โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( ( - 1 โ†‘ 2 ) โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) / 2 ) ) = 1 )
100 90 94 99 3eqtr3d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) = 1 )
101 100 oveq1d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) = ( 1 + 1 ) )
102 22 101 eqtr4id โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ 2 = ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) )
103 102 oveq1d โŠข ( ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) )
104 103 ex โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) ) )
105 83 104 impbid โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( 2 mod ๐‘ƒ ) = ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โ†” 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
106 13 24 105 3bitr2d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆ’ 1 ) = 1 โ†” 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
107 lgsval3 โŠข ( ( - 1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( - 1 /L ๐‘ƒ ) = ( ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆ’ 1 ) )
108 1 107 mpan โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( - 1 /L ๐‘ƒ ) = ( ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆ’ 1 ) )
109 108 eqeq1d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( - 1 /L ๐‘ƒ ) = 1 โ†” ( ( ( ( - 1 โ†‘ ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) + 1 ) mod ๐‘ƒ ) โˆ’ 1 ) = 1 ) )
110 4nn โŠข 4 โˆˆ โ„•
111 110 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 4 โˆˆ โ„• )
112 prmz โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค )
113 7 112 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„ค )
114 1zzd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 1 โˆˆ โ„ค )
115 moddvds โŠข ( ( 4 โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„ค โˆง 1 โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ mod 4 ) = ( 1 mod 4 ) โ†” 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
116 111 113 114 115 syl3anc โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( ๐‘ƒ mod 4 ) = ( 1 mod 4 ) โ†” 4 โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
117 106 109 116 3bitr4d โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( - 1 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 4 ) = ( 1 mod 4 ) ) )
118 1re โŠข 1 โˆˆ โ„
119 nnrp โŠข ( 4 โˆˆ โ„• โ†’ 4 โˆˆ โ„+ )
120 110 119 ax-mp โŠข 4 โˆˆ โ„+
121 0le1 โŠข 0 โ‰ค 1
122 1lt4 โŠข 1 < 4
123 modid โŠข ( ( ( 1 โˆˆ โ„ โˆง 4 โˆˆ โ„+ ) โˆง ( 0 โ‰ค 1 โˆง 1 < 4 ) ) โ†’ ( 1 mod 4 ) = 1 )
124 118 120 121 122 123 mp4an โŠข ( 1 mod 4 ) = 1
125 124 eqeq2i โŠข ( ( ๐‘ƒ mod 4 ) = ( 1 mod 4 ) โ†” ( ๐‘ƒ mod 4 ) = 1 )
126 117 125 bitrdi โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( ( - 1 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 4 ) = 1 ) )