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 · π ) ) · 𝑛 ) / 𝐶 ) ) ) )