G.356 even number odd

IX.25

If from an even number an odd number be subtracted, the remainder is odd.
even_number_odd()
prove / A C / is odd
A C D B
construct From the even number / A B / let the odd number / B C / be subtracted
construct Let the unit / C D / be subtracted from / B C /
∵ odd_number_divisible_defassert / B D / is even
assert / A B / is also even
∵ even_number_evenassert / A D / is also even
assert / C D / is an unit
∵ odd_number_divisible_def∴ / A C / is odd

Dependency Graph

digraph { bgcolor="transparent"; node [shape=box, style="rounded,filled", fontname="Helvetica", fontsize=11, color="#d6d3cd", fontcolor="#ffffff"]; edge [color="#8c857b", fontcolor="#8c857b", arrowsize=0.75]; rankdir="TB"; "G.247" [label="G.247", tooltip="G.247 (VII.def.1): Anunit is that by virtue of which each of the things that exist is called one.", fillcolor="#224422", URL="../G.247/index.html", target="_top"]; "G.302" [label="G.302", tooltip="G.302 (VII.def.6): Aneven number is that which is divisible into two equal parts.", fillcolor="#224422", URL="../G.302/index.html", target="_top"]; "G.352" [label="G.352", tooltip="G.352 (VII.def.7): Anodd number is that which is not divisible into two equal parts, or that which differs by anunit from aneven number.", fillcolor="#224422", URL="../G.352/index.html", target="_top"]; "G.355" [label="G.355", tooltip="G.355 (IX.24): If from an even number an even number be subtracted, the remainder is even.", fillcolor="#222244", URL="../G.355/index.html", target="_top"]; "G.356" [label="G.356", tooltip="G.356 (IX.25): If from an even number an odd number be subtracted, the remainder is odd.", penwidth=2.5, color="#e8b85a", fillcolor="#4a453b", URL="index.html", target="_top"]; "G.352" -> "G.247"; "G.356" -> "G.247"; "G.352" -> "G.302"; "G.355" -> "G.302"; "G.356" -> "G.302"; "G.356" -> "G.352"; "G.356" -> "G.355"; }