Theorem cxpi11d

Description: _i to the powers of A and B are equal iff A and B are a multiple of 4 apart. EDITORIAL: This theorem may be revised to a more convenient form. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	cxpi11d.a	$$⊢\phi \to A\in ℂ$$
	cxpi11d.b	$$⊢\phi \to B\in ℂ$$
Assertion	cxpi11d	$$⊢\phi \to \left({\mathrm{i}}^A={\mathrm{i}}^B\leftrightarrow \exists n\in \mathbb{Z}A=B+4n\right)$$

Proof

Step	Hyp	Ref	Expression
1		cxpi11d.a	$$⊢\phi \to A\in ℂ$$
2		cxpi11d.b	$$⊢\phi \to B\in ℂ$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4	3	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
5		ine0	$$⊢\mathrm{i}\ne 0$$
6	5	a1i	$$⊢\phi \to \mathrm{i}\ne 0$$
7		ine1	$$⊢\mathrm{i}\ne 1$$
8	7	a1i	$$⊢\phi \to \mathrm{i}\ne 1$$
9	4 1 2 6 8	cxp112d	$$⊢\phi \to \left({\mathrm{i}}^A={\mathrm{i}}^B\leftrightarrow \exists n\in \mathbb{Z}A=B+\left(\frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}\right)\right)$$
10		2cn	$$⊢2\in ℂ$$
11		picn	$$⊢\mathrm{\pi }\in ℂ$$
12	10 11	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
13	3 12	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
14	13	a1i	$$⊢n\in \mathbb{Z}\to \mathrm{i}2\mathrm{\pi }\in ℂ$$
15		zcn	$$⊢n\in \mathbb{Z}\to n\in ℂ$$
16		logcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \log \mathrm{i}\in ℂ$$
17	3 5 16	mp2an	$$⊢\log \mathrm{i}\in ℂ$$
18	17	a1i	$$⊢n\in \mathbb{Z}\to \log \mathrm{i}\in ℂ$$
19		logccne0	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge \mathrm{i}\ne 1\right)\to \log \mathrm{i}\ne 0$$
20	3 5 7 19	mp3an	$$⊢\log \mathrm{i}\ne 0$$
21	20	a1i	$$⊢n\in \mathbb{Z}\to \log \mathrm{i}\ne 0$$
22	14 15 18 21	div23d	$$⊢n\in \mathbb{Z}\to \frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}=\left(\frac{\mathrm{i}2\mathrm{\pi }}{\log \mathrm{i}}\right)n$$
23		logi	$$⊢\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
24	23	oveq2i	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{\log \mathrm{i}}=\frac{\mathrm{i}2\mathrm{\pi }}{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}$$
25	12	a1i	$$⊢\top \to 2\mathrm{\pi }\in ℂ$$
26		2ne0	$$⊢2\ne 0$$
27	11 10 26	divcli	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
28	27	a1i	$$⊢\top \to \frac{\mathrm{\pi }}{2}\in ℂ$$
29	3	a1i	$$⊢\top \to \mathrm{i}\in ℂ$$
30		pine0	$$⊢\mathrm{\pi }\ne 0$$
31	11 10 30 26	divne0i	$$⊢\frac{\mathrm{\pi }}{2}\ne 0$$
32	31	a1i	$$⊢\top \to \frac{\mathrm{\pi }}{2}\ne 0$$
33	5	a1i	$$⊢\top \to \mathrm{i}\ne 0$$
34	25 28 29 32 33	divcan5d	$$⊢\top \to \frac{\mathrm{i}2\mathrm{\pi }}{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\frac{2\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}$$
35	34	mptru	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\frac{2\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}$$
36	10 11 27 31	divassi	$$⊢\frac{2\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}=2\left(\frac{\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}\right)$$
37	11	a1i	$$⊢\top \to \mathrm{\pi }\in ℂ$$
38		2cnd	$$⊢\top \to 2\in ℂ$$
39	30	a1i	$$⊢\top \to \mathrm{\pi }\ne 0$$
40	26	a1i	$$⊢\top \to 2\ne 0$$
41	37 38 39 40	ddcand	$$⊢\top \to \frac{\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}=2$$
42	41	mptru	$$⊢\frac{\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}=2$$
43	42	oveq2i	$$⊢2\left(\frac{\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}\right)=2\cdot 2$$
44		2t2e4	$$⊢2\cdot 2=4$$
45	36 43 44	3eqtri	$$⊢\frac{2\mathrm{\pi }}{\frac{\mathrm{\pi }}{2}}=4$$
46	24 35 45	3eqtri	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{\log \mathrm{i}}=4$$
47	46	oveq1i	$$⊢\left(\frac{\mathrm{i}2\mathrm{\pi }}{\log \mathrm{i}}\right)n=4n$$
48	22 47	eqtrdi	$$⊢n\in \mathbb{Z}\to \frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}=4n$$
49	48	oveq2d	$$⊢n\in \mathbb{Z}\to B+\left(\frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}\right)=B+4n$$
50	49	eqeq2d	$$⊢n\in \mathbb{Z}\to \left(A=B+\left(\frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}\right)\leftrightarrow A=B+4n\right)$$
51	50	rexbiia	$$⊢\exists n\in \mathbb{Z}A=B+\left(\frac{\mathrm{i}2\mathrm{\pi }n}{\log \mathrm{i}}\right)\leftrightarrow \exists n\in \mathbb{Z}A=B+4n$$
52	9 51	bitrdi	$$⊢\phi \to \left({\mathrm{i}}^A={\mathrm{i}}^B\leftrightarrow \exists n\in \mathbb{Z}A=B+4n\right)$$