Metamath Proof Explorer


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 AA1111A=AA1

Proof

Step Hyp Ref Expression
1 1cnd AA11
2 simpl AA1A
3 1 2 subcld AA11A
4 simpr AA1A1
5 4 necomd AA11A
6 1 2 5 subne0d AA11A0
7 1 3 6 divcan4d AA111A1A=1
8 7 eqcomd AA11=11A1A
9 8 oveq1d AA1111A=11A1A11A
10 1 3 mulcld AA111A
11 10 1 3 6 divsubdird AA111A11A=11A1A11A
12 3 mulid2d AA111A=1A
13 12 oveq1d AA111A1=1-A-1
14 negcl AA
15 14 adantr AA1A
16 1 2 negsubd AA11+A=1A
17 16 eqcomd AA11A=1+A
18 1 15 17 mvrladdd AA11-A-1=A
19 13 18 eqtrd AA111A1=A
20 19 oveq1d AA111A11A=A1A
21 2 3 6 divneg2d AA1A1A=A1A
22 2 3 6 divnegd AA1A1A=A1A
23 1 2 negsubdi2d AA11A=A1
24 23 oveq2d AA1A1A=AA1
25 21 22 24 3eqtr3d AA1A1A=AA1
26 20 25 eqtrd AA111A11A=AA1
27 9 11 26 3eqtr2d AA1111A=AA1