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 e. CC /\ A =/= 1 ) -> ( 1 - ( 1 / ( 1 - A ) ) ) = ( A / ( A - 1 ) ) )

Proof

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