cxp112d

Description: General condition for complex exponentiation to be one-to-one with respect to the second argument. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	cxp112d.c	$⊢ φ \to C \in ℂ$
	cxp112d.a	$⊢ φ \to A \in ℂ$
	cxp112d.b	$⊢ φ \to B \in ℂ$
	cxp112d.0	$⊢ φ \to C \neq 0$
	cxp112d.1	$⊢ φ \to C \neq 1$
Assertion	cxp112d	$⊢ φ \to (C^{A} = C^{B} \leftrightarrow \exists n \in ℤ A = B + (\frac{i 2 π n}{\log C}))$

Proof

Step	Hyp	Ref	Expression
1		cxp112d.c	$⊢ φ \to C \in ℂ$
2		cxp112d.a	$⊢ φ \to A \in ℂ$
3		cxp112d.b	$⊢ φ \to B \in ℂ$
4		cxp112d.0	$⊢ φ \to C \neq 0$
5		cxp112d.1	$⊢ φ \to C \neq 1$
6	1 4 2	cxpefd	$⊢ φ \to C^{A} = e^{A \log C}$
7	1 4 3	cxpefd	$⊢ φ \to C^{B} = e^{B \log C}$
8	6 7	eqeq12d	$⊢ φ \to (C^{A} = C^{B} \leftrightarrow e^{A \log C} = e^{B \log C})$
9	1 4	logcld	$⊢ φ \to \log C \in ℂ$
10	2 9	mulcld	$⊢ φ \to A \log C \in ℂ$
11	3 9	mulcld	$⊢ φ \to B \log C \in ℂ$
12	10 11	ef11d	$⊢ φ \to (e^{A \log C} = e^{B \log C} \leftrightarrow \exists n \in ℤ A \log C = B \log C + i 2 π n)$
13	2	adantr	$⊢ (φ \land n \in ℤ) \to A \in ℂ$
14	9	adantr	$⊢ (φ \land n \in ℤ) \to \log C \in ℂ$
15	11	adantr	$⊢ (φ \land n \in ℤ) \to B \log C \in ℂ$
16		ax-icn	$⊢ i \in ℂ$
17		2cn	$⊢ 2 \in ℂ$
18		picn	$⊢ π \in ℂ$
19	17 18	mulcli	$⊢ 2 π \in ℂ$
20	16 19	mulcli	$⊢ i 2 π \in ℂ$
21	20	a1i	$⊢ (φ \land n \in ℤ) \to i 2 π \in ℂ$
22		zcn	$⊢ n \in ℤ \to n \in ℂ$
23	22	adantl	$⊢ (φ \land n \in ℤ) \to n \in ℂ$
24	21 23	mulcld	$⊢ (φ \land n \in ℤ) \to i 2 π n \in ℂ$
25	15 24	addcld	$⊢ (φ \land n \in ℤ) \to B \log C + i 2 π n \in ℂ$
26	1 4 5	logccne0d	$⊢ φ \to \log C \neq 0$
27	26	adantr	$⊢ (φ \land n \in ℤ) \to \log C \neq 0$
28	13 14 25 27	ldiv	$⊢ (φ \land n \in ℤ) \to (A \log C = B \log C + i 2 π n \leftrightarrow A = \frac{B \log C + i 2 π n}{\log C})$
29	15 24 14 27	divdird	$⊢ (φ \land n \in ℤ) \to \frac{B \log C + i 2 π n}{\log C} = (\frac{B \log C}{\log C}) + (\frac{i 2 π n}{\log C})$
30	3 9 26	divcan4d	$⊢ φ \to \frac{B \log C}{\log C} = B$
31	30	adantr	$⊢ (φ \land n \in ℤ) \to \frac{B \log C}{\log C} = B$
32	31	oveq1d	$⊢ (φ \land n \in ℤ) \to (\frac{B \log C}{\log C}) + (\frac{i 2 π n}{\log C}) = B + (\frac{i 2 π n}{\log C})$
33	29 32	eqtrd	$⊢ (φ \land n \in ℤ) \to \frac{B \log C + i 2 π n}{\log C} = B + (\frac{i 2 π n}{\log C})$
34	33	eqeq2d	$⊢ (φ \land n \in ℤ) \to (A = \frac{B \log C + i 2 π n}{\log C} \leftrightarrow A = B + (\frac{i 2 π n}{\log C}))$
35	28 34	bitrd	$⊢ (φ \land n \in ℤ) \to (A \log C = B \log C + i 2 π n \leftrightarrow A = B + (\frac{i 2 π n}{\log C}))$
36	35	rexbidva	$⊢ φ \to (\exists n \in ℤ A \log C = B \log C + i 2 π n \leftrightarrow \exists n \in ℤ A = B + (\frac{i 2 π n}{\log C}))$
37	8 12 36	3bitrd	$⊢ φ \to (C^{A} = C^{B} \leftrightarrow \exists n \in ℤ A = B + (\frac{i 2 π n}{\log C}))$

Metamath Proof Explorer

Theorem cxp112d

Proof