Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
binom21
Next ⟩
binom2sub
Metamath Proof Explorer
Ascii
Unicode
Theorem
binom21
Description:
Special case of
binom2
where
B = 1
.
(Contributed by
Scott Fenton
, 11-May-2014)
Ref
Expression
Assertion
binom21
⊢
A
∈
ℂ
→
A
+
1
2
=
A
2
+
2
⁢
A
+
1
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
binom2
⊢
A
∈
ℂ
∧
1
∈
ℂ
→
A
+
1
2
=
A
2
+
2
⁢
A
⋅
1
+
1
2
3
1
2
mpan2
⊢
A
∈
ℂ
→
A
+
1
2
=
A
2
+
2
⁢
A
⋅
1
+
1
2
4
mulid1
⊢
A
∈
ℂ
→
A
⋅
1
=
A
5
4
oveq2d
⊢
A
∈
ℂ
→
2
⁢
A
⋅
1
=
2
⁢
A
6
5
oveq2d
⊢
A
∈
ℂ
→
A
2
+
2
⁢
A
⋅
1
=
A
2
+
2
⁢
A
7
sq1
⊢
1
2
=
1
8
7
a1i
⊢
A
∈
ℂ
→
1
2
=
1
9
6
8
oveq12d
⊢
A
∈
ℂ
→
A
2
+
2
⁢
A
⋅
1
+
1
2
=
A
2
+
2
⁢
A
+
1
10
3
9
eqtrd
⊢
A
∈
ℂ
→
A
+
1
2
=
A
2
+
2
⁢
A
+
1