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

Proof

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