Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Auxiliary theorems
divsub1dir
Next ⟩
expnegico01
Metamath Proof Explorer
Ascii
Unicode
Theorem
divsub1dir
Description:
Distribution of division over subtraction by 1.
(Contributed by
AV
, 6-Jun-2020)
Ref
Expression
Assertion
divsub1dir
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
−
1
=
A
−
B
B
Proof
Step
Hyp
Ref
Expression
1
3simpc
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
B
∈
ℂ
∧
B
≠
0
2
divid
⊢
B
∈
ℂ
∧
B
≠
0
→
B
B
=
1
3
1
2
syl
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
B
B
=
1
4
3
eqcomd
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
1
=
B
B
5
4
oveq2d
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
−
1
=
A
B
−
B
B
6
divsubdir
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
−
B
B
=
A
B
−
B
B
7
1
6
syld3an3
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
−
B
B
=
A
B
−
B
B
8
5
7
eqtr4d
⊢
A
∈
ℂ
∧
B
∈
ℂ
∧
B
≠
0
→
A
B
−
1
=
A
−
B
B