Metamath Proof Explorer


Theorem mulcxplem

Description: Lemma for mulcxp . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Hypotheses mulcxp.1 φ A
mulcxp.2 φ C
Assertion mulcxplem φ 0 C = A C 0 C

Proof

Step Hyp Ref Expression
1 mulcxp.1 φ A
2 mulcxp.2 φ C
3 oveq2 C = 0 0 C = 0 0
4 0cn 0
5 cxp0 0 0 0 = 1
6 4 5 ax-mp 0 0 = 1
7 3 6 syl6eq C = 0 0 C = 1
8 oveq2 C = 0 A C = A 0
9 8 7 oveq12d C = 0 A C 0 C = A 0 1
10 7 9 eqeq12d C = 0 0 C = A C 0 C 1 = A 0 1
11 cxpcl A C A C
12 1 2 11 syl2anc φ A C
13 12 adantr φ C 0 A C
14 13 mul01d φ C 0 A C 0 = 0
15 0cxp C C 0 0 C = 0
16 2 15 sylan φ C 0 0 C = 0
17 16 oveq2d φ C 0 A C 0 C = A C 0
18 14 17 16 3eqtr4rd φ C 0 0 C = A C 0 C
19 cxp0 A A 0 = 1
20 1 19 syl φ A 0 = 1
21 20 oveq1d φ A 0 1 = 1 1
22 1t1e1 1 1 = 1
23 21 22 syl6req φ 1 = A 0 1
24 10 18 23 pm2.61ne φ 0 C = A C 0 C