Metamath Proof Explorer


Theorem mulexpz

Description: Integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion mulexpz A A 0 B B 0 N A B N = A N B N

Proof

Step Hyp Ref Expression
1 elznn0nn N N 0 N N
2 simpl A A 0 A
3 simpl B B 0 B
4 2 3 anim12i A A 0 B B 0 A B
5 mulexp A B N 0 A B N = A N B N
6 5 3expa A B N 0 A B N = A N B N
7 4 6 sylan A A 0 B B 0 N 0 A B N = A N B N
8 simplll A A 0 B B 0 N N A
9 simplrl A A 0 B B 0 N N B
10 8 9 mulcld A A 0 B B 0 N N A B
11 recn N N
12 11 ad2antrl A A 0 B B 0 N N N
13 nnnn0 N N 0
14 13 ad2antll A A 0 B B 0 N N N 0
15 expneg2 A B N N 0 A B N = 1 A B N
16 10 12 14 15 syl3anc A A 0 B B 0 N N A B N = 1 A B N
17 expneg2 A N N 0 A N = 1 A N
18 8 12 14 17 syl3anc A A 0 B B 0 N N A N = 1 A N
19 expneg2 B N N 0 B N = 1 B N
20 9 12 14 19 syl3anc A A 0 B B 0 N N B N = 1 B N
21 18 20 oveq12d A A 0 B B 0 N N A N B N = 1 A N 1 B N
22 mulexp A B N 0 A B N = A N B N
23 8 9 14 22 syl3anc A A 0 B B 0 N N A B N = A N B N
24 23 oveq2d A A 0 B B 0 N N 1 A B N = 1 A N B N
25 1t1e1 1 1 = 1
26 25 oveq1i 1 1 A N B N = 1 A N B N
27 24 26 eqtr4di A A 0 B B 0 N N 1 A B N = 1 1 A N B N
28 expcl A N 0 A N
29 8 14 28 syl2anc A A 0 B B 0 N N A N
30 simpllr A A 0 B B 0 N N A 0
31 nnz N N
32 31 ad2antll A A 0 B B 0 N N N
33 expne0i A A 0 N A N 0
34 8 30 32 33 syl3anc A A 0 B B 0 N N A N 0
35 expcl B N 0 B N
36 9 14 35 syl2anc A A 0 B B 0 N N B N
37 simplrr A A 0 B B 0 N N B 0
38 expne0i B B 0 N B N 0
39 9 37 32 38 syl3anc A A 0 B B 0 N N B N 0
40 ax-1cn 1
41 divmuldiv 1 1 A N A N 0 B N B N 0 1 A N 1 B N = 1 1 A N B N
42 40 40 41 mpanl12 A N A N 0 B N B N 0 1 A N 1 B N = 1 1 A N B N
43 29 34 36 39 42 syl22anc A A 0 B B 0 N N 1 A N 1 B N = 1 1 A N B N
44 27 43 eqtr4d A A 0 B B 0 N N 1 A B N = 1 A N 1 B N
45 21 44 eqtr4d A A 0 B B 0 N N A N B N = 1 A B N
46 16 45 eqtr4d A A 0 B B 0 N N A B N = A N B N
47 7 46 jaodan A A 0 B B 0 N 0 N N A B N = A N B N
48 1 47 sylan2b A A 0 B B 0 N A B N = A N B N
49 48 3impa A A 0 B B 0 N A B N = A N B N