[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem four-square-odd-ls
odd(j0), abs(i3) ≤ j0 / 2, abs(i4) ≤ j0 / 2, abs(i5) ≤ j0 / 2, abs(i6) ≤ j0 / 2, 0 < j0, j0 ≠ 1, 0 < i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 ⊦ i3 ^2 + i4 ^2 + i5 ^2 + i6 ^2 < j0 ^2
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
Lagrange-SumOf4Squares-primes
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 15
Proof steps: 26
Used lemmas:
Used spec theorems:
int-min
/
odd-def
int-div
/
div-add1-pospos
int-square
/
Square-def
int-abs
/
ple
int-square
/
le
int-square
/
two-ls
Used simplifier rules:
int-abs
/
lels
int-abs
/
mone-06
int-abs
/
numls-02
int-mult
/
two-zero
int-abs
/
numadd-01
int-basic2
/
add-zero
int-mult
/
one
int-div
/
div-mult-num
int-abs
/
lels-02
int-mult
/
zero-ge
int-div
/
mod-two-02
int-abs
/
forward-le-05
int-mult
/
zero-gr
int-abs
/
forward-le
int-abs
/
forward-lsle
int-abs
/
forward-lele
int-mult
/
numabs-01
int-mult
/
abs-eqall
int-mult
/
numle-02
int-mult
/
Mult-zero
int-square
/
neq
int-mult
/
eq-pos
int-abs
/
abs-16
int-abs
/
lenls
int-mult
/
numsucc
int-abs
/
forward-lels
int-abs
/
lels-01
int-mult
/
commutativity
int-mult
/
associativity
int-basic2
/
add-c
int-basic2
/
add-a
int-mult
/
add-mult-two