Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Division
divrec2
Next ⟩
divass
Metamath Proof Explorer
Ascii
Unicode
Theorem
divrec2
Description:
Relationship between division and reciprocal.
(Contributed by
NM
, 7-Feb-2006)
Ref
Expression
Assertion
divrec2
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
=
1
B
⁢
A
Proof
Step
Hyp
Ref
Expression
1
divrec
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
=
A
⁢
1
B
2
simp1
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
∈
ℂ
3
reccl
⊢
B
∈
ℂ
∧
B
≠
0
→
1
B
∈
ℂ
4
3
3adant1
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
1
B
∈
ℂ
5
2
4
mulcomd
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
⁢
1
B
=
1
B
⁢
A
6
1
5
eqtrd
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
=
1
B
⁢
A