Metamath Proof Explorer


Theorem lcmineqlem5

Description: Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem5.1 φ A
lcmineqlem5.2 φ B
lcmineqlem5.3 φ C
lcmineqlem5.4 φ C 0
Assertion lcmineqlem5 φ A B 1 C = B A C

Proof

Step Hyp Ref Expression
1 lcmineqlem5.1 φ A
2 lcmineqlem5.2 φ B
3 lcmineqlem5.3 φ C
4 lcmineqlem5.4 φ C 0
5 3 4 reccld φ 1 C
6 1 2 5 mulassd φ A B 1 C = A B 1 C
7 1 2 mulcomd φ A B = B A
8 7 oveq1d φ A B 1 C = B A 1 C
9 6 8 eqtr3d φ A B 1 C = B A 1 C
10 2 1 5 mulassd φ B A 1 C = B A 1 C
11 9 10 eqtrd φ A B 1 C = B A 1 C
12 1 3 4 divrecd φ A C = A 1 C
13 12 oveq2d φ B A C = B A 1 C
14 11 13 eqtr4d φ A B 1 C = B A C