Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
8p6e14
Next ⟩
8p7e15
Metamath Proof Explorer
Ascii
Unicode
Theorem
8p6e14
Description:
8 + 6 = 14.
(Contributed by
Mario Carneiro
, 19-Apr-2015)
Ref
Expression
Assertion
8p6e14
⊢
8
+
6
=
14
Proof
Step
Hyp
Ref
Expression
1
8nn0
⊢
8
∈
ℕ
0
2
5nn0
⊢
5
∈
ℕ
0
3
3nn0
⊢
3
∈
ℕ
0
4
df-6
⊢
6
=
5
+
1
5
df-4
⊢
4
=
3
+
1
6
8p5e13
⊢
8
+
5
=
13
7
1
2
3
4
5
6
6p5lem
⊢
8
+
6
=
14