Metamath Proof Explorer

Theorem gausslemma2dlem7

Description: Lemma 7 for gausslemma2d . (Contributed by AV, 13-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
gausslemma2d.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
Assertion gausslemma2dlem7 ( 𝜑 → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) = 1 )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3 gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4 gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
5 gausslemma2d.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
6 1 2 3 4 5 gausslemma2dlem6 ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
7 1 2 gausslemma2dlem0b ⊢ ( 𝜑 → 𝐻 ∈ ℕ )
8 7 nnnn0d ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
9 8 faccld ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℕ )
10 9 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℂ )
11 10 mulid2d ⊢ ( 𝜑 → ( 1 · ( ! ‘ 𝐻 ) ) = ( ! ‘ 𝐻 ) )
12 11 eqcomd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ( 1 · ( ! ‘ 𝐻 ) ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( 1 · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
14 13 eqeq1d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) ↔ ( ( 1 · ( ! ‘ 𝐻 ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) ) )
15 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
16 neg1z ⊢ - 1 ∈ ℤ
17 1 4 2 5 gausslemma2dlem0h ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
18 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℤ )
19 16 17 18 sylancr ⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ ℤ )
20 2z ⊢ 2 ∈ ℤ
21 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ 𝐻 ∈ ℕ0 ) → ( 2 ↑ 𝐻 ) ∈ ℤ )
22 20 8 21 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐻 ) ∈ ℤ )
23 19 22 zmulcld ⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) ∈ ℤ )
24 9 nnzd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℤ )
25 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
26 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
27 1 25 26 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
28 1 2 gausslemma2dlem0c ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 )
29 cncongrcoprm ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) ∈ ℤ ∧ ( ! ‘ 𝐻 ) ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 ) ) → ( ( ( 1 · ( ! ‘ 𝐻 ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) )
30 15 23 24 27 28 29 syl32anc ⊢ ( 𝜑 → ( ( ( 1 · ( ! ‘ 𝐻 ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) )
31 14 30 bitrd ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) ↔ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) )
32 simpr ⊢ ( ( 𝜑 ∧ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) → ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) )
33 26 nnred ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
34 prmgt1 ⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
35 33 34 jca ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
36 25 35 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
37 1mod ⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
38 1 36 37 3syl ⊢ ( 𝜑 → ( 1 mod 𝑃 ) = 1 )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) → ( 1 mod 𝑃 ) = 1 )
40 32 39 eqtr3d ⊢ ( ( 𝜑 ∧ ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) ) → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) = 1 )
41 40 ex ⊢ ( 𝜑 → ( ( 1 mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) = 1 ) )
42 31 41 sylbid ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) = 1 ) )
43 6 42 mpd ⊢ ( 𝜑 → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) mod 𝑃 ) = 1 )