Metamath Proof Explorer


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

Proof

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