Natural deduction certificates

Every theorem Grace17 accepts comes with a proof the kernel has checked: a derivation in natural deduction for first-order logic with equality, from the ZF(C/G) axioms and the theorems already admitted. Tactics, proof search, ring, and AI agents only ever produce such derivations, and the kernel admits a theorem by checking its derivation from scratch. The Workbench shows the derivation of any theorem under Kernel proof, and the ones on this page are rendered from the same checked certificates.

Two pictures of one derivation#

A natural-deduction derivation is a tree of inferences. In Gentzen's presentation the premises of a rule stand above a bar and its conclusion below, assumptions are leaves, and a rule such as →I or ∀I discharges the assumptions it closes over, which the tree shows in brackets. Fitch's presentation writes the same derivation as a numbered list: every line cites earlier lines, an assumption opens a subproof marked by a vertical rail, and the rule that discharges it cites the whole span.

The kernel stores a derivation as a directed graph of judgments Γ ⊢ φ in which a shared subproof appears once. The Fitch rendering lists each judgment once, premises before conclusions; the Gentzen rendering unfolds the graph into a tree, so a shared subproof is drawn wherever it is used. Select a Fitch line to see its inference as a rule with premises, conclusion, any freshness side condition, and the exact kernel arguments.

The first proof of the introduction is three lines of Grace17 and fourteen kernel lines:

Introduction.subset_step · 14 kernel lines · A subset fact unfolds to a universal implication, which is instantiated and applied.
Gentzen style
[A ⊆ B]
[x ∈ A]
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Bdef
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E
A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E
A ⊆ B → ∀ x ∈ A, x ∈ B↔E₁
[A ⊆ B]
∀ x ∈ A, x ∈ B→E
x ∈ A → x ∈ B∀E
[x ∈ A]
x ∈ B→E
x ∈ A → x ∈ B→I
A ⊆ B → x ∈ A → x ∈ B→I
∀ x, A ⊆ B → x ∈ A → x ∈ B∀I
∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B∀I
∀ A, ∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B∀I
Fitch style
1∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ BdefDefinition equation
def
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B
declaration
Grace.Cumulus.Set.Basic.Set.Subset
equation
equation
2∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E 1Universal specialization
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Buniversal statement · line 1
∀E
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B
term
A
3A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E 1–2Universal specialization
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Buniversal statement · line 1–2
∀E
A ⊆ B ↔ ∀ x ∈ A, x ∈ B
term
B
4A ⊆ B → ∀ x ∈ A, x ∈ B↔E₁ 1–3Forward equivalence elimination
A ⊆ B ↔ ∀ x ∈ A, x ∈ Bequivalence · line 1–3
↔E₁
A ⊆ B → ∀ x ∈ A, x ∈ B
5A ⊆ BhypHypothesis
hyp
A ⊆ B
6∀ x ∈ A, x ∈ B→E 1–4, 1–5Modus ponens
A ⊆ B → ∀ x ∈ A, x ∈ Bimplication · line 1–4
A ⊆ Bantecedent · line 1–5
→E
∀ x ∈ A, x ∈ B
7x ∈ A → x ∈ B∀E 1–6Universal specialization
∀ x ∈ A, x ∈ Buniversal statement · line 1–6
∀E
x ∈ A → x ∈ B
term
x
8x ∈ AhypHypothesis
hyp
x ∈ A
9x ∈ B→E 1–7, 1–8Modus ponens
x ∈ A → x ∈ Bimplication · line 1–7
x ∈ Aantecedent · line 1–8
→E
x ∈ B
10x ∈ A → x ∈ B→I 1–9Implication introduction
[x ∈ A]
x ∈ Bconclusion under assumption · line 1–9
→I
x ∈ A → x ∈ B
discharged assumption
x ∈ A
11A ⊆ B → x ∈ A → x ∈ B→I 10Implication introduction
[A ⊆ B]
x ∈ A → x ∈ Bconclusion under assumption · line 10
→I
A ⊆ B → x ∈ A → x ∈ B
discharged assumption
A ⊆ B
12∀ x, A ⊆ B → x ∈ A → x ∈ B∀I 11Universal introduction
A ⊆ B → x ∈ A → x ∈ Bbody for fresh variable · line 11
∀I
∀ x, A ⊆ B → x ∈ A → x ∈ B
bound variable
x
13∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B∀I 12Universal introduction
∀ x, A ⊆ B → x ∈ A → x ∈ Bbody for fresh variable · line 12
∀I
∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B
bound variable
B
14∀ A, ∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B∀I 13Universal introduction
∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ Bbody for fresh variable · line 13
∀I
∀ A, ∀ B, ∀ x, A ⊆ B → x ∈ A → x ∈ B
bound variable
A

A proof that reasons about union membership:

union.subset · 33 kernel lines
Gentzen style
[∀ A ∈ S, A ⊆ B]
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Bdef
∀ B, ⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B∀E
⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B∀E
(∀ x ∈ ⋃ S, x ∈ B) → ⋃ S ⊆ B↔E₂
[x ∈ ⋃ S]
[x ∈ ⋃ S]
∀ A, ∀ x, x ∈ ⋃ A ↔ ∃ y ∈ A, x ∈ yax
∀ x, x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y∀E
x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y∀E
x ∈ ⋃ S → ∃ y ∈ S, x ∈ y↔E₁
[x ∈ ⋃ S]
∃ y ∈ S, x ∈ y→E
x ∈ ⋃ S → ∃ y ∈ S, x ∈ y→I
[x ∈ ⋃ S]
∃ y ∈ S, x ∈ y→E
[A ∈ S ∧ x ∈ A]
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Bdef
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E
A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E
A ⊆ B → ∀ x ∈ A, x ∈ B↔E₁
[∀ A ∈ S, A ⊆ B]
A ∈ S → A ⊆ B∀E
[A ∈ S ∧ x ∈ A]
A ∈ S∧E₁
A ⊆ B→E
∀ x ∈ A, x ∈ B→E
x ∈ A → x ∈ B∀E
[A ∈ S ∧ x ∈ A]
x ∈ A∧E₂
x ∈ B→E
x ∈ B∃E
x ∈ ⋃ S → x ∈ B→I
∀ x ∈ ⋃ S, x ∈ B∀I
⋃ S ⊆ B→E
(∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B→I
∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B∀I
∀ S, ∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B∀I
Fitch style
1∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ BdefDefinition equation
def
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B
declaration
Grace.Cumulus.Set.Basic.Set.Subset
equation
equation
2∀ B, ⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B∀E 1Universal specialization
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Buniversal statement · line 1
∀E
∀ B, ⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B
term
⋃ S
3⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B∀E 1–2Universal specialization
∀ B, ⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ Buniversal statement · line 1–2
∀E
⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ B
term
B
4(∀ x ∈ ⋃ S, x ∈ B) → ⋃ S ⊆ B↔E₂ 1–3Backward equivalence elimination
⋃ S ⊆ B ↔ ∀ x ∈ ⋃ S, x ∈ Bequivalence · line 1–3
↔E₂
(∀ x ∈ ⋃ S, x ∈ B) → ⋃ S ⊆ B
5∀ A, ∀ x, x ∈ ⋃ A ↔ ∃ y ∈ A, x ∈ yaxFoundation axiom
ax
∀ A, ∀ x, x ∈ ⋃ A ↔ ∃ y ∈ A, x ∈ y
declaration
set.union
6∀ x, x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y∀E 5Universal specialization
∀ A, ∀ x, x ∈ ⋃ A ↔ ∃ y ∈ A, x ∈ yuniversal statement · line 5
∀E
∀ x, x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y
term
S
7x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y∀E 5–6Universal specialization
∀ x, x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ yuniversal statement · line 5–6
∀E
x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ y
term
x
8x ∈ ⋃ S → ∃ y ∈ S, x ∈ y↔E₁ 5–7Forward equivalence elimination
x ∈ ⋃ S ↔ ∃ y ∈ S, x ∈ yequivalence · line 5–7
↔E₁
x ∈ ⋃ S → ∃ y ∈ S, x ∈ y
9x ∈ ⋃ ShypHypothesis
hyp
x ∈ ⋃ S
10∃ y ∈ S, x ∈ y→E 5–8, 5–9Modus ponens
x ∈ ⋃ S → ∃ y ∈ S, x ∈ yimplication · line 5–8
x ∈ ⋃ Santecedent · line 5–9
→E
∃ y ∈ S, x ∈ y
11x ∈ ⋃ S → ∃ y ∈ S, x ∈ y→I 5–10Implication introduction
[x ∈ ⋃ S]
∃ y ∈ S, x ∈ yconclusion under assumption · line 5–10
→I
x ∈ ⋃ S → ∃ y ∈ S, x ∈ y
discharged assumption
x ∈ ⋃ S
12x ∈ ⋃ ShypHypothesis
hyp
x ∈ ⋃ S
13∃ y ∈ S, x ∈ y→E 11, 11–12Modus ponens
x ∈ ⋃ S → ∃ y ∈ S, x ∈ yimplication · line 11
x ∈ ⋃ Santecedent · line 11–12
→E
∃ y ∈ S, x ∈ y
14∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ BdefDefinition equation
def
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B
declaration
Grace.Cumulus.Set.Basic.Set.Subset
equation
equation
15∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E 14Universal specialization
∀ A, ∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Buniversal statement · line 14
∀E
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ B
term
A
16A ⊆ B ↔ ∀ x ∈ A, x ∈ B∀E 14–15Universal specialization
∀ B, A ⊆ B ↔ ∀ x ∈ A, x ∈ Buniversal statement · line 14–15
∀E
A ⊆ B ↔ ∀ x ∈ A, x ∈ B
term
B
17A ⊆ B → ∀ x ∈ A, x ∈ B↔E₁ 14–16Forward equivalence elimination
A ⊆ B ↔ ∀ x ∈ A, x ∈ Bequivalence · line 14–16
↔E₁
A ⊆ B → ∀ x ∈ A, x ∈ B
18∀ A ∈ S, A ⊆ BhypHypothesis
hyp
∀ A ∈ S, A ⊆ B
19A ∈ S → A ⊆ B∀E 14–18Universal specialization
∀ A ∈ S, A ⊆ Buniversal statement · line 14–18
∀E
A ∈ S → A ⊆ B
term
A
20A ∈ S ∧ x ∈ AhypHypothesis
hyp
A ∈ S ∧ x ∈ A
21A ∈ S∧E₁ 14–20Left conjunction elimination
A ∈ S ∧ x ∈ Aconjunction · line 14–20
∧E₁
A ∈ S
22A ⊆ B→E 14–19, 14–21Modus ponens
A ∈ S → A ⊆ Bimplication · line 14–19
A ∈ Santecedent · line 14–21
→E
A ⊆ B
23∀ x ∈ A, x ∈ B→E 14–17, 14–22Modus ponens
A ⊆ B → ∀ x ∈ A, x ∈ Bimplication · line 14–17
A ⊆ Bantecedent · line 14–22
→E
∀ x ∈ A, x ∈ B
24x ∈ A → x ∈ B∀E 14–23Universal specialization
∀ x ∈ A, x ∈ Buniversal statement · line 14–23
∀E
x ∈ A → x ∈ B
term
x
25x ∈ A∧E₂ 14–20Right conjunction elimination
A ∈ S ∧ x ∈ Aconjunction · line 14–20
∧E₂
x ∈ A
26x ∈ B→E 14–24, 14–25Modus ponens
x ∈ A → x ∈ Bimplication · line 14–24
x ∈ Aantecedent · line 14–25
→E
x ∈ B
27x ∈ B∃E 11–13, 14–26Existential elimination
∃ y ∈ S, x ∈ yexistential · line 11–13
[A ∈ S ∧ x ∈ A]
x ∈ Bbody for fresh witness · line 14–26
∃E
x ∈ B
fresh witness
A
28x ∈ ⋃ S → x ∈ B→I 27Implication introduction
[x ∈ ⋃ S]
x ∈ Bconclusion under assumption · line 27
→I
x ∈ ⋃ S → x ∈ B
discharged assumption
x ∈ ⋃ S
29∀ x ∈ ⋃ S, x ∈ B∀I 28Universal introduction
x ∈ ⋃ S → x ∈ Bbody for fresh variable · line 28
∀I
∀ x ∈ ⋃ S, x ∈ B
bound variable
x
30⋃ S ⊆ B→E 1–4, 28–29Modus ponens
(∀ x ∈ ⋃ S, x ∈ B) → ⋃ S ⊆ Bimplication · line 1–4
∀ x ∈ ⋃ S, x ∈ Bantecedent · line 28–29
→E
⋃ S ⊆ B
31(∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B→I 28–30Implication introduction
[∀ A ∈ S, A ⊆ B]
⋃ S ⊆ Bconclusion under assumption · line 28–30
→I
(∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B
discharged assumption
∀ A ∈ S, A ⊆ B
32∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B∀I 31Universal introduction
(∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ Bbody for fresh variable · line 31
∀I
∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B
bound variable
B
33∀ S, ∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B∀I 32Universal introduction
∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ Bbody for fresh variable · line 32
∀I
∀ S, ∀ B, (∀ A ∈ S, A ⊆ B) → ⋃ S ⊆ B
bound variable
S

What automation leaves behind#

Automation is not trusted; it is checked. The integer identity below is closed by ring in one line of Grace17, and what ring hands to the kernel is a derivation of a few hundred steps, each one an ordinary inference. The list is folded; open any line.

Introduction.difference_of_squares · 348 kernel lines · Every step is one rule of logic or one ring axiom applied to earlier lines.
Fitch style
1∀ x y : ℤ, integerMul(x, y) = x * ythmChecked theorem
thm
∀ x y : ℤ, integerMul(x, y) = x * y
declaration
Grace.Cumulus.Int.Ring.integerMulValue.notation
2∀ y_1, x + y ∈ Integer → y_1 ∈ Integer → integerMul(x + y, y_1) = (x + y) * y_1∀E 1Universal specialization
∀ x y : ℤ, integerMul(x, y) = x * yuniversal statement · line 1
∀E
∀ y_1, x + y ∈ Integer → y_1 ∈ Integer → integerMul(x + y, y_1) = (x + y) * y_1
term
integerAddValue(x, y)
3x + y ∈ Integer → x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)∀E 1–2Universal specialization
∀ y_1, x + y ∈ Integer → y_1 ∈ Integer → integerMul(x + y, y_1) = (x + y) * y_1universal statement · line 1–2
∀E
x + y ∈ Integer → x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)
term
integerSubValue(x, y)
4∀ x y : ℤ, x + y : ℤthmChecked theorem
thm
∀ x y : ℤ, x + y : ℤ
declaration
Grace.Cumulus.Int.Arithmetic.integerAddValue.integer
5∀ y, x ∈ Integer → y ∈ Integer → x + y ∈ Integer∀E 1–4Universal specialization
∀ x y : ℤ, x + y : ℤuniversal statement · line 1–4
∀E
∀ y, x ∈ Integer → y ∈ Integer → x + y ∈ Integer
term
x
6x ∈ Integer → y ∈ Integer → x + y ∈ Integer∀E 1–5Universal specialization
∀ y, x ∈ Integer → y ∈ Integer → x + y ∈ Integeruniversal statement · line 1–5
∀E
x ∈ Integer → y ∈ Integer → x + y ∈ Integer
term
y
7x : ℤhypHypothesis
hyp
x : ℤ
8y ∈ Integer → x + y ∈ Integer→E 1–6, 1–7Modus ponens
x ∈ Integer → y ∈ Integer → x + y ∈ Integerimplication · line 1–6
x : ℤantecedent · line 1–7
→E
y ∈ Integer → x + y ∈ Integer
9y : ℤhypHypothesis
hyp
y : ℤ
10x + y : ℤ→E 1–8, 1–9Modus ponens
y ∈ Integer → x + y ∈ Integerimplication · line 1–8
y : ℤantecedent · line 1–9
→E
x + y : ℤ
11x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)→E 1–3, 1–10Modus ponens
x + y ∈ Integer → x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)implication · line 1–3
x + y : ℤantecedent · line 1–10
→E
x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)
12∀ x y : ℤ, x - y : ℤthmChecked theorem
thm
∀ x y : ℤ, x - y : ℤ
declaration
Grace.Cumulus.Int.Ring.integerSubValue.integer
13∀ y, x ∈ Integer → y ∈ Integer → x - y ∈ Integer∀E 1–12Universal specialization
∀ x y : ℤ, x - y : ℤuniversal statement · line 1–12
∀E
∀ y, x ∈ Integer → y ∈ Integer → x - y ∈ Integer
term
x
14x ∈ Integer → y ∈ Integer → x - y ∈ Integer∀E 1–13Universal specialization
∀ y, x ∈ Integer → y ∈ Integer → x - y ∈ Integeruniversal statement · line 1–13
∀E
x ∈ Integer → y ∈ Integer → x - y ∈ Integer
term
y
15y ∈ Integer → x - y ∈ Integer→E 1–14, 1–7Modus ponens
x ∈ Integer → y ∈ Integer → x - y ∈ Integerimplication · line 1–14
x : ℤantecedent · line 1–7
→E
y ∈ Integer → x - y ∈ Integer
16x - y : ℤ→E 1–15, 1–9Modus ponens
y ∈ Integer → x - y ∈ Integerimplication · line 1–15
y : ℤantecedent · line 1–9
→E
x - y : ℤ
17integerMul(x + y, x - y) = (x + y) * (x - y)→E 1–11, 1–16Modus ponens
x - y ∈ Integer → integerMul(x + y, x - y) = (x + y) * (x - y)implication · line 1–11
x - y : ℤantecedent · line 1–16
→E
integerMul(x + y, x - y) = (x + y) * (x - y)
18(x + y) * (x - y) = integerMul(x + y, x - y)=sym 1–17Equality symmetry
integerMul(x + y, x - y) = (x + y) * (x - y)equality · line 1–17
=sym
(x + y) * (x - y) = integerMul(x + y, x - y)
19integerMul = integerMul=IEquality reflexivity
=I
integerMul = integerMul
term
integerMul
20∀ x y : ℤ, integerAdd(x, y) = x + ythmChecked theorem
thm
∀ x y : ℤ, integerAdd(x, y) = x + y
declaration
Grace.Cumulus.Int.Ring.integerAddValue.notation
21∀ y, x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + y∀E 1–20Universal specialization
∀ x y : ℤ, integerAdd(x, y) = x + yuniversal statement · line 1–20
∀E
∀ y, x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + y
term
x
22x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + y∀E 1–21Universal specialization
∀ y, x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + yuniversal statement · line 1–21
∀E
x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + y
term
y
23y ∈ Integer → integerAdd(x, y) = x + y→E 1–22, 1–7Modus ponens
x ∈ Integer → y ∈ Integer → integerAdd(x, y) = x + yimplication · line 1–22
x : ℤantecedent · line 1–7
→E
y ∈ Integer → integerAdd(x, y) = x + y
24integerAdd(x, y) = x + y→E 1–23, 1–9Modus ponens
y ∈ Integer → integerAdd(x, y) = x + yimplication · line 1–23
y : ℤantecedent · line 1–9
→E
integerAdd(x, y) = x + y
25x + y = integerAdd(x, y)=sym 1–24Equality symmetry
integerAdd(x, y) = x + yequality · line 1–24
=sym
x + y = integerAdd(x, y)
26∀ x, ∀ y, x - y = integerAdd(x, integerNeg(y))defDefinition equation
def
∀ x, ∀ y, x - y = integerAdd(x, integerNeg(y))
declaration
Grace.Cumulus.Int.Ring.integerSubValue
equation
equation
27∀ y, x - y = integerAdd(x, integerNeg(y))∀E 1–26Universal specialization
∀ x, ∀ y, x - y = integerAdd(x, integerNeg(y))universal statement · line 1–26
∀E
∀ y, x - y = integerAdd(x, integerNeg(y))
term
x
28x - y = integerAdd(x, integerNeg(y))∀E 1–27Universal specialization
∀ y, x - y = integerAdd(x, integerNeg(y))universal statement · line 1–27
∀E
x - y = integerAdd(x, integerNeg(y))
term
y
29integerMul(x + y, x - y) = integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y)))congr 1–19, 1–25, 1–28Function congruence
integerMul = integerMulargument equality 1 · line 1–19
x + y = integerAdd(x, y)argument equality 2 · line 1–25
x - y = integerAdd(x, integerNeg(y))argument equality 3 · line 1–28
congr
integerMul(x + y, x - y) = integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
30∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(add(x, y), z) = add(mul(x, z), mul(y, z))thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(add(x, y), z) = add(mul(x, z), mul(y, z))
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.add_mul
31∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(add(x, y), z) = add(mul(x, z), mul(y, z))∀E 1–30Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(add(x, y), z) = add(mul(x, z), mul(y, z))universal statement · line 1–30
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(add(x, y), z) = add(mul(x, z), mul(y, z))
term
ℤ
32∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))∀E 1–31Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(add(x, y), z) = add(mul(x, z), mul(y, z))universal statement · line 1–31
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))
term
integerAdd
33∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))∀E 1–32Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))universal statement · line 1–32
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))
term
integerZero
34∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))∀E 1–33Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))universal statement · line 1–33
∀E
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))
term
integerNeg
35∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))∀E 1–34Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(integerAdd(x, y), z) = integerAdd(mul(x, z), mul(y, z))universal statement · line 1–34
∀E
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))
term
integerMul
36∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))∀E 1–35Universal specialization
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))universal statement · line 1–35
∀E
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))
term
integerOne
37∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, y), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(y, z))∀E 1–36Universal specialization
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(x, y), z) = integerAdd(integerMul(x, z), integerMul(y, z))universal statement · line 1–36
∀E
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, y), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(y, z))
term
__ring_arg0
38∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(__ring_arg1, z))∀E 1–37Universal specialization
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, y), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(y, z))universal statement · line 1–37
∀E
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(__ring_arg1, z))
term
__ring_arg1
39IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))∀E 1–38Universal specialization
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(integerMul(__ring_arg0, z), integerMul(__ring_arg1, z))universal statement · line 1–38
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
term
__ring_arg2
40IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)thmChecked theorem
thm
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)
declaration
Grace.Cumulus.Int.Ring.integers.comm_ring
41__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))→E 1–39, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))implication · line 1–39
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
42∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))∀I 1–41Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))body for fresh variable · line 1–41
∀I
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
bound variable
__ring_arg2
43∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))∀I 1–42Universal introduction
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))body for fresh variable · line 1–42
∀I
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
bound variable
__ring_arg1
44∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))∀I 1–43Universal introduction
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))body for fresh variable · line 1–43
∀I
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
bound variable
__ring_arg0
45∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))∀E 1–44Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(integerMul(__ring_arg0, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))universal statement · line 1–44
∀E
∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))
term
x
46∀ __ring_arg2, x ∈ ℤ → y ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, y), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(y, __ring_arg2))∀E 1–45Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(__ring_arg1, __ring_arg2))universal statement · line 1–45
∀E
∀ __ring_arg2, x ∈ ℤ → y ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, y), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(y, __ring_arg2))
term
y
47x ∈ ℤ → y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))∀E 1–46Universal specialization
∀ __ring_arg2, x ∈ ℤ → y ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(integerAdd(x, y), __ring_arg2) = integerAdd(integerMul(x, __ring_arg2), integerMul(y, __ring_arg2))universal statement · line 1–46
∀E
x ∈ ℤ → y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))
term
integerAdd(x, integerNeg(y))
48∀ z, z ∈ Integer ↔ z ∈ ℤdefDefinition equation
def
∀ z, z ∈ Integer ↔ z ∈ ℤ
declaration
Grace.Cumulus.Int.Defs.Integer
equation
equation
49x ∈ Integer ↔ x ∈ ℤ∀E 1–48Universal specialization
∀ z, z ∈ Integer ↔ z ∈ ℤuniversal statement · line 1–48
∀E
x ∈ Integer ↔ x ∈ ℤ
term
x
50x ∈ Integer → x ∈ ℤ↔E₁ 1–49Forward equivalence elimination
x ∈ Integer ↔ x ∈ ℤequivalence · line 1–49
↔E₁
x ∈ Integer → x ∈ ℤ
51x ∈ ℤ→E 1–50, 1–7Modus ponens
x ∈ Integer → x ∈ ℤimplication · line 1–50
x : ℤantecedent · line 1–7
→E
x ∈ ℤ
52y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))→E 1–47, 1–51Modus ponens
x ∈ ℤ → y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))implication · line 1–47
x ∈ ℤantecedent · line 1–51
→E
y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))
53y ∈ Integer ↔ y ∈ ℤ∀E 1–48Universal specialization
∀ z, z ∈ Integer ↔ z ∈ ℤuniversal statement · line 1–48
∀E
y ∈ Integer ↔ y ∈ ℤ
term
y
54y ∈ Integer → y ∈ ℤ↔E₁ 1–53Forward equivalence elimination
y ∈ Integer ↔ y ∈ ℤequivalence · line 1–53
↔E₁
y ∈ Integer → y ∈ ℤ
55y ∈ ℤ→E 1–54, 1–9Modus ponens
y ∈ Integer → y ∈ ℤimplication · line 1–54
y : ℤantecedent · line 1–9
→E
y ∈ ℤ
56integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))→E 1–52, 1–55Modus ponens
y ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))implication · line 1–52
y ∈ ℤantecedent · line 1–55
→E
integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))
57∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) ∈ AthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) ∈ A
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.add_closed
58∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) ∈ ℤ∀E 1–57Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) ∈ Auniversal statement · line 1–57
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) ∈ ℤ
term
ℤ
59∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–58Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) ∈ ℤuniversal statement · line 1–58
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
integerAdd
60∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–59Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–59
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
integerZero
61∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–60Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–60
∀E
∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
integerNeg
62∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–61Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–61
∀E
∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
integerMul
63∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–62Universal specialization
∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–62
∀E
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
integerOne
64∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ∀E 1–63Universal specialization
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–63
∀E
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤ
term
x
65IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ∀E 1–64Universal specialization
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–64
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ
term
integerNeg(y)
66∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(A, add, zero, neg, mul, one) → IsRing(A, add, zero, neg, mul, one)thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(A, add, zero, neg, mul, one) → IsRing(A, add, zero, neg, mul, one)
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.ring
67∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, add, zero, neg, mul, one) → IsRing(ℤ, add, zero, neg, mul, one)∀E 1–66Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(A, add, zero, neg, mul, one) → IsRing(A, add, zero, neg, mul, one)universal statement · line 1–66
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, add, zero, neg, mul, one) → IsRing(ℤ, add, zero, neg, mul, one)
term
ℤ
68∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → IsRing(ℤ, integerAdd, zero, neg, mul, one)∀E 1–67Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, add, zero, neg, mul, one) → IsRing(ℤ, add, zero, neg, mul, one)universal statement · line 1–67
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → IsRing(ℤ, integerAdd, zero, neg, mul, one)
term
integerAdd
69∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → IsRing(ℤ, integerAdd, 0, neg, mul, one)∀E 1–68Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → IsRing(ℤ, integerAdd, zero, neg, mul, one)universal statement · line 1–68
∀E
∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → IsRing(ℤ, integerAdd, 0, neg, mul, one)
term
integerZero
70∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, mul, one)∀E 1–69Universal specialization
∀ neg, ∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → IsRing(ℤ, integerAdd, 0, neg, mul, one)universal statement · line 1–69
∀E
∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, mul, one)
term
integerNeg
71∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one)∀E 1–70Universal specialization
∀ mul, ∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, mul, one)universal statement · line 1–70
∀E
∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one)
term
integerMul
72IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)∀E 1–71Universal specialization
∀ one, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one)universal statement · line 1–71
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)
term
integerOne
73IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)→E 1–72, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)implication · line 1–72
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)
74x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ→E 1–65, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤimplication · line 1–65
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ
75integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ→E 1–74, 1–51Modus ponens
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤimplication · line 1–74
x ∈ ℤantecedent · line 1–51
→E
integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤ
76∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → neg(x) ∈ AthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → neg(x) ∈ A
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.neg_closed
77∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ∀E 1–76Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → neg(x) ∈ Auniversal statement · line 1–76
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ
term
ℤ
78∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ∀E 1–77Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤuniversal statement · line 1–77
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ
term
integerAdd
79∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ∀E 1–78Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤuniversal statement · line 1–78
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤ
term
integerZero
80∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤ∀E 1–79Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → neg(x) ∈ ℤuniversal statement · line 1–79
∀E
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤ
term
integerNeg
81∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤ∀E 1–80Universal specialization
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤuniversal statement · line 1–80
∀E
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤ
term
integerMul
82∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(x) ∈ ℤ∀E 1–81Universal specialization
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerNeg(x) ∈ ℤuniversal statement · line 1–81
∀E
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(x) ∈ ℤ
term
integerOne
83IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → integerNeg(y) ∈ ℤ∀E 1–82Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(x) ∈ ℤuniversal statement · line 1–82
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → integerNeg(y) ∈ ℤ
term
y
84y ∈ ℤ → integerNeg(y) ∈ ℤ→E 1–83, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → integerNeg(y) ∈ ℤimplication · line 1–83
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
y ∈ ℤ → integerNeg(y) ∈ ℤ
85integerNeg(y) ∈ ℤ→E 1–84, 1–55Modus ponens
y ∈ ℤ → integerNeg(y) ∈ ℤimplication · line 1–84
y ∈ ℤantecedent · line 1–55
→E
integerNeg(y) ∈ ℤ
86integerAdd(x, integerNeg(y)) ∈ ℤ→E 1–75, 1–85Modus ponens
integerNeg(y) ∈ ℤ → integerAdd(x, integerNeg(y)) ∈ ℤimplication · line 1–75
integerNeg(y) ∈ ℤantecedent · line 1–85
→E
integerAdd(x, integerNeg(y)) ∈ ℤ
87integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))→E 1–56, 1–86Modus ponens
integerAdd(x, integerNeg(y)) ∈ ℤ → integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))implication · line 1–56
integerAdd(x, integerNeg(y)) ∈ ℤantecedent · line 1–86
→E
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))
88integerAdd = integerAdd=IEquality reflexivity
=I
integerAdd = integerAdd
term
integerAdd
89∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.mul_add
90∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))∀E 1–89Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))universal statement · line 1–89
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))
term
ℤ
91∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))∀E 1–90Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, add(y, z)) = add(mul(x, y), mul(x, z))universal statement · line 1–90
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))
term
integerAdd
92∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))∀E 1–91Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))universal statement · line 1–91
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))
term
integerZero
93∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))∀E 1–92Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))universal statement · line 1–92
∀E
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))
term
integerNeg
94∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))∀E 1–93Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → mul(x, integerAdd(y, z)) = integerAdd(mul(x, y), mul(x, z))universal statement · line 1–93
∀E
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))
term
integerMul
95∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))∀E 1–94Universal specialization
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))universal statement · line 1–94
∀E
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))
term
integerOne
96∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(y, z)) = integerAdd(integerMul(__ring_arg0, y), integerMul(__ring_arg0, z))∀E 1–95Universal specialization
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(x, integerAdd(y, z)) = integerAdd(integerMul(x, y), integerMul(x, z))universal statement · line 1–95
∀E
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(y, z)) = integerAdd(integerMul(__ring_arg0, y), integerMul(__ring_arg0, z))
term
__ring_arg0
97∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, z))∀E 1–96Universal specialization
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(y, z)) = integerAdd(integerMul(__ring_arg0, y), integerMul(__ring_arg0, z))universal statement · line 1–96
∀E
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, z))
term
__ring_arg1
98IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))∀E 1–97Universal specialization
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, z))universal statement · line 1–97
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))
term
__ring_arg2
99__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))→E 1–98, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))implication · line 1–98
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))
100∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))∀I 1–99Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))body for fresh variable · line 1–99
∀I
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))
bound variable
__ring_arg2
101∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))∀I 1–100Universal introduction
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))body for fresh variable · line 1–100
∀I
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))
bound variable
__ring_arg1
102∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))∀I 1–101Universal introduction
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))body for fresh variable · line 1–101
∀I
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))
bound variable
__ring_arg0
103∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(x, __ring_arg1), integerMul(x, __ring_arg2))∀E 1–102Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))universal statement · line 1–102
∀E
∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(x, __ring_arg1), integerMul(x, __ring_arg2))
term
x
104∀ __ring_arg2, x ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(x, x), integerMul(x, __ring_arg2))∀E 1–103Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, x ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(x, __ring_arg1), integerMul(x, __ring_arg2))universal statement · line 1–103
∀E
∀ __ring_arg2, x ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(x, x), integerMul(x, __ring_arg2))
term
x
105x ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))∀E 1–104Universal specialization
∀ __ring_arg2, x ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(x, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(x, x), integerMul(x, __ring_arg2))universal statement · line 1–104
∀E
x ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))
term
integerNeg(y)
106x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))→E 1–105, 1–51Modus ponens
x ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))implication · line 1–105
x ∈ ℤantecedent · line 1–51
→E
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))
107integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))→E 1–106, 1–51Modus ponens
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))implication · line 1–106
x ∈ ℤantecedent · line 1–51
→E
integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))
108integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))→E 1–107, 1–85Modus ponens
integerNeg(y) ∈ ℤ → integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))implication · line 1–107
integerNeg(y) ∈ ℤantecedent · line 1–85
→E
integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))
109integerMul(x, x) = integerMul(x, x)=IEquality reflexivity
=I
integerMul(x, x) = integerMul(x, x)
term
integerMul(x, x)
110∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, neg(y)) = neg(mul(x, y))thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, neg(y)) = neg(mul(x, y))
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.mul_neg
111∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))∀E 1–110Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, neg(y)) = neg(mul(x, y))universal statement · line 1–110
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))
term
ℤ
112∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))∀E 1–111Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))universal statement · line 1–111
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))
term
integerAdd
113∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))∀E 1–112Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))universal statement · line 1–112
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))
term
integerZero
114∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, integerNeg(y)) = integerNeg(mul(x, y))∀E 1–113Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, neg(y)) = neg(mul(x, y))universal statement · line 1–113
∀E
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, integerNeg(y)) = integerNeg(mul(x, y))
term
integerNeg
115∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))∀E 1–114Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, integerNeg(y)) = integerNeg(mul(x, y))universal statement · line 1–114
∀E
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))
term
integerMul
116∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))∀E 1–115Universal specialization
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))universal statement · line 1–115
∀E
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))
term
integerOne
117∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, integerNeg(y)) = integerNeg(integerMul(__ring_arg0, y))∀E 1–116Universal specialization
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))universal statement · line 1–116
∀E
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, integerNeg(y)) = integerNeg(integerMul(__ring_arg0, y))
term
__ring_arg0
118IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))∀E 1–117Universal specialization
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, integerNeg(y)) = integerNeg(integerMul(__ring_arg0, y))universal statement · line 1–117
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))
term
__ring_arg1
119__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))→E 1–118, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))implication · line 1–118
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))
120∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))∀I 1–119Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))body for fresh variable · line 1–119
∀I
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))
bound variable
__ring_arg1
121∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))∀I 1–120Universal introduction
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))body for fresh variable · line 1–120
∀I
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))
bound variable
__ring_arg0
122∀ __ring_arg1, x ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(x, integerNeg(__ring_arg1)) = integerNeg(integerMul(x, __ring_arg1))∀E 1–121Universal specialization
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))universal statement · line 1–121
∀E
∀ __ring_arg1, x ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(x, integerNeg(__ring_arg1)) = integerNeg(integerMul(x, __ring_arg1))
term
x
123x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))∀E 1–122Universal specialization
∀ __ring_arg1, x ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(x, integerNeg(__ring_arg1)) = integerNeg(integerMul(x, __ring_arg1))universal statement · line 1–122
∀E
x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))
term
y
124y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))→E 1–123, 1–51Modus ponens
x ∈ ℤ → y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))implication · line 1–123
x ∈ ℤantecedent · line 1–51
→E
y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))
125integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))→E 1–124, 1–55Modus ponens
y ∈ ℤ → integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))implication · line 1–124
y ∈ ℤantecedent · line 1–55
→E
integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))
126integerAdd(integerMul(x, x), integerMul(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))congr 1–88, 1–109, 1–125Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerMul(x, x) = integerMul(x, x)argument equality 2 · line 1–109
integerMul(x, integerNeg(y)) = integerNeg(integerMul(x, y))argument equality 3 · line 1–125
congr
integerAdd(integerMul(x, x), integerMul(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
127integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))=trans 1–108, 1–126Equality transitivity
integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerMul(x, integerNeg(y)))left equality · line 1–108
integerAdd(integerMul(x, x), integerMul(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))right equality · line 1–126
=trans
integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))
128∀ __ring_arg1, ∀ __ring_arg2, y ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(y, __ring_arg1), integerMul(y, __ring_arg2))∀E 1–102Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerMul(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(__ring_arg0, __ring_arg1), integerMul(__ring_arg0, __ring_arg2))universal statement · line 1–102
∀E
∀ __ring_arg1, ∀ __ring_arg2, y ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(y, __ring_arg1), integerMul(y, __ring_arg2))
term
y
129∀ __ring_arg2, y ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(y, x), integerMul(y, __ring_arg2))∀E 1–128Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, y ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(integerMul(y, __ring_arg1), integerMul(y, __ring_arg2))universal statement · line 1–128
∀E
∀ __ring_arg2, y ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(y, x), integerMul(y, __ring_arg2))
term
x
130y ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))∀E 1–129Universal specialization
∀ __ring_arg2, y ∈ ℤ → x ∈ ℤ → __ring_arg2 ∈ ℤ → integerMul(y, integerAdd(x, __ring_arg2)) = integerAdd(integerMul(y, x), integerMul(y, __ring_arg2))universal statement · line 1–129
∀E
y ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))
term
integerNeg(y)
131x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))→E 1–130, 1–55Modus ponens
y ∈ ℤ → x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))implication · line 1–130
y ∈ ℤantecedent · line 1–55
→E
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))
132integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))→E 1–131, 1–51Modus ponens
x ∈ ℤ → integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))implication · line 1–131
x ∈ ℤantecedent · line 1–51
→E
integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))
133integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))→E 1–132, 1–85Modus ponens
integerNeg(y) ∈ ℤ → integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))implication · line 1–132
integerNeg(y) ∈ ℤantecedent · line 1–85
→E
integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))
134∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) = mul(y, x)thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) = mul(y, x)
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.mul_comm
135∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)∀E 1–134Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) = mul(y, x)universal statement · line 1–134
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)
term
ℤ
136∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)∀E 1–135Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)universal statement · line 1–135
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)
term
integerAdd
137∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)∀E 1–136Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)universal statement · line 1–136
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)
term
integerZero
138∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)∀E 1–137Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)universal statement · line 1–137
∀E
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)
term
integerNeg
139∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)∀E 1–138Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) = mul(y, x)universal statement · line 1–138
∀E
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)
term
integerMul
140∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)∀E 1–139Universal specialization
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)universal statement · line 1–139
∀E
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)
term
integerOne
141∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, y) = integerMul(y, __ring_arg0)∀E 1–140Universal specialization
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) = integerMul(y, x)universal statement · line 1–140
∀E
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, y) = integerMul(y, __ring_arg0)
term
__ring_arg0
142IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)∀E 1–141Universal specialization
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerMul(__ring_arg0, y) = integerMul(y, __ring_arg0)universal statement · line 1–141
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)
term
__ring_arg1
143__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)→E 1–142, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)implication · line 1–142
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)
144∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)∀I 1–143Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)body for fresh variable · line 1–143
∀I
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)
bound variable
__ring_arg1
145∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)∀I 1–144Universal introduction
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)body for fresh variable · line 1–144
∀I
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)
bound variable
__ring_arg0
146∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, __ring_arg1) = integerMul(__ring_arg1, y)∀E 1–145Universal specialization
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, __ring_arg1) = integerMul(__ring_arg1, __ring_arg0)universal statement · line 1–145
∀E
∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, __ring_arg1) = integerMul(__ring_arg1, y)
term
y
147y ∈ ℤ → x ∈ ℤ → integerMul(y, x) = integerMul(x, y)∀E 1–146Universal specialization
∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, __ring_arg1) = integerMul(__ring_arg1, y)universal statement · line 1–146
∀E
y ∈ ℤ → x ∈ ℤ → integerMul(y, x) = integerMul(x, y)
term
x
148x ∈ ℤ → integerMul(y, x) = integerMul(x, y)→E 1–147, 1–55Modus ponens
y ∈ ℤ → x ∈ ℤ → integerMul(y, x) = integerMul(x, y)implication · line 1–147
y ∈ ℤantecedent · line 1–55
→E
x ∈ ℤ → integerMul(y, x) = integerMul(x, y)
149integerMul(y, x) = integerMul(x, y)→E 1–148, 1–51Modus ponens
x ∈ ℤ → integerMul(y, x) = integerMul(x, y)implication · line 1–148
x ∈ ℤantecedent · line 1–51
→E
integerMul(y, x) = integerMul(x, y)
150∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, integerNeg(__ring_arg1)) = integerNeg(integerMul(y, __ring_arg1))∀E 1–121Universal specialization
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerMul(__ring_arg0, integerNeg(__ring_arg1)) = integerNeg(integerMul(__ring_arg0, __ring_arg1))universal statement · line 1–121
∀E
∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, integerNeg(__ring_arg1)) = integerNeg(integerMul(y, __ring_arg1))
term
y
151y ∈ ℤ → y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))∀E 1–150Universal specialization
∀ __ring_arg1, y ∈ ℤ → __ring_arg1 ∈ ℤ → integerMul(y, integerNeg(__ring_arg1)) = integerNeg(integerMul(y, __ring_arg1))universal statement · line 1–150
∀E
y ∈ ℤ → y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))
term
y
152y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))→E 1–151, 1–55Modus ponens
y ∈ ℤ → y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))implication · line 1–151
y ∈ ℤantecedent · line 1–55
→E
y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))
153integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))→E 1–152, 1–55Modus ponens
y ∈ ℤ → integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))implication · line 1–152
y ∈ ℤantecedent · line 1–55
→E
integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))
154integerAdd(integerMul(y, x), integerMul(y, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))congr 1–88, 1–149, 1–153Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerMul(y, x) = integerMul(x, y)argument equality 2 · line 1–149
integerMul(y, integerNeg(y)) = integerNeg(integerMul(y, y))argument equality 3 · line 1–153
congr
integerAdd(integerMul(y, x), integerMul(y, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
155integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))=trans 1–133, 1–154Equality transitivity
integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(y, x), integerMul(y, integerNeg(y)))left equality · line 1–133
integerAdd(integerMul(y, x), integerMul(y, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))right equality · line 1–154
=trans
integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
156integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y)))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))congr 1–88, 1–127, 1–155Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerMul(x, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerNeg(integerMul(x, y)))argument equality 2 · line 1–127
integerMul(y, integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))argument equality 3 · line 1–155
congr
integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y)))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
157integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))=trans 1–87, 1–156Equality transitivity
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y))))left equality · line 1–87
integerAdd(integerMul(x, integerAdd(x, integerNeg(y))), integerMul(y, integerAdd(x, integerNeg(y)))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))right equality · line 1–156
=trans
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))
158∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(add(x, y), z) = add(x, add(y, z))thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(add(x, y), z) = add(x, add(y, z))
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.add_assoc
159∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(add(x, y), z) = add(x, add(y, z))∀E 1–158Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(add(x, y), z) = add(x, add(y, z))universal statement · line 1–158
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(add(x, y), z) = add(x, add(y, z))
term
ℤ
160∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))∀E 1–159Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(add(x, y), z) = add(x, add(y, z))universal statement · line 1–159
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))
term
integerAdd
161∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))∀E 1–160Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))universal statement · line 1–160
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))
term
integerZero
162∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))∀E 1–161Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))universal statement · line 1–161
∀E
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))
term
integerNeg
163∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))∀E 1–162Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))universal statement · line 1–162
∀E
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))
term
integerMul
164∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))∀E 1–163Universal specialization
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))universal statement · line 1–163
∀E
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))
term
integerOne
165∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, y), z) = integerAdd(__ring_arg0, integerAdd(y, z))∀E 1–164Universal specialization
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(x, y), z) = integerAdd(x, integerAdd(y, z))universal statement · line 1–164
∀E
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, y), z) = integerAdd(__ring_arg0, integerAdd(y, z))
term
__ring_arg0
166∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, z))∀E 1–165Universal specialization
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, y), z) = integerAdd(__ring_arg0, integerAdd(y, z))universal statement · line 1–165
∀E
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, z))
term
__ring_arg1
167IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))∀E 1–166Universal specialization
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), z) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, z))universal statement · line 1–166
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))
term
__ring_arg2
168__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))→E 1–167, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))implication · line 1–167
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))
169∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))∀I 1–168Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))body for fresh variable · line 1–168
∀I
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))
bound variable
__ring_arg2
170∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))∀I 1–169Universal introduction
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))body for fresh variable · line 1–169
∀I
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))
bound variable
__ring_arg1
171∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))∀I 1–170Universal introduction
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))body for fresh variable · line 1–170
∀I
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))
bound variable
__ring_arg0
172∀ __ring_arg1, ∀ __ring_arg2, integerMul(x, x) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(__ring_arg1, __ring_arg2))∀E 1–171Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))universal statement · line 1–171
∀E
∀ __ring_arg1, ∀ __ring_arg2, integerMul(x, x) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(__ring_arg1, __ring_arg2))
term
integerMul(x, x)
173∀ __ring_arg2, integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), __ring_arg2))∀E 1–172Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, integerMul(x, x) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), __ring_arg1), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(__ring_arg1, __ring_arg2))universal statement · line 1–172
∀E
∀ __ring_arg2, integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), __ring_arg2))
term
integerNeg(integerMul(x, y))
174integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))∀E 1–173Universal specialization
∀ __ring_arg2, integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), __ring_arg2) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), __ring_arg2))universal statement · line 1–173
∀E
integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
term
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
175∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) ∈ AthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) ∈ A
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.mul_closed
176∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ∀E 1–175Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → mul(x, y) ∈ Auniversal statement · line 1–175
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ
term
ℤ
177∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ∀E 1–176Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤuniversal statement · line 1–176
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ
term
integerAdd
178∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ∀E 1–177Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤuniversal statement · line 1–177
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ
term
integerZero
179∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ∀E 1–178Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤuniversal statement · line 1–178
∀E
∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤ
term
integerNeg
180∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ∀E 1–179Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → mul(x, y) ∈ ℤuniversal statement · line 1–179
∀E
∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ
term
integerMul
181∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ∀E 1–180Universal specialization
∀ one, ∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤuniversal statement · line 1–180
∀E
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ
term
integerOne
182∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ∀E 1–181Universal specialization
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤuniversal statement · line 1–181
∀E
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ
term
x
183IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤ∀E 1–182Universal specialization
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤuniversal statement · line 1–182
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤ
term
x
184x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤ→E 1–183, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤimplication · line 1–183
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤ
185x ∈ ℤ → integerMul(x, x) ∈ ℤ→E 1–184, 1–51Modus ponens
x ∈ ℤ → x ∈ ℤ → integerMul(x, x) ∈ ℤimplication · line 1–184
x ∈ ℤantecedent · line 1–51
→E
x ∈ ℤ → integerMul(x, x) ∈ ℤ
186integerMul(x, x) ∈ ℤ→E 1–185, 1–51Modus ponens
x ∈ ℤ → integerMul(x, x) ∈ ℤimplication · line 1–185
x ∈ ℤantecedent · line 1–51
→E
integerMul(x, x) ∈ ℤ
187integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–174, 1–186Modus ponens
integerMul(x, x) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–174
integerMul(x, x) ∈ ℤantecedent · line 1–186
→E
integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
188IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ∀E 1–82Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(x) ∈ ℤuniversal statement · line 1–82
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ
term
integerMul(x, y)
189integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ→E 1–188, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤimplication · line 1–188
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤ
190IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ∀E 1–182Universal specialization
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤuniversal statement · line 1–182
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ
term
y
191x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ→E 1–190, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤimplication · line 1–190
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤ
192y ∈ ℤ → integerMul(x, y) ∈ ℤ→E 1–191, 1–51Modus ponens
x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤimplication · line 1–191
x ∈ ℤantecedent · line 1–51
→E
y ∈ ℤ → integerMul(x, y) ∈ ℤ
193integerMul(x, y) ∈ ℤ→E 1–192, 1–55Modus ponens
y ∈ ℤ → integerMul(x, y) ∈ ℤimplication · line 1–192
y ∈ ℤantecedent · line 1–55
→E
integerMul(x, y) ∈ ℤ
194integerNeg(integerMul(x, y)) ∈ ℤ→E 1–189, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(x, y)) ∈ ℤimplication · line 1–189
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerNeg(integerMul(x, y)) ∈ ℤ
195integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–187, 1–194Modus ponens
integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–187
integerNeg(integerMul(x, y)) ∈ ℤantecedent · line 1–194
→E
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
196∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → y_1 ∈ ℤ → integerAdd(integerMul(x, y), y_1) ∈ ℤ∀E 1–63Universal specialization
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–63
∀E
∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → y_1 ∈ ℤ → integerAdd(integerMul(x, y), y_1) ∈ ℤ
term
integerMul(x, y)
197IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ∀E 1–196Universal specialization
∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → y_1 ∈ ℤ → integerAdd(integerMul(x, y), y_1) ∈ ℤuniversal statement · line 1–196
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ
term
integerNeg(integerMul(y, y))
198integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ→E 1–197, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–197
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ
199integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ→E 1–198, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–198
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ
200IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ∀E 1–82Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerNeg(x) ∈ ℤuniversal statement · line 1–82
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ
term
integerMul(y, y)
201integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ→E 1–200, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤimplication · line 1–200
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ
202∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y_1 ∈ ℤ → integerMul(y, y_1) ∈ ℤ∀E 1–181Universal specialization
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerMul(x, y) ∈ ℤuniversal statement · line 1–181
∀E
∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y_1 ∈ ℤ → integerMul(y, y_1) ∈ ℤ
term
y
203IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤ∀E 1–202Universal specialization
∀ y_1, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y_1 ∈ ℤ → integerMul(y, y_1) ∈ ℤuniversal statement · line 1–202
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤ
term
y
204y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤ→E 1–203, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤimplication · line 1–203
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤ
205y ∈ ℤ → integerMul(y, y) ∈ ℤ→E 1–204, 1–55Modus ponens
y ∈ ℤ → y ∈ ℤ → integerMul(y, y) ∈ ℤimplication · line 1–204
y ∈ ℤantecedent · line 1–55
→E
y ∈ ℤ → integerMul(y, y) ∈ ℤ
206integerMul(y, y) ∈ ℤ→E 1–205, 1–55Modus ponens
y ∈ ℤ → integerMul(y, y) ∈ ℤimplication · line 1–205
y ∈ ℤantecedent · line 1–55
→E
integerMul(y, y) ∈ ℤ
207integerNeg(integerMul(y, y)) ∈ ℤ→E 1–201, 1–206Modus ponens
integerMul(y, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤimplication · line 1–201
integerMul(y, y) ∈ ℤantecedent · line 1–206
→E
integerNeg(integerMul(y, y)) ∈ ℤ
208integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ→E 1–199, 1–207Modus ponens
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–199
integerNeg(integerMul(y, y)) ∈ ℤantecedent · line 1–207
→E
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ
209integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–195, 1–208Modus ponens
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–195
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤantecedent · line 1–208
→E
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
210integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))=trans 1–157, 1–209Equality transitivity
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))left equality · line 1–157
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))right equality · line 1–209
=trans
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
211integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))=trans 1–29, 1–210Equality transitivity
integerMul(x + y, x - y) = integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y)))left equality · line 1–29
integerMul(integerAdd(x, y), integerAdd(x, integerNeg(y))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))right equality · line 1–210
=trans
integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
212integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))=sym 1–209Equality symmetry
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))equality · line 1–209
=sym
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))
213∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, zero) = xthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, zero) = x
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.add_right_identity
214∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, zero) = x∀E 1–213Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, zero) = xuniversal statement · line 1–213
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, zero) = x
term
ℤ
215∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, zero) = x∀E 1–214Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, zero) = xuniversal statement · line 1–214
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, zero) = x
term
integerAdd
216∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = x∀E 1–215Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, zero) = xuniversal statement · line 1–215
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = x
term
integerZero
217∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = x∀E 1–216Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = xuniversal statement · line 1–216
∀E
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = x
term
integerNeg
218∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, 0) = x∀E 1–217Universal specialization
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, 0) = xuniversal statement · line 1–217
∀E
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, 0) = x
term
integerMul
219∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, 0) = x∀E 1–218Universal specialization
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, 0) = xuniversal statement · line 1–218
∀E
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, 0) = x
term
integerOne
220IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0∀E 1–219Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, 0) = xuniversal statement · line 1–219
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0
term
__ring_arg0
221__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0→E 1–220, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0implication · line 1–220
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0
222∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, 0) = __ring_arg0∀I 1–221Universal introduction
__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, 0) = __ring_arg0body for fresh variable · line 1–221
∀I
∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, 0) = __ring_arg0
bound variable
__ring_arg0
223integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))∀E 1–222Universal specialization
∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, 0) = __ring_arg0universal statement · line 1–222
∀E
integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))
term
integerNeg(integerMul(x, y))
224integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))→E 1–223, 1–194Modus ponens
integerNeg(integerMul(x, y)) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))implication · line 1–223
integerNeg(integerMul(x, y)) ∈ ℤantecedent · line 1–194
→E
integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))
225integerNeg(integerMul(x, y)) = integerAdd(integerNeg(integerMul(x, y)), 0)=sym 1–224Equality symmetry
integerAdd(integerNeg(integerMul(x, y)), 0) = integerNeg(integerMul(x, y))equality · line 1–224
=sym
integerNeg(integerMul(x, y)) = integerAdd(integerNeg(integerMul(x, y)), 0)
226integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))=IEquality reflexivity
=I
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
term
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
227integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))congr 1–88, 1–225, 1–226Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerNeg(integerMul(x, y)) = integerAdd(integerNeg(integerMul(x, y)), 0)argument equality 2 · line 1–225
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) = integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))argument equality 3 · line 1–226
congr
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
228∀ __ring_arg1, ∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), __ring_arg1), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(__ring_arg1, __ring_arg2))∀E 1–171Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(integerAdd(__ring_arg0, __ring_arg1), __ring_arg2) = integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2))universal statement · line 1–171
∀E
∀ __ring_arg1, ∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), __ring_arg1), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(__ring_arg1, __ring_arg2))
term
integerNeg(integerMul(x, y))
229∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, __ring_arg2))∀E 1–228Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), __ring_arg1), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(__ring_arg1, __ring_arg2))universal statement · line 1–228
∀E
∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, __ring_arg2))
term
integerZero
230integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))∀E 1–229Universal specialization
∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, __ring_arg2))universal statement · line 1–229
∀E
integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
term
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))
2310 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–230, 1–194Modus ponens
integerNeg(integerMul(x, y)) ∈ ℤ → 0 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–230
integerNeg(integerMul(x, y)) ∈ ℤantecedent · line 1–194
→E
0 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
232∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(A, add, zero, neg, mul, one) → zero ∈ AthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(A, add, zero, neg, mul, one) → zero ∈ A
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.zero_in_carrier
233∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, add, zero, neg, mul, one) → zero ∈ ℤ∀E 1–232Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(A, add, zero, neg, mul, one) → zero ∈ Auniversal statement · line 1–232
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, add, zero, neg, mul, one) → zero ∈ ℤ
term
ℤ
234∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, zero, neg, mul, one) → zero ∈ ℤ∀E 1–233Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, add, zero, neg, mul, one) → zero ∈ ℤuniversal statement · line 1–233
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, zero, neg, mul, one) → zero ∈ ℤ
term
integerAdd
235∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, neg, mul, one) → 0 ∈ ℤ∀E 1–234Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, zero, neg, mul, one) → zero ∈ ℤuniversal statement · line 1–234
∀E
∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, neg, mul, one) → 0 ∈ ℤ
term
integerZero
236∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → 0 ∈ ℤ∀E 1–235Universal specialization
∀ neg, ∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, neg, mul, one) → 0 ∈ ℤuniversal statement · line 1–235
∀E
∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → 0 ∈ ℤ
term
integerNeg
237∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → 0 ∈ ℤ∀E 1–236Universal specialization
∀ mul, ∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → 0 ∈ ℤuniversal statement · line 1–236
∀E
∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → 0 ∈ ℤ
term
integerMul
238IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ∀E 1–237Universal specialization
∀ one, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → 0 ∈ ℤuniversal statement · line 1–237
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ
term
integerOne
2390 ∈ ℤ→E 1–238, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤimplication · line 1–238
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
0 ∈ ℤ
240integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–231, 1–239Modus ponens
0 ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–231
0 ∈ ℤantecedent · line 1–239
→E
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
241integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))→E 1–240, 1–208Modus ponens
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))implication · line 1–240
integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))) ∈ ℤantecedent · line 1–208
→E
integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
242integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))=trans 1–227, 1–241Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))left equality · line 1–227
integerAdd(integerAdd(integerNeg(integerMul(x, y)), 0), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))right equality · line 1–241
=trans
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))
243integerNeg(integerMul(x, y)) = integerNeg(integerMul(x, y))=IEquality reflexivity
=I
integerNeg(integerMul(x, y)) = integerNeg(integerMul(x, y))
term
integerNeg(integerMul(x, y))
244∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(x, add(y, z)) = add(y, add(x, z))thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(x, add(y, z)) = add(y, add(x, z))
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.add_swap
245∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(x, add(y, z)) = add(y, add(x, z))∀E 1–244Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → z ∈ A → add(x, add(y, z)) = add(y, add(x, z))universal statement · line 1–244
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(x, add(y, z)) = add(y, add(x, z))
term
ℤ
246∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))∀E 1–245Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → add(x, add(y, z)) = add(y, add(x, z))universal statement · line 1–245
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))
term
integerAdd
247∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))∀E 1–246Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))universal statement · line 1–246
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))
term
integerZero
248∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))∀E 1–247Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))universal statement · line 1–247
∀E
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))
term
integerNeg
249∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))∀E 1–248Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))universal statement · line 1–248
∀E
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))
term
integerMul
250∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))∀E 1–249Universal specialization
∀ one, ∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))universal statement · line 1–249
∀E
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))
term
integerOne
251∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(y, z)) = integerAdd(y, integerAdd(__ring_arg0, z))∀E 1–250Universal specialization
∀ x, ∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(x, integerAdd(y, z)) = integerAdd(y, integerAdd(x, z))universal statement · line 1–250
∀E
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(y, z)) = integerAdd(y, integerAdd(__ring_arg0, z))
term
__ring_arg0
252∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, z))∀E 1–251Universal specialization
∀ y, ∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(y, z)) = integerAdd(y, integerAdd(__ring_arg0, z))universal statement · line 1–251
∀E
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, z))
term
__ring_arg1
253IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))∀E 1–252Universal specialization
∀ z, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → z ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, z)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, z))universal statement · line 1–252
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))
term
__ring_arg2
254__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))→E 1–253, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))implication · line 1–253
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))
255∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))∀I 1–254Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))body for fresh variable · line 1–254
∀I
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))
bound variable
__ring_arg2
256∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))∀I 1–255Universal introduction
∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))body for fresh variable · line 1–255
∀I
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))
bound variable
__ring_arg1
257∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))∀I 1–256Universal introduction
∀ __ring_arg1, ∀ __ring_arg2, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))body for fresh variable · line 1–256
∀I
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))
bound variable
__ring_arg0
258∀ __ring_arg1, ∀ __ring_arg2, 0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(0, __ring_arg2))∀E 1–257Universal specialization
∀ __ring_arg0 __ring_arg1 __ring_arg2 ∈ ℤ, integerAdd(__ring_arg0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(__ring_arg0, __ring_arg2))universal statement · line 1–257
∀E
∀ __ring_arg1, ∀ __ring_arg2, 0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(0, __ring_arg2))
term
integerZero
259∀ __ring_arg2, 0 ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), __ring_arg2)) = integerAdd(integerMul(x, y), integerAdd(0, __ring_arg2))∀E 1–258Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, 0 ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(__ring_arg1, __ring_arg2)) = integerAdd(__ring_arg1, integerAdd(0, __ring_arg2))universal statement · line 1–258
∀E
∀ __ring_arg2, 0 ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), __ring_arg2)) = integerAdd(integerMul(x, y), integerAdd(0, __ring_arg2))
term
integerMul(x, y)
2600 ∈ ℤ → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))∀E 1–259Universal specialization
∀ __ring_arg2, 0 ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), __ring_arg2)) = integerAdd(integerMul(x, y), integerAdd(0, __ring_arg2))universal statement · line 1–259
∀E
0 ∈ ℤ → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))
term
integerNeg(integerMul(y, y))
261integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))→E 1–260, 1–239Modus ponens
0 ∈ ℤ → integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))implication · line 1–260
0 ∈ ℤantecedent · line 1–239
→E
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))
262integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))→E 1–261, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))implication · line 1–261
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))
263integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))→E 1–262, 1–207Modus ponens
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))implication · line 1–262
integerNeg(integerMul(y, y)) ∈ ℤantecedent · line 1–207
→E
integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))
264integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))congr 1–88, 1–243, 1–263Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerNeg(integerMul(x, y)) = integerNeg(integerMul(x, y))argument equality 2 · line 1–243
integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))argument equality 3 · line 1–263
congr
integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
265integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))=trans 1–242, 1–264Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))left equality · line 1–242
integerAdd(integerNeg(integerMul(x, y)), integerAdd(0, integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))right equality · line 1–264
=trans
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
266∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), __ring_arg2))∀E 1–228Universal specialization
∀ __ring_arg1, ∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), __ring_arg1), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(__ring_arg1, __ring_arg2))universal statement · line 1–228
∀E
∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), __ring_arg2))
term
integerMul(x, y)
267integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))∀E 1–266Universal specialization
∀ __ring_arg2, integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → __ring_arg2 ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), __ring_arg2) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), __ring_arg2))universal statement · line 1–266
∀E
integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
term
integerAdd(integerZero, integerNeg(integerMul(y, y)))
268integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))→E 1–267, 1–194Modus ponens
integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))implication · line 1–267
integerNeg(integerMul(x, y)) ∈ ℤantecedent · line 1–194
→E
integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
269integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))→E 1–268, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))implication · line 1–268
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
270∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → y ∈ ℤ → integerAdd(0, y) ∈ ℤ∀E 1–63Universal specialization
∀ x, ∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) ∈ ℤuniversal statement · line 1–63
∀E
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → y ∈ ℤ → integerAdd(0, y) ∈ ℤ
term
integerZero
271IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ∀E 1–270Universal specialization
∀ y, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → y ∈ ℤ → integerAdd(0, y) ∈ ℤuniversal statement · line 1–270
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ
term
integerNeg(integerMul(y, y))
2720 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ→E 1–271, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → 0 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–271
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
0 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ
273integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ→E 1–272, 1–239Modus ponens
0 ∈ ℤ → integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–272
0 ∈ ℤantecedent · line 1–239
→E
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ
274integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ→E 1–273, 1–207Modus ponens
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤimplication · line 1–273
integerNeg(integerMul(y, y)) ∈ ℤantecedent · line 1–207
→E
integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ
275integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))→E 1–269, 1–274Modus ponens
integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤ → integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))implication · line 1–269
integerAdd(0, integerNeg(integerMul(y, y))) ∈ ℤantecedent · line 1–274
→E
integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))
276integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))=sym 1–275Equality symmetry
integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))equality · line 1–275
=sym
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))
277integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))=trans 1–265, 1–276Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y)))))left equality · line 1–265
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerAdd(0, integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))right equality · line 1–276
=trans
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))
278∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) = add(y, x)thmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) = add(y, x)
declaration
Grace.Cumulus.Algebra.Ring.Core.IsCommRing.add_comm
279∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) = add(y, x)∀E 1–278Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(A, add, zero, neg, mul, one) → x ∈ A → y ∈ A → add(x, y) = add(y, x)universal statement · line 1–278
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) = add(y, x)
term
ℤ
280∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)∀E 1–279Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → add(x, y) = add(y, x)universal statement · line 1–279
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)
term
integerAdd
281∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)∀E 1–280Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)universal statement · line 1–280
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)
term
integerZero
282∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)∀E 1–281Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)universal statement · line 1–281
∀E
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)
term
integerNeg
283∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)∀E 1–282Universal specialization
∀ mul, ∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)universal statement · line 1–282
∀E
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)
term
integerMul
284∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)∀E 1–283Universal specialization
∀ one, ∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)universal statement · line 1–283
∀E
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)
term
integerOne
285∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerAdd(__ring_arg0, y) = integerAdd(y, __ring_arg0)∀E 1–284Universal specialization
∀ x, ∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → y ∈ ℤ → integerAdd(x, y) = integerAdd(y, x)universal statement · line 1–284
∀E
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerAdd(__ring_arg0, y) = integerAdd(y, __ring_arg0)
term
__ring_arg0
286IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)∀E 1–285Universal specialization
∀ y, IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → y ∈ ℤ → integerAdd(__ring_arg0, y) = integerAdd(y, __ring_arg0)universal statement · line 1–285
∀E
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)
term
__ring_arg1
287__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)→E 1–286, 1–40Modus ponens
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)implication · line 1–286
IsCommRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–40
→E
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)
288∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)∀I 1–287Universal introduction
__ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)body for fresh variable · line 1–287
∀I
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)
bound variable
__ring_arg1
289∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)∀I 1–288Universal introduction
∀ __ring_arg1, __ring_arg0 ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)body for fresh variable · line 1–288
∀I
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)
bound variable
__ring_arg0
290∀ __ring_arg1, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), __ring_arg1) = integerAdd(__ring_arg1, integerNeg(integerMul(x, y)))∀E 1–289Universal specialization
∀ __ring_arg0 __ring_arg1 ∈ ℤ, integerAdd(__ring_arg0, __ring_arg1) = integerAdd(__ring_arg1, __ring_arg0)universal statement · line 1–289
∀E
∀ __ring_arg1, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), __ring_arg1) = integerAdd(__ring_arg1, integerNeg(integerMul(x, y)))
term
integerNeg(integerMul(x, y))
291integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))∀E 1–290Universal specialization
∀ __ring_arg1, integerNeg(integerMul(x, y)) ∈ ℤ → __ring_arg1 ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), __ring_arg1) = integerAdd(__ring_arg1, integerNeg(integerMul(x, y)))universal statement · line 1–290
∀E
integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))
term
integerMul(x, y)
292integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))→E 1–291, 1–194Modus ponens
integerNeg(integerMul(x, y)) ∈ ℤ → integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))implication · line 1–291
integerNeg(integerMul(x, y)) ∈ ℤantecedent · line 1–194
→E
integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))
293integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))→E 1–292, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))implication · line 1–292
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))
294∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, neg(x)) = zerothmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, neg(x)) = zero
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.add_inverse_right
295∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, neg(x)) = zero∀E 1–294Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(x, neg(x)) = zerouniversal statement · line 1–294
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, neg(x)) = zero
term
ℤ
296∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = zero∀E 1–295Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(x, neg(x)) = zerouniversal statement · line 1–295
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = zero
term
integerAdd
297∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = 0∀E 1–296Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = zerouniversal statement · line 1–296
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = 0
term
integerZero
298∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0∀E 1–297Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(x, neg(x)) = 0universal statement · line 1–297
∀E
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0
term
integerNeg
299∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0∀E 1–298Universal specialization
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0universal statement · line 1–298
∀E
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0
term
integerMul
300∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0∀E 1–299Universal specialization
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0universal statement · line 1–299
∀E
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0
term
integerOne
301IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0∀E 1–300Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(x, integerNeg(x)) = 0universal statement · line 1–300
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0
term
__ring_arg0
302__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0→E 1–301, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0implication · line 1–301
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0
303∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0∀I 1–302Universal introduction
__ring_arg0 ∈ ℤ → integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0body for fresh variable · line 1–302
∀I
∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0
bound variable
__ring_arg0
304integerMul(x, y) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0∀E 1–303Universal specialization
∀ __ring_arg0 ∈ ℤ, integerAdd(__ring_arg0, integerNeg(__ring_arg0)) = 0universal statement · line 1–303
∀E
integerMul(x, y) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0
term
integerMul(x, y)
305integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0→E 1–304, 1–193Modus ponens
integerMul(x, y) ∈ ℤ → integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0implication · line 1–304
integerMul(x, y) ∈ ℤantecedent · line 1–193
→E
integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0
306integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = 0=trans 1–293, 1–305Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = integerAdd(integerMul(x, y), integerNeg(integerMul(x, y)))left equality · line 1–293
integerAdd(integerMul(x, y), integerNeg(integerMul(x, y))) = 0right equality · line 1–305
=trans
integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = 0
307∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(zero, x) = xthmChecked theorem
thm
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(zero, x) = x
declaration
Grace.Cumulus.Algebra.Ring.Core.IsRing.add_left_identity
308∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(zero, x) = x∀E 1–307Universal specialization
∀ A, ∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(A, add, zero, neg, mul, one) → x ∈ A → add(zero, x) = xuniversal statement · line 1–307
∀E
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(zero, x) = x
term
ℤ
309∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(zero, x) = x∀E 1–308Universal specialization
∀ add, ∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, add, zero, neg, mul, one) → x ∈ ℤ → add(zero, x) = xuniversal statement · line 1–308
∀E
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(zero, x) = x
term
integerAdd
310∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(0, x) = x∀E 1–309Universal specialization
∀ zero, ∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, zero, neg, mul, one) → x ∈ ℤ → integerAdd(zero, x) = xuniversal statement · line 1–309
∀E
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(0, x) = x
term
integerZero
311∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(0, x) = x∀E 1–310Universal specialization
∀ neg, ∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, neg, mul, one) → x ∈ ℤ → integerAdd(0, x) = xuniversal statement · line 1–310
∀E
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(0, x) = x
term
integerNeg
312∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(0, x) = x∀E 1–311Universal specialization
∀ mul, ∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, mul, one) → x ∈ ℤ → integerAdd(0, x) = xuniversal statement · line 1–311
∀E
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(0, x) = x
term
integerMul
313∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(0, x) = x∀E 1–312Universal specialization
∀ one, ∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, one) → x ∈ ℤ → integerAdd(0, x) = xuniversal statement · line 1–312
∀E
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(0, x) = x
term
integerOne
314IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0∀E 1–313Universal specialization
∀ x, IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → x ∈ ℤ → integerAdd(0, x) = xuniversal statement · line 1–313
∀E
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0
term
__ring_arg0
315__ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0→E 1–314, 1–73Modus ponens
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1) → __ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0implication · line 1–314
IsRing(ℤ, integerAdd, 0, integerNeg, integerMul, 1)antecedent · line 1–73
→E
__ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0
316∀ __ring_arg0 ∈ ℤ, integerAdd(0, __ring_arg0) = __ring_arg0∀I 1–315Universal introduction
__ring_arg0 ∈ ℤ → integerAdd(0, __ring_arg0) = __ring_arg0body for fresh variable · line 1–315
∀I
∀ __ring_arg0 ∈ ℤ, integerAdd(0, __ring_arg0) = __ring_arg0
bound variable
__ring_arg0
317integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))∀E 1–316Universal specialization
∀ __ring_arg0 ∈ ℤ, integerAdd(0, __ring_arg0) = __ring_arg0universal statement · line 1–316
∀E
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))
term
integerNeg(integerMul(y, y))
318integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))→E 1–317, 1–207Modus ponens
integerNeg(integerMul(y, y)) ∈ ℤ → integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))implication · line 1–317
integerNeg(integerMul(y, y)) ∈ ℤantecedent · line 1–207
→E
integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))
319integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))congr 1–88, 1–306, 1–318Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)) = 0argument equality 2 · line 1–306
integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))argument equality 3 · line 1–318
congr
integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
320integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))=trans 1–277, 1–319Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y))))left equality · line 1–277
integerAdd(integerAdd(integerNeg(integerMul(x, y)), integerMul(x, y)), integerAdd(0, integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))right equality · line 1–319
=trans
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))
321integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerNeg(integerMul(y, y))=trans 1–320, 1–318Equality transitivity
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(0, integerNeg(integerMul(y, y)))left equality · line 1–320
integerAdd(0, integerNeg(integerMul(y, y))) = integerNeg(integerMul(y, y))right equality · line 1–318
=trans
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerNeg(integerMul(y, y))
322integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))congr 1–88, 1–109, 1–321Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
integerMul(x, x) = integerMul(x, x)argument equality 2 · line 1–109
integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerNeg(integerMul(y, y))argument equality 3 · line 1–321
congr
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
323integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))=trans 1–209, 1–322Equality transitivity
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))left equality · line 1–209
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))right equality · line 1–322
=trans
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
324integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))=trans 1–212, 1–323Equality transitivity
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))left equality · line 1–212
integerAdd(integerAdd(integerMul(x, x), integerNeg(integerMul(x, y))), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))right equality · line 1–323
=trans
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
325integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))=trans 1–211, 1–324Equality transitivity
integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y)))))left equality · line 1–211
integerAdd(integerMul(x, x), integerAdd(integerNeg(integerMul(x, y)), integerAdd(integerMul(x, y), integerNeg(integerMul(y, y))))) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))right equality · line 1–324
=trans
integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
326(x + y) * (x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))=trans 1–18, 1–325Equality transitivity
(x + y) * (x - y) = integerMul(x + y, x - y)left equality · line 1–18
integerMul(x + y, x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))right equality · line 1–325
=trans
(x + y) * (x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
327∀ y, x * x - y = integerAdd(x * x, integerNeg(y))∀E 1–26Universal specialization
∀ x, ∀ y, x - y = integerAdd(x, integerNeg(y))universal statement · line 1–26
∀E
∀ y, x * x - y = integerAdd(x * x, integerNeg(y))
term
integerMulValue(x, x)
328x * x - y * y = integerAdd(x * x, integerNeg(y * y))∀E 1–327Universal specialization
∀ y, x * x - y = integerAdd(x * x, integerNeg(y))universal statement · line 1–327
∀E
x * x - y * y = integerAdd(x * x, integerNeg(y * y))
term
integerMulValue(y, y)
329∀ y, x ∈ Integer → y ∈ Integer → integerMul(x, y) = x * y∀E 1Universal specialization
∀ x y : ℤ, integerMul(x, y) = x * yuniversal statement · line 1
∀E
∀ y, x ∈ Integer → y ∈ Integer → integerMul(x, y) = x * y
term
x
330x ∈ Integer → x ∈ Integer → integerMul(x, x) = x * x∀E 1–329Universal specialization
∀ y, x ∈ Integer → y ∈ Integer → integerMul(x, y) = x * yuniversal statement · line 1–329
∀E
x ∈ Integer → x ∈ Integer → integerMul(x, x) = x * x
term
x
331x ∈ Integer → integerMul(x, x) = x * x→E 1–330, 1–7Modus ponens
x ∈ Integer → x ∈ Integer → integerMul(x, x) = x * ximplication · line 1–330
x : ℤantecedent · line 1–7
→E
x ∈ Integer → integerMul(x, x) = x * x
332integerMul(x, x) = x * x→E 1–331, 1–7Modus ponens
x ∈ Integer → integerMul(x, x) = x * ximplication · line 1–331
x : ℤantecedent · line 1–7
→E
integerMul(x, x) = x * x
333x * x = integerMul(x, x)=sym 1–332Equality symmetry
integerMul(x, x) = x * xequality · line 1–332
=sym
x * x = integerMul(x, x)
334integerNeg = integerNeg=IEquality reflexivity
=I
integerNeg = integerNeg
term
integerNeg
335∀ y_1, y ∈ Integer → y_1 ∈ Integer → integerMul(y, y_1) = y * y_1∀E 1Universal specialization
∀ x y : ℤ, integerMul(x, y) = x * yuniversal statement · line 1
∀E
∀ y_1, y ∈ Integer → y_1 ∈ Integer → integerMul(y, y_1) = y * y_1
term
y
336y ∈ Integer → y ∈ Integer → integerMul(y, y) = y * y∀E 1–335Universal specialization
∀ y_1, y ∈ Integer → y_1 ∈ Integer → integerMul(y, y_1) = y * y_1universal statement · line 1–335
∀E
y ∈ Integer → y ∈ Integer → integerMul(y, y) = y * y
term
y
337y ∈ Integer → integerMul(y, y) = y * y→E 1–336, 1–9Modus ponens
y ∈ Integer → y ∈ Integer → integerMul(y, y) = y * yimplication · line 1–336
y : ℤantecedent · line 1–9
→E
y ∈ Integer → integerMul(y, y) = y * y
338integerMul(y, y) = y * y→E 1–337, 1–9Modus ponens
y ∈ Integer → integerMul(y, y) = y * yimplication · line 1–337
y : ℤantecedent · line 1–9
→E
integerMul(y, y) = y * y
339y * y = integerMul(y, y)=sym 1–338Equality symmetry
integerMul(y, y) = y * yequality · line 1–338
=sym
y * y = integerMul(y, y)
340integerNeg(y * y) = integerNeg(integerMul(y, y))congr 1–334, 1–339Function congruence
integerNeg = integerNegargument equality 1 · line 1–334
y * y = integerMul(y, y)argument equality 2 · line 1–339
congr
integerNeg(y * y) = integerNeg(integerMul(y, y))
function
apply
341integerAdd(x * x, integerNeg(y * y)) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))congr 1–88, 1–333, 1–340Function congruence
integerAdd = integerAddargument equality 1 · line 1–88
x * x = integerMul(x, x)argument equality 2 · line 1–333
integerNeg(y * y) = integerNeg(integerMul(y, y))argument equality 3 · line 1–340
congr
integerAdd(x * x, integerNeg(y * y)) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
function
Grace.Cumulus.Algebra.Foundation.Algebra.call2
342x * x - y * y = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))=trans 1–328, 1–341Equality transitivity
x * x - y * y = integerAdd(x * x, integerNeg(y * y))left equality · line 1–328
integerAdd(x * x, integerNeg(y * y)) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))right equality · line 1–341
=trans
x * x - y * y = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))
343integerAdd(integerMul(x, x), integerNeg(integerMul(y, y))) = x * x - y * y=sym 1–342Equality symmetry
x * x - y * y = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))equality · line 1–342
=sym
integerAdd(integerMul(x, x), integerNeg(integerMul(y, y))) = x * x - y * y
344(x + y) * (x - y) = x * x - y * y=trans 1–326, 1–343Equality transitivity
(x + y) * (x - y) = integerAdd(integerMul(x, x), integerNeg(integerMul(y, y)))left equality · line 1–326
integerAdd(integerMul(x, x), integerNeg(integerMul(y, y))) = x * x - y * yright equality · line 1–343
=trans
(x + y) * (x - y) = x * x - y * y
345y ∈ Integer → (x + y) * (x - y) = x * x - y * y→I 1–344Implication introduction
[y : ℤ]
(x + y) * (x - y) = x * x - y * yconclusion under assumption · line 1–344
→I
y ∈ Integer → (x + y) * (x - y) = x * x - y * y
discharged assumption
y : ℤ
346x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * y→I 345Implication introduction
[x : ℤ]
y ∈ Integer → (x + y) * (x - y) = x * x - y * yconclusion under assumption · line 345
→I
x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * y
discharged assumption
x : ℤ
347∀ y, x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * y∀I 346Universal introduction
x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * ybody for fresh variable · line 346
∀I
∀ y, x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * y
bound variable
y
348∀ x y : ℤ, (x + y) * (x - y) = x * x - y * y∀I 347Universal introduction
∀ y, x ∈ Integer → y ∈ Integer → (x + y) * (x - y) = x * x - y * ybody for fresh variable · line 347
∀I
∀ x y : ℤ, (x + y) * (x - y) = x * x - y * y
bound variable
x

The principle of mathematical induction in Cumulus (natural.induction) is twenty lines of tactics and about nine hundred kernel lines; open its derivation in the Workbench to read it.

Reading derivations in the library#

Every module page of Cumulus lists its theorems with a derivation link. The link opens the module in the Workbench, checks it in your browser, and opens the Kernel proof drawer at that theorem. Nothing is sent to a server, and the derivation you read is the one the kernel checked a moment earlier.

The same certificates are what the independent checkers verify. The kernel format is their specification, and soundness describes what is trusted.