#|
Copyright (C) 1994 by David Russinoff.  All Rights Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by David Russinoff.  All Rights
Reserved."
NO WARRANTY
David Russinoff PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL David Russinoff BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
; Mon Sep 17 12:10:54 CDT 1990
; This events file is an addition to the events files described in A
; Computational Logic Handbook.
; This file is a new version of the proof of Gauss's law of quadratic
; reciprocity.  It was composed entirely by David Russinoff, who also
; composed the Wilson and Gauss events in basic.events.  According to
; Russinoff, the version below is much better than the one in basic.events.
; This version also corresponds to a forthcoming paper of Russinoff in
; the Journal of Automated Reasoning.

Event: Start with the library "wilson" using the compiled version.

Definition: squares (n, p)

= if n ≃ 0 then cons (0, nil)

else cons ((n ∗ n) mod p, squares (n − 1, p)) endif

Definition: residue (a, p) = ((a mod p) ∈ squares (p, p))

Theorem: all-squares-1 ((p ≄ 0) ∧ (m ≤ n)) → (((m ∗ m) mod p) ∈ squares (n, p))

Theorem: all-squares-2 ((y ∗ y) mod p) = (((y mod p) ∗ (y mod p)) mod p)

Theorem: all-squares ((p ≄ 0) ∧ (x ∉ squares (p, p))) → (x ≠ ((y ∗ y) mod p))

Theorem: euler-1-1 (¬ divides (2, p)) → ((2 ∗ (p ÷ 2)) = (p − 1))

Theorem: euler-1-2 (¬ divides (2, p)) → (exp (i ∗ i, p ÷ 2) = exp (i, p − 1))

Theorem: euler-1-3 ((a mod p) = (b mod p)) → ((exp (a, c) mod p) = (exp (b, c) mod p))

Theorem: euler-1-4 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, i))) → ((exp (i ∗ i, p ÷ 2) mod p) = 1)

Theorem: euler-1-5 (prime (p) ∧ (¬ divides (p, a)) ∧ ((a mod p) = ((i ∗ i) mod p))) → (¬ divides (p, i))

Theorem: euler-1-6 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ ((a mod p) = ((i ∗ i) mod p))) → ((exp (a, p ÷ 2) mod p) = 1)

Theorem: euler-1-7 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ ((a mod p) ∈ squares (i, p))) → ((exp (a, p ÷ 2) mod p) = 1)

Theorem: euler-1 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ residue (a, p)) → ((exp (a, p ÷ 2) mod p) = 1)

Definition: complement (j , a, p) = ((inverse (j , p) ∗ a) mod p)

Event: Disable inverse.

Theorem: complement-works (prime (p) ∧ (¬ divides (p, j ))) → (((j ∗ complement (j , a, p)) mod p) = (a mod p))

Theorem: bounded-complement (p ≄ 0) → (complement (j , a, p) < p)

Event: Disable complement.

Theorem: non-zerop-complement (prime (p) ∧ (¬ divides (p, j )) ∧ (¬ divides (p, a))) → (complement (j , a, p) ≄ 0)

Theorem: complement-is-unique (prime (p) ∧ (¬ divides (p, a)) ∧ (((j ∗ x) mod p) = (a mod p))) → (complement (j , a, p) = (x mod p))

Event: Disable squares.

Theorem: no-self-complement (prime (p) ∧ (¬ divides (p, j )) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → (j ≠ complement (j , a, p))

Theorem: complement-of-complement (prime (p) ∧ (¬ divides (p, j )) ∧ (¬ divides (p, a))) → (complement (complement (j , a, p), a, p) = (j mod p))

Definition: complements (i, a, p) = if i ≃ 0 then nil

elseif i ∈ complements (i − 1, a, p) then complements (i − 1, a, p) else cons (i, cons (complement (i, a, p), complements (i − 1, a, p))) endif

Theorem: all-non-zerop-complements (prime (p) ∧ (i < p) ∧ (¬ divides (p, a))) → all-non-zerop (complements (i, a, p))

Theorem: bounded-complements (i < p) → all-lesseqp (complements (i, a, p), p − 1)

Theorem: subsetp-positives-complements subsetp (positives (n), complements (n, a, p))

Theorem: complements-closed-1 (prime (p) ∧ (i ≄ 0) ∧ (i < p) ∧ (¬ divides (p, a)) ∧ (j ∈ complements (i, a, p))) → (complement (j , a, p) ∈ complements (i, a, p))

Theorem: complements-closed-2 (prime (p) ∧ (i ≄ 0) ∧ (j ≄ 0) ∧ (i < p) ∧ (j < p) ∧ (¬ divides (p, a)) ∧ (complement (j , a, p) ∈ complements (i, a, p))) → (j ∈ complements (i, a, p))

Theorem: all-distinct-complements-1 (prime (p) ∧ (i < p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p)) ∧ all-distinct (complements (i − 1, a, p))) → all-distinct (complements (i, a, p))

Theorem: all-distinct-complements (prime (p) ∧ (i < p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → all-distinct (complements (i, a, p))

Theorem: perm-positives-complements (prime (p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → perm (positives (p − 1), complements (p − 1, a, p))

Theorem: complements-fact (prime (p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → (times-list (complements (p − 1, a, p)) = fact (p − 1))

Theorem: times-mod-4 (((i ∗ j ) mod p) = (a mod p)) → (((i ∗ (j ∗ k)) mod p) = ((a ∗ (k mod p)) mod p))

Theorem: times-complements-1 ((((i ∗ complement (i, a, p)) mod p) = (a mod p)) ∧ ((i ≄ 0) ∧ (i ∉ complements (i − 1, a, p)))) → ((times-list (complements (i, a, p)) mod p)

= ((a ∗ (times-list (complements (i − 1, a, p)) mod p)) mod p))

Theorem: times-complements-2 (prime (p) ∧ (¬ divides (p, i)) ∧ (i ∉ complements (i − 1, a, p))) → ((times-list (complements (i, a, p)) mod p)

= ((a ∗ (times-list (complements (i − 1, a, p)) mod p)) mod p))

Theorem: quotient-plus-1 ((n ≄ 0) ∧ (x ∈ N) ∧ (y = (x + n))) → ((y ÷ n) = (1 + (x ÷ n)))

Theorem: times-complements-3 ((i ≄ 0) ∧ (i ∉ complements (i − 1, a, p))) → ((length (complements (i, a, p)) ÷ 2)

= (1 + (length (complements (i − 1, a, p)) ÷ 2)))

Theorem: times-complements-4 (prime (p) ∧ (i ≄ 0) ∧ (i < p) ∧ ((times-list (complements (i − 1, a, p)) mod p)

= (exp (a, length (complements (i − 1, a, p)) ÷ 2) mod p))) → ((times-list (complements (i, a, p)) mod p)

= (exp (a, length (complements (i, a, p)) ÷ 2) mod p))

Theorem: times-complements-5 (i ≃ 0) → ((times-list (complements (i, a, p)) mod p)

= (exp (a, length (complements (i, a, p)) ÷ 2) mod p))

Theorem: times-complements (prime (p) ∧ (i < p)) → ((times-list (complements (i, a, p)) mod p)

= (exp (a, length (complements (i, a, p)) ÷ 2) mod p))

Theorem: sub1-length-delete (x ∈ b) → (length (delete (x, b)) = (length (b) − 1))

Theorem: equal-length-perm perm (a, b) → (length (a) = length (b))

Theorem: length-positives length (positives (n)) = fix (n)

Theorem: euler-2-1 (prime (p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → ((exp (a, length (complements (p − 1, a, p)) ÷ 2) mod p) = (p − 1))

Theorem: euler-2-2 (prime (p) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → (length (complements (p − 1, a, p)) = (p − 1))

Theorem: euler-2-3 (p ≄ 0) → (divides (2, p) = (¬ divides (2, p − 1)))

Theorem: euler-2-4 (¬ divides (2, p)) → (((p − 1) ÷ 2) = (p ÷ 2))

Theorem: euler-2 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ (¬ residue (a, p))) → ((exp (a, p ÷ 2) mod p) = (p − 1))

Definition: evenp (x) = if x ≃ 0 then t

else ¬ evenp (x − 1) endif

Theorem: evenp-plus evenp (a + b) = (evenp (a) = evenp (b))

Theorem: evenp-diff evenp (p − x) = ((p < x) ∨ (evenp (p) = evenp (x)))

Theorem: evenp-times evenp (a ∗ b) = (evenp (a) ∨ evenp (b))

Theorem: evenp-even even (p) = evenp (p)

Theorem: even-plus even (a + b) = (even (a) = even (b))

Theorem: even-diff even (p − x) = ((p < x) ∨ (even (p) = even (x)))

Theorem: even-times even (a ∗ b) = (even (a) ∨ even (b))

Theorem: even-rem (¬ even (p)) → (even (p − (x mod p)) = (¬ even (x mod p)))

Theorem: even-add1 even (1 + x) = (¬ even (x))

Event: Disable evenp-even.

Theorem: even-prime-2 (prime (p) ∧ (p ≠ 2)) → (¬ even (p))

Theorem: even-prime (prime (p) ∧ (p ≠ 2)) → ((p mod 2) ≠ 0)

Theorem: euler-criterion (prime (p) ∧ (p ≠ 2) ∧ (¬ divides (p, a))) → ((exp (a, p ÷ 2) mod p)

= if residue (a, p) then 1 else p − 1 endif)

Event: Disable euler-1.

Event: Disable euler-2.

Definition: res1 (n, a, p) = if n ≃ 0 then t

elseif (p ÷ 2) < ((a ∗ n) mod p) then ¬ res1 (n − 1, a, p) else res1 (n − 1, a, p) endif

Definition: reflections (n, a, p) = if n ≃ 0 then nil

elseif (p ÷ 2) < ((a ∗ n) mod p)

then cons (p − ((a ∗ n) mod p), reflections (n − 1, a, p)) else cons ((a ∗ n) mod p, reflections (n − 1, a, p)) endif

Theorem: diff-mod-1 (b ≤ a) → (((a − (b mod p)) mod p) = ((a − b) mod p))

Theorem: rem-diff-times ((x < p) ∧ ((x ≄ 0) ∧ (b ≄ 0))) → ((((b ∗ p) − x) mod p) = (p − x))

Theorem: reflect-commutes-with-times-1 (y ≤ p) → ((((p − y) ∗ x) mod p) = ((p − ((y ∗ x) mod p)) mod p))

Theorem: reflect-commutes-with-times-2 (y ≤ p) → (((x ∗ (p − y)) mod p) = ((p − ((x ∗ y) mod p)) mod p))

Theorem: times-exp-fact (n ≄ 0) → ((((a ∗ n) ∗ (exp (a, n − 1) ∗ fact (n − 1))) mod p)

= ((exp (a, n) ∗ fact (n)) mod p))

Theorem: rem-reflections-1 ((p ≄ 0) ∧ (n ≄ 0) ∧ ((p ÷ 2) ≮ ((a ∗ n) mod p)) ∧ ((times-list (reflections (n − 1, a, p)) mod p)

= ((exp (a, n − 1) ∗ fact (n − 1)) mod p))) → ((times-list (reflections (n, a, p)) mod p)

= ((exp (a, n) ∗ fact (n)) mod p))

Theorem: rem-reflections-2 ((p ≄ 0) ∧ (n ≄ 0) ∧ ((p ÷ 2) < ((a ∗ n) mod p)) ∧ ((times-list (reflections (n − 1, a, p)) mod p)

= ((exp (a, n − 1) ∗ fact (n − 1)) mod p))) → ((times-list (reflections (n, a, p)) mod p)

= ((p − ((exp (a, n) ∗ fact (n)) mod p)) mod p))

Theorem: rem-reflections-3 ((p ≄ 0) ∧ (n ≄ 0) ∧ (((a ∗ n) mod p) ≤ (p ÷ 2)) ∧ ((times-list (reflections (n − 1, a, p)) mod p)

= ((p − ((exp (a, n − 1) ∗ fact (n − 1)) mod p)) mod p))) → ((times-list (reflections (n, a, p)) mod p)

= ((p − ((exp (a, n) ∗ fact (n)) mod p)) mod p))

Theorem: double-reflect (a ≤ p) → (((p − ((p − a) mod p)) mod p) = (a mod p))

Theorem: rem-reflections-4 ((p ≄ 0)

∧ (n ≄ 0) ∧ ((p ÷ 2) < ((a ∗ n) mod p)) ∧ ((times-list (reflections (n − 1, a, p)) mod p)

= ((p − ((exp (a, n − 1) ∗ fact (n − 1)) mod p)) mod p))) → ((times-list (reflections (n, a, p)) mod p)

= ((exp (a, n) ∗ fact (n)) mod p))

Theorem: rem-reflections-base-case (n ≃ 0) → ((times-list (reflections (n, a, p)) mod p)

= ((exp (a, n) ∗ fact (n)) mod p))

Theorem: rem-reflections (p ≄ 0) → ((times-list (reflections (n, a, p)) mod p)

= if res1 (n, a, p) then (exp (a, n) ∗ fact (n)) mod p else (p − ((exp (a, n) ∗ fact (n)) mod p)) mod p endif)

Theorem: length-reflections length (reflections (n, a, p)) = fix (n)

Theorem: all-lesseqp-reflections-1 ((p ÷ 2) < x) → ((p ÷ 2) ≮ (p − x))

Theorem: all-lesseqp-reflections all-lesseqp (reflections (n, a, p), p ÷ 2)

Theorem: all-non-zerop-reflections (prime (p) ∧ (¬ divides (p, a)) ∧ (b < p)) → all-non-zerop (reflections (b, a, p))

Theorem: all-distinct-reflections-1 (prime (p) ∧ (j < i) ∧ (i < p) ∧ (¬ divides (p, a))) → (((a ∗ i) mod p) ≠ ((a ∗ j ) mod p))

Theorem: all-distinct-reflections-2 ((x ∈ N) ∧ (y ∈ N) ∧ (x < p) ∧ (y < p)) → (((p − x) = (p − y)) = (x = y))

Theorem: numberp-remainder (a mod p) ∈ N

Theorem: all-distinct-reflections-3 (prime (p) ∧ (j < i) ∧ (i < p) ∧ (¬ divides (p, a))) → ((p − ((a ∗ i) mod p)) ≠ (p − ((a ∗ j ) mod p)))

Theorem: plus-mod-1 (((x mod p) + y) mod p) = ((x + y) mod p)

Theorem: plus-mod-2 ((y + (x mod p)) mod p) = ((x + y) mod p)

Theorem: all-distinct-reflections-4 ((x = (p − y)) ∧ (y < p)) → (((x + y) mod p) = '0)

Theorem: all-distinct-reflections-5 ((((a ∗ i) mod p) = (p − ((a ∗ j ) mod p))) ∧ (p ≄ 0)) → (((a ∗ (i + j )) mod p) = '0)

Theorem: all-distinct-reflections-6 ((i ≤ (p ÷ 2)) ∧ (j < i)) → (((i + j ) ≄ 0) ∧ ((i + j ) < p))

Theorem: all-distinct-reflections-7 (prime (p) ∧ (¬ divides (p, a)) ∧ (i ≤ (p ÷ 2)) ∧ (j < i)) → (((a ∗ i) mod p) ≠ (p − ((a ∗ j ) mod p)))

Theorem: all-distinct-reflections-8 (prime (p) ∧ (¬ divides (p, a)) ∧ (i ≤ (p ÷ 2)) ∧ (j < i)) → ((p − ((a ∗ i) mod p)) ≠ ((a ∗ j ) mod p))

Theorem: all-distinct-reflections-9 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ (i ≤ (p ÷ 2)) ∧ (j < i)) → (((a ∗ i) mod p) ∉ reflections (j , a, p))

Theorem: all-distinct-reflections-10 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ (i ≤ (p ÷ 2)) ∧ (j < i)) → ((p − ((a ∗ i) mod p)) ∉ reflections (j , a, p))

Theorem: all-distinct-reflections (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ (i ≤ (p ÷ 2))) → all-distinct (reflections (i, a, p))

Theorem: times-reflections (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a))) → (times-list (reflections (p ÷ 2, a, p)) = fact (p ÷ 2))

Theorem: plus-x-x-even ((x + x) mod 2) = '0

Theorem: res1-rem-1-1 ((x ≄ 0) ∧ (¬ divides (2, p))) → (((p − x) mod p) ≠ x)

Theorem: res1-rem-1 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ res1 (p ÷ 2, a, p)) → ((exp (a, p ÷ 2) mod p) = 1)

Theorem: remainder-lessp (a < p) → ((a mod p) = fix (a))

Theorem: res1-rem-2 (prime (p) ∧ (¬ divides (2, p)) ∧ (¬ divides (p, a)) ∧ (¬ res1 (p ÷ 2, a, p))) → ((exp (a, p ÷ 2) mod p) ≠ 1)

Theorem: two-even (¬ divides (2, p)) → ((p − 1) ≠ 1)

Theorem: perm-reflections (prime (p) ∧ (p ≠ 2) ∧ (¬ divides (p, a))) → perm (positives (p ÷ 2), reflections (p ÷ 2, a, p))

Theorem: gauss-lemma-lemma (prime (p) ∧ (¬ divides (p, a)) ∧ (¬ divides (2, p))) → (res1 (p ÷ 2, a, p) = residue (a, p))

Definition: mu (n, a, p) = if n ≃ 0 then t

elseif (p ÷ 2) < ((a ∗ n) mod p) then 1 + mu (n − 1, a, p) else mu (n − 1, a, p) endif

Definition: gauss (a, p) = even (mu (p ÷ 2, a, p))

Theorem: res1-gauss res1 (n, a, p) = even (mu (n, a, p))

Theorem: gauss-lemma (prime (p) ∧ (p ≠ 2) ∧ (¬ divides (p, a))) → (gauss (a, p) = residue (a, p))

Definition: sum (l) = if listp (l) then car (l) + sum (cdr (l))

else 0 endif

Definition: quotients (n, a, p) = if n ≃ 0 then nil

else cons ((a ∗ n) ÷ p, quotients (n − 1, a, p)) endif

Definition: remainders (n, a, p) = if n ≃ 0 then nil

else cons ((a ∗ n) mod p, remainders (n − 1, a, p)) endif

Theorem: quotient-remainder-sum (a ∗ sum (positives (n))) = ((p ∗ sum (quotients (n, a, p))) + sum (remainders (n, a, p)))

Theorem: quotient-remainder-sum-parity even (a ∗ sum (positives (n))) = even ((p ∗ sum (quotients (n, a, p))) + sum (remainders (n, a, p)))

Theorem: even-mu (¬ even (p)) → (even (mu (n, a, p))

= (even (sum (remainders (n, a, p))) ↔ even (sum (reflections (n, a, p)))))

Theorem: perm-sum-lemma (x ∈ m) → ((x + sum (delete (x, m))) = sum (m))

Theorem: perm-sum perm (l, m) → (sum (l) = sum (m))

Theorem: sum-reflections (prime (p) ∧ (p ≠ 2) ∧ (¬ divides (p, a))) → (sum (reflections (p ÷ 2, a, p)) = sum (positives (p ÷ 2)))

Theorem: gauss-quotients (prime (p) ∧ (p ≠ 2) ∧ (¬ even (a)) ∧ (¬ divides (p, a))) → (gauss (a, p) = even (sum (quotients (p ÷ 2, a, p))))

Theorem: equal-residue-even-plus (prime (p) ∧ (p ≠ 2) ∧ prime (q) ∧ (q ≠ 2) ∧ (p ≠ q)) → ((residue (q, p) = residue (p, q))

= even (sum (quotients (p ÷ 2, q, p)) + sum (quotients (q ÷ 2, p, q))))

Definition: w (x, l) = if listp (l)

then if car (l) < x then 1 + w (x, cdr (l))

else w (x, cdr (l)) endif else 0 endif

Definition: wins (k, l) = if listp (k) then w (car (k), l) + wins (cdr (k), l)

else 0 endif

Definition: all-numberp (l) = if listp (l) then (car (l) ∈ N) ∧ all-numberp (cdr (l))

else t endif

Definition: l (x, l) = if listp (l)

then if x < car (l) then 1 + l (x, cdr (l))

else l (x, cdr (l)) endif else 0 endif

Definition: losses (k, l) = if listp (k) then l (car (k), l) + losses (cdr (k), l)

else 0 endif

Theorem: plus-l-w ((x ∉ l) ∧ (x ∈ N) ∧ all-numberp (l)) → ((l (x, l) + w (x, l)) = length (l))

Theorem: plus-wins-losses ((intersect (l, m) ≃ nil) ∧ all-numberp (l) ∧ all-numberp (m)) → ((wins (l, m) + losses (l, m)) = (length (l) ∗ length (m)))

Theorem: equal-wins-losses losses (l, m) = wins (m, l)

Theorem: plus-wins-wins ((intersect (l, m) ≃ nil) ∧ all-numberp (l) ∧ all-numberp (m)) → ((wins (l, m) + wins (m, l)) = (length (l) ∗ length (m)))

Definition: mults (n, p) = if n ≃ 0 then nil

else cons (n ∗ p, mults (n − 1, p)) endif

Theorem: all-numberp-mults (p ≄ 0) → all-numberp (mults (n, p))

Theorem: empty-intersect-mults-lemma (prime (p) ∧ prime (q) ∧ (p ≠ q) ∧ (i < q) ∧ (j < p)) → ((i ∗ p) ∉ mults (j , q))

Theorem: empty-intersect-mults (prime (p) ∧ prime (q) ∧ (p ≠ q) ∧ (i < q)) → (¬ listp (intersect (mults (i, p), mults (p ÷ 2, q))))

Theorem: length-mults (n ∈ N) → (length (mults (n, p)) = n)

Theorem: lessp-a (p ≄ 0) → (a < ((1 + (a ÷ p)) ∗ p))

Theorem: leq-w-n n ≮ w (a, mults (n, p))

Theorem: lessp-rewrite ((a < (m ∗ p)) ∧ (m ≤ n)) → (a < (n ∗ p))

Theorem: lessp-w-m (a < (m ∗ p)) → (w (a, mults (n, p)) < m)

Theorem: leq-w-quotient (p ≄ 0) → (w (a, mults (n, p)) ≤ (a ÷ p))

Theorem: monotone-w (m ≤ n) → (w (a, mults (m, p)) ≤ w (a, mults (n, p)))

Theorem: leq-n-w ((n ∗ p) < a) → (n ≤ w (a, mults (n, p)))

Theorem: leq-quotient-w ((p ≄ 0) ∧ (¬ divides (p, a)) ∧ ((a ÷ p) ≤ n)) → ((a ÷ p) ≤ w (a, mults (n, p)))

Definition: lqq-induct (a, b, c, d) = if b ≃ 0 then t

elseif d ≃ 0 then t

elseif a < d then t

elseif c < b then t

else lqq-induct (a − d, b, c − b, d) endif

Theorem: leq-times-quot ((b ≄ 0) ∧ ((a ∗ b) ≤ (c ∗ d))) → ((a ÷ d) ≤ (c ÷ b))

Theorem: leq-j-a (j ≤ a) → ((j ∗ q) ≤ (a ∗ q))

Theorem: leq-quot-times (j ≤ (p ÷ 2)) → (((j ∗ q) ÷ p) ≤ (q ÷ 2))

Theorem: equal-quot-w (prime (p) ∧ (¬ divides (p, q)) ∧ (j ≄ 0) ∧ (j ≤ (p ÷ 2))) → (w (j ∗ q, mults (q ÷ 2, p)) = ((j ∗ q) ÷ p))

Theorem: equal-wins-sum-quotients (prime (p) ∧ (¬ divides (p, q)) ∧ (j ≤ (p ÷ 2))) → (sum (quotients (j , q, p)) = wins (mults (j , q), mults (q ÷ 2, p)))

Theorem: law-of-quadratic-reciprocity (prime (p) ∧ (p ≠ 2) ∧ prime (q) ∧ (q ≠ 2) ∧ (p ≠ q)) → ((residue (q, p) = residue (p, q)) = even ((p ÷ 2) ∗ (q ÷ 2)))

Index

all-distinct, 4, 10 all-distinct-complements, 4 all-distinct-complements-1, 4 all-distinct-reflections, 10 all-distinct-reflections-1, 9 all-distinct-reflections-10, 10 all-distinct-reflections-2, 9 all-distinct-reflections-3, 9 all-distinct-reflections-4, 10 all-distinct-reflections-5, 10 all-distinct-reflections-6, 10 all-distinct-reflections-7, 10 all-distinct-reflections-8, 10 all-distinct-reflections-9, 10 all-lesseqp, 4, 9 all-lesseqp-reflections, 9 all-lesseqp-reflections-1, 9 all-non-zerop, 3, 9 all-non-zerop-complements, 3 all-non-zerop-reflections, 9 all-numberp, 13, 14 all-numberp-mults, 14 all-squares, 2 all-squares-1, 2 all-squares-2, 2

bounded-complement, 3 bounded-complements, 4

complement, 3–5 complement-is-unique, 3 complement-of-complement, 3 complement-works, 3 complements, 3–6 complements-closed-1, 4 complements-closed-2, 4 complements-fact, 4

delete, 5, 12 diff-mod-1, 7 divides, 2–7, 9–13, 15 double-reflect, 8

empty-intersect-mults, 14 empty-intersect-mults-lemma, 14 equal-length-perm, 5 equal-quot-w, 15 equal-residue-even-plus, 13 equal-wins-losses, 14 equal-wins-sum-quotients, 15 euler-1, 2 euler-1-1, 2 euler-1-2, 2 euler-1-3, 2 euler-1-4, 2 euler-1-5, 2 euler-1-6, 2 euler-1-7, 2 euler-2, 6 euler-2-1, 6 euler-2-2, 6 euler-2-3, 6 euler-2-4, 6 euler-criterion, 7 even, 6, 7, 11–13, 15 even-add1, 7 even-diff, 6 even-mu, 12 even-plus, 6 even-prime, 7 even-prime-2, 7 even-rem, 7 even-times, 6 evenp, 6 evenp-diff, 6 evenp-even, 6 evenp-plus, 6 evenp-times, 6 exp, 2, 5–9, 11

fact, 4, 8, 9, 11

gauss, 11–13 gauss-lemma, 12 gauss-lemma-lemma, 11 gauss-quotients, 13

intersect, 13, 14 inverse, 3

l, 13 law-of-quadratic-reciprocity, 15 length, 5, 6, 9, 13, 14 length-mults, 14 length-positives, 5 length-reflections, 9 leq-j-a, 15 leq-n-w, 14 leq-quot-times, 15 leq-quotient-w, 15 leq-times-quot, 15 leq-w-n, 14 leq-w-quotient, 14 lessp-a, 14 lessp-rewrite, 14 lessp-w-m, 14 losses, 13, 14 lqq-induct, 15

monotone-w, 14 mu, 11, 12 mults, 14, 15

no-self-complement, 3 non-zerop-complement, 3 numberp-remainder, 9

perm, 4, 5, 11, 12 perm-positives-complements, 4 perm-reflections, 11 perm-sum, 12 perm-sum-lemma, 12 plus-l-w, 13 plus-mod-1, 10 plus-mod-2, 10 plus-wins-losses, 13 plus-wins-wins, 14 plus-x-x-even, 11 positives, 4, 5, 11, 12 prime, 2–7, 9–15

quotient-plus-1, 5

quotient-remainder-sum, 12

quotient-remainder-sum-parity, 12 quotients, 12, 13, 15

reflect-commutes-with-times-1, 8 reflect-commutes-with-times-2, 8 reflections, 7–12 rem-diff-times, 7 rem-reflections, 9 rem-reflections-1, 8 rem-reflections-2, 8 rem-reflections-3, 8 rem-reflections-4, 8 rem-reflections-base-case, 9 remainder-lessp, 11 remainders, 12 res1, 7, 9, 11, 12 res1-gauss, 12 res1-rem-1, 11 res1-rem-1-1, 11 res1-rem-2, 11 residue, 2–4, 6, 7, 11–13, 15

squares, 1, 2

sub1-length-delete, 5

subsetp, 4

subsetp-positives-complements, 4 sum, 12, 13, 15 sum-reflections, 12

times-complements, 5 times-complements-1, 5 times-complements-2, 5 times-complements-3, 5 times-complements-4, 5 times-complements-5, 5 times-exp-fact, 8 times-list, 4, 5, 8, 9, 11 times-mod-4, 4 times-reflections, 11 two-even, 11 w, 13–15 wins, 13–15

18