Metamath Proof Explorer


Theorem remulcan2d

Description: mulcan2d for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023)

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

Proof

Step Hyp Ref Expression
1 remulcan2d.1 φ A
2 remulcan2d.2 φ B
3 remulcan2d.3 φ C
4 remulcan2d.4 φ C 0
5 ax-rrecex C C 0 x C x = 1
6 3 4 5 syl2anc φ x C x = 1
7 oveq1 A C = B C A C x = B C x
8 1 adantr φ x C x = 1 A
9 8 recnd φ x C x = 1 A
10 3 adantr φ x C x = 1 C
11 10 recnd φ x C x = 1 C
12 simprl φ x C x = 1 x
13 12 recnd φ x C x = 1 x
14 9 11 13 mulassd φ x C x = 1 A C x = A C x
15 simprr φ x C x = 1 C x = 1
16 15 oveq2d φ x C x = 1 A C x = A 1
17 ax-1rid A A 1 = A
18 8 17 syl φ x C x = 1 A 1 = A
19 14 16 18 3eqtrd φ x C x = 1 A C x = A
20 2 adantr φ x C x = 1 B
21 20 recnd φ x C x = 1 B
22 21 11 13 mulassd φ x C x = 1 B C x = B C x
23 15 oveq2d φ x C x = 1 B C x = B 1
24 ax-1rid B B 1 = B
25 20 24 syl φ x C x = 1 B 1 = B
26 22 23 25 3eqtrd φ x C x = 1 B C x = B
27 19 26 eqeq12d φ x C x = 1 A C x = B C x A = B
28 7 27 syl5ib φ x C x = 1 A C = B C A = B
29 6 28 rexlimddv φ A C = B C A = B
30 oveq1 A = B A C = B C
31 29 30 impbid1 φ A C = B C A = B