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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 − ( 1 / ( 1 − 𝐴 ) ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → 1 ∈ ℂ )
2 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
3 1 2 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ∈ ℂ )
4 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
5 4 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → 1 ≠ 𝐴 )
6 1 2 5 subne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ≠ 0 )
7 1 3 6 divcan4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( 1 · ( 1 − 𝐴 ) ) / ( 1 − 𝐴 ) ) = 1 )
8 7 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → 1 = ( ( 1 · ( 1 − 𝐴 ) ) / ( 1 − 𝐴 ) ) )
9 8 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 − ( 1 / ( 1 − 𝐴 ) ) ) = ( ( ( 1 · ( 1 − 𝐴 ) ) / ( 1 − 𝐴 ) ) − ( 1 / ( 1 − 𝐴 ) ) ) )
10 1 3 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 · ( 1 − 𝐴 ) ) ∈ ℂ )
11 10 1 3 6 divsubdird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( ( 1 · ( 1 − 𝐴 ) ) − 1 ) / ( 1 − 𝐴 ) ) = ( ( ( 1 · ( 1 − 𝐴 ) ) / ( 1 − 𝐴 ) ) − ( 1 / ( 1 − 𝐴 ) ) ) )
12 3 mullidd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 · ( 1 − 𝐴 ) ) = ( 1 − 𝐴 ) )
13 12 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( 1 · ( 1 − 𝐴 ) ) − 1 ) = ( ( 1 − 𝐴 ) − 1 ) )
14 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → - 𝐴 ∈ ℂ )
16 1 2 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 + - 𝐴 ) = ( 1 − 𝐴 ) )
17 1 15 16 mvlladdcd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) − 1 ) = - 𝐴 )
18 13 17 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( 1 · ( 1 − 𝐴 ) ) − 1 ) = - 𝐴 )
19 18 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( ( 1 · ( 1 − 𝐴 ) ) − 1 ) / ( 1 − 𝐴 ) ) = ( - 𝐴 / ( 1 − 𝐴 ) ) )
20 2 3 6 divneg2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → - ( 𝐴 / ( 1 − 𝐴 ) ) = ( 𝐴 / - ( 1 − 𝐴 ) ) )
21 2 3 6 divnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → - ( 𝐴 / ( 1 − 𝐴 ) ) = ( - 𝐴 / ( 1 − 𝐴 ) ) )
22 1 2 negsubdi2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → - ( 1 − 𝐴 ) = ( 𝐴 − 1 ) )
23 22 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 𝐴 / - ( 1 − 𝐴 ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
24 20 21 23 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
25 19 24 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( ( ( 1 · ( 1 − 𝐴 ) ) − 1 ) / ( 1 − 𝐴 ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
26 9 11 25 3eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 1 ) → ( 1 − ( 1 / ( 1 − 𝐴 ) ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )