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 A A 1 1 1 1 A = A A 1

Proof

Step Hyp Ref Expression
1 1cnd A A 1 1
2 simpl A A 1 A
3 1 2 subcld A A 1 1 A
4 simpr A A 1 A 1
5 4 necomd A A 1 1 A
6 1 2 5 subne0d A A 1 1 A 0
7 1 3 6 divcan4d A A 1 1 1 A 1 A = 1
8 7 eqcomd A A 1 1 = 1 1 A 1 A
9 8 oveq1d A A 1 1 1 1 A = 1 1 A 1 A 1 1 A
10 1 3 mulcld A A 1 1 1 A
11 10 1 3 6 divsubdird A A 1 1 1 A 1 1 A = 1 1 A 1 A 1 1 A
12 3 mulid2d A A 1 1 1 A = 1 A
13 12 oveq1d A A 1 1 1 A 1 = 1 - A - 1
14 negcl A A
15 14 adantr A A 1 A
16 1 2 negsubd A A 1 1 + A = 1 A
17 16 eqcomd A A 1 1 A = 1 + A
18 1 15 17 mvrladdd A A 1 1 - A - 1 = A
19 13 18 eqtrd A A 1 1 1 A 1 = A
20 19 oveq1d A A 1 1 1 A 1 1 A = A 1 A
21 2 3 6 divneg2d A A 1 A 1 A = A 1 A
22 2 3 6 divnegd A A 1 A 1 A = A 1 A
23 1 2 negsubdi2d A A 1 1 A = A 1
24 23 oveq2d A A 1 A 1 A = A A 1
25 21 22 24 3eqtr3d A A 1 A 1 A = A A 1
26 20 25 eqtrd A A 1 1 1 A 1 1 A = A A 1
27 9 11 26 3eqtr2d A A 1 1 1 1 A = A A 1