Database
REAL AND COMPLEX NUMBERS
Integer sets
Simple number properties
2halvesd
Next ⟩
rehalfcld
Metamath Proof Explorer
Ascii
Unicode
Theorem
2halvesd
Description:
Two halves make a whole.
(Contributed by
Mario Carneiro
, 27-May-2016)
Ref
Expression
Hypothesis
2timesd.1
⊢
φ
→
A
∈
ℂ
Assertion
2halvesd
⊢
φ
→
A
2
+
A
2
=
A
Proof
Step
Hyp
Ref
Expression
1
2timesd.1
⊢
φ
→
A
∈
ℂ
2
2halves
⊢
A
∈
ℂ
→
A
2
+
A
2
=
A
3
1
2
syl
⊢
φ
→
A
2
+
A
2
=
A