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 ‘ 𝐶 ) ) ) ) )