expmulz - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > expmulz		Structured version Unicode version

Theorem expmulz 12115

Description: Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 7-Jul-2014.)

**Assertion**
Ref	Expression
expmulz	$/\$ $/\$ $/\$

**Proof of Theorem expmulz**
Step	Hyp	Ref	Expression
1		elznn0nn 10795	. . 3 $\/$ $/\$
2		elznn0nn 10795	. . . 4 $\/$ $/\$
3		expmul 12114	. . . . . . . 8 $/\$ $/\$
4	3	3expia 1196	. . . . . . 7 $/\$
5	4	adantlr 712	. . . . . 6 $/\$ $/\$
6		simp2l 1020	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
7	6	recnd 9533	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
8		simp3 996	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	8	nn0cnd 10771	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
10	7, 9	mulneg1d 9927	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
11	10	oveq2d 6212	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
12		simp1l 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
13		simp2r 1021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
14	13	nnnn0d 10769	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
15		expmul 12114	. . . . . . . . . . . 12 $/\$ $/\$
16	12, 14, 8, 15	syl3anc 1226	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	11, 16	eqtr3d 2425	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	17	oveq2d 6212	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19		expcl 12087	. . . . . . . . . . 11 $/\$
20	12, 14, 19	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
21		simp1r 1019	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
22	13	nnzd 10883	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
23		expne0i 12101	. . . . . . . . . . 11 $/\$ $/\$
24	12, 21, 22, 23	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
25	8	nn0zd 10882	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
26		exprec 12110	. . . . . . . . . 10 $/\$ $/\$
27	20, 24, 25, 26	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	18, 27	eqtr4d 2426	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
29	7, 9	mulcld 9527	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	14, 8	nn0mulcld 10774	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
31	10, 30	eqeltrrd 2471	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
32		expneg2 12078	. . . . . . . . 9 $/\$ $/\$
33	12, 29, 31, 32	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
34		expneg2 12078	. . . . . . . . . 10 $/\$ $/\$
35	12, 7, 14, 34	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
36	35	oveq1d 6211	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
37	28, 33, 36	3eqtr4d 2433	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	37	3expia 1196	. . . . . 6 $/\$ $/\$ $/\$
39	5, 38	jaodan 783	. . . . 5 $/\$ $/\$ $\/$ $/\$
40		simp2 995	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
41	40	nn0cnd 10771	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
42		simp3l 1022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
43	42	recnd 9533	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
44	41, 43	mulneg2d 9928	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
45	44	oveq2d 6212	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
46		simp1l 1018	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
47		simp3r 1023	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	47	nnnn0d 10769	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
49		expmul 12114	. . . . . . . . . . 11 $/\$ $/\$
50	46, 40, 48, 49	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	45, 50	eqtr3d 2425	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
52	51	oveq2d 6212	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
53	41, 43	mulcld 9527	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
54	40, 48	nn0mulcld 10774	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
55	44, 54	eqeltrrd 2471	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
56	46, 53, 55, 32	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
57		expcl 12087	. . . . . . . . . 10 $/\$
58	46, 40, 57	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
59		expneg2 12078	. . . . . . . . 9 $/\$ $/\$
60	58, 43, 48, 59	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
61	52, 56, 60	3eqtr4d 2433	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
62	61	3expia 1196	. . . . . 6 $/\$ $/\$ $/\$
63		simp1l 1018	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
64		simp2l 1020	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	recnd 9533	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
66		simp2r 1021	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
67	66	nnnn0d 10769	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
68	63, 65, 67, 34	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
69	68	oveq1d 6211	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
70	63, 67, 19	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
71		simp1r 1019	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
72	66	nnzd 10883	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
73	63, 71, 72, 23	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
74	70, 73	reccld 10230	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3l 1022	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
76	75	recnd 9533	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
77		simp3r 1023	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
78	77	nnnn0d 10769	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
79		expneg2 12078	. . . . . . . . 9 $/\$ $/\$
80	74, 76, 78, 79	syl3anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
81	77	nnzd 10883	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
82		exprec 12110	. . . . . . . . . . 11 $/\$ $/\$
83	70, 73, 81, 82	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
84	83	oveq2d 6212	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
85		expcl 12087	. . . . . . . . . . 11 $/\$
86	70, 78, 85	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
87		expne0i 12101	. . . . . . . . . . 11 $/\$ $/\$
88	70, 73, 81, 87	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
89	86, 88	recrecd 10234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
90		expmul 12114	. . . . . . . . . . 11 $/\$ $/\$
91	63, 67, 78, 90	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
92	65, 76	mul2negd 9929	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	oveq2d 6212	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
94	91, 93	eqtr3d 2425	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
95	84, 89, 94	3eqtrd 2427	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
96	69, 80, 95	3eqtrrd 2428	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
97	96	3expia 1196	. . . . . 6 $/\$ $/\$ $/\$ $/\$
98	62, 97	jaodan 783	. . . . 5 $/\$ $/\$ $\/$ $/\$ $/\$
99	39, 98	jaod 378	. . . 4 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
100	2, 99	sylan2b 473	. . 3 $/\$ $/\$ $\/$ $/\$
101	1, 100	syl5bi 217	. 2 $/\$ $/\$
102	101	impr 617	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wne 2577 (class class class)co 6196

cc 9401

cr 9402

cc0 9403

c1 9404

cmul 9408

cneg 9719

cdiv 10123

cn 10452

cn0 10712

cz 10781

cexp 12069

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-2nd 6700 df-recs 6960 df-rdg 6994 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-n0 10713 df-z 10782 df-uz 11002 df-seq 12011 df-exp 12070

This theorem is referenced by: iexpcyc 12175 iseraltlem2 13507 iseraltlem3 13508 dvexp3 22464 cxpeq 23218 atantayl2 23385 basellem3 23473 lgseisenlem1 23741 lgseisenlem4 23744 lgsquadlem1 23746 lgsquad2lem1 23750 m1lgs 23754 jm2.21 31102 m1expevenALTV 32490 oexpnegnz 32520

W3C validator