cxp111d

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

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

Proof

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

Metamath Proof Explorer

Theorem cxp111d

Proof