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 ( 𝜑𝐶 ∈ ℂ )
cxp112d.a ( 𝜑𝐴 ∈ ℂ )
cxp112d.b ( 𝜑𝐵 ∈ ℂ )
cxp112d.0 ( 𝜑𝐶 ≠ 0 )
cxp112d.1 ( 𝜑𝐶 ≠ 1 )
Assertion cxp112d ( 𝜑 → ( ( 𝐶𝑐 𝐴 ) = ( 𝐶𝑐 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cxp112d.c ( 𝜑𝐶 ∈ ℂ )
2 cxp112d.a ( 𝜑𝐴 ∈ ℂ )
3 cxp112d.b ( 𝜑𝐵 ∈ ℂ )
4 cxp112d.0 ( 𝜑𝐶 ≠ 0 )
5 cxp112d.1 ( 𝜑𝐶 ≠ 1 )
6 1 4 2 cxpefd ( 𝜑 → ( 𝐶𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝐶 ) ) ) )
7 1 4 3 cxpefd ( 𝜑 → ( 𝐶𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐶 ) ) ) )
8 6 7 eqeq12d ( 𝜑 → ( ( 𝐶𝑐 𝐴 ) = ( 𝐶𝑐 𝐵 ) ↔ ( exp ‘ ( 𝐴 · ( log ‘ 𝐶 ) ) ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐶 ) ) ) ) )
9 1 4 logcld ( 𝜑 → ( log ‘ 𝐶 ) ∈ ℂ )
10 2 9 mulcld ( 𝜑 → ( 𝐴 · ( log ‘ 𝐶 ) ) ∈ ℂ )
11 3 9 mulcld ( 𝜑 → ( 𝐵 · ( log ‘ 𝐶 ) ) ∈ ℂ )
12 10 11 ef11d ( 𝜑 → ( ( exp ‘ ( 𝐴 · ( log ‘ 𝐶 ) ) ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐶 ) ) ) ↔ ∃ 𝑛 ∈ ℤ ( 𝐴 · ( log ‘ 𝐶 ) ) = ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
13 2 adantr ( ( 𝜑𝑛 ∈ ℤ ) → 𝐴 ∈ ℂ )
14 9 adantr ( ( 𝜑𝑛 ∈ ℤ ) → ( log ‘ 𝐶 ) ∈ ℂ )
15 11 adantr ( ( 𝜑𝑛 ∈ ℤ ) → ( 𝐵 · ( log ‘ 𝐶 ) ) ∈ ℂ )
16 ax-icn i ∈ ℂ
17 2cn 2 ∈ ℂ
18 picn π ∈ ℂ
19 17 18 mulcli ( 2 · π ) ∈ ℂ
20 16 19 mulcli ( i · ( 2 · π ) ) ∈ ℂ
21 20 a1i ( ( 𝜑𝑛 ∈ ℤ ) → ( i · ( 2 · π ) ) ∈ ℂ )
22 zcn ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
23 22 adantl ( ( 𝜑𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
24 21 23 mulcld ( ( 𝜑𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
25 15 24 addcld ( ( 𝜑𝑛 ∈ ℤ ) → ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ∈ ℂ )
26 1 4 5 logccne0d ( 𝜑 → ( log ‘ 𝐶 ) ≠ 0 )
27 26 adantr ( ( 𝜑𝑛 ∈ ℤ ) → ( log ‘ 𝐶 ) ≠ 0 )
28 13 14 25 27 ldiv ( ( 𝜑𝑛 ∈ ℤ ) → ( ( 𝐴 · ( log ‘ 𝐶 ) ) = ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ 𝐴 = ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) / ( log ‘ 𝐶 ) ) ) )
29 15 24 14 27 divdird ( ( 𝜑𝑛 ∈ ℤ ) → ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) / ( log ‘ 𝐶 ) ) = ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐶 ) ) + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) )
30 3 9 26 divcan4d ( 𝜑 → ( ( 𝐵 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐶 ) ) = 𝐵 )
31 30 adantr ( ( 𝜑𝑛 ∈ ℤ ) → ( ( 𝐵 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐶 ) ) = 𝐵 )
32 31 oveq1d ( ( 𝜑𝑛 ∈ ℤ ) → ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐶 ) ) + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) )
33 29 32 eqtrd ( ( 𝜑𝑛 ∈ ℤ ) → ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) / ( log ‘ 𝐶 ) ) = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) )
34 33 eqeq2d ( ( 𝜑𝑛 ∈ ℤ ) → ( 𝐴 = ( ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) / ( log ‘ 𝐶 ) ) ↔ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) ) )
35 28 34 bitrd ( ( 𝜑𝑛 ∈ ℤ ) → ( ( 𝐴 · ( log ‘ 𝐶 ) ) = ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) ) )
36 35 rexbidva ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( 𝐴 · ( log ‘ 𝐶 ) ) = ( ( 𝐵 · ( log ‘ 𝐶 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) ) )
37 8 12 36 3bitrd ( 𝜑 → ( ( 𝐶𝑐 𝐴 ) = ( 𝐶𝑐 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ 𝐶 ) ) ) ) )