Metamath Proof Explorer


Theorem 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 φ A
cxp111d.b φ B
cxp111d.c φ C
cxp111d.1 φ A 0
cxp111d.2 φ B 0
cxp111d.3 φ C 0
Assertion cxp111d φ A C = B C n log A = log B + i 2 π n C

Proof

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