Theorem recexpt 6526

Description: Nonnegative integer exponentiation of a reciprocal.

Assertion

Ref	Expression
recexpt	|- ((A e. CC /\ N e. NN0 /\ A =/= 0) -> ((1 / A)^N) = (1 / (A^N)))

Proof of Theorem recexpt

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . . 7 |- (j = 0 -> ((1 / A)^j) = ((1 / A)^0))
2		opreq2 3954	. . . . . . . 8 |- (j = 0 -> (A^j) = (A^0))
3	2	opreq2d 3961	. . . . . . 7 |- (j = 0 -> (1 / (A^j)) = (1 / (A^0)))
4	1, 3	eqeq12d 1481	. . . . . 6 |- (j = 0 -> (((1 / A)^j) = (1 / (A^j)) <-> ((1 / A)^0) = (1 / (A^0))))
5	4	imbi2d 610	. . . . 5 |- (j = 0 -> (((A e. CC /\ A =/= 0) -> ((1 / A)^j) = (1 / (A^j))) <-> ((A e. CC /\ A =/= 0) -> ((1 / A)^0) = (1 / (A^0)))))
6		opreq2 3954	. . . . . . 7 |- (j = k -> ((1 / A)^j) = ((1 / A)^k))
7		opreq2 3954	. . . . . . . 8 |- (j = k -> (A^j) = (A^k))
8	7	opreq2d 3961	. . . . . . 7 |- (j = k -> (1 / (A^j)) = (1 / (A^k)))
9	6, 8	eqeq12d 1481	. . . . . 6 |- (j = k -> (((1 / A)^j) = (1 / (A^j)) <-> ((1 / A)^k) = (1 / (A^k))))
10	9	imbi2d 610	. . . . 5 |- (j = k -> (((A e. CC /\ A =/= 0) -> ((1 / A)^j) = (1 / (A^j))) <-> ((A e. CC /\ A =/= 0) -> ((1 / A)^k) = (1 / (A^k)))))
11		opreq2 3954	. . . . . . 7 |- (j = (k + 1) -> ((1 / A)^j) = ((1 / A)^(k + 1)))
12		opreq2 3954	. . . . . . . 8 |- (j = (k + 1) -> (A^j) = (A^(k + 1)))
13	12	opreq2d 3961	. . . . . . 7 |- (j = (k + 1) -> (1 / (A^j)) = (1 / (A^(k + 1))))
14	11, 13	eqeq12d 1481	. . . . . 6 |- (j = (k + 1) -> (((1 / A)^j) = (1 / (A^j)) <-> ((1 / A)^(k + 1)) = (1 / (A^(k + 1)))))
15	14	imbi2d 610	. . . . 5 |- (j = (k + 1) -> (((A e. CC /\ A =/= 0) -> ((1 / A)^j) = (1 / (A^j))) <-> ((A e. CC /\ A =/= 0) -> ((1 / A)^(k + 1)) = (1 / (A^(k + 1))))))
16		opreq2 3954	. . . . . . 7 |- (j = N -> ((1 / A)^j) = ((1 / A)^N))
17		opreq2 3954	. . . . . . . 8 |- (j = N -> (A^j) = (A^N))
18	17	opreq2d 3961	. . . . . . 7 |- (j = N -> (1 / (A^j)) = (1 / (A^N)))
19	16, 18	eqeq12d 1481	. . . . . 6 |- (j = N -> (((1 / A)^j) = (1 / (A^j)) <-> ((1 / A)^N) = (1 / (A^N))))
20	19	imbi2d 610	. . . . 5 |- (j = N -> (((A e. CC /\ A =/= 0) -> ((1 / A)^j) = (1 / (A^j))) <-> ((A e. CC /\ A =/= 0) -> ((1 / A)^N) = (1 / (A^N)))))
21		recclt 5684	. . . . . . 7 |- ((A e. CC /\ A =/= 0) -> (1 / A) e. CC)
22		exp0t 6503	. . . . . . 7 |- ((1 / A) e. CC -> ((1 / A)^0) = 1)
23	21, 22	syl 10	. . . . . 6 |- ((A e. CC /\ A =/= 0) -> ((1 / A)^0) = 1)
24		exp0t 6503	. . . . . . . . 9 |- (A e. CC -> (A^0) = 1)
25	24	opreq2d 3961	. . . . . . . 8 |- (A e. CC -> (1 / (A^0)) = (1 / 1))
26		ax1cn 5241	. . . . . . . . 9 |- 1 e. CC
27	26	div1 5728	. . . . . . . 8 |- (1 / 1) = 1
28	25, 27	syl6eq 1515	. . . . . . 7 |- (A e. CC -> (1 / (A^0)) = 1)
29	28	adantr 389	. . . . . 6 |- ((A e. CC /\ A =/= 0) -> (1 / (A^0)) = 1)
30	23, 29	eqtr4d 1502	. . . . 5 |- ((A e. CC /\ A =/= 0) -> ((1 / A)^0) = (1 / (A^0)))
31		opreq1 3953	. . . . . . . . . . 11 |- (((1 / A)^k) = (1 / (A^k)) -> (((1 / A)^k) x. (1 / A)) = ((1 / (A^k)) x. (1 / A)))
32	31	ad2antll 407	. . . . . . . . . 10 |- (((A e. CC /\ k e. NN0) /\ (A =/= 0 /\ ((1 / A)^k) = (1 / (A^k)))) -> (((1 / A)^k) x. (1 / A)) = ((1 / (A^k)) x. (1 / A)))
33		expp1t 6506	. . . . . . . . . . . . 13 |- (((1 / A) e. CC /\ k e. NN0) -> ((1 / A)^(k + 1)) = (((1 / A)^k) x. (1 / A)))
34	33, 21	sylan 448	. . . . . . . . . . . 12 |- (((A e. CC /\ A =/= 0) /\ k e. NN0) -> ((1 / A)^(k + 1)) = (((1 / A)^k) x. (1 / A)))
35	34	an1rs 488	. . . . . . . . . . 11 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> ((1 / A)^(k + 1)) = (((1 / A)^k) x. (1 / A)))
36	35	adantrr 395	. . . . . . . . . 10 |- (((A e. CC /\ k e. NN0) /\ (A =/= 0 /\ ((1 / A)^k) = (1 / (A^k)))) -> ((1 / A)^(k + 1)) = (((1 / A)^k) x. (1 / A)))
37		expp1t 6506	. . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
38	37	opreq2d 3961	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. NN0) -> (1 / (A^(k + 1))) = (1 / ((A^k) x. A)))
39	38	adantr 389	. . . . . . . . . . . 12 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> (1 / (A^(k + 1))) = (1 / ((A^k) x. A)))
40		divmuldivt 5736	. . . . . . . . . . . . . 14 |- ((((1 e. CC /\ (A^k) e. CC) /\ (1 e. CC /\ A e. CC)) /\ ((A^k) =/= 0 /\ A =/= 0)) -> ((1 / (A^k)) x. (1 / A)) = ((1 x. 1) / ((A^k) x. A)))
41		expclt 6513	. . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
42	41, 26	jctil 292	. . . . . . . . . . . . . . . 16 |- ((A e. CC /\ k e. NN0) -> (1 e. CC /\ (A^k) e. CC))
43		pm3.26 319	. . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ k e. NN0) -> A e. CC)
44	43, 26	jctil 292	. . . . . . . . . . . . . . . 16 |- ((A e. CC /\ k e. NN0) -> (1 e. CC /\ A e. CC))
45	42, 44	jca 288	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ k e. NN0) -> ((1 e. CC /\ (A^k) e. CC) /\ (1 e. CC /\ A e. CC)))
46	45	adantr 389	. . . . . . . . . . . . . 14 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> ((1 e. CC /\ (A^k) e. CC) /\ (1 e. CC /\ A e. CC)))
47		expne0it 6519	. . . . . . . . . . . . . . . 16 |- ((A e. CC /\ k e. NN0 /\ A =/= 0) -> (A^k) =/= 0)
48	47	3expa 831	. . . . . . . . . . . . . . 15 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> (A^k) =/= 0)
49		pm3.27 323	. . . . . . . . . . . . . . 15 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> A =/= 0)
50	48, 49	jca 288	. . . . . . . . . . . . . 14 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> ((A^k) =/= 0 /\ A =/= 0))
51	40, 46, 50	sylanc 471	. . . . . . . . . . . . 13 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> ((1 / (A^k)) x. (1 / A)) = ((1 x. 1) / ((A^k) x. A)))
52	26	mulid1 5304	. . . . . . . . . . . . . 14 |- (1 x. 1) = 1
53	52	opreq1i 3956	. . . . . . . . . . . . 13 |- ((1 x. 1) / ((A^k) x. A)) = (1 / ((A^k) x. A))
54	51, 53	syl6req 1516	. . . . . . . . . . . 12 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> (1 / ((A^k) x. A)) = ((1 / (A^k)) x. (1 / A)))
55	39, 54	eqtrd 1499	. . . . . . . . . . 11 |- (((A e. CC /\ k e. NN0) /\ A =/= 0) -> (1 / (A^(k + 1))) = ((1 / (A^k)) x. (1 / A)))
56	55</