(*** MAKROER BEGYNDER ***)

1 Makrodefinitioner

Dette afsnit indeholder dé makrodefinitioner, som vi vil gøre brug af i resten af rapporten. Definitionerne drejer sig for det meste om mængdeteoretiske begreber, f.eks. “ækvivalensklasse” og “partition”. Til sidst i afsnittet formulerer vi hovedresultatet — at der til enhver ækvivalensrelation svarer en partition — som et formelt teorem.

1.1 Konnektiver

Ud fra de to basale konnektiver [ ˙¬ x] og [x ⇒ y] definerer vi konjunktion, disjunktion og dobbeltimplikation:

[x ˙∧ y ¨= ˙¬ (x ⇒ ˙¬ y)]
[x ˙∨ y ¨= ˙¬ x ⇒ y]
[x ˙⇔ y ¨= (x ⇒ y) ˙∧ (y ⇒ x)]

1.2 Negerede formler

Det er ganske enkelt at definere negeret lighed (x ≠ y) og negeret medlemskab (x ∉ y):

[x ≠ y ¨= ˙¬ x==y]
[x ∉ y ¨= ˙¬ x ∈ y]^{1}

1.3 Delmængde

Mængden x er en delmængde af y hviss ethvert medlem af x også tilhører y:

[x ⊆ y ¨= (s ∈ x ⇒ s ∈ y)]

1.4 Singleton-mængde

[{x}] er mængden, der indeholder x som sit eneste element. Vi definerer [{x}] ved at parre x med sig selv:

[{x} ¨= {x, x}]

1.5 Binær foreningsmængde og fællesmængde

Vi definerer foreningsmængden mellem to mængder x og y som følger:

[x ∪ y ¨= ∪{{x}, {y}}]

1Højresiderne i disse definitioner skal læses som hhv. [ ˙¬ (x==y)] og [ ˙¬ (x ∈ y)].

Fællesmængden mellem to mængder x og y er en delmængde af deres foreningsmængde:

[x ∩ y ¨= {ph ∈ x ∪ y | ph_{3} ∈ x ˙∧ ph_{3} ∈ y}]

1.6 Relation

Det ordnede par ⟨x, y⟩ indeholder x som “førstekomponent” og y som “andenkomponent”. Den følgende definition af ⟨x, y⟩ er den mest udbredte i litteraturen (se f.eks. afsnit 4.3 i [?] og afsnit 2.1 i [?]):

[⟨x, y⟩ ¨= {{x}, {x, y}}]

Vi kan nu definere en “relation” som en mængde af ordnede par. Vi udtrykker denne definition ved at formalisere, hvad det vil sige, at x er relateret til y i kraft af relationen r:

[r(x, y) ¨= ⟨x, y⟩ ∈ r]

Vi kommer faktisk ikke til at bruge disse to definitioner i rapporten; beviserne vil behandle [r(x, y)] som en primitiv konstruktion. Men det er alligevel betryggende at have det formelle grundlag for relationsbegrebet på plads.

1.7 Ækvivalensrelation

At en relation er refleksiv på en mængde x vil sige, at alle elementer i x er relateret til sig selv:

[ReflRel(r, x) ¨= ∀s: (s ∈ x ⇒ r(s, s))]

At en relation er symmetrisk på en mængde x vil sige, at alle elementer i x opfylder den følgende implikation:

[SymRel(r, x) ¨= ∀s, t: (s ∈ x ⇒ t ∈ x ⇒ r(s, t) ⇒ r(t, s))]

At en relation er transitiv på en mængde x vil sige, at alle elementer i x opfylder den følgende implikation:

[TransRel(r, x) ¨=

∀s, t, u: (s ∈ x ⇒ t ∈ x ⇒ u ∈ x ⇒ r(s, t) ⇒ r(t, u) ⇒ r(s, u))]

Endelig er en ækvivalensrelation det samme som en relation, der er refleksiv, symmetrisk og transitiv:

[EqRel(r, x) ¨= ReflRel(r, x) ˙∧ SymRel(r, x) ˙∧ TransRel(r, x)]

1.8 Mængde-variable

Mange af rapportens beviser sker i forhold til en uspecificeret mængde. Vi vil referere til denne mængde med metavariablen BS og objektvariablen OBS:

[BS ¨= \underline{bs}]
[OBS ¨= \overline{bs}]^{2}

Vi vil så vidt muligt bruge metavariablen, men i afsnit ?? og senere bliver det nødvendigt at gå over til objektvariablen.

1.9 Ækvivalensklasse

Lad r være en ækvivalensrelation defineret på bs, og lad x være et medlem af bs. Vi definerer ækvivalensklassen [x ∈ bs]_{r} som den delmængde af bs, hvis medlemmer står i forhold til x:

[[x ∈ bs]_{r} ¨= {ph ∈ bs | r(ph_{1}, x)}]

Ækvivalenssystemet bs/r er mængden af alle de ækvivalensklasser, som bs definerer på r. Vi definerer bs/r som en delmængde af potensmængden P(bs):

[bs/r ¨= {ph ∈ P(bs) | Ex_{20} ∈ bs ˙∧ [Ex_{20} ∈ bs]_{r} ==ph_{2}}]

2Navnene “BS” og “OBS” står for hhv. for “big set” og “object big set”. Konstruktionerne [\underline{x}] og [\overline{x}] omdanner x til hhv. en meta- og en objektvariabel. Variablen [bs] vil også blive brugt i nogle af de kommende definitioner, men ikke i selve beviserne.

1.10 Partition

En partition af en mængde bs er en mængde p, som opfylder tre krav:

1. Ingen af mængderne i p er tomme.

2. Alle mængderne i p er indbyrdes disjunkte.

3. Foreningsmængden af alle mængderne i p er lig med bs.

Den formelle version af denne definition ser således ud:

[Partition(p, bs) ¨= (∀s: (s ∈ p ⇒ s ≠ Ø)) ˙∧ (∀s, t: (s ∈ p ⇒ t ∈ p ⇒ s ≠ t ⇒ s ∩ t ==Ø)) ˙∧ ∪ p==bs]

(*** MAKROER SLUTTER ***)

2 Deduktionsreglen

Dette bilag præsenterer dén version af deduktionsreglen fra [?], som jeg har gjort brug af. Underafsnit ?? forklarer, hvorfor jeg har ændret på den oprindelige regel, og underafsnit 2.1 indeholder selve den ændrede kode (som er skrevet i L).

2.1 Kode

Funktionen [Dedu(p, c)] er en kopi af [Ded(p, c)] fra [?]:

[Dedu(p, c) ¨= λx.Dedu_{0}(⌈p⌉, ⌈c⌉)]

Jeg har ændret funktionen [Ded_{0}(p, c)], så den kalder [Dedu_{s}(Dedu_{7}(p), c, T)] i stedet for [Ded_{1}(Ded_{7}(p), c, T)]:

[Dedu_{0}(p, c) ˙= c!Dedu_{8}(p, T) ¨∧ Dedu_{s}(Dedu_{7}(p), c, T)]

Funktionen [Dedu_{s}(p, c, s)] giver straks kontrollen videre til [Ded_{1}(p, c, s)] — medmindre p og c begynder med et antal identiske sidebetingelser. I så fald flyttes disse sidebetingelser fra p og c over til listen s, før kontrollen går videre til [Ded_{1}(p, c, s)]:

[Dedu_{s}(p, c, s) ˙= if p =^{r} ⌈x ⊢⊢ y⌉ then c =^{r} ⌈x ⊢⊢ y⌉ ∧ p^{1} =^{t} c^{1} ∧ Dedu_{s}(p^{2}, c^{2}, c^{1} : : s) else Dedu_{1}(p, c, s)]

Fra og med [Ded_{1}(p, c, s)] er koden kopieret fra appendikset til [?]:

[Dedu_{1}(p, c, s) ˙= if c =^{r} ⌈x ⊢⊢ y⌉ then Dedu_{1}(p, c^{2}, c^{1} : : s) else Dedu_{2}(p, c, s)]

[Dedu_{2}(p, c, s) ˙= s!

p =^{r} ⌈x ⊢ y⌉ ∧ c =^{r} ⌈x ⇒ y⌉ \{ \begin{matrix}Dedu_{3}(p^{1}, c^{1}, s, T) ∧ Dedu_{2}(p^{2}, c^{2}, s) \\ Dedu_{4}(p, c, s, Dedu_{6}(p, c, T, T)) \end{matrix} ] [Dedu_{3}(p, c, s, b) ˙= if ¬c =^{r} ⌈∀x: y⌉ then Dedu_{4}(p, c, s, b) else if p =^{r} ⌈∀x: y⌉ ∧ p^{1} =^{t} c^{1} then Dedu_{4}(p, c, s, b) else Dedu_{3}(p, c^{2}, s, (c^{1} : : c^{1}) : : b)]

[Dedu_{4}(p, c, s, b) ˙= s!b! if p =^{r} ⌈x⌉ then lookup(p, b, T) =^{t} c else if ¬p =^{r} c then F else if p =^{r} ⌈∀x: y⌉ then p^{1} =^{t} c^{1} ∧ Dedu_{4}(p^{2}, c^{2}, s, (p^{1} : : p^{1}) : : b) else if ¬p =^{r} ⌈X ⌉ then Dedu_{4}^{∗}(p^{t}, c^{t}, s, b) else p^{1} =^{t} c^{1} ∧ Dedu_{5}(p, s, b)]

[Dedu_{4}^{∗}(p, c, s, b) ˙= c!s!b!if p then T else Dedu_{4}(p^{h}, c^{h}, s, b) ∧ Dedu_{4}^{∗}(p^{t}, c^{t}, s, b)]

[Dedu_{5}(p, s, b) ˙= p!s!if b then T else ⟨⌈x#y⌉^{h}, ⟨⌈⌈∗⌉⌉^{h}, b^{h}^{h}⟩, ⟨⌈⌈x⌉⌉^{h}, p⟩⟩ ∈_{t} s ∧ Dedu_{5}(p, s, b^{t})]

[Dedu_{6}(p, c, e, b) ˙= p!c!b!e!

if p =^{r} ⌈x⌉ then p ∈_{t} e \{ \begin{matrix}b \\ (p : : c) : : b \end{matrix} else

if ¬p =^{r} c then T else if p =^{r} ⌈A⌉ then b else if p =^{r} ⌈∀x: y⌉ then Dedu_{6}(p^{2}, c^{2}, c^{1} : : e, b) else Dedu_{6}^{∗}(p^{t}, c^{t}, e, b)]

[Dedu_{6}^{∗}(p, c, e, b) ˙= p!c!b!e!if p then b else Dedu_{6}^{∗}(p^{t}, c^{t}, e, Dedu_{6}(p^{h}, c^{h}, e, b))]

[Dedu_{7}(p) ˙= p =^{r} ⌈Πx: y⌉ \{ \begin{matrix}Dedu_{7}(p^{2}) \\ p \end{matrix} ]

[Dedu_{8}(p, b) ˙= if p =^{r} ⌈Πx: y⌉ then Dedu_{8}(p^{2}, p^{1} : : b) else if p =^{r} ⌈A⌉ then p ∈_{t} b else Dedu_{8}^{∗}(p^{t}, b)]

[Dedu_{8}^{∗}(p, b) ˙= b!if p then T else Dedu_{8}(p^{h}, b) ¨∧ Dedu_{8}^{∗}(p^{t}, b)]

(*** EKSISTENS-VARIABLE ***)

[x^{Ex} ˙= x =^{r} ⌈x_{Ex}⌉]

Vi kan da definere de fire eksistens-variable, som denne rapport vil gøre brug af (jvf. bilag ??):

[Ex_{1} ¨= a_{Ex}]

[Ex_{2} ¨= b_{Ex}]

[Ex_{10} ¨= j_{Ex}]

[Ex_{20} ¨= t_{Ex}] [⟨a≡b|x:==t⟩_{Ex} ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:==⌈t⌉⟩_{Ex}] [⟨a≡^{0}b|x:==t⟩_{Ex} ˙= λc.x^{Ex} ∧ ⟨a≡^{1}b|x:==t⟩_{Ex}] [⟨a≡^{1}b|x:==t⟩_{Ex} ˙= a!x!t! if b =^{r} ⌈∀u: v⌉ then F else if b^{Ex} ∧ b =^{t} x then a =^{t} t else a =^{r} b ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:==t⟩_{Ex}] [⟨a≡^{∗}b|x:==t⟩_{Ex} ˙= b!x!t!If(a, T, ⟨a^{h}≡^{1}b^{h}|x:==t⟩_{Ex} ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:==t⟩_{Ex})]

(*** AKSIOMATISK SYSTEM ***)

[Theory ZFsub] [ZFsub rule MP: ΠA, B: A ⇒ B ⊢ A ⊢ B] [ZFsub rule Gen: ΠX , A: A ⊢ ∀X: A] [ZFsub rule Repetition: ΠA: A ⊢ A] [ZFsub rule Neg: ΠA, B: ˙¬ B ⇒ A ⊢ ˙¬ B ⇒ ˙¬ A ⊢ B] [ZFsub rule Ded: ΠA, B: Dedu(A, B) ⊢⊢ A ⊢ B] [ZFsub rule ExistIntro: ΠX , T , A, B: ⟨A≡B|X:==T ⟩_{Ex} ⊢⊢ A ⊢ B] [ZFsub rule Extensionality: ΠX , Y: X ==Y ˙⇔ ∀s: (s ∈ X ˙⇔ s ∈ Y)] [ZFsub rule Ødef: ΠS: ˙¬ S ∈ Ø] [ZFsub rule PairDef: ΠS, X , Y: S ∈ {X , Y} ˙⇔ S ==X ˙∨ S ==Y] [ZFsub rule UnionDef: ΠS, X: S ∈ ∪X ˙⇔ (S ∈ Ex_{10} ˙∧ Ex_{10} ∈ X)] [ZFsub rule PowerDef: ΠS, X: S ∈ P(X) ˙⇔ ∀s: (s ∈ S ⇒ s ∈ X)] [ZFsub rule SeparationDef: ΠA, B, P, X , Z: P^{Ph} ∧ ⟨B≡A|P:==Z⟩_{Ph} ⊢⊢ Z ∈ {ph ∈ X | A} ˙⇔ Z ∈ X ˙∧ B]

3 Udsagnslogisk bibliotek

I dette afsnit vil jeg bevise en samling af udsagnslogiske sandheder ( eller “tautologier”), som vil blive brugt i de følgende afsnit. De fleste af disse tautologier har mange andre anvendelser end lige netop mængdelære. Beviserne er fordelt på syv underafsnit; figur 1 giver et overblik over, hvordan beviserne forholder sig til hinanden. Jeg vil kommentere de fleste af beviserne; dog er nogle af dem så tekniske, at jeg har ladet dem stå alene.

3.1 MP-lemmaer

Man får ofte brug for at anvende slutningsreglen MP flere gange i træk. Derfor vil jeg begynde med at vise fire lemmaer, der kan klare mellem 2 og 5 anvendelser af MP^{3}:

[ZFsub lemma MP2: ΠA, B, C: A ⇒ B ⇒ C ⊢ A ⊢ B ⊢ C]

[ZFsub lemma MP3: ΠA, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ A ⊢ B ⊢ C ⊢ D]

[ZFsub lemma MP4: ΠA, B, C, D, E: A ⇒ B ⇒ C ⇒ D ⇒ E ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E]

[ZFsub lemma MP5: ΠA, B, C, D, E, F: A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E ⊢ F]

3.1.1 Det første bevis

Vi begynder med at bevise MP2:

[ZFsub lemma MP2: ΠA, B, C: A ⇒ B ⇒ C ⊢ A ⊢ B ⊢ C]

ZFsub proof of MP2:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: MP ⊳ L02 ⊳ L03 ≫  B ⇒ C  ;
L06: MP ⊳ L05 ⊳ L04 ≫  C  □

Da dette er rapportens første bevis, vil jeg bringe nogle ekstra kommentarer^{4}. Oven over beviset har jeg gentaget definitionen af det, der skal bevises; dette er kun for overblikkets skyld — det er ikke en formel nødvendighed. Selve beviset for MP2 består af seks linier, nummereret fra 1 til 6. En bevislinie kan have to former. Den første form er:

     Argumentation ≫ Konklusion

hvor Konklusion er det som linien beviser, mens teksten i Argumentation udgør en begrundelse for, at Konklusion gælder. F.eks. siger linie 5, at meta-formlen [B ⇒ C] gælder, fordi den kan udledes fra slutningsreglen MP ved substitution. Argumentationen skal læses på den måde, at konklusionerne fra linie 2 og 3 bliver brugt som præmisser til MP. Den generelle betydning af konstruktionen [x ⊳ y] er, at konklusionen fra linie y bliver brugt som præmis i forhold til x.

Den anden form, en bevislinie kan have, er:

     Nøgleord ≫ Konklusion

3I afsnit ?? får vi faktisk brug for at anvende MP 6 gange i træk; men et eller andet sted skal man jo stoppe.

4Denne beskrivelse er en revideret udgave af afsnit 5.1 i [?].

hvor Nøgleord er et af de tre ord “Arbitrary”, “Premise” eller “Side-condition”. Betydningen af ordene “Premise” og “Side-condition” er åbenlys: De angiver, at liniens konklusion indgår som en præmis (hhv. sidebetingelse) i den sætning, der skal bevises. F.eks. siger bevisets linie 2, at MP2 bruger meta-formlen [A ⇒ B ⇒ C] som præmis. Når ordet “Arbitrary” bruges, består konklusionen af en liste af meta-variable (f.eks. [A, B, C] i linie 1). Ideen hermed er at udtrykke, at vi ikke antager noget om de pågældende meta-variable, og at vi derfor har ret til at binde dem med en meta-alkvantor i den sætning, der skal bevises. I det forhåndenværende bevis berettiger linien med “Arbitrary” altså, at MP2 er kvantificeret med [ΠA, B, C: (⋯)].

Alt dette har drejet sig om den formelle syntaks for et Logiweb bevis. Der er ikke så meget at sige om selve beviset for MP2; vi indkapsler simpelthen to på hinanden følgende anvendelser af MP.

3.1.2 Beviser for de andre MP-lemmaer

Beviserne for de øvrige MP-lemmaer er lige ud ad landevejen:

[ZFsub lemma MP3: ΠA, B, C, D: A ⇒ B ⇒ C ⇒ D ⊢ A ⊢ B ⊢ C ⊢ D]

ZFsub proof of MP3:

L01: Arbitrary ≫  A, B, C, D  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D  ;
L07: MP ⊳ L06 ⊳ L05 ≫  D  □

[ZFsub lemma MP4: ΠA, B, C, D, E: A ⇒ B ⇒ C ⇒ D ⇒ E ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E]

ZFsub proof of MP4:

L01: Arbitrary ≫  A, B, C, D, E  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E  ;
L03: Premise ≫  A  ;
L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: MP2 ⊳ L02 ⊳ L03 ⊳ L04 ≫  C ⇒ D ⇒ E  ;
L08: MP2 ⊳ L07 ⊳ L05 ⊳ L06 ≫  E  □

[ZFsub lemma MP5: ΠA, B, C, D, E, F: A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F ⊢ A ⊢ B ⊢ C ⊢ D ⊢ E ⊢ F]

ZFsub proof of MP5:

L01: Arbitrary ≫  A, B, C, D, E, F  ;
L02: Premise ≫  A ⇒ B ⇒ C ⇒ D ⇒ E ⇒ F  ;
L03: Premise ≫  A  ;

L04: Premise ≫  B  ;
L05: Premise ≫  C  ;
L06: Premise ≫  D  ;
L07: Premise ≫  E  ;
L08: MP3⊳L02⊳L03⊳L04⊳L05 ≫ D ⇒ E ⇒ F  ;
L09: MP2 ⊳ L08 ⊳ L06 ⊳ L07 ≫  F  □

3.2 Implikation

Dette afsnit indeholder en række lemmaer vedr. implikation, grupperet i fire under-underafsnit.

3.2.1 Refleksivitet; blok-konstruktionen

Lemmaet AutoImply udsiger, at implikations-relationen er refleksiv:

[ZFsub lemma AutoImply: ΠA: A ⇒ A]

ZFsub proof of AutoImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  A  ;
L04: Repetition ⊳ L03 ≫  A  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  A ⇒ A  □

Beviset for AutoImply indeholder to nye ting i forhold til de hidtidige beviser: En bevisblok, og en anvendelse af deduktions-reglen. En bevisblok er selvstændig enhed i et bevis; den afhænger ikke af den øvrige del af beviset. Den ovenstående bevisblok indeholder et bevis for lemmaet [ΠA: A ⊢ A]. Pointen er nu, at blokkens sidste linie (linie 5) fungerer som en forkortelse for dette lemma. Vi kan da anvende deduktionsreglen på denne linie til at omdanne inferensen [ΠA: A ⊢ A] til implikationen [A ⇒ A]. Det vigtigste formål med deduktionsreglen er netop, at vi let kan skifte fra inferens til implikation.

3.2.2 Transitivitet

Lemmaet ImplyTransitivity udsiger, at implikations-relationen er transitiv:

[ZFsub lemma ImplyTransitivity: ΠA, B, C: A ⇒ B ⊢ B ⇒ C ⊢ A ⇒ C]

Vi viser ImplyTransitivity ved hjælp af MP og deduktionsreglen:

ZFsub proof of ImplyTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C  ;
L03: Premise ≫  A ⇒ B  ;

L04: Premise ≫  B ⇒ C  ;
L05: Premise ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: MP ⊳ L04 ⊳ L06 ≫  C  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  A, B, C  ;
L10: Premise ≫  A ⇒ B  ;
L11: Premise ≫  B ⇒ C  ;
L12: Ded ⊳ L08 ≫  (A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C ;
L13: MP2 ⊳ L12 ⊳ L10 ⊳ L11 ≫  A ⇒ C  □

3.2.3 Svækkelse

Vi får ofte brug for det følgende ræsonnement: Hvis formlen A gælder ubetinget, så gælder den også under antagelse af en vilkårlig anden formel B. Lemmaet Weakening udtrykker dette ræsonnement som følger:

[ZFsub lemma Weakening: ΠA, B: B ⊢ A ⇒ B]

Vi beviser Weakening ved hjælp af deduktionsreglen:

ZFsub proof of Weakening:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B  ;
L04: Premise ≫  A  ;
L05: Repetition ⊳ L03 ≫  B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  B ⇒ A ⇒ B  ;
L09: Premise ≫  B  ;
L10: MP ⊳ L08 ⊳ L09 ≫  A ⇒ B  □

3.2.4 Modsigelse

Det sidste lemma i dette afsnit vedrører strengt taget ikke implikation, men derimod inferens (x ⊢ y). Lemmaet FromContradiction udsiger, at vi kan bevise hvad som helst, hvis vi har bevist to formler, der modsiger hinanden:

[ZFsub lemma FromContradiction: ΠA, B: A ⊢ ˙¬ A ⊢ B]

Beviset bruger Weakening og slutningsreglen Neg:

ZFsub proof of FromContradiction:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A  ;
L03: Premise ≫  ˙¬ A  ;
L04: Weakening ⊳ L02 ≫  ˙¬ B ⇒ A  ;

L05: Weakening ⊳ L03 ≫  ˙¬ B ⇒ ˙¬ A  ;
L06: Neg ⊳ L04 ⊳ L05 ≫  B  □

3.3 Håndtering af dobbeltnegationer

De to lemmaer RemoveDoubleNeg og AddDoubleNeg tillader os hhv. at fjerne og tilføje dobbeltnegationer. Jeg vil ikke kommentere beviserne: [ZFsub lemma RemoveDoubleNeg: ΠA: ˙¬ ˙¬ A ⊢ A] ZFsub proof of RemoveDoubleNeg:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  ˙¬ ˙¬ A  ;
L03: Weakening ⊳ L02 ≫  ˙¬ A ⇒ ˙¬ ˙¬ A  ;
L04: AutoImply ≫  ˙¬ A ⇒ ˙¬ A  ;
L05: Neg ⊳ L04 ⊳ L03 ≫  A  □

[ZFsub lemma AddDoubleNeg: ΠA: A ⊢ ˙¬ ˙¬ A] ZFsub proof of AddDoubleNeg:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  ˙¬ ˙¬ ˙¬ A  ;
L04: RemoveDoubleNeg ⊳ L03 ≫  ˙¬ A  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A  ;
L07: Ded ⊳ L05 ≫  ˙¬ ˙¬ ˙¬ A ⇒ ˙¬ A  ;
L08: Premise ≫  A  ;
L09: Weakening ⊳ L08 ≫  ˙¬ ˙¬ ˙¬ A ⇒ A  ;
L10: Neg ⊳ L09 ⊳ L07 ≫  ˙¬ ˙¬ A  □

3.4 Modus tollens og beslægtede lemmaer

Hovedresultatet fra dette afsnit er slutningsreglen modus tollens, bevist som et lemma: [ZFsub lemma MT: ΠA, B: A ⇒ B ⊢ ˙¬ B ⊢ ˙¬ A] For at vise MT begynder vi med et teknisk lemma, der ikke har den store værdi i sig selv: [ZFsub lemma Technicality: ΠA, B: A ⇒ B ⊢ ˙¬ ˙¬ A ⇒ B] ZFsub proof of Technicality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ ˙¬ A  ;

L05: RemoveDoubleNeg ⊳ L04 ≫  A  ;
L06: MP ⊳ L03 ⊳ L05 ≫  B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (A ⇒ B) ⇒ ˙¬ ˙¬ A ⇒ B  ;
L10: Premise ≫  A ⇒ B  ;
L11: MP ⊳ L09 ⊳ L10 ≫  ˙¬ ˙¬ A ⇒ B  □

Uafhængigt af Technicality kan vi vise en version af MT, hvor A optræder i negeret form: [ZFsub lemma NegativeMT: ΠA, B: ˙¬ A ⇒ B ⊢ ˙¬ B ⊢ A] ZFsub proof of NegativeMT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ˙¬ A ⇒ B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Weakening ⊳ L03 ≫  ˙¬ A ⇒ ˙¬ B  ;
L05: Neg ⊳ L02 ⊳ L04 ≫  A  □

Ud fra Technicality og NegativeMT kan vi nu vise MT: [ZFsub lemma MT: ΠA, B: A ⇒ B ⊢ ˙¬ B ⊢ ˙¬ A] ZFsub proof of MT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Technicality ≫  ˙¬ ˙¬ A ⇒ B  ;
L05: NegativeMT ⊳ L04 ⊳ L03 ≫  ˙¬ A  □

Vi slutter dette underafsnit med en variant af MT, som erstatter en inferens med en implikation: [ZFsub lemma Contrapositive: ΠA, B: A ⇒ B ⊢ ˙¬ B ⇒ ˙¬ A] Når en inferens skal erstattes med en implikation, er det altid deduktionsreglen, der skal i spil: ZFsub proof of Contrapositive:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ˙¬ B  ;
L05: MT ⊳ L03 ⊳ L04 ≫  ˙¬ A  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Premise ≫  A ⇒ B  ;

L09: Ded ⊳ L06 ≫  (A ⇒ B) ⇒ ˙¬ B ⇒ ˙¬ A  ;
L10: MP ⊳ L09 ⊳ L08 ≫  ˙¬ B ⇒ ˙¬ A  □

3.5 Konjunktion

Hovedmålet med dette underafsnit er at konvertere mellem formlerne A og B og deres konjunktion [A ˙∧ B].

3.5.1 Forening af konjunkter

Vi begynder med at slå A og B sammen til [A ˙∧ B]:

[ZFsub lemma JoinConjuncts: ΠA, B: A ⊢ B ⊢ A ˙∧ B]

Beviset for JoinConjuncts er af teknisk karakter. Vi viser den makroekspanderede form [ ˙¬ (A ⇒ ˙¬ B)], som vi i bevisets sidste linie konverterer til [A ˙∧ B]. Denne sidste linie er ikke nødvendig for bevischeckeren, men den gør beviset lidt nemmere at læse:

ZFsub proof of JoinConjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  A ⇒ ˙¬ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  ˙¬ B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ (A ⇒ ˙¬ B) ⇒ ˙¬ B  ;
L09: Premise ≫  A  ;
L10: Premise ≫  B  ;
L11: MP ⊳ L08 ⊳ L09 ≫  (A ⇒ ˙¬ B) ⇒ ˙¬ B  ;
L12: AddDoubleNeg ⊳ L10 ≫  ˙¬ ˙¬ B  ;
L13: MT ⊳ L11 ⊳ L12 ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L14: Repetition ⊳ L13 ≫  A ˙∧ B  □

3.5.2 Udskilning af anden konjunkt

Tautologien SecondConjunct lader os udskille den anden konjunkt fra [A ˙∧ B]. Jeg vil ikke kommentere beviset:

[ZFsub lemma SecondConjunct: ΠA, B: A ˙∧ B ⊢ B]

ZFsub proof of SecondConjunct:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Weakening ⊳ L03 ≫  A ⇒ ˙¬ B  ;
L05: Block ≫  End  ;

L06: Arbitrary ≫  A, B  ;
L07: Ded ⊳ L05 ≫  ˙¬ B ⇒ A ⇒ ˙¬ B  ;
L08: Premise ≫  A ˙∧ B  ;
L09: Repetition ⊳ L08 ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L10: NegativeMT ⊳ L07 ⊳ L09 ≫  B  □

3.5.3 Udskilning af første konjunkt

For at udskille A fra [A ˙∧ B] viser vi først, at [A ˙∧ B] er kommutativ. Jeg vil ikke kommentere beviset:

[ZFsub lemma AndCommutativity: ΠA, B: A ˙∧ B ⊢ B ˙∧ A]

ZFsub proof of AndCommutativity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  B ⇒ ˙¬ A  ;
L04: Premise ≫  A  ;
L05: AddDoubleNeg ⊳ L04 ≫  ˙¬ ˙¬ A  ;
L06: MT ⊳ L03 ⊳ L05 ≫  ˙¬ B  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  A, B  ;
L09: Ded ⊳ L07 ≫  (B ⇒ ˙¬ A) ⇒ A ⇒ ˙¬ B  ;
L10: Premise ≫  A ˙∧ B  ;
L11: Repetition ≫  ˙¬ (A ⇒ ˙¬ B)  ;
L12: MT ⊳ L09 ⊳ L11 ≫  ˙¬ (B ⇒ ˙¬ A)  ;
L13: Repetition ⊳ L12 ≫  B ˙∧ A  □

Nu er det let at udskille den første konjunkt fra [A ˙∧ B]: Først vender vi konjunktionen om til [B ˙∧ A] ved hjælp af AndCommutativity, og så udskiller vi A ved hjælp af SecondConjunct:

[ZFsub lemma FirstConjunct: ΠA, B: A ˙∧ B ⊢ A]

ZFsub proof of FirstConjunct:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∧ B  ;
L03: AndCommutativity ⊳ L02 ≫  B ˙∧ A  ;
L04: SecondConjunct ⊳ L03 ≫  A  □

3.6 Dobbeltimplikation

I dette underafsnit viser vi tre enkle resultater vedr. dobbeltimplikation.

3.6.1 Brug sammen med modus ponens

De følgende to tautologier gør det let at bruge anvende slutningsreglen MP på dobbeltimplikationer. Beviserne er enkle og kræver ingen kommentarer:

[ZFsub lemma IffFirst: ΠA, B: A ˙⇔ B ⊢ B ⊢ A] ZFsub proof of IffFirst:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  B  ;
L04: SecondConjunct ⊳ L02 ≫  B ⇒ A  ;
L05: MP ⊳ L04 ⊳ L03 ≫  A  □

[ZFsub lemma IffSecond: ΠA, B: A ˙⇔ B ⊢ A ⊢ B] ZFsub proof of IffSecond:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Premise ≫  A  ;
L04: FirstConjunct ⊳ L02 ≫  A ⇒ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  B  □

3.6.2 Kommutativitet Lemmaet IffCommutativity følger direkte af, at operatoren [x ˙∧ y] er kommutativ: [ZFsub lemma IffCommutativity: ΠA, B: A ˙⇔ B ⊢ B ˙⇔ A] ZFsub proof of IffCommutativity:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙⇔ B  ;
L03: Repetition ⊳ L02 ≫  (A ⇒ B) ˙∧ (B ⇒ A)  ;
L04: AndCommutativity ⊳ L03 ≫  (B ⇒ A) ˙∧ (A ⇒ B)  ;
L05: Repetition ⊳ L04 ≫  B ˙⇔ A  □

3.7 Disjunktion

Dette underafsnit indeholder tre lemmaer vedr. disjunktion, som vi fordeler på to under-underafsnit. 3.7.1 Svækkelse Givet en påstand B vil vi gerne udlede de svagere påstande [A ˙∨ B] og [B ˙∨ A]. Den første slutning varetages af lemmaet WeakenOr1: [ZFsub lemma WeakenOr1: ΠA, B: B ⊢ A ˙∨ B] Beviset består af en simpel anvendelse af Weakening: ZFsub proof of WeakenOr1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  B  ;

L03: Weakening ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L04: Repetition ⊳ L03 ≫  A ˙∨ B  □

Slutningen fra A til [A ˙∨ B] varetages af lemmaet WeakenOr2: [ZFsub lemma WeakenOr2: ΠA, B: A ⊢ A ˙∨ B] Kernen i beviset for WeakenOr2 er en anvendelse af FromContradiction: ZFsub proof of WeakenOr2:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ˙¬ A  ;

L05: FromContradiction ⊳ L03 ⊳

L04 ≫ B ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  A, B  ;
L08: Ded ⊳ L06 ≫  A ⇒ ˙¬ A ⇒ B  ;
L09: Premise ≫  A  ;
L10: MP ⊳ L08 ⊳ L09 ≫  ˙¬ A ⇒ B  ;
L11: Repetition ⊳ L10 ≫  A ˙∨ B  □

3.7.2 Slutning ud fra disjunktion Lemmaet FromDisjuncts lader os drage slutninger ud fra en disjunktion: [ZFsub lemma FromDisjuncts: ΠA, B, C: A ˙∨ B ⊢ A ⇒ C ⊢ B ⇒ C ⊢ C] Om beviset vil jeg kun sige, at det er en ret elegant øvelse i bevisteknik: ZFsub proof of FromDisjuncts:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  A ⇒ C  ;
L04: Premise ≫  B ⇒ C  ;
L05: Repetition ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L06: Contrapositive ⊳ L05 ≫  ˙¬ B ⇒ ˙¬ ˙¬ A  ;
L07: Technicality ⊳ L03 ≫  ˙¬ ˙¬ A ⇒ C  ;
L08: ImplyTransitivity⊳L06⊳L07 ≫ ˙¬ B ⇒ C  ;
L09: Contrapositive ⊳ L08 ≫  ˙¬ C ⇒ ˙¬ ˙¬ B  ;
L10: Contrapositive ⊳ L04 ≫  ˙¬ C ⇒ ˙¬ B  ;
L11: Neg ⊳ L10 ⊳ L09 ≫  C  □

(********************) Priority table Preassociative [am], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [a], [b], [c], [d], [e], [f ], [g], [h], [i], [j ], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [x], [y], [z], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [(⋯)], [Objekt-var], [Ex-var], [Ph-var], [Værdi], [Variabel], [Op(∗)], [Op(∗, ∗)], [∗ ¨ == ∗], [ContainsEmpty(∗)], [Dedu(∗, ∗)], [Dedu_{0}(∗, ∗)], [Dedu_{s}(∗, ∗, ∗)], [Dedu_{1}(∗, ∗, ∗)], [Dedu_{2}(∗, ∗, ∗)], [Dedu_{3}(∗, ∗, ∗, ∗)], [Dedu_{4}(∗, ∗, ∗, ∗)], [Dedu_{4}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{5}(∗, ∗, ∗)], [Dedu_{6}(∗, ∗, ∗, ∗)], [Dedu_{6}^{∗}(∗, ∗, ∗, ∗)], [Dedu_{7}(∗)], [Dedu_{8}(∗, ∗)], [Dedu_{8}^{∗}(∗, ∗)], [Ex_{1}], [Ex_{2}], [Ex3], [Ex_{10}], [Ex_{20}], [∗_{Ex}], [∗^{Ex}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex}], [ph_{1}], [ph_{2}], [ph_{3}], [∗_{Ph}], [∗^{Ph}], [⟨∗≡ ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph}], [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph}], [bs], [OBS], [BS], [Ø], [ZFsub], [MP], [Gen], [Repetition], [Neg], [Ded], [ExistIntro], [Extensionality], [Ødef], [PairDef], [UnionDef], [PowerDef], [SeparationDef], [AddDoubleNeg], [RemoveDoubleNeg], [AndCommutativity], [AutoImply], [Contrapositive], [FirstConjunct], [SecondConjunct], [FromContradiction], [FromDisjuncts], [IffCommutativity], [IffFirst], [IffSecond], [ImplyTransitivity], [JoinConjuncts], [MP2], [MP3], [MP4], [MP5], [MT], [NegativeMT], [Technicality], [Weakening], [WeakenOr1], [WeakenOr2], [Formula2Pair], [Pair2Formula], [Formula2Union], [Union2Formula], [Formula2Sep], [Sep2Formula], [SubsetInPower], [HelperPowerIsSub], [PowerIsSub], [(Switch)HelperPowerIsSub], [(Switch)PowerIsSub], [ToSetEquality], [HelperToSetEquality(t)], [ToSetEquality(t)], [HelperFromSetEquality], [FromSetEquality], [HelperReflexivity], [Reflexivity], [HelperSymmetry], [Symmetry], [HelperTransitivity], [Transitivity], [ERisReflexive], [ERisSymmetric], [ERisTransitive], [ØisSubset], [HelperMemberNotØ], [MemberNotØ], [HelperUniqueØ], [UniqueØ], [==Reflexivity], [==Symmetry], [Helper==Transitivity], [==Transitivity], [HelperTransferNotEq], [TransferNotEq], [HelperPairSubset], [Helper(2)PairSubset], [PairSubset], [SamePair], [SameSingleton], [UnionSubset], [SameUnion], [SeparationSubset], [SameSeparation], [SameBinaryUnion], [IntersectionSubset], [SameIntersection], [AutoMember], [HelperEqSysNotØ], [EqSysNotØ], [HelperEqSubset], [EqSubset], [HelperEqNecessary], [EqNecessary], [HelperNoneEqNecessary], [Helper(2)NoneEqNecessary], [NoneEqNecessary], [EqClassIsSubset], [EqClassesAreDisjoint], [AllDisjoint], [AllDisjointImply], [BSsubset], [Union(BS/R)subset], [UnionIdentity], [EqSysIsPartition], [(ϵ)], [(fx)], [(fy)], [(fz)], [(fv)], [var fv], [(rx)], [(ry)], [(rz)], [(ru)], [ϵ], [FX], [FY], [FZ], [FU], [FV], [RX], [RY], [RZ], [RU], [0], [1], [(−1)], [2], [1/2], [0f], [1f], [00], [01], [leqReflexivity], [leqAntisymmetryAxiom], [leqTransitivityAxiom], [leqTotality], [leqAdditionAxiom], [leqMultiplicationAxiom], [plusAssociativity], [plusCommutativity], [Negative], [plus0], [timesAssociativity], [timesCommutativity], [ReciprocalAxiom], [times1], [Distribution], [0not1], [equalityAxiom], [eqLeqAxiom], [eqAdditionAxiom], [eqMultiplicationAxiom], [SENC1], [SENC2], [IfThenElse(T)], [IfThenElse(F)], [From = f], [To = f], [From < f], [To < f], [PlusF], [TimesF], [MinusF], [0f], [1f], [FromSF], [ToSF], [To == XX], [From ==], [To ==], [From << XX], [From << (1)], [From << (2)], [to << XX], [From <<], [To <<], [FromInR], [PlusR], [TimesR], [leqAntisymmetry], [leqTransitivity], [leqAddition], [leqMultiplication], [Reciprocal], [Equality], [eqLeq], [eqAddition], [eqMultiplication], [ToNegatedImply], [TND], [ImplyNegation], [FromNegations], [From3Disjuncts], [From2 ∗ 2Disjuncts], [NegateDisjunct1], [NegateDisjunct2], [ExpandDisjuncts], [eqReflexivity], [eqSymmetry], [eqTransitivity], [eqTransitivity4], [eqTransitivity5], [eqTransitivity6], [plus0Left], [times1Left], [lemma eqAdditionLeft], [EqMultiplicationLeft], [DistributionOut], [Three2twoTerms], [Three2threeTerms], [Three2threeFactors], [AddEquations], [SubtractEquations], [SubtractEquationsLeft], [EqNegated], [PositiveToRight(Eq)], [PositiveToLeft(Eq)(1term)], [NegativeToLeft(Eq)], [LessNeq], [NeqSymmetry], [NeqNegated], [SubNeqRight], [SubNeqLeft], [NeqAddition], [NeqMultiplication], [UniqueNegative], [DoubleMinus], [LeqLessEq], [LessLeq], [FromLeqGeq], [subLeqRight], [subLeqLeft], [Leq + 1], [PositiveToRight(Leq)], [PositiveToRight(Leq)(1term)], [negativeToLeft(Leq)], [LeqAdditionLeft], [leqSubtraction], [leqSubtractionLeft], [thirdGeq], [LeqNegated], [AddEquations(Leq)], [ThirdGeqSeries], [LeqNeqLess], [FromLess], [ToLess], [fromNotLess], [toNotLess], [NegativeLessPositive], [leqLessTransitivity], [LessLeqTransitivity], [LessTransitivity], [LessTotality], [SubLessRight], [SubLessLeft], [LessAddition], [LessAdditionLeft], [LessMultiplication], [LessMultiplicationLeft], [LessDivision], [AddEquations(Less)], [LessNegated], [PositiveNegated], [NonpositiveNegated], [NegativeNegated], [NonnegativeNegated], [PositiveHalved], [NonnegativeNumerical], [NegativeNumerical], [PositiveNumerical], [lemma nonpositiveNumerical], [|0| = 0], [0 <= |x|], [SameNumerical], [SignNumerical(+)], [SignNumerical], [NumericalDifference], [SplitNumericalSumHelper], [splitNumericalSum(++)], [splitNumericalSum(−−)], [splitNumericalSum(+ − small)], [splitNumericalSum(+ − big)], [splitNumericalSum(+−)], [splitNumericalSum(−+)], [splitNumericalSum], [insertMiddleTerm(Numerical)], [x + y = zBackwards], [x ∗ y = zBackwards], [x = x + (y − y)], [x = x + y − y], [], [insertMiddleTerm(Sum)], [insertMiddleTerm(Difference)], [x ∗ 0 + x = x], [x ∗ 0 = 0], [(−1) ∗ (−1) + (−1) ∗ 1 = 0], [(−1) ∗ (−1) = 1], [0 < 1Helper], [0 < 1], [0 < 2], [0 < 1/2], [TwoWholes], [TwoHalves], [−x − y = −(x + y)], [MinusNegated], [Times(−1)], [Times(−1)Left], [−0 = 0], [SFsymmetry], [SFtransitivity], [= fToSameF], [PlusF(Sym)], [TimesF(Sym)], [f2R(Plus)], [f2R(Times)], [PlusR(Sym)], [TimesR(Sym)], [LessLeq(R)], [eqLeq(R)], [SubLessRight(R)], [SubLessLeft(R)], [<< TransitivityHelper(Q)], [<< Transitivity], [<<== Reflexivity], [<<== AntisymmetryHelper(Q)], [<<== Antisymmetry], [<<== Transitivity], [Plus0f], [Plus00], [== Addition], [== AdditionLeft], [<< Addition], [<<== Addition], [PlusAssociativity(F)], [PlusAssociativity(R)], [Negative(R)], [PlusCommutativity(F)], [PlusCommutativity(R)], [TimesAssociativity(F)], [TimesAssociativity(R)], [Times1f], [Times01], [TimesCommutativity(F)], [TimesCommutativity(R)], [Distribution(F)], [Distribution(R)]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗^{hide}]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], ["∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗′], [R(∗)], [− − R(∗)], [rec∗]; Preassociative [∗/∗], [∗ ∩ ∗], [∗[∗]]; Preassociative [∪∗], [∗ ∪ ∗], [P(∗)]; Preassociative [{∗}]; Preassociative [{∗, ∗}], [⟨∗, ∗⟩], [−∗], [−_{f}∗]; Preassociative [∗ ∈ ∗], [∗(∗, ∗)], [ReflRel(∗, ∗)], [SymRel(∗, ∗)], [TransRel(∗, ∗)], [EqRel(∗, ∗)], [[∗ ∈ ∗]_{∗}], [Partition(∗, ∗)]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ∗ ∗], [∗ ∗_{f} ∗], [∗ ∗ ∗∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ + ∗], [∗ − ∗], [∗ +_{f} ∗], [∗ −_{f} ∗], [∗ + +∗], [R(∗) − −R(∗)]; Preassociative [| ∗ |], [if(∗, ∗, ∗)]; Preassociative [∗ = ∗], [∗ ≠ ∗], [∗ <= ∗], [∗ < ∗], [∗ =_{f} ∗], [∗ <_{f} ∗], [SF(∗, ∗)], [∗ == ∗], [∗ << ∗], [∗ <<== ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗==∗], [∗ ⊆ ∗]; Preassociative [¬∗], [ ˙¬ ∗], [∗ ∉ ∗], [∗ ≠ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ˙∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗], [∗ ˙⇔ ∗]; Preassociative [{ph ∈ ∗ | ∗}]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗], [Π∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; End table

A Pyk definitioner

([(⋯) →^{pyk} “cdots”] [Objekt-var →^{pyk} “object-var”] [Ex-var →^{pyk} “ex-var”] [Ph-var →^{pyk} “ph-var”] [Værdi →^{pyk} “vaerdi”] [Variabel →^{pyk} “variabel”] [Op(∗) →^{pyk} “op " end op”] [Op(∗, ∗) →^{pyk} “op2 " comma " end op2”] [∗ ¨ == ∗ →^{pyk} “define-equal " comma " end equal”] [ContainsEmpty(∗) →^{pyk} “contains-empty " end empty”] [Dedu(∗, ∗) →^{pyk} “1deduction " conclude " end 1deduction”] [Dedu_{0}(∗, ∗) →^{pyk} “1deduction zero " conclude " end 1deduction”] [Dedu_{s}(∗, ∗, ∗) →^{pyk} “1deduction side " conclude " condition " end 1deduction”] [Dedu_{1}(∗, ∗, ∗) →^{pyk} “1deduction one " conclude " condition " end 1deduction”] [Dedu_{2}(∗, ∗, ∗) →^{pyk} “1deduction two " conclude " condition " end 1deduction”] [Dedu_{3}(∗, ∗, ∗, ∗) →^{pyk} “1deduction three " conclude " condition " bound " end 1deduction”] [Dedu_{4}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four " conclude " condition " bound " end 1deduction”] [Dedu_{4}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction four star " conclude " condition " bound " end 1deduction”] [Dedu_{5}(∗, ∗, ∗) →^{pyk} “1deduction five " condition " bound " end 1deduction”] [Dedu_{6}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six " conclude " exception " bound " end 1deduction”] [Dedu_{6}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “1deduction six star " conclude " exception " bound " end 1deduction”] [Dedu_{7}(∗) →^{pyk} “1deduction seven " end 1deduction”] [Dedu_{8}(∗, ∗) →^{pyk} “1deduction eight " bound " end 1deduction”] [Dedu_{8}^{∗}(∗, ∗) →^{pyk} “1deduction eight star " bound " end 1deduction”]

[Ex_{1} →^{pyk} “ex1”]

[Ex_{2} →^{pyk} “ex2”]

[Ex3 →^{pyk} “ex3”]

[Ex_{10} →^{pyk} “ex10”]

[Ex_{20} →^{pyk} “ex20”]

[∗_{Ex} →^{pyk} “existential var " end var”] [∗^{Ex} →^{pyk} “" is existential var”] [⟨∗≡ ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex} →^{pyk} “exist-sub∗ " is " where " is " end sub”] [ph_{1} →^{pyk} “placeholder-var1”] [ph_{2} →^{pyk} “placeholder-var2”] [ph_{3} →^{pyk} “placeholder-var3”] [∗_{Ph} →^{pyk} “placeholder-var " end var”] [∗^{Ph} →^{pyk} “" is placeholder-var”] [⟨∗≡ ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub " is " where " is " end sub”] [⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub0 " is " where " is " end sub”] [⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub1 " is " where " is " end sub”] [⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph} →^{pyk} “ph-sub∗ " is " where " is " end sub”] [bs →^{pyk} “var big set”] [OBS →^{pyk} “object big set”] [BS →^{pyk} “meta big set”] [Ø →^{pyk} “zermelo empty set”] [ZFsub →^{pyk} “system Q”] [MP →^{pyk} “1rule mp”] [Gen →^{pyk} “1rule gen”] [Repetition →^{pyk} “1rule repetition”] [Neg →^{pyk} “1rule ad absurdum”] [Ded →^{pyk} “1rule deduction”] [ExistIntro →^{pyk} “1rule exist intro”] [Extensionality →^{pyk} “axiom extensionality”] [Ødef →^{pyk} “axiom empty set”] [PairDef →^{pyk} “axiom pair definition”] [UnionDef →^{pyk} “axiom union definition”] [PowerDef →^{pyk} “axiom power definition”] [SeparationDef →^{pyk} “axiom separation definition”] [AddDoubleNeg →^{pyk} “prop lemma add double neg”] [RemoveDoubleNeg →^{pyk} “prop lemma remove double neg”] [AndCommutativity →^{pyk} “prop lemma and commutativity”] [AutoImply →^{pyk} “prop lemma auto imply”] [Contrapositive →^{pyk} “prop lemma contrapositive”] [FirstConjunct →^{pyk} “prop lemma first conjunct”] [SecondConjunct →^{pyk} “prop lemma second conjunct”] [FromContradiction →^{pyk} “prop lemma from contradiction”] [FromDisjuncts →^{pyk} “prop lemma from disjuncts”] [IffCommutativity →^{pyk} “prop lemma iff commutativity”] [IffFirst →^{pyk} “prop lemma iff first”] [IffSecond →^{pyk} “prop lemma iff second”] [ImplyTransitivity →^{pyk} “prop lemma imply transitivity”] [JoinConjuncts →^{pyk} “prop lemma join conjuncts”] [MP2 →^{pyk} “prop lemma mp2”] [MP3 →^{pyk} “prop lemma mp3”] [MP4 →^{pyk} “prop lemma mp4”] [MP5 →^{pyk} “prop lemma mp5”] [MT →^{pyk} “prop lemma mt”] [NegativeMT →^{pyk} “prop lemma negative mt”] [Technicality →^{pyk} “prop lemma technicality”] [Weakening →^{pyk} “prop lemma weakening”] [WeakenOr1 →^{pyk} “prop lemma weaken or first”] [WeakenOr2 →^{pyk} “prop lemma weaken or second”] [Formula2Pair →^{pyk} “lemma formula2pair”] [Pair2Formula →^{pyk} “lemma pair2formula”] [Formula2Union →^{pyk} “lemma formula2union”] [Union2Formula →^{pyk} “lemma union2formula”] [Formula2Sep →^{pyk} “lemma formula2separation”] [Sep2Formula →^{pyk} “lemma separation2formula”] [SubsetInPower →^{pyk} “lemma subset in power set”] [HelperPowerIsSub →^{pyk} “lemma power set is subset0”] [PowerIsSub →^{pyk} “lemma power set is subset”] [(Switch)HelperPowerIsSub →^{pyk} “lemma power set is subset0-switch”] [(Switch)PowerIsSub →^{pyk} “lemma power set is subset-switch”] [ToSetEquality →^{pyk} “lemma set equality suff condition”] [HelperToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)0”] [ToSetEquality(t) →^{pyk} “lemma set equality suff condition(t)”] [HelperFromSetEquality →^{pyk} “lemma set equality skip quantifier”] [FromSetEquality →^{pyk} “lemma set equality nec condition”] [HelperReflexivity →^{pyk} “lemma reflexivity0”] [Reflexivity →^{pyk} “lemma reflexivity”] [HelperSymmetry →^{pyk} “lemma symmetry0”] [Symmetry →^{pyk} “lemma symmetry”] [HelperTransitivity →^{pyk} “lemma transitivity0”] [Transitivity →^{pyk} “lemma transitivity”] [ERisReflexive →^{pyk} “lemma er is reflexive”] [ERisSymmetric →^{pyk} “lemma er is symmetric”] [ERisTransitive →^{pyk} “lemma er is transitive”] [ØisSubset →^{pyk} “lemma empty set is subset”] [HelperMemberNotØ →^{pyk} “lemma member not empty0”] [MemberNotØ →^{pyk} “lemma member not empty”] [HelperUniqueØ →^{pyk} “lemma unique empty set0”] [UniqueØ →^{pyk} “lemma unique empty set”] [==Reflexivity →^{pyk} “lemma ==Reflexivity”] [==Symmetry →^{pyk} “lemma ==Symmetry”] [Helper==Transitivity →^{pyk} “lemma ==Transitivity0”] [==Transitivity →^{pyk} “lemma ==Transitivity”] [HelperTransferNotEq →^{pyk} “lemma transfer ˜ is0”] [TransferNotEq →^{pyk} “lemma transfer ˜ is”] [HelperPairSubset →^{pyk} “lemma pair subset0”] [Helper(2)PairSubset →^{pyk} “lemma pair subset1”] [PairSubset →^{pyk} “lemma pair subset”] [SamePair →^{pyk} “lemma same pair”] [SameSingleton →^{pyk} “lemma same singleton”] [UnionSubset →^{pyk} “lemma union subset”] [SameUnion →^{pyk} “lemma same union”] [SeparationSubset →^{pyk} “lemma separation subset”] [SameSeparation →^{pyk} “lemma same separation”] [SameBinaryUnion →^{pyk} “lemma same binary union”] [IntersectionSubset →^{pyk} “lemma intersection subset”] [SameIntersection →^{pyk} “lemma same intersection”] [AutoMember →^{pyk} “lemma auto member”] [HelperEqSysNotØ →^{pyk} “lemma eq-system not empty0”] [EqSysNotØ →^{pyk} “lemma eq-system not empty”] [HelperEqSubset →^{pyk} “lemma eq subset0”] [EqSubset →^{pyk} “lemma eq subset”] [HelperEqNecessary →^{pyk} “lemma equivalence nec condition0”] [EqNecessary →^{pyk} “lemma equivalence nec condition”] [HelperNoneEqNecessary →^{pyk} “lemma none-equivalence nec condition0”] [Helper(2)NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition1”] [NoneEqNecessary →^{pyk} “lemma none-equivalence nec condition”] [EqClassIsSubset →^{pyk} “lemma equivalence class is subset”] [EqClassesAreDisjoint →^{pyk} “lemma equivalence classes are disjoint”] [AllDisjoint →^{pyk} “lemma all disjoint”] [AllDisjointImply →^{pyk} “lemma all disjoint-imply”] [BSsubset →^{pyk} “lemma bs subset union(bs/r)”] [Union(BS/R)subset →^{pyk} “lemma union(bs/r) subset bs”] [UnionIdentity →^{pyk} “lemma union(bs/r) is bs”] [EqSysIsPartition →^{pyk} “theorem eq-system is partition”] [(ϵ) →^{pyk} “var ep”] [(fx) →^{pyk} “var fx”] [(fy) →^{pyk} “var fy”] [(fz) →^{pyk} “var fz”] [(fv) →^{pyk} “var fu”] [var fv →^{pyk} “var fv”] [(rx) →^{pyk} “var rx”] [(ry) →^{pyk} “var ry”] [(rz) →^{pyk} “var rz”] [(ru) →^{pyk} “var ru”] [ϵ →^{pyk} “meta ep”] [FX →^{pyk} “meta fx”] [FY →^{pyk} “meta fy”] [FZ →^{pyk} “meta fz”] [FU →^{pyk} “meta fu”] [FV →^{pyk} “meta fv”] [RX →^{pyk} “meta rx”] [RY →^{pyk} “meta ry”] [RZ →^{pyk} “meta rz”] [RU →^{pyk} “meta ru”]

[0 →^{pyk} “0”]

[1 →^{pyk} “1”]

[(−1) →^{pyk} “(-1)”]

[2 →^{pyk} “2”]

[1/2 →^{pyk} “1/2”]

[0f →^{pyk} “0f”]

[1f →^{pyk} “1f”]

[00 →^{pyk} “00”]

[01 →^{pyk} “01”]

[leqReflexivity →^{pyk} “axiom leqReflexivity”] [leqAntisymmetryAxiom →^{pyk} “axiom leqAntisymmetry”] [leqTransitivityAxiom →^{pyk} “axiom leqTransitivity”] [leqTotality →^{pyk} “axiom leqTotality”] [leqAdditionAxiom →^{pyk} “axiom leqAddition”] [leqMultiplicationAxiom →^{pyk} “axiom leqMultiplication”] [plusAssociativity →^{pyk} “axiom plusAssociativity”] [plusCommutativity →^{pyk} “axiom plusCommutativity”] [Negative →^{pyk} “axiom negative”] [plus0 →^{pyk} “axiom plus0”] [timesAssociativity →^{pyk} “axiom timesAssociativity”] [timesCommutativity →^{pyk} “axiom timesCommutativity”] [ReciprocalAxiom →^{pyk} “axiom reciprocal”] [times1 →^{pyk} “axiom times1”] [Distribution →^{pyk} “axiom distribution”] [0not1 →^{pyk} “axiom 0not1”] [equalityAxiom →^{pyk} “axiom equality”] [eqLeqAxiom →^{pyk} “axiom eqLeq”] [eqAdditionAxiom →^{pyk} “axiom eqAddition”] [eqMultiplicationAxiom →^{pyk} “axiom eqMultiplication”] [SENC1 →^{pyk} “lemma set equality nec condition(1)”] [SENC2 →^{pyk} “lemma set equality nec condition(2)”] [IfThenElse(T) →^{pyk} “1rule ifThenElse true”] [IfThenElse(F) →^{pyk} “1rule ifThenElse false”] [From = f →^{pyk} “1rule from=f”] [To = f →^{pyk} “1rule to=f”] [From < f →^{pyk} “1rule from<f”] [To < f →^{pyk} “1rule to<f”] [PlusF →^{pyk} “axiom plusF”] [TimesF →^{pyk} “axiom timesF”] [MinusF →^{pyk} “axiom minusF”] [0f →^{pyk} “axiom 0f”] [1f →^{pyk} “axiom 1f”] [FromSF →^{pyk} “1rule fromSameF”] [ToSF →^{pyk} “1rule toSameF”] [To == XX →^{pyk} “1rule to==XX”] [From == →^{pyk} “1rule from==”] [To == →^{pyk} “1rule to==”] [From << XX →^{pyk} “1rule from<<XX”] [From << (1) →^{pyk} “1rule from<<XX(1)”] [From << (2) →^{pyk} “1rule from<<XX(2)”] [to << XX →^{pyk} “1rule to<<XX”] [From << →^{pyk} “1rule from<<”] [To << →^{pyk} “1rule to<<”] [FromInR →^{pyk} “1rule fromInR”] [PlusR →^{pyk} “axiom plusR”] [TimesR →^{pyk} “axiom timesR”] [leqAntisymmetry →^{pyk} “lemma leqAntisymmetry”] [leqTransitivity →^{pyk} “lemma leqTransitivity”] [leqAddition →^{pyk} “lemma leqAddition”] [leqMultiplication →^{pyk} “lemma leqMultiplication”] [Reciprocal →^{pyk} “lemma reciprocal”] [Equality →^{pyk} “lemma equality”] [eqLeq →^{pyk} “lemma eqLeq”] [eqAddition →^{pyk} “lemma eqAddition”] [eqMultiplication →^{pyk} “lemma eqMultiplication”] [ToNegatedImply →^{pyk} “prop lemma to negated imply”] [TND →^{pyk} “prop lemma tertium non datur”] [ImplyNegation →^{pyk} “prop lemma imply negation”] [FromNegations →^{pyk} “prop lemma from negations”] [From3Disjuncts →^{pyk} “prop lemma from three disjuncts”] [From2 ∗ 2Disjuncts →^{pyk} “prop lemma from two times two disjuncts”] [NegateDisjunct1 →^{pyk} “prop lemma negate first disjunct”] [NegateDisjunct2 →^{pyk} “prop lemma negate second disjunct”] [ExpandDisjuncts →^{pyk} “prop lemma expand disjuncts”] [eqReflexivity →^{pyk} “lemma eqReflexivity”] [eqSymmetry →^{pyk} “lemma eqSymmetry”] [eqTransitivity →^{pyk} “lemma eqTransitivity”] [eqTransitivity4 →^{pyk} “lemma eqTransitivity4”] [eqTransitivity5 →^{pyk} “lemma eqTransitivity5”] [eqTransitivity6 →^{pyk} “lemma eqTransitivity6”] [plus0Left →^{pyk} “lemma plus0Left”] [times1Left →^{pyk} “lemma times1Left”] [lemma eqAdditionLeft →^{pyk} “lemma eqAdditionLeft”] [EqMultiplicationLeft →^{pyk} “lemma eqMultiplicationLeft”] [DistributionOut →^{pyk} “lemma distributionOut”] [Three2twoTerms →^{pyk} “lemma three2twoTerms”] [Three2threeTerms →^{pyk} “lemma three2threeTerms”] [Three2threeFactors →^{pyk} “lemma three2twoFactors”] [AddEquations →^{pyk} “lemma addEquations”] [SubtractEquations →^{pyk} “lemma subtractEquations”] [SubtractEquationsLeft →^{pyk} “lemma subtractEquationsLeft”] [EqNegated →^{pyk} “lemma eqNegated”] [PositiveToRight(Eq) →^{pyk} “lemma positiveToRight(Eq)”] [PositiveToLeft(Eq)(1term) →^{pyk} “lemma positiveToLeft(Eq)(1 term)”] [NegativeToLeft(Eq) →^{pyk} “lemma negativeToLeft(Eq)”] [LessNeq →^{pyk} “lemma lessNeq”] [NeqSymmetry →^{pyk} “lemma neqSymmetry”] [NeqNegated →^{pyk} “lemma neqNegated”] [SubNeqRight →^{pyk} “lemma subNeqRight”] [SubNeqLeft →^{pyk} “lemma subNeqLeft”] [NeqAddition →^{pyk} “lemma neqAddition”] [NeqMultiplication →^{pyk} “lemma neqMultiplication”] [UniqueNegative →^{pyk} “lemma uniqueNegative”] [DoubleMinus →^{pyk} “lemma doubleMinus”] [LeqLessEq →^{pyk} “lemma leqLessEq”] [LessLeq →^{pyk} “lemma lessLeq”] [FromLeqGeq →^{pyk} “lemma from leqGeq”] [subLeqRight →^{pyk} “lemma subLeqRight”] [subLeqLeft →^{pyk} “lemma subLeqLeft”] [Leq + 1 →^{pyk} “lemma leqPlus1”] [PositiveToRight(Leq) →^{pyk} “lemma positiveToRight(Leq)”] [PositiveToRight(Leq)(1term) →^{pyk} “lemma positiveToRight(Leq)(1 term)”] [negativeToLeft(Leq) →^{pyk} “lemma negativeToLeft(Leq)”] [LeqAdditionLeft →^{pyk} “lemma leqAdditionLeft”] [leqSubtraction →^{pyk} “lemma leqSubtraction”] [leqSubtractionLeft →^{pyk} “lemma leqSubtractionLeft”] [thirdGeq →^{pyk} “lemma thirdGeq”] [LeqNegated →^{pyk} “lemma leqNegated”] [AddEquations(Leq) →^{pyk} “lemma addEquations(Leq)”] [ThirdGeqSeries →^{pyk} “lemma thirdGeqSeries”] [LeqNeqLess →^{pyk} “lemma leqNeqLess”] [FromLess →^{pyk} “lemma fromLess”] [ToLess →^{pyk} “lemma toLess”] [fromNotLess →^{pyk} “lemma fromNotLess”] [toNotLess →^{pyk} “lemma toNotLess”] [NegativeLessPositive →^{pyk} “lemma negativeLessPositive”] [leqLessTransitivity →^{pyk} “lemma leqLessTransitivity”] [LessLeqTransitivity →^{pyk} “lemma lessLeqTransitivity”] [LessTransitivity →^{pyk} “lemma lessTransitivity”] [LessTotality →^{pyk} “lemma lessTotality”] [SubLessRight →^{pyk} “lemma subLessRight”] [SubLessLeft →^{pyk} “lemma subLessLeft”] [LessAddition →^{pyk} “lemma lessAddition”] [LessAdditionLeft →^{pyk} “lemma lessAdditionLeft”] [LessMultiplication →^{pyk} “lemma lessMultiplication”] [LessMultiplicationLeft →^{pyk} “lemma lessMultiplicationLeft”] [LessDivision →^{pyk} “lemma lessDivision”] [AddEquations(Less) →^{pyk} “lemma addEquations(Less)”] [LessNegated →^{pyk} “lemma lessNegated”] [PositiveNegated →^{pyk} “lemma positiveNegated”] [NonpositiveNegated →^{pyk} “lemma nonpositiveNegated”] [NegativeNegated →^{pyk} “lemma negativeNegated”] [NonnegativeNegated →^{pyk} “lemma nonnegativeNegated”] [PositiveHalved →^{pyk} “lemma positiveHalved”] [NonnegativeNumerical →^{pyk} “lemma nonnegativeNumerical”] [NegativeNumerical →^{pyk} “lemma negativeNumerical”] [PositiveNumerical →^{pyk} “lemma positiveNumerical”] [lemma nonpositiveNumerical →^{pyk} “lemma nonpositiveNumerical”] [|0| = 0 →^{pyk} “lemma |0|=0”] [0 <= |x| →^{pyk} “lemma 0<=|x|”] [SameNumerical →^{pyk} “lemma sameNumerical”] [SignNumerical(+) →^{pyk} “lemma signNumerical(+)”] [SignNumerical →^{pyk} “lemma signNumerical”] [NumericalDifference →^{pyk} “lemma numericalDifference”] [SplitNumericalSumHelper →^{pyk} “lemma splitNumericalSumHelper”] [splitNumericalSum(++) →^{pyk} “lemma splitNumericalSum(++)”] [splitNumericalSum(−−) →^{pyk} “lemma splitNumericalSum(--)”] [splitNumericalSum(+ − small) →^{pyk} “lemma splitNumericalSum(+-, smallNegative)”] [splitNumericalSum(+ − big) →^{pyk} “lemma splitNumericalSum(+-, bigNegative)”] [splitNumericalSum(+−) →^{pyk} “lemma splitNumericalSum(+-)”] [splitNumericalSum(−+) →^{pyk} “lemma splitNumericalSum(-+)”] [splitNumericalSum →^{pyk} “lemma splitNumericalSum”] [insertMiddleTerm(Numerical) →^{pyk} “lemma insertMiddleTerm(Numerical)”] [x + y = zBackwards →^{pyk} “lemma x+y=zBackwards”] [x ∗ y = zBackwards →^{pyk} “lemma x∗y=zBackwards”] [x = x + (y − y) →^{pyk} “lemma x=x+(y-y)”] [x = x + y − y →^{pyk} “lemma x=x+y-y”] [ →^{pyk} “lemma x=x∗y∗(1/y)”] [insertMiddleTerm(Sum) →^{pyk} “lemma insertMiddleTerm(Sum)”] [insertMiddleTerm(Difference) →^{pyk} “lemma insertMiddleTerm(Difference)”] [x ∗ 0 + x = x →^{pyk} “lemma x∗0+x=x”] [x ∗ 0 = 0 →^{pyk} “lemma x∗0=0”] [(−1) ∗ (−1) + (−1) ∗ 1 = 0 →^{pyk} “lemma (-1)∗(-1)+(-1)∗1=0”] [(−1) ∗ (−1) = 1 →^{pyk} “lemma (-1)∗(-1)=1”] [0 < 1Helper →^{pyk} “lemma 0<1Helper”] [0 < 1 →^{pyk} “lemma 0<1”] [0 < 2 →^{pyk} “lemma 0<2”] [0 < 1/2 →^{pyk} “lemma 0<1/2”] [TwoWholes →^{pyk} “lemma x+x=2∗x”] [TwoHalves →^{pyk} “lemma (1/2)x+(1/2)x=x”] [−x − y = −(x + y) →^{pyk} “lemma -x-y=-(x+y)”] [MinusNegated →^{pyk} “lemma minusNegated”] [Times(−1) →^{pyk} “lemma times(-1)”] [Times(−1)Left →^{pyk} “lemma times(-1)Left”] [−0 = 0 →^{pyk} “lemma -0=0”] [SFsymmetry →^{pyk} “lemma sameFsymmetry”] [SFtransitivity →^{pyk} “lemma sameFtransitivity”] [= fToSameF →^{pyk} “lemma =f to sameF”] [PlusF(Sym) →^{pyk} “lemma plusF(Sym)”] [TimesF(Sym) →^{pyk} “lemma timesF(Sym)”] [f2R(Plus) →^{pyk} “lemma f2R(Plus)”] [f2R(Times) →^{pyk} “lemma f2R(Times)”] [PlusR(Sym) →^{pyk} “lemma plusR(Sym)”] [TimesR(Sym) →^{pyk} “lemma timesR(Sym)”] [LessLeq(R) →^{pyk} “lemma lessLeq(R)”] [eqLeq(R) →^{pyk} “lemma eqLeq(R)”] [SubLessRight(R) →^{pyk} “lemma subLessRight(R)”] [SubLessLeft(R) →^{pyk} “lemma subLessLeft(R)”] [<< TransitivityHelper(Q) →^{pyk} “lemma <<TransitivityHelper(Q)”] [<< Transitivity →^{pyk} “lemma <<Transitivity”] [<<== Reflexivity →^{pyk} “lemma <<==Reflexivity”] [<<== AntisymmetryHelper(Q) →^{pyk} “lemma <<==AntisymmetryHelper(Q)”] [<<== Antisymmetry →^{pyk} “lemma <<==Antisymmetry”] [<<== Transitivity →^{pyk} “lemma <<==Transitivity”] [Plus0f →^{pyk} “lemma plus0f”] [Plus00 →^{pyk} “lemma plus00”] [== Addition →^{pyk} “lemma ==Addition”] [== AdditionLeft →^{pyk} “lemma ==AdditionLeft”] [<< Addition →^{pyk} “lemma <<Addition”] [<<== Addition →^{pyk} “lemma <<==Addition”] [PlusAssociativity(F) →^{pyk} “lemma plusAssociativity(F)”] [PlusAssociativity(R) →^{pyk} “lemma plusAssociativity(R)”] [Negative(R) →^{pyk} “lemma negative(R)”] [PlusCommutativity(F) →^{pyk} “lemma plusCommutativity(F)”] [PlusCommutativity(R) →^{pyk} “lemma plusCommutativity(R)”] [TimesAssociativity(F) →^{pyk} “lemma timesAssociativity(F)”] [TimesAssociativity(R) →^{pyk} “lemma timesAssociativity(R)”] [Times1f →^{pyk} “lemma times1f”] [Times01 →^{pyk} “lemma times01”] [TimesCommutativity(F) →^{pyk} “lemma timesCommutativity(F)”] [TimesCommutativity(R) →^{pyk} “lemma timesCommutativity(R)”] [Distribution(F) →^{pyk} “lemma distribution(F)”] [Distribution(R) →^{pyk} “lemma distribution(R)”]

[R(∗) →^{pyk} “R( " )”]

[− − R(∗) →^{pyk} “--R( " )”]

[rec∗ →^{pyk} “1/ "”]

[∗/∗ →^{pyk} “eq-system of " modulo "”] [∗ ∩ ∗ →^{pyk} “intersection " comma " end intersection”]

[∗[∗] →^{pyk} “[ " ; " ]”]

[∪∗ →^{pyk} “union " end union”] [∗ ∪ ∗ →^{pyk} “binary-union " comma " end union”] [P(∗) →^{pyk} “power " end power”] [{∗} →^{pyk} “zermelo singleton " end singleton”] [{∗, ∗} →^{pyk} “zermelo pair " comma " end pair”] [⟨∗, ∗⟩ →^{pyk} “zermelo ordered pair " comma " end pair”]

[−∗ →^{pyk} “- "”]

[−_{f}∗ →^{pyk} “-f "”]

[∗ ∈ ∗ →^{pyk} “" in0 "”]

[∗(∗, ∗) →^{pyk} “" is related to " under "”] [ReflRel(∗, ∗) →^{pyk} “" is reflexive relation in "”] [SymRel(∗, ∗) →^{pyk} “" is symmetric relation in "”] [TransRel(∗, ∗) →^{pyk} “" is transitive relation in "”] [EqRel(∗, ∗) →^{pyk} “" is equivalence relation in "”] [[∗ ∈ ∗]_{∗} →^{pyk} “equivalence class of " in " modulo "”] [Partition(∗, ∗) →^{pyk} “" is partition of "”]

[∗ ∗ ∗ →^{pyk} “" ∗ "”]

[∗ ∗_{f} ∗ →^{pyk} “" ∗f "”]

[∗ ∗ ∗∗ →^{pyk} “" ∗∗ "”]

[∗ + ∗ →^{pyk} “" + "”]

[∗ − ∗ →^{pyk} “" - "”]

[∗ +_{f} ∗ →^{pyk} “" +f "”]

[∗ −_{f} ∗ →^{pyk} “" -f "”]

[∗ + +∗ →^{pyk} “" ++ "”]

[R(∗) − −R(∗) →^{pyk} “R( " ) -- R( " )”]

[| ∗ | →^{pyk} “| " |”]

[if(∗, ∗, ∗) →^{pyk} “if( " , " , " )”]

[∗ = ∗ →^{pyk} “" = "”]

[∗ ≠ ∗ →^{pyk} “" != "”]

[∗ <= ∗ →^{pyk} “" <= "”]

[∗ < ∗ →^{pyk} “" < "”]

[∗ =_{f} ∗ →^{pyk} “" =f "”]

[∗ <_{f} ∗ →^{pyk} “" <f "”]

[SF(∗, ∗) →^{pyk} “" sameF "”]

[∗ == ∗ →^{pyk} “" == "”]

[∗ << ∗ →^{pyk} “" << "”]

[∗ <<== ∗ →^{pyk} “" <<== "”]

[∗==∗ →^{pyk} “" zermelo is "”] [∗ ⊆ ∗ →^{pyk} “" is subset of "”]

[ ˙¬ ∗ →^{pyk} “not0 "”]

[∗ ∉ ∗ →^{pyk} “" zermelo ˜ in "”] [∗ ≠ ∗ →^{pyk} “" zermelo ˜ is "”]

[∗ ˙∧ ∗ →^{pyk} “" and0 "”]

[∗ ˙∨ ∗ →^{pyk} “" or0 "”]

[∗ ˙⇔ ∗ →^{pyk} “" iff "”]

[{ph ∈ ∗ | ∗} →^{pyk} “the set of ph in " such that " end set”]

[am →^{pyk} “am”]

)^{p}

B TEX definitioner

[am =^{tex} “am”]

[(⋯) =^{tex} “(\cdots{})”]

[Objekt-var =^{tex} “\texttt{Objekt-var}”]

[Ex-var =^{tex} “\texttt{Ex-var}”]

[Ph-var =^{tex} “\texttt{Ph-var}”]

[Værdi =^{tex} “\texttt{V\ae{}rdi}”]

[Variabel =^{tex} “\texttt{Variabel}”]

[Op(x) =^{tex} “Op(#1. )”]

[Op(x, y) =^{tex} “Op(#1. , #2. )”]

[x ¨ == y =^{tex} “#1.

\mathrel {\ddot {==}} #2.”]

[ContainsEmpty(x) =^{tex} “ContainsEmpty(#1. )”]

[Dedu(x, y) =^{tex} “ Dedu(#1. , #2. )”]

[Dedu_{0}(x, y) =^{tex} “ Dedu 0(#1. , #2. )”]

[Dedu_{s}(x, y, z) =^{tex} “Dedu {s}(#1. , #2. , #3. )”]

[Dedu_{1}(x, y, z) =^{tex} “ Dedu 1(#1. , #2. , #3. )”] [Dedu_{2}(x, y, z) =^{tex} “ Dedu 2(#1. , #2. , #3. )”]

[Dedu_{3}(x, y, z, u) =^{tex} “ Dedu 3(#1. , #2. , #3. , #4. )”]

[Dedu_{4}(x, y, z, u) =^{tex} “ Dedu 4(#1. , #2. , #3. , #4. )”]

[Dedu_{4}^{∗}(x, y, z, u) =^{tex} “ Dedu 4ˆ ∗(#1. , #2. , #3. , #4. )”]

[Dedu_{5}(x, y, z) =^{tex} “ Dedu 5(#1. , #2. , #3. )”]

[Dedu_{6}(p, c, e, b) =^{tex} “ Dedu 6(#1. , #2. , #3. , #4. )”]

[Dedu_{6}^{∗}(p, c, e, b) =^{tex} “ Dedu 6ˆ ∗(#1. , #2. , #3. , #4. )”]

[Dedu_{7}(p) =^{tex} “ Dedu 7(#1.

)”]

[Dedu_{8}(p, b) =^{tex} “ Dedu 8(#1. , #2. )”]

[Dedu_{8}^{∗}(p, b) =^{tex} “ Dedu 8ˆ ∗(#1. , #2. )”]

[Ex_{1} =^{tex} “Ex {1}”]

[Ex_{2} =^{tex} “Ex {2}”]

[Ex_{10} =^{tex} “Ex {10}”]

[Ex_{20} =^{tex} “Ex {20}”]

[x_{Ex} =^{tex} “#1.

{Ex}”]

[x^{Ex} =^{tex} “#1.

ˆ {Ex}”]

[⟨x≡y|z:==u⟩_{Ex} =^{tex} “\langle #1. {\equiv} #2. | #3. {:==} #4. \rangle {Ex} ”]

[⟨x≡^{0}y|z:==u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ 0 #2. | #3. {:==} #4. \rangle {Ex} ”]

[⟨x≡^{1}y|z:==u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:==} #4. \rangle {Ex} ”]

[⟨x≡^{∗}y|z:==u⟩_{Ex} =^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:==} #4. \rangle {Ex} ”]

[ph_{1} =^{tex} “ph {1}”]

[ph_{2} =^{tex} “ph {2}”]

[ph_{3} =^{tex} “ph {3}”]

[x_{Ph} =^{tex} “#1.

{Ph} ”]

[x^{Ph} =^{tex} “#1.

ˆ {Ph}”]

[⟨x≡y|z:==u⟩_{Ph} =^{tex} “\langle #1. {\equiv} #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{0}y|z:==u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ 0 #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{1}y|z:==u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ 1 #2. | #3. {:==} #4. \rangle {Ph} ”]

[⟨x≡^{∗}y|z:==u⟩_{Ph} =^{tex} “\langle #1. {\equiv}ˆ ∗ #2. | #3. {:==} #4. \rangle {Ph} ”]

[bs =^{tex} “\mathsf {bs}”]

[OBS =^{tex} “ \mathsf {OBS}”]

[BS =^{tex} “{\cal BS}”]

[Ø =^{tex} “\mathrm{\O}”]

[ZFsub =^{tex} “ZFsub”]

[MP =^{tex} “MP”]

[Gen =^{tex} “Gen”] [Repetition =^{tex} “Repetition”] [Neg =^{tex} “Neg”] [Ded =^{tex} “Ded”] [ExistIntro =^{tex} “ExistIntro”] [Extensionality =^{tex} “Extensionality”] [Ødef =^{tex} “\O{}def”] [PairDef =^{tex} “PairDef”] [UnionDef =^{tex} “UnionDef”] [PowerDef =^{tex} “PowerDef”] [SeparationDef =^{tex} “SeparationDef”] [AddDoubleNeg =^{tex} “AddDoubleNeg”] [RemoveDoubleNeg =^{tex} “RemoveDoubleNeg”] [AndCommutativity =^{tex} “AndCommutativity”] [AutoImply =^{tex} “AutoImply”] [Contrapositive =^{tex} “Contrapositive”] [FirstConjunct =^{tex} “FirstConjunct”] [SecondConjunct =^{tex} “SecondConjunct”] [FromContradiction =^{tex} “FromContradiction”] [FromDisjuncts =^{tex} “FromDisjuncts”] [IffCommutativity =^{tex} “IffCommutativity”] [IffFirst =^{tex} “IffFirst”] [IffSecond =^{tex} “IffSecond”] [ImplyTransitivity =^{tex} “ImplyTransitivity”] [JoinConjuncts =^{tex} “JoinConjuncts”]

[MP2 =^{tex} “MP2”]

[MP3 =^{tex} “MP3”]

[MP4 =^{tex} “MP4”]

[MP5 =^{tex} “MP5”]

[MT =^{tex} “MT”]

[NegativeMT =^{tex} “NegativeMT”] [Technicality =^{tex} “Technicality”] [Weakening =^{tex} “Weakening”] [WeakenOr1 =^{tex} “WeakenOr1”] [WeakenOr2 =^{tex} “WeakenOr2”] [Pair2Formula =^{tex} “Pair2Formula”] [Formula2Pair =^{tex} “Formula2Pair”] [Union2Formula =^{tex} “Union2Formula”] [Formula2Union =^{tex} “Formula2Union”] [Sep2Formula =^{tex} “Sep2Formula”] [Formula2Sep =^{tex} “Formula2Sep”] [SubsetInPower =^{tex} “SubsetInPower”] [HelperPowerIsSub =^{tex} “HelperPowerIsSub”] [PowerIsSub =^{tex} “PowerIsSub”] [(Switch)HelperPowerIsSub =^{tex} “(Switch)HelperPowerIsSub”] [(Switch)PowerIsSub =^{tex} “(Switch)PowerIsSub”] [ToSetEquality =^{tex} “ToSetEquality”] [HelperToSetEquality(t) =^{tex} “HelperToSetEquality(t)”] [ToSetEquality(t) =^{tex} “ToSetEquality(t)”] [HelperFromSetEquality =^{tex} “HelperFromSetEquality”] [FromSetEquality =^{tex} “FromSetEquality”] [HelperReflexivity =^{tex} “HelperReflexivity”] [Reflexivity =^{tex} “Reflexivity”] [HelperSymmetry =^{tex} “HelperSymmetry”] [Symmetry =^{tex} “Symmetry”] [HelperTransitivity =^{tex} “HelperTransitivity”] [Transitivity =^{tex} “Transitivity”], [ERisReflexive =^{tex} “ERisReflexive”] [ERisSymmetric =^{tex} “ERisSymmetric”] [ERisTransitive =^{tex} “ERisTransitive”] [ØisSubset =^{tex} “\O{}isSubset”] [HelperMemberNotØ =^{tex} “HelperMemberNot\O{}”] [MemberNotØ =^{tex} “MemberNot\O{}”] [HelperUniqueØ =^{tex} “HelperUnique\O{}”] [UniqueØ =^{tex} “Unique\O{}”] [==Reflexivity =^{tex} “==\!{}Reflexivity”] [==Symmetry =^{tex} “==\!{}Symmetry”] [Helper==Transitivity =^{tex} “Helper\!{}==\!{}Transitivity”] [==Transitivity =^{tex} “\!{}==\!{}Transitivity”] [HelperTransferNotEq =^{tex} “HelperTransferNotEq”] [TransferNotEq =^{tex} “TransferNotEq”] [HelperPairSubset =^{tex} “HelperPairSubset”] [Helper(2)PairSubset =^{tex} “Helper(2)PairSubset”] [PairSubset =^{tex} “PairSubset”] [SamePair =^{tex} “SamePair”] [SameSingleton =^{tex} “SameSingleton”] [UnionSubset =^{tex} “UnionSubset”] [SameUnion =^{tex} “SameUnion”] [SeparationSubset =^{tex} “SeparationSubset”] [SameSeparation =^{tex} “SameSeparation”] [SameBinaryUnion =^{tex} “SameBinaryUnion”] [IntersectionSubset =^{tex} “IntersectionSubset”] [SameIntersection =^{tex} “SameIntersection”] [AutoMember =^{tex} “AutoMember”] [HelperEqSysNotØ =^{tex} “HelperEqSysNot\O{}”] [EqSysNotØ =^{tex} “EqSysNot\O{}”] [HelperEqSubset =^{tex} “HelperEqSubset”] [EqSubset =^{tex} “EqSubset”] [EqNecessary =^{tex} “EqNecessary”] [HelperEqNecessary =^{tex} “HelperEqNecessary”] [HelperNoneEqNecessary =^{tex} “HelperNoneEqNecessary”] [Helper(2)NoneEqNecessary =^{tex} “Helper(2)NoneEqNecessary”] [NoneEqNecessary =^{tex} “NoneEqNecessary”] [EqClassIsSubset =^{tex} “EqClassIsSubset”] [EqClassesAreDisjoint =^{tex} “EqClassesAreDisjoint”] [AllDisjoint =^{tex} “AllDisjoint”] [AllDisjointImply =^{tex} “AllDisjointImply”] [BSsubset =^{tex} “BSsubset”] [Union(BS/R)subset =^{tex} “Union(BS/R)subset”] [UnionIdentity =^{tex} “UnionIdentity”] [EqSysIsPartition =^{tex} “EqSysIsPartition”]

[x/y =^{tex} “#1.

/ #2.”]

[x ∩ y =^{tex} “#1.

\cap #2.”]

[∪x =^{tex} “\cup #1.”]

[x ∪ y =^{tex} “#1.

\mathrel{\cup} #2.”]

[P(x) =^{tex} “P(#1.

)”]

[{x} =^{tex} “\{#1.

\}”]

[{x, y} =^{tex} “\{#1.

, #2. \}”]

[⟨x, y⟩ =^{tex} “\langle #1. , #2. \rangle”],

[x ∈ y =^{tex} “#1.

\mathrel{\in} #2.”]

[z(x, y) =^{tex} “#3.

(#1. , #2. )”]

[ReflRel(r, x) =^{tex} “ReflRel(#1. , #2. )”]

[SymRel(r, x) =^{tex} “SymRel(#1. , #2. )”]

[TransRel(r, x) =^{tex} “TransRel(#1. , #2. )”]

[EqRel(r, x) =^{tex} “EqRel(#1. , #2. )”]

[[x ∈ bs]_{r} =^{tex} “[#1.

\mathrel{\in} #2. ] {#3. }”]

[Partition(x, y) =^{tex} “Partition(#1. , #2. )”]

[x==y =^{tex} “#1.

\!\mathrel{==}\! #2.”]

[x ⊆ y =^{tex} “#1.

\mathrel{\subseteq} #2.”]

[ ˙¬ x =^{tex} “\dot{\neg}\, #1.”]

[x ∉ y =^{tex} “#1.

\mathrel{\notin} #2.”]

[x ≠ y =^{tex} “#1.

\mathrel{\neq} #2.”]

[x ˙∧ y =^{tex} “#1.

\mathrel{\dot{\wedge}} #2.”]

[x ˙∨ y =^{tex} “#1.

\mathrel{\dot{\vee}} #2.”]

[x ˙⇔ y =^{tex} “#1.

\mathrel{\dot{\Leftrightarrow}} #2.”]

[{ph ∈ x | a} =^{tex} “ \{ ph \mathrel{\in} #1. \mid #2. \}”]

————- RRRRRRRRRRRRRRR ————-

(*** aksiomer ***)

[ZFsub rule leqReflexivity: ΠX: X <= X]

[ZFsub rule leqAntisymmetryAxiom: ΠX , Y: X <= Y ⇒ Y <= X ⇒ X = Y]

[ZFsub rule leqTransitivityAxiom: ΠX , Y, Z: X <= Y ⇒ Y <= Z ⇒ X <= Z]

[ZFsub rule leqTotality: ΠX , Y: X <= Y ˙∨ Y <= X]

[ZFsub rule leqAdditionAxiom: ΠX , Y, Z: X <= Y ⇒ X + Z <= Y + Z] [ZFsub rule leqMultiplicationAxiom: ΠX , Y, Z: 0 <= Z ⇒ X <= Y ⇒ X ∗

Z <= Y ∗ Z] [ZFsub rule plusAssociativity: ΠX , Y, Z: (X + Y) + Z = X + (Y + Z)] [ZFsub rule plusCommutativity: ΠX , Y: X + Y = Y + X] [ZFsub rule Negative: ΠX: X + (−X) = 0] [ZFsub rule plus0: ΠX: X + 0 = X] [ZFsub rule timesAssociativity: ΠX , Y, Z: (X ∗ Y) ∗ Z = X ∗ (Y ∗ Z)] [ZFsub rule timesCommutativity: ΠX , Y: X ∗ Y = Y ∗ X] [ZFsub rule ReciprocalAxiom: ΠX: X ≠ 0 ⇒ X ∗ recX = 1] [ZFsub rule times1: ΠX: X ∗ 1 = X] [ZFsub rule Distribution: ΠX , Y, Z: X ∗ (Y + Z) = (X ∗ Y) + (X ∗ Z)] [ZFsub rule 0not1: 0 ≠ 1] [ZFsub rule equalityAxiom: ΠX , Y, Z: X = Y ⇒ X = Z ⇒ Y = Z] [ZFsub rule eqLeqAxiom: ΠX , Y: X = Y ⇒ X <= Y] [ZFsub rule eqAdditionAxiom: ΠX , Y, Z: X = Y ⇒ X + Z = Y + Z] [ZFsub rule eqMultiplicationAxiom: ΠX , Y, Z: X = Y ⇒ X ∗ Z = Y ∗ Z] (*** XX snydeaksiomer ***) [ZFsub rule ==Reflexivity: ΠRX: RX == RX] [ZFsub rule ==Symmetry: ΠRX, RY: RX == RY ⊢ RY == RX] [ZFsub rule == Transitivity: ΠRX, RY, RZ: RX == RY ⊢ RY == RZ ⊢

RX == RZ]

XX ikke 100procent identisk med originalen fra equivalence-relations [ZFsub rule SENC1: ΠFX, RX, RY: RX == RY ⊢ FX ∈ RX ⊢ FX ∈ RY]

XX boer bevises ud fra nummer 1 [ZFsub rule SENC2: ΠFX, RX, RY: RX == RY ⊢ FX ∈ RY ⊢ FX ∈ RX]

[ZFsub rule IfThenElse(T): ΠA, X , Y: A ⊢ if(A, X , Y) = X] [ZFsub rule IfThenElse(F): ΠA, X , Y: ˙¬ A ⊢ if(A, X , Y) = Y] [ZFsub rule FromSF: ΠM, ϵ, FX, FY: SF(FX, FY) ⊢ 0 < ϵ ⊢ Ex3 <= M ⇒

|FX[M] − FY[M]| < ϵ]

[ZFsub rule ToSF: ΠM, ϵ, FX, FY: 0 < ϵ ⇒ Ex3 <= M ⇒ |FX[M] − FY[M]| < ϵ ⊢ SF(FX, FY)]

[ZFsub rule From = f: ΠM, FX, FY: FX =_{f} FY ⊢ FX[M] = FY[M]] XX hm... det er nok med bare 1 meta m XX loesning: objektkvantor [ZFsub rule To =

f: ΠM, FX, FY: FX[M] = FY[M] ⊢ FX =_{f} FY]

[ZFsub rule From < f: ΠM, ϵ, FX, FY: FX <_{f} FY ⊢ 0 < ϵ ⊢ Ex3 <= M ⇒ FX[M] <= FY[M] − ϵ]

[ZFsub rule To < f: ΠM, ϵ, FX, FY: 0 < ϵ ⇒ Ex3 <= M ⇒ FX[M] <= FY[M] − ϵ ⊢ FX <_{f} FY]

[ZFsub rule PlusF: ΠM, FX, FY: FX +_{f} FY[M] = FX[M] + FY[M]] [ZFsub rule MinusF: ΠM, FX: −_{f}FX[M] = −FX[M]] [ZFsub rule TimesF: ΠM, FX, FY: FX ∗_{f} FY[M] = FX[M] ∗ FY[M]] [ZFsub rule 0f: ΠM: 0f[M] = 0] [ZFsub rule 1f: ΠM: 1f[M] = 1] [ZFsub rule To == XX: ΠFX, FY, RX, RY: FX ∈ RX ⇒ FY ∈ RY ⇒

SF(FX, FY) ⊢ RX == RY] [ZFsub rule From ==: ΠFX, FY: R(FX) == R(FY) ⊢ SF(FX, FY)] [ZFsub rule To ==: ΠFX, FY: SF(FX, FY) ⊢ R(FX) == R(FY)]

[ZFsub rule From << XX: ΠM, ϵ, FX, FY, RX, RY: RX << RY ⊢ FX ∈ RX ⊢ FY ∈ RY ⊢ 0 < ϵ ⊢ Ex_{1} <= M ⇒ FX[M] <= FY[M] − ϵ]

[ZFsub rule From << (1): ΠRX, RY: RX << RY ⊢ Ex_{10} ∈ RX] [ZFsub rule From << (2): ΠRX, RY: RX << RY ⊢ Ex_{20} ∈ RY] [ZFsub rule to << XX: ΠM, N , ϵ, FX, FY, RX, RY: FX ∈ RX ⇒ FY ∈

RY ⇒ 0 < ϵ ⇒ Ex_{1} <= M ⇒ FX[M] <= FY[M] − ϵ ⊢ RX << RY] [ZFsub rule From <<: ΠFX, FY: R(FX) << R(FY) ⊢ FX <_{f} FY] [ZFsub rule To <<: ΠFX, FY: FX <_{f} FY ⊢ R(FX) << R(FY)] [ZFsub rule FromInR: ΠFX, FY: FX ∈ R(FY) ⊢ SF(FX, FY)] [ZFsub rule PlusR: ΠFX, FY: R(FX) + +R(FY) == R(FX +_{f} FY)] [ZFsub rule TimesR: ΠFX, FY: R(FX) ∗ ∗R(FY) == R(FX ∗_{f} FY)] (*** makroer ***) [ϵ ¨= \underline{(ϵ)}] [FX ¨= \underline{(fx)}] [FY ¨= \underline{(fy)}] [FZ ¨= \underline{(fz)}] [FU ¨= \underline{(fv)}] [FV ¨= \underline{var fv}]

[RX ¨= \underline{(rx)}] [RY ¨= \underline{(ry)}] [RZ ¨= \underline{(rz)}] [RU ¨= \underline{(ru)}] [Ex3 ¨= c_{Ex}] [x <<== y ¨= x << y ˙∨ x == y] [(−1) ¨= −1] [2 ¨= (1 + 1)] [1/2 ¨= rec2] [x < y ¨= x <= y ˙∧ x ≠ y] [x ≠ y ¨= ˙¬ x = y] [x − y ¨= x + (−y)] [|x| ¨= if(0 <= x, x, −x)] [00 ¨= R(0f)] [01 ¨= R(1f)] [R((fx)) + +R((fy)) ¨= R((fx) +_{f} (fy))] [− − R((fx)) ¨= R(−_{f}(fx))] XX noedvendig? [R((fx)) − −R((fy)) ¨= R((fx)) + +R(−_{f}(fy))] XX noedvendigt med [R( ) –

R( )] konstruktionen?

(*** REGELLEMMAER ***) [ZFsub lemma leqTransitivity: ΠX , Y, Z: X <= Y ⊢ Y <= Z ⊢ X <= Z] ZFsub proof of leqTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  Y <= Z  ;
L04: leqTransitivityAxiom ≫  {X <= Y ⇒ Y <= Z ⇒ X <= \atop Z  ;}
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  X <= Z  □

[ZFsub lemma leqAntisymmetry: ΠX , Y: X <= Y ⊢ Y <= X ⊢ X = Y] ZFsub proof of leqAntisymmetry:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  Y <= X  ;
L04: leqAntisymmetryAxiom ≫  X <= Y ⇒ Y <= X ⇒ X = Y ;
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫ X = Y □

[ZFsub lemma leqAddition: ΠX , Y, Z: X <= Y ⊢ X + Z <= Y + Z]

ZFsub proof of leqAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: leqAdditionAxiom ≫  X <= Y ⇒ X + Z <= Y + Z ;
L04: MP ⊳ L03 ⊳ L02 ≫ X + Z <= Y + Z □

[ZFsub lemma leqMultiplication: ΠX , Y, Z: 0 <= Z ⊢ X <= Y ⊢ X ∗Z <= Y ∗ Z]

ZFsub proof of leqMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 <= Z  ;
L03: Premise ≫  X <= Y  ;
L04: leqMultiplicationAxiom ≫  {0 <= Z ⇒ X <= Y ⇒ X ∗ \atop Z <= Y ∗ Z  ;}
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  X ∗ Z <= Y ∗ Z  □

[ZFsub lemma Reciprocal: ΠX: X ≠ 0 ⊢ X ∗ recX = 1]

ZFsub proof of Reciprocal:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X ≠ 0  ;
L03: ReciprocalAxiom ≫  X ≠ 0 ⇒ X ∗ recX = 1  ;
L04: MP ⊳ L03 ⊳ L02 ≫  X ∗ recX = 1  □

[ZFsub lemma Equality: ΠX , Y, Z: X = Y ⊢ X = Z ⊢ Y = Z]

ZFsub proof of Equality:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X = Z  ;
L04: equalityAxiom ≫  X = Y ⇒ X = Z ⇒ Y = Z  ;
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  Y = Z  □

[ZFsub lemma eqLeq: ΠX , Y: X = Y ⊢ X <= Y]

ZFsub proof of eqLeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqLeqAxiom ≫  X = Y ⇒ X <= Y  ;
L04: MP ⊳ L03 ⊳ L02 ≫  X <= Y  □

[ZFsub lemma eqAddition: ΠX , Y, Z: X = Y ⊢ X + Z = Y + Z] ZFsub proof of eqAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: eqAdditionAxiom ≫  X = Y ⇒ X + Z = Y + Z  ;
L04: MP ⊳ L03 ⊳ L02 ≫  X + Z = Y + Z  □

[ZFsub lemma eqMultiplication: ΠX , Y, Z: X = Y ⊢ X ∗ Z = Y ∗ Z] ZFsub proof of eqMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: eqMultiplicationAxiom ≫  X = Y ⇒ X ∗ Z = Y ∗ Z  ;
L04: MP ⊳ L03 ⊳ L02 ≫  X ∗ Z = Y ∗ Z  □

(*** UDSAGNSLOGIK ***)

[ZFsub lemma ToNegatedImply: ΠA, B: A ⊢ ˙¬ B ⊢ ˙¬ (A ⇒ B)]

ZFsub proof of ToNegatedImply:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ˙¬ B  ;
L05: Premise ≫  ˙¬ ˙¬ (A ⇒ B)  ;
L06: RemoveDoubleNeg ⊳ L05 ≫  A ⇒ B  ;
L07: MP ⊳ L06 ⊳ L03 ≫  B  ;

L08: FromContradiction ⊳ L07 ⊳

L04 ≫ ˙¬ (A ⇒ B) ;

L09: Block ≫  End  ;
L10: Arbitrary ≫  A, B  ;
L11: Ded ⊳ L09 ≫  {A ⇒ ˙¬ B ⇒ ˙¬ ˙¬ (A ⇒ B) ⇒ \atop ˙¬ (A ⇒ B)  ;}
L12: Premise ≫  A  ;
L13: Premise ≫  ˙¬ B  ;
L14: MP2 ⊳ L11 ⊳ L12 ⊳ L13 ≫  ˙¬ ˙¬ (A ⇒ B) ⇒ ˙¬ (A ⇒ B)  ;
L15: AutoImply ≫  ˙¬ ˙¬ (A ⇒ B) ⇒ ˙¬ ˙¬ (A ⇒ B)  ;
L16: Neg ⊳ L14 ⊳ L15 ≫  ˙¬ (A ⇒ B)  □

[ZFsub lemma TND: ΠA: A ˙∨ ˙¬ A]

ZFsub proof of TND:

L01: Arbitrary ≫  A  ;
L02: AutoImply ≫  ˙¬ A ⇒ ˙¬ A  ;
L03: Repetition ⊳ L02 ≫  A ˙∨ ˙¬ A  □

[ZFsub lemma FromNegations: ΠA, B: A ⇒ B ⊢ ˙¬ A ⇒ B ⊢ B]

ZFsub proof of FromNegations:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ˙¬ A ⇒ B  ;
L04: TND ≫  A ˙∨ ˙¬ A  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ B □

[ZFsub lemma ImplyNegation: ΠA: A ⇒ ˙¬ A ⊢ ˙¬ A]

ZFsub proof of ImplyNegation:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  A ⇒ ˙¬ A  ;
L03: AutoImply ≫  ˙¬ A ⇒ ˙¬ A  ;
L04: TND ≫  A ˙∨ ˙¬ A  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ ˙¬ A □

[ZFsub lemma From3Disjuncts: ΠA, B, C, D: A ˙∨ B ˙∨ C ⊢ A ⇒ D ⊢ B ⇒ D ⊢ C ⇒ D ⊢ D]

ZFsub proof of From3Disjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D  ;

L03: Premise ≫  A ˙∨ B ˙∨ C  ;
L04: Premise ≫  B ⇒ D  ;
L05: Premise ≫  C ⇒ D  ;
L06: Premise ≫  ˙¬ A  ;
L07: Repetition ⊳ L03 ≫  ˙¬ A ⇒ (B ˙∨ C)  ;
L08: MP ⊳ L07 ⊳ L06 ≫  B ˙∨ C  ;

L09: FromDisjuncts ⊳ L08 ⊳ L04 ⊳

L05 ≫ D ;

L10: Block ≫  End  ;
L11: Arbitrary ≫  A, B, C, D  ;
L12: Ded ⊳ L10 ≫  {A ˙∨ B ˙∨ C ⇒ (B ⇒ D) ⇒ (C ⇒ \atop D) ⇒ ˙¬ A ⇒ D  ;}
L13: AutoImply ≫  (A ⇒ D) ⇒ A ⇒ D  ;
L14: Premise ≫  A ˙∨ B ˙∨ C  ;
L15: Premise ≫  A ⇒ D  ;
L16: Premise ≫  B ⇒ D  ;
L17: Premise ≫  C ⇒ D  ;
L18: MP3⊳L12⊳L14⊳L16⊳L17 ≫ ˙¬ A ⇒ D  ;
L19: MP ⊳ L13 ⊳ L15 ≫ A ⇒ D ;
L20: FromNegations ⊳ L19 ⊳ L18 ≫ D  □

[ZFsub lemma NegateDisjunct1: ΠA, B: A ˙∨ B ⊢ ˙¬ A ⊢ B]

ZFsub proof of NegateDisjunct1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  ˙¬ A  ;
L04: Repetition ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L05: MP ⊳ L04 ⊳ L03 ≫  B  □

[ZFsub lemma NegateDisjunct2: ΠA, B: A ˙∨ B ⊢ ˙¬ B ⊢ A]

ZFsub proof of NegateDisjunct2:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ˙∨ B  ;
L03: Premise ≫  ˙¬ B  ;
L04: Repetition ⊳ L02 ≫  ˙¬ A ⇒ B  ;
L05: NegativeMT ⊳ L04 ⊳ L03 ≫  A  □

(***)

[ZFsub lemma ExpandDisjuncts: ΠA, B, C, D: A ˙∨ B ⊢ C ˙∨ D ⊢ B ˙∨ D ˙∨ (A ˙∧ C)]

ZFsub proof of ExpandDisjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D  ;
L03: Premise ≫  A ˙∨ B  ;
L04: Premise ≫  C ˙∨ D  ;
L05: Premise ≫  ˙¬ B  ;
L06: Premise ≫  ˙¬ D  ;
L07: NegateDisjunct2⊳L03⊳L05 ≫ A  ;
L08: NegateDisjunct2⊳L04⊳L06 ≫ C  ;

L09: JoinConjuncts ⊳ L07 ⊳ L08 ≫ A ˙∧ C  ;
L10: Block ≫  End  ;
L11: Arbitrary ≫  A, B, C, D  ;
L12: Ded ⊳ L10 ≫  {A ˙∨ B ⇒ C ˙∨ D ⇒ ˙¬ B ⇒ \atop ˙¬ D ⇒ A ˙∧ C  ;}
L13: Premise ≫  A ˙∨ B  ;
L14: Premise ≫  C ˙∨ D  ;
L15: MP2 ⊳ L12 ⊳ L13 ⊳ L14 ≫  ˙¬ B ⇒ ˙¬ D ⇒ A ˙∧ C  ;
L16: Repetition ⊳ L15 ≫  B ˙∨ D ˙∨ (A ˙∧ C)  □

[ZFsub lemma From2 ∗ 2Disjuncts: ΠA, B, C, D, E: A ˙∨ B ⊢ C ˙∨ D ⊢ A ⇒ C ⇒ E ⊢ A ⇒ D ⇒ E ⊢ B ⇒ C ⇒ E ⊢ B ⇒ D ⇒ E ⊢ E]

ZFsub proof of From2 ∗ 2Disjuncts:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, B, C, D, E  ;
L03: Premise ≫  C ˙∨ D  ;
L04: Premise ≫  A ⇒ C ⇒ E  ;
L05: Premise ≫  A ⇒ D ⇒ E  ;
L06: Premise ≫  A  ;
L07: MP ⊳ L04 ⊳ L06 ≫  C ⇒ E  ;
L08: MP ⊳ L05 ⊳ L06 ≫  D ⇒ E  ;

L09: FromDisjuncts ⊳ L03 ⊳ L07 ⊳

L08 ≫ E ;

L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  A, B, C, D, E  ;
L13: Premise ≫  A ˙∨ B  ;
L14: Premise ≫  C ˙∨ D  ;
L15: Premise ≫  B ⇒ C ⇒ E  ;
L16: Premise ≫  B ⇒ D ⇒ E  ;
L17: Premise ≫  ˙¬ A  ;
L18: NegateDisjunct1⊳L13⊳L17 ≫ B  ;
L19: MP ⊳ L15 ⊳ L18 ≫  C ⇒ E  ;
L20: MP ⊳ L16 ⊳ L18 ≫  D ⇒ E  ;

L21: FromDisjuncts ⊳ L14 ⊳ L19 ⊳

L20 ≫ E ;

L22: Block ≫  End  ;
L23: Arbitrary ≫  A, B, C, D, E  ;
L24: Ded ⊳ L10 ≫  {C ˙∨ D ⇒ (A ⇒ C ⇒ E) ⇒ \atop (A ⇒ D ⇒ E) ⇒ A ⇒ E  ;}
L25: Ded ⊳ L22 ≫  A ˙∨ B ⇒ C ˙∨ D ⇒ (B ⇒ C ⇒ ; E) ⇒ (B ⇒ D ⇒ E) ⇒ ˙¬ A ⇒ ; E  ;

L26: Premise ≫  A ˙∨ B  ;
L27: Premise ≫  C ˙∨ D  ;
L28: Premise ≫  A ⇒ C ⇒ E  ;
L29: Premise ≫  A ⇒ D ⇒ E  ;

L30: Premise ≫  B ⇒ C ⇒ E  ;
L31: Premise ≫  B ⇒ D ⇒ E  ;
L32: MP3⊳L24⊳L27⊳L28⊳L29 ≫ A ⇒ E  ;

L33: MP4 ⊳ L25 ⊳ L26 ⊳ L27 ⊳

L30 ⊳ L31 ≫ ˙¬ A ⇒ E ;

L34: FromNegations ⊳ L32 ⊳ L33 ≫ E  □

(*** EQUALITY ***)

[ZFsub lemma eqReflexivity: ΠX: X = X]

ZFsub proof of eqReflexivity:

L01: Arbitrary ≫  X  ;
L02: leqReflexivity ≫  X <= X  ;
L03: leqAntisymmetry⊳L02⊳L02 ≫ X = X  □

[ZFsub lemma eqSymmetry: ΠX , Y: X = Y ⊢ Y = X]

ZFsub proof of eqSymmetry:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqReflexivity ≫  X = X  ;
L04: Equality ⊳ L02 ⊳ L03 ≫  Y = X  □

[ZFsub lemma eqTransitivity: ΠX , Y, Z: X = Y ⊢ Y = Z ⊢ X = Z] ZFsub proof of eqTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: eqSymmetry ⊳ L02 ≫  Y = X  ;
L05: Equality ⊳ L04 ⊳ L03 ≫  X = Z  □

[ZFsub lemma eqTransitivity4: ΠX , Y, Z, U: X = Y ⊢ Y = Z ⊢ Z = U ⊢ X = U]

ZFsub proof of eqTransitivity4:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: eqTransitivity ⊳ L02 ⊳ L03 ≫ X = Z  ;
L06: eqTransitivity ⊳ L05 ⊳ L04 ≫ X = U  □

[ZFsub lemma eqTransitivity5: ΠX , Y, Z, U, V: X = Y ⊢ Y = Z ⊢ Z = U ⊢ U = V ⊢ X = V]

ZFsub proof of eqTransitivity5:

L01: Arbitrary ≫  X , Y, Z, U, V  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: Premise ≫  U = V  ;

L06: eqTransitivity4 ⊳ L02 ⊳ L03 ⊳

L04 ≫ X = U ;

L07: eqTransitivity ⊳ L06 ⊳ L05 ≫ X = V  □

[ZFsub lemma eqTransitivity6: ΠX , Y, Z, U, V, W: X = Y ⊢ Y = Z ⊢ Z = U ⊢ U = V ⊢ V = W ⊢ X = W]

ZFsub proof of eqTransitivity6:

L01: Arbitrary ≫  X , Y, Z, U, V, W  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: Premise ≫  U = V  ;
L06: Premise ≫  V = W  ;

L07: eqTransitivity5 ⊳ L02 ⊳ L03 ⊳

L04 ⊳ L05 ≫ X = V ;

L08: eqTransitivity ⊳ L07 ⊳ L06 ≫ X = W  □

[ZFsub lemma plus0Left: ΠX: 0 + X = X]

ZFsub proof of plus0Left:

L01: Arbitrary ≫  X  ;
L02: plus0 ≫  X + 0 = X  ;
L03: plusCommutativity ≫  0 + X = X + 0  ;
L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ 0 + X = X  □

[ZFsub lemma times1Left: ΠX: 1 ∗ X = X]

ZFsub proof of times1Left:

L01: Arbitrary ≫  X  ;
L02: times1 ≫  X ∗ 1 = X  ;
L03: timesCommutativity ≫  1 ∗ X = X ∗ 1  ;
L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ 1 ∗ X = X  □

[ZFsub lemma lemma eqAdditionLeft: ΠX , Y, Z: X = Y ⊢ Z + X = Z + Y] ZFsub proof of lemma eqAdditionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: eqAddition ⊳ L02 ≫  X + Z = Y + Z  ;
L04: plusCommutativity ≫  Z + X = X + Z  ;
L05: plusCommutativity ≫  Y + Z = Z + Y  ;

L06: eqTransitivity4 ⊳ L04 ⊳ L03 ⊳

L05 ≫ Z + X = Z + Y □

[ZFsub lemma EqMultiplicationLeft: ΠX , Y, Z: X = Y ⊢ Z ∗ X = Z ∗ Y] ZFsub proof of EqMultiplicationLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: eqMultiplication ⊳ L02 ≫  X ∗ Z = Y ∗ Z  ;
L04: timesCommutativity ≫  Z ∗ X = X ∗ Z  ;
L05: timesCommutativity ≫  Y ∗ Z = Z ∗ Y  ;

L06: eqTransitivity4 ⊳ L04 ⊳ L03 ⊳

L05 ≫ Z ∗ X = Z ∗ Y □

[ZFsub lemma DistributionOut: ΠX , Y, Z: X ∗ Y + X ∗ Z = X ∗ (Y + Z)] ZFsub proof of DistributionOut:

L01: Arbitrary ≫ X , Y, Z ;
L02: Distribution ≫  X ∗ (Y + Z) = X ∗ Y + X ∗ Z ;

L03: eqSymmetry ⊳ L02 ≫  X ∗ Y + X ∗ Z = X ∗ (Y + Z) □

[ZFsub lemma Three2twoTerms: ΠX , Y, Z, U: Y + Z = U ⊢ X + Y + Z = X + U]

ZFsub proof of Three2twoTerms:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  Y + Z = U  ;
L03: lemma eqAdditionLeft⊳L02 ≫ X + (Y + Z) = X + U  ;
L04: plusAssociativity ≫ X + Y + Z = X + (Y + Z) ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ X + Y + Z = X + U  □

[ZFsub lemma Three2threeTerms: ΠX , Y, Z: X + Y + Z = X + Z + Y] ZFsub proof of Three2threeTerms:

L01: Arbitrary ≫  X , Y, Z  ;
L02: plusCommutativity ≫  Y + Z = Z + Y  ;
L03: Three2twoTerms ⊳ L02 ≫  X + Y + Z = X + (Z + Y)  ;
L04: plusAssociativity ≫  X + Z + Y = X + (Z + Y)  ;
L05: eqSymmetry ⊳ L04 ≫  X + (Z + Y) = X + Z + Y  ;
L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ X + Y + Z = X + Z + Y  □

[ZFsub lemma Three2threeFactors: ΠX , Y, Z, U: Y ∗ Z = U ⊢ X ∗ Y ∗ Z = X ∗ U]

ZFsub proof of Three2threeFactors:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  Y ∗ Z = U  ;
L03: EqMultiplicationLeft ⊳ L02 ≫ X ∗ (Y ∗ Z) = X ∗ U  ;
L04: timesAssociativity ≫ X ∗ Y ∗ Z = X ∗ (Y ∗ Z) ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ X ∗ Y ∗ Z = X ∗ U  □

[ZFsub lemma AddEquations: ΠX , Y, Z, U: X = Y ⊢ Z = U ⊢ X + Z = Y + U]

ZFsub proof of AddEquations:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z = U  ;
L04: eqAddition ⊳ L02 ≫  X + Z = Y + Z  ;
L05: lemma eqAdditionLeft⊳L03 ≫ Y + Z = Y + U  ;
L06: eqTransitivity ⊳ L04 ⊳ L05 ≫ X + Z = Y + U  □

[ZFsub lemma SubtractEquations: ΠX , Y, Z, U: X + Z = Y + U ⊢ Z = U ⊢ X = Y]

ZFsub proof of SubtractEquations:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X + Z = Y + U  ;
L03: Premise ≫  Z = U  ;
L04: eqAddition ⊳ L02 ≫  X + Z − Z = Y + U − Z  ;
L05: plus0Left ≫  0 + Z = Z  ;
L06: eqTransitivity ⊳ L05 ⊳ L03 ≫ 0 + Z = U  ;
L07: PositiveToRight(Eq) ⊳ L06 ≫ 0 = U − Z  ;
L08: eqSymmetry ⊳ L07 ≫ U − Z = 0 ;
L09: lemma eqAdditionLeft⊳L08 ≫ Y + (U − Z) = Y + 0  ;

L10: plusAssociativity ≫  Y + U − Z = Y + (U − Z)  ;
L11: plus0 ≫  Y + 0 = Y  ;

L12: eqTransitivity4 ⊳ L10 ⊳ L09 ⊳

L11 ≫ Y + U − Z = Y ;

L13: x = x + y − y ≫ X = X + Z − Z ;

L14: eqTransitivity4 ⊳ L13 ⊳ L04 ⊳

L12 ≫ X = Y □

[ZFsub lemma SubtractEquationsLeft: ΠX , Y, Z, U: X + Z = Y + U ⊢ X = Y ⊢ Z = U]

ZFsub proof of SubtractEquationsLeft:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X + Z = Y + U  ;
L03: Premise ≫  X = Y  ;
L04: plusCommutativity ≫  Z + X = X + Z  ;
L05: plusCommutativity ≫  Y + U = U + Y  ;

L06: eqTransitivity4 ⊳ L04 ⊳ L02 ⊳

L05 ≫ Z + X = U + Y ;

L07: SubtractEquations ⊳ L06 ⊳

L03 ≫ Z = U □

[ZFsub lemma EqNegated: ΠX , Y: X = Y ⊢ −X = −Y]

ZFsub proof of EqNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: Negative ≫  X − X = 0  ;
L04: Negative ≫  Y − Y = 0  ;
L05: eqSymmetry ⊳ L04 ≫  0 = Y − Y  ;
L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ X − X = Y − Y  ;

L07: SubtractEquationsLeft ⊳ L06 ⊳

L02 ≫ −X = −Y □

[ZFsub lemma PositiveToRight(Eq): ΠX , Y, Z: X + Y = Z ⊢ X = Z − Y] ZFsub proof of PositiveToRight(Eq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X + Y = Z  ;
L03: eqAddition ⊳ L02 ≫  X + Y − Y = Z − Y  ;
L04: x = x + y − y ≫  X = X + Y − Y  ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ X = Z − Y  □

[ZFsub lemma PositiveToLeft(Eq)(1term): ΠX , Y: X = Y ⊢ X − Y = 0] ZFsub proof of PositiveToLeft(Eq)(1term):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqAddition ⊳ L02 ≫  X − Y = Y − Y  ;
L04: Negative ≫  Y − Y = 0  ;
L05: eqTransitivity ⊳ L03 ⊳ L04 ≫ X − Y = 0  □

[ZFsub lemma PositiveToRight(Leq)(1term): ΠY, Z: Y <= Z ⊢ 0 <= Z − Y]

ZFsub proof of PositiveToRight(Leq)(1term):

L01: Arbitrary ≫  Y, Z  ;
L02: Premise ≫  Y <= Z  ;
L03: plus0Left ≫  0 + Y = Y  ;
L04: eqSymmetry ⊳ L03 ≫  Y = 0 + Y  ;
L05: subLeqLeft ⊳ L04 ⊳ L02 ≫  0 + Y <= Z  ;
L06: PositiveToRight(Leq) ⊳ L05 ≫ 0 <= Z − Y  □

[ZFsub lemma NegativeToLeft(Eq): ΠX , Y, Z: X = Y − Z ⊢ X + Z = Y] ZFsub proof of NegativeToLeft(Eq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y − Z  ;
L03: eqAddition ⊳ L02 ≫  X + Z = Y − Z + Z  ;
L04: Three2threeTerms ≫  Y − Z + Z = Y + Z − Z  ;
L05: x = x + y − y ≫  Y = Y + Z − Z  ;
L06: eqSymmetry ⊳ L05 ≫  Y + Z − Z = Y  ;

L07: eqTransitivity4 ⊳ L03 ⊳ L04 ⊳

L06 ≫ X + Z = Y □

(*** NO EQUALITY ***)

[ZFsub lemma LessNeq: ΠX , Y: X < Y ⊢ X ≠ Y]

ZFsub proof of LessNeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: Repetition ⊳ L02 ≫  X <= Y ˙∧ ˙¬ (X = Y)  ;
L04: SecondConjunct ⊳ L03 ≫  X ≠ Y  □

[ZFsub lemma NeqSymmetry: ΠX , Y: X ≠ Y ⊢ Y ≠ X]

ZFsub proof of NeqSymmetry:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  Y = X  ;
L04: eqSymmetry ⊳ L03 ≫  X = Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  Y = X ⇒ X = Y  ;
L08: Premise ≫  X ≠ Y  ;
L09: MT ⊳ L07 ⊳ L08 ≫  Y ≠ X  □

[ZFsub lemma NeqNegated: ΠX , Y: X ≠ Y ⊢ −X ≠ −Y]

ZFsub proof of NeqNegated:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X ≠ Y  ;
L04: Premise ≫  −X = −Y  ;
L05: EqNegated ⊳ L04 ≫  − − X = − − Y  ;
L06: DoubleMinus ≫  − − X = X  ;
L07: eqSymmetry ⊳ L06 ≫  X = − − X  ;
L08: DoubleMinus ≫  − − Y = Y  ;

L09: eqTransitivity4 ⊳ L07 ⊳ L05 ⊳

L08 ≫ X = Y ;

L10: FromContradiction ⊳ L09 ⊳

L03 ≫ −X ≠ −Y ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y  ;
L13: Ded ⊳ L11 ≫  {X ≠ Y ⇒ −X = −Y ⇒ ˙¬ − \atop X = −Y  ;}
L14: Premise ≫  X ≠ Y  ;
L15: MP ⊳ L13 ⊳ L14 ≫  −X = −Y ⇒ ˙¬ − X = −Y  ;
L16: ImplyNegation ⊳ L15 ≫  ˙¬ − X = −Y  □

[ZFsub lemma SubNeqRight: ΠX , Y, Z: X = Y ⊢ Z ≠ X ⊢ Z ≠ Y] ZFsub proof of SubNeqRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z ≠ X  ;
L04: NeqSymmetry ⊳ L03 ≫  X ≠ Z  ;
L05: SubNeqLeft ⊳ L02 ⊳ L04 ≫  Y ≠ Z  ;
L06: NeqSymmetry ⊳ L05 ≫  Z ≠ Y  □

[ZFsub lemma SubNeqLeft: ΠX , Y, Z: X = Y ⊢ X ≠ Z ⊢ Y ≠ Z] ZFsub proof of SubNeqLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X ≠ Z  ;
L04: equalityAxiom ≫  Y = X ⇒ Y = Z ⇒ X = Z  ;
L05: eqSymmetry ⊳ L02 ≫  Y = X  ;
L06: MP ⊳ L04 ⊳ L05 ≫  Y = Z ⇒ X = Z  ;
L07: Contrapositive ⊳ L06 ≫  X ≠ Z ⇒ Y ≠ Z  ;
L08: MP ⊳ L07 ⊳ L03 ≫  Y ≠ Z  □

[ZFsub lemma NeqAddition: ΠX , Y, Z: X ≠ Y ⊢ X + Z ≠ Y + Z] ZFsub proof of NeqAddition:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X ≠ Y  ;
L04: Premise ≫  X + Z = Y + Z  ;
L05: eqReflexivity ≫  Z = Z  ;

L06: SubtractEquations ⊳ L04 ⊳

L05 ≫ X = Y ;

L07: FromContradiction ⊳ L06 ⊳

L03 ≫ X + Z ≠ Y + Z ;

L08: Block ≫  End  ;
L09: Arbitrary ≫  X , Y, Z  ;
L10: Ded ⊳ L08 ≫  {X ≠ Y ⇒ X + Z = Y + Z ⇒ \atop X + Z ≠ Y + Z  ;}
L11: Premise ≫  X ≠ Y  ;
L12: MP ⊳ L10 ⊳ L11 ≫  X +Z = Y+Z ⇒ X +Z ≠ Y+Z ;
L13: ImplyNegation ⊳ L12 ≫  X + Z ≠ Y + Z  □

[ZFsub lemma NeqMultiplication: ΠX , Y, Z: Z ≠ 0 ⊢ X ≠ Y ⊢ X ∗ Z ≠ Y ∗ Z]

ZFsub proof of NeqMultiplication:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  Z ≠ 0  ;
L04: Premise ≫  X ≠ Y  ;
L05: Premise ≫  X ∗ Z = Y ∗ Z  ;
L06: ⊳L03 ≫  X = X ∗ Z ∗ recZ  ;
L07: eqMultiplication ⊳ L05 ≫  X ∗ Z ∗ recZ = Y ∗ Z ∗ recZ  ;
L08: ⊳L03 ≫  Y = Y ∗ Z ∗ recZ  ;
L09: eqSymmetry ⊳ L08 ≫  Y ∗ Z ∗ recZ = Y  ;

L10: eqTransitivity4 ⊳ L06 ⊳ L07 ⊳

L09 ≫ X = Y ;

L11: FromContradiction ⊳ L10 ⊳

L04 ≫ X ∗ Z ≠ Y ∗ Z ;

L12: Block ≫  End  ;
L13: Arbitrary ≫  X , Y, Z  ;
L14: Ded ⊳ L12 ≫  {Z ≠ 0 ⇒ X ≠ Y ⇒ X ∗ Z = \atop Y ∗ Z ⇒ X ∗ Z ≠ Y ∗ Z  ;}
L15: Premise ≫  Z ≠ 0  ;
L16: Premise ≫  X ≠ Y  ;
L17: MP2 ⊳ L14 ⊳ L15 ⊳ L16 ≫  X ∗ Z = Y ∗ Z ⇒ X ∗ Z ≠ Y ∗ Z ;
L18: ImplyNegation ⊳ L17 ≫ X ∗ Z ≠ Y ∗ Z □

(*** NEGATIVE ***)

[ZFsub lemma UniqueNegative: ΠX , Y, Z: X +Y = 0 ⊢ X +Z = 0 ⊢ Y = Z] ZFsub proof of UniqueNegative:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X + Y = 0  ;
L03: Premise ≫  X + Z = 0  ;
L04: plusCommutativity ≫  Y + X = X + Y  ;
L05: eqTransitivity ⊳ L04 ⊳ L02 ≫ Y + X = 0  ;
L06: PositiveToRight(Eq) ⊳ L05 ≫ Y = 0 − X  ;
L07: plusCommutativity ≫ Z + X = X + Z ;
L08: eqTransitivity ⊳ L07 ⊳ L03 ≫ Z + X = 0  ;
L09: PositiveToRight(Eq) ⊳ L08 ≫ Z = 0 − X  ;
L10: eqSymmetry ⊳ L09 ≫ 0 − X = Z ;
L11: eqTransitivity ⊳ L06 ⊳ L10 ≫ Y = Z  □

[ZFsub lemma DoubleMinus: ΠX: − − X = X]

ZFsub proof of DoubleMinus:

L01: Arbitrary ≫  X  ;
L02: Negative ≫  −X − −X = 0  ;
L03: x + y = zBackwards ⊳ L02 ≫ 0 = − − X − X  ;
L04: NegativeToLeft(Eq) ⊳ L03 ≫ 0 + X = − − X  ;
L05: plus0Left ≫  0 + X = X  ;
L06: Equality ⊳ L04 ⊳ L05 ≫  − − X = X  □

(*** LEQ, nummer 1 af 2 ***)

[ZFsub lemma LeqLessEq: ΠX , Y: X <= Y ⊢ X < Y ˙∨ X = Y]

ZFsub proof of LeqLessEq:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  ˙¬ X < Y  ;
L05: fromNotLess ⊳ L04 ≫  Y <= X  ;
L06: leqAntisymmetry⊳L03⊳L05 ≫ X = Y  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  X , Y  ;
L09: Ded ⊳ L07 ≫  X <= Y ⇒ ˙¬ X < Y ⇒ X = Y ;
L10: Premise ≫  X <= Y  ;
L11: MP ⊳ L09 ⊳ L10 ≫  ˙¬ X < Y ⇒ X = Y  ;
L12: Repetition ⊳ L11 ≫  X < Y ˙∨ X = Y  □

[ZFsub lemma LessLeq: ΠX , Y: X < Y ⊢ X <= Y]

ZFsub proof of LessLeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: Repetition ⊳ L02 ≫  X <= Y ˙∧ ˙¬ (X = Y)  ;
L04: FirstConjunct ⊳ L03 ≫  X <= Y  □

[ZFsub lemma FromLeqGeq: ΠA, X , Y: X <= Y ⇒ A ⊢ Y <= X ⇒ A ⊢ A]

ZFsub proof of FromLeqGeq:

L01: Arbitrary ≫  A, X , Y  ;
L02: Premise ≫  X <= Y ⇒ A  ;
L03: Premise ≫  Y <= X ⇒ A  ;
L04: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ A □

[ZFsub lemma subLeqRight: ΠX , Y, Z: X = Y ⊢ Z <= X ⊢ Z <= Y] ZFsub proof of subLeqRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z <= X  ;
L04: eqLeq ⊳ L02 ≫  X <= Y  ;
L05: leqTransitivity ⊳ L03 ⊳ L04 ≫ Z <= Y  □

[ZFsub lemma subLeqLeft: ΠX , Y, Z: X = Y ⊢ X <= Z ⊢ Y <= Z] ZFsub proof of subLeqLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X <= Z  ;
L04: eqSymmetry ⊳ L02 ≫  Y = X  ;
L05: eqLeq ⊳ L04 ≫  Y <= X  ;
L06: leqTransitivity ⊳ L05 ⊳ L03 ≫ Y <= Z  □

[ZFsub lemma Leq + 1: ΠX , Y: X <= Y ⊢ X < Y + 1]

ZFsub proof of Leq + 1:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: 0 < 1 ≫  0 < 1  ;
L04: LessAdditionLeft ⊳ L03 ≫  Y + 0 < Y + 1  ;
L05: plus0 ≫  Y + 0 = Y  ;
L06: SubLessLeft ⊳ L05 ⊳ L04 ≫  Y < Y + 1  ;

L07: leqLessTransitivity ⊳ L02 ⊳

L06 ≫ X < Y + 1 □

[ZFsub lemma PositiveToRight(Leq): ΠX , Y, Z: X + Y <= Z ⊢ X <= Z − Y]

ZFsub proof of PositiveToRight(Leq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X + Y <= Z  ;
L03: leqAddition ⊳ L02 ≫  X + Y − Y <= Z − Y  ;
L04: x = x + y − y ≫  X = X + Y − Y  ;
L05: eqSymmetry ⊳ L04 ≫  X + Y − Y = X  ;
L06: subLeqLeft ⊳ L05 ⊳ L03 ≫  X <= Z − Y  □

[ZFsub lemma LeqAdditionLeft: ΠX , Y, Z: X <= Y ⊢ Z + X <= Z + Y] ZFsub proof of LeqAdditionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: leqAddition ⊳ L02 ≫  X + Z <= Y + Z  ;
L04: plusCommutativity ≫  X + Z = Z + X  ;
L05: plusCommutativity ≫  Y + Z = Z + Y  ;
L06: subLeqLeft ⊳ L04 ⊳ L03 ≫  Z + X <= Y + Z  ;
L07: subLeqRight ⊳ L05 ⊳ L06 ≫  Z + X <= Z + Y  □

[ZFsub lemma leqSubtraction: ΠX , Y, Z: X + Z <= Y + Z ⊢ X <= Y] ZFsub proof of leqSubtraction:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X + Z <= Y + Z  ;
L03: leqAddition ⊳ L02 ≫  X + Z − Z <= Y + Z − Z  ;
L04: x = x + y − y ≫  X = X + Z − Z  ;
L05: eqSymmetry ⊳ L04 ≫  X + Z − Z = X  ;
L06: x = x + y − y ≫  Y = Y + Z − Z  ;
L07: eqSymmetry ⊳ L06 ≫  Y + Z − Z = Y  ;
L08: subLeqLeft ⊳ L05 ⊳ L03 ≫  X <= Y + Z − Z  ;
L09: subLeqRight ⊳ L07 ⊳ L08 ≫  X <= Y  □

[ZFsub lemma leqSubtractionLeft: ΠX , Y, Z: Z + X <= Z + Y ⊢ X <= Y] ZFsub proof of leqSubtractionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  Z + X <= Z + Y  ;
L03: plusCommutativity ≫  Z + X = X + Z  ;
L04: plusCommutativity ≫  Z + Y = Y + Z  ;
L05: subLeqLeft ⊳ L03 ⊳ L02 ≫  X + Z <= Z + Y  ;

L06: subLeqRight ⊳ L04 ⊳ L05 ≫  X + Z <= Y + Z  ;
L07: leqSubtraction ⊳ L06 ≫  X <= Y  □

[ZFsub lemma thirdGeq: ΠX , Y: X <= Ex3 ˙∧ Y <= Ex3]

ZFsub proof of thirdGeq:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: leqReflexivity ≫  Y <= Y  ;
L05: JoinConjuncts ⊳ L03 ⊳ L04 ≫ X <= Y ˙∧ Y <= Y  ;
L06: ExistIntro @ Ex3 @ Y ⊳ L05 ≫ X <= Ex3 ˙∧ Y <= Ex3  ;
L07: Block ≫  End  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  X , Y  ;
L10: Premise ≫  Y <= X  ;
L11: leqReflexivity ≫  X <= X  ;
L12: JoinConjuncts ⊳ L11 ⊳ L10 ≫ X <= X ˙∧ Y <= X  ;
L13: ExistIntro @ Ex3 @ X ⊳ L12 ≫ X <= Ex3 ˙∧ Y <= Ex3  ;
L14: Block ≫  End  ;
L15: Arbitrary ≫  X , Y  ;
L16: Ded ⊳ L07 ≫  {X <= Y ⇒ X <= Ex3 ˙∧ Y <= \atop Ex3  ;}
L17: Ded ⊳ L14 ≫  {Y <= X ⇒ X <= Ex3 ˙∧ Y <= \atop Ex3  ;}
L18: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L19: FromDisjuncts ⊳ L18 ⊳ L16 ⊳

L17 ≫ X <= Ex3 ˙∧ Y <= Ex3 □

[ZFsub lemma LeqNegated: ΠX , Y: X <= Y ⊢ −Y <= −X]

ZFsub proof of LeqNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: leqAddition ⊳ L02 ≫  X − X <= Y − X  ;
L04: Negative ≫  X − X = 0  ;
L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  0 <= Y − X  ;
L06: plusCommutativity ≫  Y − X = −X + Y  ;
L07: subLeqRight ⊳ L06 ⊳ L05 ≫  0 <= −X + Y  ;
L08: leqAddition ⊳ L07 ≫  0 − Y <= −X + Y − Y  ;
L09: plus0Left ≫  0 − Y = −Y  ;
L10: x = x + y − y ≫  −X = −X + Y − Y  ;
L11: eqSymmetry ⊳ L10 ≫  −X + Y − Y = −X  ;
L12: subLeqLeft ⊳ L09 ⊳ L08 ≫  −Y <= −X + Y − Y  ;
L13: subLeqRight ⊳ L11 ⊳ L12 ≫  −Y <= −X  □

[ZFsub lemma AddEquations(Leq): ΠX , Y, Z, U: X <= Y ⊢ Z <= U ⊢ X + Z <= Y + U]

ZFsub proof of AddEquations(Leq):

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X <= Y  ;

L03: Premise ≫  Z <= U  ;
L04: leqAddition ⊳ L02 ≫  X + Z <= Y + Z  ;
L05: LeqAdditionLeft ⊳ L03 ≫  Y + Z <= Y + U  ;
L06: leqTransitivity ⊳ L04 ⊳ L05 ≫ X + Z <= Y + U  □

(*** LESS ***)

[ZFsub lemma LeqNeqLess: ΠX , Y: X <= Y ⊢ X ≠ Y ⊢ X < Y] ZFsub proof of LeqNeqLess:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  X ≠ Y  ;
L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫ X <= Y ˙∧ X ≠ Y  ;
L05: Repetition ⊳ L04 ≫ X < Y □

[ZFsub lemma FromLess: ΠX , Y: X < Y ⊢ ˙¬ Y <= X]

ZFsub proof of FromLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  Y <= X  ;
L04: toNotLess ⊳ L03 ≫  ˙¬ X < Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  Y <= X ⇒ ˙¬ X < Y  ;
L08: Premise ≫  X < Y  ;
L09: AddDoubleNeg ⊳ L08 ≫  ˙¬ ˙¬ X < Y  ;
L10: MT ⊳ L07 ⊳ L09 ≫  ˙¬ Y <= X  □

[ZFsub lemma ToLess: ΠX , Y: ˙¬ X <= Y ⊢ Y < X]

ZFsub proof of ToLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ Y < X  ;
L04: fromNotLess ⊳ L03 ≫  X <= Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  ˙¬ Y < X ⇒ X <= Y  ;
L08: Premise ≫  ˙¬ X <= Y  ;
L09: NegativeMT ⊳ L07 ⊳ L08 ≫  Y < X  □

[ZFsub lemma fromNotLess: ΠX , Y: ˙¬ (X < Y) ⊢ Y <= X] ZFsub proof of fromNotLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ (X < Y)  ;
L04: Premise ≫  X <= Y  ;
L05: Repetition ⊳ L03 ≫  ˙¬ ˙¬ (X <= Y ⇒ ˙¬ X ≠ Y)  ;
L06: RemoveDoubleNeg ⊳ L05 ≫  X <= Y ⇒ ˙¬ X ≠ Y  ;
L07: MP ⊳ L06 ⊳ L04 ≫  ˙¬ X ≠ Y  ;
L08: RemoveDoubleNeg ⊳ L07 ≫  X = Y  ;
L09: eqSymmetry ⊳ L08 ≫  Y = X  ;

L10: eqLeq ⊳ L09 ≫  Y <= X  ;
L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y  ;
L13: Ded ⊳ L11 ≫  {˙¬ X < Y ⇒ X <= Y ⇒ Y <= \atop X  ;}
L14: Premise ≫  ˙¬ X < Y  ;
L15: MP ⊳ L13 ⊳ L14 ≫  X <= Y ⇒ Y <= X  ;
L16: AutoImply ≫  Y <= X ⇒ Y <= X  ;
L17: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L18: FromDisjuncts ⊳ L17 ⊳ L15 ⊳

L16 ≫ Y <= X □

[ZFsub lemma toNotLess: ΠX , Y: X <= Y ⊢ ˙¬ Y < X]

ZFsub proof of toNotLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  Y <= X  ;
L05: leqAntisymmetry⊳L04⊳L03 ≫ Y = X  ;
L06: AddDoubleNeg ⊳ L05 ≫  ˙¬ ˙¬ Y = X  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  X , Y  ;
L09: Ded ⊳ L07 ≫  {X <= Y ⇒ Y <= X ⇒ \atop ˙¬ ˙¬ Y = X  ;}
L10: Premise ≫  X <= Y  ;
L11: MP ⊳ L09 ⊳ L10 ≫  Y <= X ⇒ ˙¬ ˙¬ Y = X  ;
L12: AddDoubleNeg ⊳ L11 ≫  ˙¬ ˙¬ (Y <= X ⇒ ˙¬ ˙¬ Y = X)  ;
L13: Repetition ⊳ L12 ≫  ˙¬ (Y <= X ˙∧ ˙¬ Y = X)  ;
L14: Repetition ⊳ L13 ≫  ˙¬ Y < X  □

[ZFsub lemma LessAddition: ΠX , Y, Z: X < Y ⊢ X + Z < Y + Z] ZFsub proof of LessAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: LessLeq ⊳ L02 ≫  X <= Y  ;
L04: leqAddition ⊳ L03 ≫  X + Z <= Y + Z  ;
L05: LessNeq ⊳ L02 ≫  X ≠ Y  ;
L06: NeqAddition ⊳ L05 ≫  X + Z ≠ Y + Z  ;
L07: JoinConjuncts ⊳ L04 ⊳ L06 ≫ X + Z < Y + Z  □

[ZFsub lemma LessAdditionLeft: ΠX , Y, Z: X < Y ⊢ Z + X < Z + Y] ZFsub proof of LessAdditionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: LessAddition ⊳ L02 ≫  X + Z < Y + Z  ;
L04: plusCommutativity ≫  X + Z = Z + X  ;
L05: SubLessLeft ⊳ L04 ⊳ L03 ≫  Z + X < Y + Z  ;
L06: plusCommutativity ≫  Y + Z = Z + Y  ;

L07: SubLessRight ⊳ L06 ⊳ L05 ≫ Z + X < Z + Y  □

[ZFsub lemma LessMultiplication: ΠX , Y, Z: 0 < Z ⊢ X < Y ⊢ X ∗ Z < Y ∗ Z]

ZFsub proof of LessMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 < Z  ;
L03: Premise ≫  X < Y  ;
L04: LessLeq ⊳ L03 ≫  X <= Y  ;
L05: LessLeq ⊳ L02 ≫  0 <= Z  ;
L06: leqMultiplication⊳L05⊳L04 ≫ X ∗ Z <= Y ∗ Z  ;
L07: LessNeq ⊳ L03 ≫  X ≠ Y  ;
L08: LessNeq ⊳ L02 ≫  0 ≠ Z  ;
L09: NeqSymmetry ⊳ L08 ≫  Z ≠ 0  ;

L10: NeqMultiplication ⊳ L09 ⊳

L07 ≫ X ∗ Z ≠ Y ∗ Z ;

L11: LeqNeqLess ⊳ L06 ⊳ L10 ≫ X ∗ Z < Y ∗ Z □

[ZFsub lemma LessMultiplicationLeft: ΠX , Y, Z: 0 < Z ⊢ X < Y ⊢ Z∗X < Z ∗ Y]

ZFsub proof of LessMultiplicationLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 < Z  ;
L03: Premise ≫  X < Y  ;

L04: LessMultiplication ⊳ L02 ⊳

L03 ≫ X ∗ Z < Y ∗ Z ;

L05: timesCommutativity ≫  X ∗ Z = Z ∗ X  ;
L06: timesCommutativity ≫  Y ∗ Z = Z ∗ Y  ;
L07: SubLessLeft ⊳ L05 ⊳ L04 ≫  Z ∗ X < Y ∗ Z  ;
L08: SubLessRight ⊳ L06 ⊳ L07 ≫ Z ∗ X < Z ∗ Y  □

[ZFsub lemma LessDivision: ΠX , Y, Z: 0 <= Z ⊢ X ∗ Z < Y ∗ Z ⊢ X < Y] ZFsub proof of LessDivision:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 <= Z  ;
L03: Premise ≫  X ∗ Z < Y ∗ Z  ;
L04: FromLess ⊳ L03 ≫  ˙¬ Y ∗ Z <= X ∗ Z  ;
L05: leqMultiplicationAxiom ≫  {0 <= Z ⇒ Y <= X ⇒ Y ∗ \atop Z <= X ∗ Z  ;}
L06: MP ⊳ L05 ⊳ L02 ≫  Y <= X ⇒ Y ∗ Z <= X ∗ Z  ;
L07: Contrapositive ⊳ L06 ≫  ˙¬ Y ∗ Z <= X ∗ Z ⇒ ˙¬ Y <= X ;
L08: MP ⊳ L07 ⊳ L04 ≫  ˙¬ Y <= X  ;
L09: ToLess ⊳ L08 ≫  X < Y  □

[ZFsub lemma AddEquations(Less): ΠX , Y, Z, U: X < Y ⊢ Z < U ⊢ X + Z < Y + U]

ZFsub proof of AddEquations(Less):

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X < Y  ;

L03: Premise ≫  Z < U  ;
L04: LessAddition ⊳ L02 ≫  X + Z < Y + Z  ;
L05: LessAdditionLeft ⊳ L03 ≫  Y + Z < Y + U  ;
L06: LessTransitivity⊳L04⊳L05 ≫ X + Z < Y + U  □

[ZFsub lemma leqLessTransitivity: ΠX , Y, Z: X <= Y ⊢ Y < Z ⊢ X < Z] ZFsub proof of leqLessTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  Y < Z  ;
L05: Premise ≫  X = Z  ;
L06: FirstConjunct ⊳ L04 ≫  Y <= Z  ;
L07: SecondConjunct ⊳ L04 ≫  Y ≠ Z  ;
L08: subLeqLeft ⊳ L05 ⊳ L03 ≫  Z <= Y  ;
L09: leqAntisymmetry⊳L06⊳L08 ≫ Y = Z  ;

L10: FromContradiction ⊳ L09 ⊳

L07 ≫ X ≠ Z ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y, Z  ;
L13: Ded ⊳ L11 ≫  {X <= Y ⇒ Y < Z ⇒ X = \atop Z ⇒ X ≠ Z  ;}
L14: Premise ≫  X <= Y  ;
L15: Premise ≫  Y < Z  ;
L16: MP2 ⊳ L13 ⊳ L14 ⊳ L15 ≫  X = Z ⇒ X ≠ Z  ;
L17: ImplyNegation ⊳ L16 ≫  X ≠ Z  ;
L18: FirstConjunct ⊳ L15 ≫  Y <= Z  ;
L19: leqTransitivity ⊳ L14 ⊳ L18 ≫ X <= Z  ;
L20: JoinConjuncts ⊳ L19 ⊳ L17 ≫ X < Z  □

[ZFsub lemma LessLeqTransitivity: ΠX , Y, Z: X < Y ⊢ Y <= Z ⊢ X < Z] ZFsub proof of LessLeqTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X < Y  ;
L04: Premise ≫  Y <= Z  ;
L05: Premise ≫  Z = X  ;
L06: FirstConjunct ⊳ L03 ≫  X <= Y  ;
L07: SecondConjunct ⊳ L03 ≫  X ≠ Y  ;
L08: subLeqRight ⊳ L05 ⊳ L04 ≫  Y <= X  ;
L09: leqAntisymmetry⊳L06⊳L08 ≫ X = Y  ;

L10: FromContradiction ⊳ L09 ⊳

L07 ≫ Z ≠ X ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y, Z  ;
L13: Ded ⊳ L11 ≫  {X < Y ⇒ Y <= Z ⇒ Z = \atop X ⇒ Z ≠ X  ;}

L14: Premise ≫  X < Y  ;
L15: Premise ≫  Y <= Z  ;
L16: MP2 ⊳ L13 ⊳ L14 ⊳ L15 ≫  Z = X ⇒ Z ≠ X  ;
L17: ImplyNegation ⊳ L16 ≫  Z ≠ X  ;
L18: NeqSymmetry ⊳ L17 ≫  X ≠ Z  ;
L19: FirstConjunct ⊳ L14 ≫  X <= Y  ;
L20: leqTransitivity ⊳ L19 ⊳ L15 ≫ X <= Z  ;
L21: JoinConjuncts ⊳ L20 ⊳ L18 ≫ X < Z  □

[ZFsub lemma LessTransitivity: ΠX , Y, Z: X < Y ⊢ Y < Z ⊢ X < Z] ZFsub proof of LessTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: Premise ≫  Y < Z  ;
L04: FirstConjunct ⊳ L03 ≫  Y <= Z  ;

L05: LessLeqTransitivity ⊳ L02 ⊳

L04 ≫ X < Z □

[ZFsub lemma LessTotality: ΠX , Y: X < Y ˙∨ X = Y ˙∨ Y < X] ZFsub proof of LessTotality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ X < Y  ;
L04: Premise ≫  X ≠ Y  ;
L05: fromNotLess ⊳ L03 ≫  Y <= X  ;
L06: NeqSymmetry ⊳ L04 ≫  Y ≠ X  ;
L07: LeqNeqLess ⊳ L05 ⊳ L06 ≫  Y < X  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  X , Y  ;
L10: Ded ⊳ L08 ≫  ˙¬ X < Y ⇒ X ≠ Y ⇒ Y < X  ;
L11: Repetition ⊳ L10 ≫  X < Y ˙∨ X = Y ˙∨ Y < X  □

[ZFsub lemma SubLessRight: ΠX , Y, Z: X = Y ⊢ Z < X ⊢ Z < Y] ZFsub proof of SubLessRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z < X  ;
L04: Repetition ⊳ L03 ≫  Z <= X ˙∧ Z ≠ X  ;
L05: FirstConjunct ⊳ L04 ≫  Z <= X  ;
L06: subLeqRight ⊳ L02 ⊳ L05 ≫  Z <= Y  ;
L07: SecondConjunct ⊳ L04 ≫  Z ≠ X  ;
L08: SubNeqRight ⊳ L02 ⊳ L07 ≫  Z ≠ Y  ;
L09: JoinConjuncts ⊳ L06 ⊳ L08 ≫ Z < Y  □

[ZFsub lemma SubLessLeft: ΠX , Y, Z: X = Y ⊢ X < Z ⊢ Y < Z] ZFsub proof of SubLessLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X < Z  ;
L04: Repetition ⊳ L03 ≫  X <= Z ˙∧ X ≠ Z  ;

L05: FirstConjunct ⊳ L04 ≫  X <= Z  ;
L06: subLeqLeft ⊳ L02 ⊳ L05 ≫  Y <= Z  ;
L07: SecondConjunct ⊳ L04 ≫  X ≠ Z  ;
L08: SubNeqLeft ⊳ L02 ⊳ L07 ≫  Y ≠ Z  ;
L09: JoinConjuncts ⊳ L06 ⊳ L08 ≫ Y < Z  □

[ZFsub lemma NegativeLessPositive: ΠX: 0 < X ⊢ −X < X] ZFsub proof of NegativeLessPositive:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: FirstConjunct ⊳ L02 ≫  0 <= X  ;
L04: leqAddition ⊳ L03 ≫  0 − X <= X − X  ;
L05: plus0Left ≫  0 − X = −X  ;
L06: Negative ≫  X − X = 0  ;
L07: subLeqLeft ⊳ L05 ⊳ L04 ≫  −X <= X − X  ;
L08: subLeqRight ⊳ L06 ⊳ L07 ≫  −X <= 0  ;

L09: leqLessTransitivity ⊳ L08 ⊳

L02 ≫ −X < X □

[ZFsub lemma LessNegated: ΠX , Y: X < Y ⊢ −Y < −X] ZFsub proof of LessNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: LessLeq ⊳ L02 ≫  X <= Y  ;
L04: LeqNegated ⊳ L03 ≫  −Y <= −X  ;
L05: LessNeq ⊳ L02 ≫  X ≠ Y  ;
L06: NeqNegated ⊳ L05 ≫  ˙¬ − X = −Y  ;
L07: NeqSymmetry ⊳ L06 ≫  ˙¬ − Y = −X  ;
L08: LeqNeqLess ⊳ L04 ⊳ L07 ≫  −Y < −X  □

[ZFsub lemma PositiveNegated: ΠX: 0 < X ⊢ −X < 0] ZFsub proof of PositiveNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: LessNegated ⊳ L02 ≫  −X < −0  ;
L04: −0 = 0 ≫  −0 = 0  ;
L05: SubLessRight ⊳ L04 ⊳ L03 ≫ −X < 0  □

[ZFsub lemma NonpositiveNegated: ΠX: X <= 0 ⊢ 0 <= −X] ZFsub proof of NonpositiveNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X <= 0  ;
L03: LeqNegated ⊳ L02 ≫  −0 <= −X  ;
L04: −0 = 0 ≫  −0 = 0  ;
L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  0 <= −X  □

[ZFsub lemma NegativeNegated: ΠX: X < 0 ⊢ 0 < −X] ZFsub proof of NegativeNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X < 0  ;
L03: LessNegated ⊳ L02 ≫  −0 < −X  ;

L04: −0 = 0 ≫  −0 = 0  ;
L05: SubLessLeft ⊳ L04 ⊳ L03 ≫  0 < −X  □

[ZFsub lemma NonnegativeNegated: ΠX: 0 <= X ⊢ −X <= 0] ZFsub proof of NonnegativeNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 <= X  ;
L03: LeqNegated ⊳ L02 ≫  −X <= −0  ;
L04: −0 = 0 ≫  −0 = 0  ;
L05: subLeqRight ⊳ L04 ⊳ L03 ≫  −X <= 0  □

[ZFsub lemma PositiveHalved: ΠX: 0 < X ⊢ 0 < 1/2 ∗ X]

ZFsub proof of PositiveHalved:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: 0 < 1/2 ≫  0 < 1/2  ;

L04: LessMultiplicationLeft ⊳ L03 ⊳

L02 ≫ 1/2 ∗ 0 < 1/2 ∗ X ;

L05: x ∗ 0 = 0 ≫  1/2 ∗ 0 = 0  ;
L06: SubLessLeft ⊳ L05 ⊳ L04 ≫  0 < 1/2 ∗ X  □

(*** NUMERISK ***)

[ZFsub lemma NonnegativeNumerical: ΠX: 0 <= X ⊢ |X | = X] ZFsub proof of NonnegativeNumerical:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 <= X  ;
L03: IfThenElse(T) ⊳ L02 ≫  if(0 <= X , X , −X) = X  ;
L04: Repetition ⊳ L03 ≫  |X | = X  □

[ZFsub lemma PositiveNumerical: ΠX: 0 < X ⊢ |X | = X]

ZFsub proof of PositiveNumerical:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: LessLeq ⊳ L02 ≫  0 <= X  ;
L04: NonnegativeNumerical⊳L03 ≫ |X | = X  □

[ZFsub lemma NegativeNumerical: ΠX: X < 0 ⊢ |X | = −X]

ZFsub proof of NegativeNumerical:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X < 0  ;
L03: FromLess ⊳ L02 ≫  ˙¬ 0 <= X  ;
L04: IfThenElse(F) ⊳ L03 ≫  if(0 <= X , X , −X) = −X  ;
L05: Repetition ⊳ L04 ≫  |X | = −X  □

[ZFsub lemma lemma nonpositiveNumerical: ΠX: X <= 0 ⊢ |X | = −X] ZFsub proof of lemma nonpositiveNumerical:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;
L03: Premise ≫  X < 0  ;
L04: NegativeNumerical ⊳ L03 ≫  |X | = −X  ;
L05: Block ≫  End  ;

L06: Block ≫  Begin  ;
L07: Arbitrary ≫  X  ;
L08: Premise ≫  X = 0  ;
L09: eqSymmetry ⊳ L08 ≫  0 = X  ;
L10: eqLeq ⊳ L09 ≫  0 <= X  ;
L11: NonnegativeNumerical⊳L10 ≫ |X | = X  ;
L12: −0 = 0 ≫  −0 = 0  ;
L13: eqSymmetry ⊳ L12 ≫  0 = −0  ;
L14: EqNegated ⊳ L09 ≫  −0 = −X  ;

L15: eqTransitivity5 ⊳ L11 ⊳ L08 ⊳

L13 ⊳ L14 ≫ |X | = −X ;

L16: Block ≫  End  ;
L17: Arbitrary ≫  X  ;
L18: Ded ⊳ L05 ≫  X < 0 ⇒ |X | = −X  ;
L19: Ded ⊳ L16 ≫  X = 0 ⇒ |X | = −X  ;
L20: Premise ≫  X <= 0  ;
L21: LeqLessEq ⊳ L20 ≫  X < 0 ˙∨ X = 0  ;

L22: FromDisjuncts ⊳ L21 ⊳ L18 ⊳

L19 ≫ |X | = −X □

[ZFsub lemma |0| = 0: |0| = 0]

ZFsub proof of |0| = 0:

L01: leqReflexivity ≫  0 <= 0  ;
L02: NonnegativeNumerical⊳L01 ≫ |0| = 0  □

[ZFsub lemma 0 <= |x|: ΠX: 0 <= |X |] ZFsub proof of 0 <= |x|:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;
L03: Premise ≫  0 <= X  ;
L04: NonnegativeNumerical⊳L03 ≫ |X | = X  ;
L05: eqSymmetry ⊳ L04 ≫  X = |X |  ;
L06: subLeqRight ⊳ L05 ⊳ L03 ≫  0 <= |X |  ;
L07: Block ≫  End  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  X  ;
L10: Premise ≫  ˙¬ 0 <= X  ;
L11: ToLess ⊳ L10 ≫  X < 0  ;
L12: NegativeNumerical ⊳ L11 ≫  |X | = −X  ;
L13: eqSymmetry ⊳ L12 ≫  −X = |X |  ;
L14: NegativeNegated ⊳ L11 ≫  0 < −X  ;
L15: LessLeq ⊳ L14 ≫  0 <= −X  ;
L16: subLeqRight ⊳ L13 ⊳ L15 ≫  0 <= |X |  ;
L17: Block ≫  End  ;
L18: Arbitrary ≫  X  ;

L19: Ded ⊳ L07 ≫  0 <= X ⇒ 0 <= |X |  ;
L20: Ded ⊳ L17 ≫  ˙¬ 0 <= X ⇒ 0 <= |X |  ;
L21: FromNegations ⊳ L19 ⊳ L20 ≫ 0 <= |X |  □

[ZFsub lemma SameNumerical: ΠX , Y: X = Y ⊢ |X | = |Y|] ZFsub proof of SameNumerical:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  0 <= X  ;
L04: Premise ≫  X = Y  ;
L05: NonnegativeNumerical⊳L03 ≫ |X | = X  ;
L06: subLeqRight ⊳ L04 ⊳ L03 ≫  0 <= Y  ;
L07: NonnegativeNumerical⊳L06 ≫ |Y| = Y  ;
L08: eqSymmetry ⊳ L07 ≫ Y = |Y| ;

L09: eqTransitivity4 ⊳ L05 ⊳ L04 ⊳

L08 ≫ |X | = |Y| ;

L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  X , Y  ;
L13: Premise ≫  ˙¬ 0 <= X  ;
L14: Premise ≫  X = Y  ;
L15: ToLess ⊳ L13 ≫  X < 0  ;
L16: NegativeNumerical ⊳ L15 ≫  |X | = −X  ;
L17: SubLessLeft ⊳ L14 ⊳ L15 ≫  Y < 0  ;
L18: NegativeNumerical ⊳ L17 ≫  |Y| = −Y  ;
L19: eqSymmetry ⊳ L18 ≫  −Y = |Y|  ;
L20: EqNegated ⊳ L14 ≫  −X = −Y  ;

L21: eqTransitivity4 ⊳ L16 ⊳ L20 ⊳

L19 ≫ |X | = |Y| ;

L22: Block ≫  End  ;
L23: Arbitrary ≫  X , Y  ;
L24: Premise ≫  X = Y  ;
L25: Ded ⊳ L10 ≫  0 <= X ⇒ X = Y ⇒ |X | = |Y| ;
L26: Ded ⊳ L22 ≫  {˙¬ 0 <= X ⇒ X = Y ⇒ |X | = \atop |Y|  ;}
L27: FromNegations ⊳ L25 ⊳ L26 ≫ X = Y ⇒ |X | = |Y|  ;
L28: MP ⊳ L27 ⊳ L24 ≫ |X | = |Y| □

[ZFsub lemma SignNumerical(+): ΠX: 0 < X ⊢ |X | = | − X |] ZFsub proof of SignNumerical(+):

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: PositiveNumerical ⊳ L02 ≫  |X | = X  ;
L04: PositiveNegated ⊳ L02 ≫  −X < 0  ;
L05: NegativeNumerical ⊳ L04 ≫  | − X | = − − X  ;
L06: DoubleMinus ≫  − − X = X  ;

L07: eqTransitivity ⊳ L05 ⊳ L06 ≫ | − X | = X  ;
L08: eqSymmetry ⊳ L07 ≫ X = | − X | ;
L09: eqTransitivity ⊳ L03 ⊳ L08 ≫ |X | = | − X |  □

[ZFsub lemma SignNumerical: ΠX: |X | = | − X |]

ZFsub proof of SignNumerical:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;
L03: Premise ≫  X < 0  ;
L04: NegativeNegated ⊳ L03 ≫  0 < −X  ;
L05: SignNumerical(+) ⊳ L04 ≫  | − X | = | − −X |  ;
L06: DoubleMinus ≫  − − X = X  ;
L07: SameNumerical ⊳ L06 ≫  | − −X | = |X |  ;
L08: eqTransitivity ⊳ L05 ⊳ L07 ≫ | − X | = |X |  ;
L09: eqSymmetry ⊳ L08 ≫  |X | = | − X |  ;
L10: Block ≫  End  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  X  ;
L03: Premise ≫  X = 0  ;
L04: EqNegated ⊳ L03 ≫  −X = −0  ;
L05: −0 = 0 ≫  −0 = 0  ;
L06: eqSymmetry ⊳ L03 ≫  0 = X  ;

L07: eqTransitivity4 ⊳ L04 ⊳ L05 ⊳

L06 ≫ −X = X ;

L08: eqSymmetry ⊳ L07 ≫  X = −X  ;
L13: SameNumerical ⊳ L08 ≫  |X | = | − X |  ;
L14: Block ≫  End  ;
L15: Block ≫  Begin  ;
L16: Arbitrary ≫  X  ;
L03: Premise ≫  0 < X  ;
L17: SignNumerical(+) ⊳ L03 ≫  |X | = | − X |  ;
L18: Block ≫  End  ;
L19: Arbitrary ≫  X  ;
L20: Ded ⊳ L10 ≫  X < 0 ⇒ |X | = | − X |  ;
L21: Ded ⊳ L14 ≫  X = 0 ⇒ |X | = | − X |  ;
L22: Ded ⊳ L18 ≫  0 < X ⇒ |X | = | − X |  ;
L23: LessTotality ≫  X < 0 ˙∨ X = 0 ˙∨ 0 < X  ;

L24: From3Disjuncts ⊳ L23 ⊳ L20 ⊳

L21 ⊳ L22 ≫ |X | = | − X | □

[ZFsub lemma NumericalDifference: ΠX , Y: |X − Y| = |Y − X |] ZFsub proof of NumericalDifference:

L01: Arbitrary ≫  X , Y  ;
L02: SignNumerical ≫  |X − Y| = | − (X − Y)|  ;
L03: MinusNegated ≫  −(X − Y) = Y − X  ;
L04: SameNumerical ⊳ L03 ≫  | − (X − Y)| = |Y − X |  ;
L05: eqTransitivity ⊳ L02 ⊳ L04 ≫ |X − Y| = |Y − X |  □

[ZFsub lemma SplitNumericalSumHelper: ΠX , Y: | − X − Y| <= | − X | + | − Y| ⊢ |X + Y| <= |X | + |Y|]

ZFsub proof of SplitNumericalSumHelper:

L01: Arbitrary ≫ X , Y ;
L02: Premise ≫  | − X − Y| <= | − X | + | − Y| ;
L03: SignNumerical ≫  |X | = | − X |  ;
L04: SignNumerical ≫  |Y| = | − Y|  ;
L05: AddEquations ⊳ L03 ⊳ L04 ≫ |X | + |Y| = | − X | + | − Y|  ;
L06: eqSymmetry ⊳ L05 ≫  | − X | + | − Y| = |X | + |Y|  ;
L07: −x − y = −(x + y) ≫  −X − Y = −(X + Y)  ;
L08: SameNumerical ⊳ L07 ≫  | − X − Y| = | − (X + Y)|  ;
L09: SignNumerical ≫  |X + Y| = | − (X + Y)|  ;
L10: eqSymmetry ⊳ L09 ≫  | − (X + Y)| = |X + Y|  ;
L11: eqTransitivity ⊳ L08 ⊳ L10 ≫ | − X − Y| = |X + Y|  ;
L12: subLeqRight ⊳ L06 ⊳ L02 ≫  | − X − Y| <= |X | + |Y|  ;
L13: subLeqLeft ⊳ L11 ⊳ L12 ≫  |X + Y| <= |X | + |Y|  □

[ZFsub lemma splitNumericalSum(++): ΠX , Y: 0 <= X ⊢ 0 <= Y ⊢ |X + Y| <= |X | + |Y|]

ZFsub proof of splitNumericalSum(++):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  0 <= X  ;
L03: Premise ≫  0 <= Y  ;

L04: AddEquations(Leq) ⊳ L02 ⊳

L03 ≫ 0 + 0 <= X + Y ;

L05: plus0 ≫  0 + 0 = 0  ;
L06: subLeqLeft ⊳ L05 ⊳ L04 ≫  0 <= X + Y  ;
L07: NonnegativeNumerical⊳L06 ≫ |X + Y| = X + Y  ;
L08: NonnegativeNumerical⊳L02 ≫ |X | = X  ;
L09: NonnegativeNumerical⊳L03 ≫ |Y| = Y  ;
L10: AddEquations ⊳ L08 ⊳ L09 ≫ |X | + |Y| = X + Y  ;
L11: eqSymmetry ⊳ L10 ≫ X + Y = |X | + |Y| ;
L12: eqTransitivity ⊳ L07 ⊳ L11 ≫ |X + Y| = |X | + |Y|  ;
L13: eqLeq ⊳ L12 ≫ |X + Y| <= |X | + |Y| □

[ZFsub lemma splitNumericalSum(−−): ΠX , Y: X <= 0 ⊢ Y <= 0 ⊢ |X + Y| <= |X | + |Y|]

ZFsub proof of splitNumericalSum(−−):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= 0  ;
L03: Premise ≫  Y <= 0  ;
L04: NonpositiveNegated ⊳ L02 ≫ 0 <= −X  ;
L05: NonpositiveNegated ⊳ L03 ≫ 0 <= −Y  ;

L06: splitNumericalSum(++) ⊳

L04 ⊳ L05 ≫ | − X − Y| <= | − X | + | − Y| ;

L07: SplitNumericalSumHelper ⊳

L06 ≫ |X + Y| <= |X | + |Y| □

[ZFsub lemma splitNumericalSum(+ − small): ΠX , Y: 0 <= X ⊢ Y <= 0 ⊢ |Y| <= |X | ⊢ |X + Y| <= |X |]

ZFsub proof of splitNumericalSum(+ − small):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  0 <= X  ;
L03: Premise ≫  Y <= 0  ;
L04: Premise ≫  |Y| <= |X |  ;
L05: LeqAdditionLeft ⊳ L03 ≫  X + Y <= X + 0  ;
L06: plus0 ≫  X + 0 = X  ;
L07: subLeqRight ⊳ L06 ⊳ L05 ≫  X + Y <= X  ;

L08: PositiveToRight(Leq)(1term) ⊳

L04 ≫ 0 <= |X | − |Y| ;

L09: lemma nonpositiveNumerical ⊳

L03 ≫ |Y| = −Y ;

L10: EqNegated ⊳ L09 ≫  −|Y| = − − Y  ;
L11: DoubleMinus ≫  − − Y = Y  ;
L12: eqTransitivity ⊳ L10 ⊳ L11 ≫ −|Y| = Y  ;
L13: NonnegativeNumerical⊳L02 ≫ |X | = X  ;
L14: AddEquations ⊳ L13 ⊳ L12 ≫ |X | − |Y| = X + Y  ;
L15: subLeqRight ⊳ L14 ⊳ L08 ≫  0 <= X + Y  ;
L16: NonnegativeNumerical⊳L15 ≫ |X + Y| = X + Y  ;
L17: eqSymmetry ⊳ L16 ≫  X + Y = |X + Y|  ;
L18: eqSymmetry ⊳ L13 ≫  X = |X |  ;
L19: subLeqLeft ⊳ L17 ⊳ L07 ≫  |X + Y| <= X  ;
L20: subLeqRight ⊳ L18 ⊳ L19 ≫  |X + Y| <= |X |  □

[ZFsub lemma splitNumericalSum(+ − big): ΠX , Y: 0 <= X ⊢ Y <= 0 ⊢ |X | < |Y| ⊢ |X + Y| <= |Y|]

ZFsub proof of splitNumericalSum(+ − big):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  0 <= X  ;
L03: Premise ≫  Y <= 0  ;
L04: Premise ≫  |X | < |Y|  ;
L05: NonnegativeNegated ⊳ L02 ≫ −X <= 0  ;
L06: NonpositiveNegated ⊳ L03 ≫ 0 <= −Y  ;
L07: SignNumerical ≫  |X | = | − X |  ;
L08: SubLessLeft ⊳ L07 ⊳ L04 ≫  | − X | < |Y|  ;
L09: SignNumerical ≫  |Y| = | − Y|  ;
L10: SubLessRight ⊳ L09 ⊳ L08 ≫ | − X | < | − Y|  ;
L11: LessLeq ⊳ L10 ≫ | − X | <= | − Y| ;

L12: splitNumericalSum(+ − small) ⊳ L06 ⊳ L05 ⊳ L11 ≫

| − Y − X | <= | − Y| ;

L13: SignNumerical ≫  |X + Y| = | − (X + Y)|  ;

L14: −x − y = −(x + y) ≫  −X − Y = −(X + Y)  ;
L15: plusCommutativity ≫  −X − Y = −Y − X  ;
L16: Equality ⊳ L14 ⊳ L15 ≫  −(X + Y) = −Y − X  ;
L17: SameNumerical ⊳ L16 ≫  | − (X + Y)| = | − Y − X |  ;
L18: eqTransitivity ⊳ L13 ⊳ L17 ≫ |X + Y| = | − Y − X |  ;
L19: eqSymmetry ⊳ L18 ≫  | − Y − X | = |X + Y|  ;
L20: eqSymmetry ⊳ L09 ≫  | − Y| = |Y|  ;
L21: subLeqLeft ⊳ L19 ⊳ L12 ≫  |X + Y| <= | − Y|  ;
L22: subLeqRight ⊳ L20 ⊳ L21 ≫  |X + Y| <= |Y|  □

[ZFsub lemma splitNumericalSum(+−): ΠX , Y: 0 <= X ⊢ Y <= 0 ⊢ |X + Y| <= |X | + |Y|]

ZFsub proof of splitNumericalSum(+−):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  |Y| <= |X |  ;
L04: Premise ≫  0 <= X  ;
L05: Premise ≫  Y <= 0  ;

L06: splitNumericalSum(+ − small) ⊳ L04 ⊳ L05 ⊳ L03 ≫

|X + Y| <= |X | ;
L07: 0 <= |x| ≫  0 <= |Y|  ;
L08: LeqAdditionLeft ⊳ L07 ≫  |X | + 0 <= |X | + |Y|  ;
L09: plus0 ≫  |X | + 0 = |X |  ;
L10: subLeqLeft ⊳ L09 ⊳ L08 ≫  |X | <= |X | + |Y|  ;
L11: leqTransitivity ⊳ L06 ⊳ L10 ≫ |X + Y| <= |X | + |Y|  ;
L12: Block ≫  End  ;
L13: Block ≫  Begin  ;
L14: Arbitrary ≫  X , Y  ;
L15: Premise ≫  ˙¬ |Y| <= |X |  ;
L16: Premise ≫  0 <= X  ;
L17: Premise ≫  Y <= 0  ;
L18: ToLess ⊳ L15 ≫  |X | < |Y|  ;

L19: splitNumericalSum(+ − big) ⊳

L16 ⊳ L17 ⊳ L18 ≫ |X + Y| <= |Y| ;

L20: 0 <= |x| ≫  0 <= |X |  ;
L21: leqAddition ⊳ L20 ≫  0 + |Y| <= |X | + |Y|  ;
L22: plus0Left ≫  0 + |Y| = |Y|  ;
L23: subLeqLeft ⊳ L22 ⊳ L21 ≫  |Y| <= |X | + |Y|  ;
L24: leqTransitivity ⊳ L19 ⊳ L23 ≫ |X + Y| <= |X | + |Y|  ;
L25: Block ≫  End  ;
L26: Arbitrary ≫  X , Y  ;
L27: Ded ⊳ L12 ≫  {|Y| <= |X | ⇒ 0 <= X ⇒ \atop Y <= 0 ⇒ |X +Y| <= |X |+|Y| ;}
L28: Ded ⊳ L25 ≫  {˙¬ |Y| <= |X | ⇒ 0 <= X ⇒ \atop Y <= 0 ⇒ |X +Y| <= |X |+|Y| ;}
L29: Premise ≫  0 <= X  ;
L30: Premise ≫  Y <= 0  ;

L31: FromNegations ⊳ L27 ⊳ L28 ≫ {0 <= X ⇒ Y <= 0 ⇒ |X + \atop Y| <= |X | + |Y|  ;}
L32: MP2 ⊳ L31 ⊳ L29 ⊳ L30 ≫  |X + Y| <= |X | + |Y|  □

[ZFsub lemma splitNumericalSum(−+): ΠX , Y: X <= 0 ⊢ 0 <= Y ⊢ |X + Y| <= |X | + |Y|]

ZFsub proof of splitNumericalSum(−+):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= 0  ;
L03: Premise ≫  0 <= Y  ;
L04: NonpositiveNegated ⊳ L02 ≫ 0 <= −X  ;
L05: NonnegativeNegated ⊳ L03 ≫ −Y <= 0  ;

L06: splitNumericalSum(+−) ⊳

L04 ⊳ L05 ≫ | − X − Y| <= | − X | + | − Y| ;

L07: SplitNumericalSumHelper ⊳

L06 ≫ |X + Y| <= |X | + |Y| □

[ZFsub lemma splitNumericalSum: ΠX , Y: |X + Y| <= |X | + |Y|] ZFsub proof of splitNumericalSum:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  0 <= X  ;
L04: Premise ≫  0 <= Y  ;

L05: splitNumericalSum(++) ⊳

L03 ⊳ L04 ≫ |X + Y| <= |X | + |Y| ;

L06: Block ≫  End  ;
L07: Block ≫  Begin  ;
L08: Arbitrary ≫  X , Y  ;
L09: Premise ≫  0 <= X  ;
L10: Premise ≫  Y <= 0  ;

L11: splitNumericalSum(+−) ⊳

L09 ⊳ L10 ≫ |X + Y| <= |X | + |Y| ;

L12: Block ≫  End  ;
L13: Block ≫  Begin  ;
L14: Arbitrary ≫  X , Y  ;
L15: Premise ≫  X <= 0  ;
L16: Premise ≫  0 <= Y  ;

L17: splitNumericalSum(−+) ⊳

L15 ⊳ L16 ≫ |X + Y| <= |X | + |Y| ;

L18: Block ≫  End  ;
L19: Block ≫  Begin  ;
L20: Arbitrary ≫  X , Y  ;
L21: Premise ≫  X <= 0  ;
L22: Premise ≫  Y <= 0  ;

L23: splitNumericalSum(−−) ⊳

L21 ⊳ L22 ≫ |X + Y| <= |X | + |Y| ;

L24: Block ≫  End  ;
L25: Arbitrary ≫  X , Y  ;