Theorem 1subrec1sub

Description: Subtract the reciprocal of 1 minus a number from 1 results in the number divided by the number minus 1. (Contributed by AV, 15-Feb-2023)

	Ref	Expression
Assertion	1subrec1sub	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-\left(\frac{1}{1-A}\right)=\frac{A}{A-1}$$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\in ℂ$$
2		simpl	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to A\in ℂ$$
3	1 2	subcld	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-A\in ℂ$$
4		simpr	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to A\ne 1$$
5	4	necomd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\ne A$$
6	1 2 5	subne0d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-A\ne 0$$
7	1 3 6	divcan4d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{1\left(1-A\right)}{1-A}=1$$
8	7	eqcomd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1=\frac{1\left(1-A\right)}{1-A}$$
9	8	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-\left(\frac{1}{1-A}\right)=\left(\frac{1\left(1-A\right)}{1-A}\right)-\left(\frac{1}{1-A}\right)$$
10	1 3	mulcld	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\left(1-A\right)\in ℂ$$
11	10 1 3 6	divsubdird	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{1\left(1-A\right)-1}{1-A}=\left(\frac{1\left(1-A\right)}{1-A}\right)-\left(\frac{1}{1-A}\right)$$
12	3	mulid2d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\left(1-A\right)=1-A$$
13	12	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\left(1-A\right)-1=1-A-1$$
14		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
15	14	adantr	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to -A\in ℂ$$
16	1 2	negsubd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1+\left(-A\right)=1-A$$
17	16	eqcomd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-A=1+\left(-A\right)$$
18	1 15 17	mvrladdd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-A-1=-A$$
19	13 18	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1\left(1-A\right)-1=-A$$
20	19	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{1\left(1-A\right)-1}{1-A}=\frac{-A}{1-A}$$
21	2 3 6	divneg2d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to -\frac{A}{1-A}=\frac{A}{-\left(1-A\right)}$$
22	2 3 6	divnegd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to -\frac{A}{1-A}=\frac{-A}{1-A}$$
23	1 2	negsubdi2d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to -\left(1-A\right)=A-1$$
24	23	oveq2d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{A}{-\left(1-A\right)}=\frac{A}{A-1}$$
25	21 22 24	3eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{-A}{1-A}=\frac{A}{A-1}$$
26	20 25	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to \frac{1\left(1-A\right)-1}{1-A}=\frac{A}{A-1}$$
27	9 11 26	3eqtr2d	$$⊢\left(A\in ℂ\wedge A\ne 1\right)\to 1-\left(\frac{1}{1-A}\right)=\frac{A}{A-1}$$