Metamath Proof Explorer


Theorem gausslemma2dlem4

Description: Lemma 4 for gausslemma2d . (Contributed by AV, 16-Jun-2021)

Ref Expression
Hypotheses gausslemma2d.p
|- ( ph -> P e. ( Prime \ { 2 } ) )
gausslemma2d.h
|- H = ( ( P - 1 ) / 2 )
gausslemma2d.r
|- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
gausslemma2d.m
|- M = ( |_ ` ( P / 4 ) )
Assertion gausslemma2dlem4
|- ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2d.h
 |-  H = ( ( P - 1 ) / 2 )
3 gausslemma2d.r
 |-  R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
4 gausslemma2d.m
 |-  M = ( |_ ` ( P / 4 ) )
5 1 2 3 gausslemma2dlem1
 |-  ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
6 eldif
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ -. P e. { 2 } ) )
7 prm23ge5
 |-  ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) )
8 eleq1
 |-  ( P = 2 -> ( P e. { 2 } <-> 2 e. { 2 } ) )
9 8 notbid
 |-  ( P = 2 -> ( -. P e. { 2 } <-> -. 2 e. { 2 } ) )
10 2ex
 |-  2 e. _V
11 10 snid
 |-  2 e. { 2 }
12 11 2a1i
 |-  ( P = 2 -> ( prod_ k e. ( 1 ... H ) ( R ` k ) =/= ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) -> 2 e. { 2 } ) )
13 12 necon1bd
 |-  ( P = 2 -> ( -. 2 e. { 2 } -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
14 13 a1dd
 |-  ( P = 2 -> ( -. 2 e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
15 9 14 sylbid
 |-  ( P = 2 -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
16 3lt4
 |-  3 < 4
17 breq1
 |-  ( P = 3 -> ( P < 4 <-> 3 < 4 ) )
18 16 17 mpbiri
 |-  ( P = 3 -> P < 4 )
19 3nn0
 |-  3 e. NN0
20 eleq1
 |-  ( P = 3 -> ( P e. NN0 <-> 3 e. NN0 ) )
21 19 20 mpbiri
 |-  ( P = 3 -> P e. NN0 )
22 4nn
 |-  4 e. NN
23 divfl0
 |-  ( ( P e. NN0 /\ 4 e. NN ) -> ( P < 4 <-> ( |_ ` ( P / 4 ) ) = 0 ) )
24 21 22 23 sylancl
 |-  ( P = 3 -> ( P < 4 <-> ( |_ ` ( P / 4 ) ) = 0 ) )
25 18 24 mpbid
 |-  ( P = 3 -> ( |_ ` ( P / 4 ) ) = 0 )
26 4 25 syl5eq
 |-  ( P = 3 -> M = 0 )
27 oveq2
 |-  ( M = 0 -> ( 1 ... M ) = ( 1 ... 0 ) )
28 27 adantr
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... M ) = ( 1 ... 0 ) )
29 fz10
 |-  ( 1 ... 0 ) = (/)
30 28 29 eqtrdi
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... M ) = (/) )
31 30 prodeq1d
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... M ) ( R ` k ) = prod_ k e. (/) ( R ` k ) )
32 prod0
 |-  prod_ k e. (/) ( R ` k ) = 1
33 31 32 eqtrdi
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... M ) ( R ` k ) = 1 )
34 oveq1
 |-  ( M = 0 -> ( M + 1 ) = ( 0 + 1 ) )
35 34 adantr
 |-  ( ( M = 0 /\ ph ) -> ( M + 1 ) = ( 0 + 1 ) )
36 0p1e1
 |-  ( 0 + 1 ) = 1
37 35 36 eqtrdi
 |-  ( ( M = 0 /\ ph ) -> ( M + 1 ) = 1 )
38 37 oveq1d
 |-  ( ( M = 0 /\ ph ) -> ( ( M + 1 ) ... H ) = ( 1 ... H ) )
39 38 prodeq1d
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
40 33 39 oveq12d
 |-  ( ( M = 0 /\ ph ) -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) = ( 1 x. prod_ k e. ( 1 ... H ) ( R ` k ) ) )
41 fzfid
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... H ) e. Fin )
42 oveq1
 |-  ( x = k -> ( x x. 2 ) = ( k x. 2 ) )
43 42 breq1d
 |-  ( x = k -> ( ( x x. 2 ) < ( P / 2 ) <-> ( k x. 2 ) < ( P / 2 ) ) )
44 42 oveq2d
 |-  ( x = k -> ( P - ( x x. 2 ) ) = ( P - ( k x. 2 ) ) )
45 43 42 44 ifbieq12d
 |-  ( x = k -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) )
46 simpr
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> k e. ( 1 ... H ) )
47 elfzelz
 |-  ( k e. ( 1 ... H ) -> k e. ZZ )
48 47 zcnd
 |-  ( k e. ( 1 ... H ) -> k e. CC )
49 2cnd
 |-  ( k e. ( 1 ... H ) -> 2 e. CC )
50 48 49 mulcld
 |-  ( k e. ( 1 ... H ) -> ( k x. 2 ) e. CC )
51 50 adantl
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( k x. 2 ) e. CC )
52 eldifi
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
53 prmz
 |-  ( P e. Prime -> P e. ZZ )
54 53 zcnd
 |-  ( P e. Prime -> P e. CC )
55 1 52 54 3syl
 |-  ( ph -> P e. CC )
56 55 adantr
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> P e. CC )
57 56 51 subcld
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( P - ( k x. 2 ) ) e. CC )
58 51 57 ifcld
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) e. CC )
59 3 45 46 58 fvmptd3
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( R ` k ) = if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) )
60 59 58 eqeltrd
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
61 60 adantll
 |-  ( ( ( M = 0 /\ ph ) /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
62 41 61 fprodcl
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) e. CC )
63 62 mulid2d
 |-  ( ( M = 0 /\ ph ) -> ( 1 x. prod_ k e. ( 1 ... H ) ( R ` k ) ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
64 40 63 eqtr2d
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
65 64 ex
 |-  ( M = 0 -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
66 26 65 syl
 |-  ( P = 3 -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
67 66 a1d
 |-  ( P = 3 -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
68 1 4 gausslemma2dlem0d
 |-  ( ph -> M e. NN0 )
69 68 nn0red
 |-  ( ph -> M e. RR )
70 69 ltp1d
 |-  ( ph -> M < ( M + 1 ) )
71 fzdisj
 |-  ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
72 70 71 syl
 |-  ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
73 72 adantl
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
74 eluzelre
 |-  ( P e. ( ZZ>= ` 5 ) -> P e. RR )
75 4re
 |-  4 e. RR
76 75 a1i
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 e. RR )
77 4ne0
 |-  4 =/= 0
78 77 a1i
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 =/= 0 )
79 74 76 78 redivcld
 |-  ( P e. ( ZZ>= ` 5 ) -> ( P / 4 ) e. RR )
80 79 flcld
 |-  ( P e. ( ZZ>= ` 5 ) -> ( |_ ` ( P / 4 ) ) e. ZZ )
81 nnrp
 |-  ( 4 e. NN -> 4 e. RR+ )
82 22 81 ax-mp
 |-  4 e. RR+
83 eluz2
 |-  ( P e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) )
84 4lt5
 |-  4 < 5
85 5re
 |-  5 e. RR
86 85 a1i
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> 5 e. RR )
87 zre
 |-  ( P e. ZZ -> P e. RR )
88 87 adantl
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> P e. RR )
89 ltleletr
 |-  ( ( 4 e. RR /\ 5 e. RR /\ P e. RR ) -> ( ( 4 < 5 /\ 5 <_ P ) -> 4 <_ P ) )
90 75 86 88 89 mp3an2i
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> ( ( 4 < 5 /\ 5 <_ P ) -> 4 <_ P ) )
91 84 90 mpani
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> ( 5 <_ P -> 4 <_ P ) )
92 91 3impia
 |-  ( ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) -> 4 <_ P )
93 83 92 sylbi
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 <_ P )
94 divge1
 |-  ( ( 4 e. RR+ /\ P e. RR /\ 4 <_ P ) -> 1 <_ ( P / 4 ) )
95 82 74 93 94 mp3an2i
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 <_ ( P / 4 ) )
96 1zzd
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 e. ZZ )
97 flge
 |-  ( ( ( P / 4 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( P / 4 ) <-> 1 <_ ( |_ ` ( P / 4 ) ) ) )
98 79 96 97 syl2anc
 |-  ( P e. ( ZZ>= ` 5 ) -> ( 1 <_ ( P / 4 ) <-> 1 <_ ( |_ ` ( P / 4 ) ) ) )
99 95 98 mpbid
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 <_ ( |_ ` ( P / 4 ) ) )
100 elnnz1
 |-  ( ( |_ ` ( P / 4 ) ) e. NN <-> ( ( |_ ` ( P / 4 ) ) e. ZZ /\ 1 <_ ( |_ ` ( P / 4 ) ) ) )
101 80 99 100 sylanbrc
 |-  ( P e. ( ZZ>= ` 5 ) -> ( |_ ` ( P / 4 ) ) e. NN )
102 101 adantl
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( |_ ` ( P / 4 ) ) e. NN )
103 oddprm
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
104 103 adantr
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( ( P - 1 ) / 2 ) e. NN )
105 prmuz2
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
106 52 105 syl
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 2 ) )
107 106 adantr
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> P e. ( ZZ>= ` 2 ) )
108 fldiv4lem1div2uz2
 |-  ( P e. ( ZZ>= ` 2 ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
109 107 108 syl
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
110 102 104 109 3jca
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
111 110 ex
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. ( ZZ>= ` 5 ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) ) )
112 1 111 syl
 |-  ( ph -> ( P e. ( ZZ>= ` 5 ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) ) )
113 112 impcom
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
114 2 oveq2i
 |-  ( 1 ... H ) = ( 1 ... ( ( P - 1 ) / 2 ) )
115 4 114 eleq12i
 |-  ( M e. ( 1 ... H ) <-> ( |_ ` ( P / 4 ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
116 elfz1b
 |-  ( ( |_ ` ( P / 4 ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
117 115 116 bitri
 |-  ( M e. ( 1 ... H ) <-> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
118 113 117 sylibr
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> M e. ( 1 ... H ) )
119 fzsplit
 |-  ( M e. ( 1 ... H ) -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
120 118 119 syl
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
121 fzfid
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( 1 ... H ) e. Fin )
122 60 adantll
 |-  ( ( ( P e. ( ZZ>= ` 5 ) /\ ph ) /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
123 73 120 121 122 fprodsplit
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
124 123 ex
 |-  ( P e. ( ZZ>= ` 5 ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
125 124 a1d
 |-  ( P e. ( ZZ>= ` 5 ) -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
126 15 67 125 3jaoi
 |-  ( ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
127 7 126 syl
 |-  ( P e. Prime -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
128 127 imp
 |-  ( ( P e. Prime /\ -. P e. { 2 } ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
129 6 128 sylbi
 |-  ( P e. ( Prime \ { 2 } ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
130 1 129 mpcom
 |-  ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
131 5 130 eqtrd
 |-  ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )