# Metamath Proof Explorer

## Theorem mulcxplem

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

Ref Expression
Hypotheses mulcxp.1
`|- ( ph -> A e. CC )`
mulcxp.2
`|- ( ph -> C e. CC )`
Assertion mulcxplem
`|- ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )`

### Proof

Step Hyp Ref Expression
1 mulcxp.1
` |-  ( ph -> A e. CC )`
2 mulcxp.2
` |-  ( ph -> C e. CC )`
3 oveq2
` |-  ( C = 0 -> ( 0 ^c C ) = ( 0 ^c 0 ) )`
4 0cn
` |-  0 e. CC`
5 cxp0
` |-  ( 0 e. CC -> ( 0 ^c 0 ) = 1 )`
6 4 5 ax-mp
` |-  ( 0 ^c 0 ) = 1`
7 3 6 eqtrdi
` |-  ( C = 0 -> ( 0 ^c C ) = 1 )`
8 oveq2
` |-  ( C = 0 -> ( A ^c C ) = ( A ^c 0 ) )`
9 8 7 oveq12d
` |-  ( C = 0 -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c 0 ) x. 1 ) )`
10 7 9 eqeq12d
` |-  ( C = 0 -> ( ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) <-> 1 = ( ( A ^c 0 ) x. 1 ) ) )`
11 cxpcl
` |-  ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC )`
12 1 2 11 syl2anc
` |-  ( ph -> ( A ^c C ) e. CC )`
` |-  ( ( ph /\ C =/= 0 ) -> ( A ^c C ) e. CC )`
14 13 mul01d
` |-  ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. 0 ) = 0 )`
15 0cxp
` |-  ( ( C e. CC /\ C =/= 0 ) -> ( 0 ^c C ) = 0 )`
16 2 15 sylan
` |-  ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = 0 )`
17 16 oveq2d
` |-  ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c C ) x. 0 ) )`
18 14 17 16 3eqtr4rd
` |-  ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )`
19 cxp0
` |-  ( A e. CC -> ( A ^c 0 ) = 1 )`
20 1 19 syl
` |-  ( ph -> ( A ^c 0 ) = 1 )`
21 20 oveq1d
` |-  ( ph -> ( ( A ^c 0 ) x. 1 ) = ( 1 x. 1 ) )`
22 1t1e1
` |-  ( 1 x. 1 ) = 1`
23 21 22 eqtr2di
` |-  ( ph -> 1 = ( ( A ^c 0 ) x. 1 ) )`
24 10 18 23 pm2.61ne
` |-  ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )`