Step |
Hyp |
Ref |
Expression |
1 |
|
gausslemma2dlem0.p |
|- ( ph -> P e. ( Prime \ { 2 } ) ) |
2 |
|
gausslemma2dlem0.m |
|- M = ( |_ ` ( P / 4 ) ) |
3 |
|
gausslemma2dlem0.h |
|- H = ( ( P - 1 ) / 2 ) |
4 |
|
gausslemma2dlem0.n |
|- N = ( H - M ) |
5 |
1 3
|
gausslemma2dlem0b |
|- ( ph -> H e. NN ) |
6 |
5
|
nnzd |
|- ( ph -> H e. ZZ ) |
7 |
1 2
|
gausslemma2dlem0d |
|- ( ph -> M e. NN0 ) |
8 |
7
|
nn0zd |
|- ( ph -> M e. ZZ ) |
9 |
6 8
|
zsubcld |
|- ( ph -> ( H - M ) e. ZZ ) |
10 |
1 2 3
|
gausslemma2dlem0g |
|- ( ph -> M <_ H ) |
11 |
5
|
nnred |
|- ( ph -> H e. RR ) |
12 |
7
|
nn0red |
|- ( ph -> M e. RR ) |
13 |
11 12
|
subge0d |
|- ( ph -> ( 0 <_ ( H - M ) <-> M <_ H ) ) |
14 |
10 13
|
mpbird |
|- ( ph -> 0 <_ ( H - M ) ) |
15 |
|
elnn0z |
|- ( ( H - M ) e. NN0 <-> ( ( H - M ) e. ZZ /\ 0 <_ ( H - M ) ) ) |
16 |
9 14 15
|
sylanbrc |
|- ( ph -> ( H - M ) e. NN0 ) |
17 |
4 16
|
eqeltrid |
|- ( ph -> N e. NN0 ) |