Metamath Proof Explorer


Theorem ef11d

Description: General condition for the exponential function to be one-to-one. efper shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses ef11d.a ( 𝜑𝐴 ∈ ℂ )
ef11d.b ( 𝜑𝐵 ∈ ℂ )
Assertion ef11d ( 𝜑 → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 ef11d.a ( 𝜑𝐴 ∈ ℂ )
2 ef11d.b ( 𝜑𝐵 ∈ ℂ )
3 1 2 efsubd ( 𝜑 → ( exp ‘ ( 𝐴𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )
4 3 eqeq1d ( 𝜑 → ( ( exp ‘ ( 𝐴𝐵 ) ) = 1 ↔ ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = 1 ) )
5 ax-icn i ∈ ℂ
6 5 a1i ( 𝜑 → i ∈ ℂ )
7 2cnd ( 𝜑 → 2 ∈ ℂ )
8 picn π ∈ ℂ
9 8 a1i ( 𝜑 → π ∈ ℂ )
10 7 9 mulcld ( 𝜑 → ( 2 · π ) ∈ ℂ )
11 6 10 mulcld ( 𝜑 → ( i · ( 2 · π ) ) ∈ ℂ )
12 1 2 subcld ( 𝜑 → ( 𝐴𝐵 ) ∈ ℂ )
13 ine0 i ≠ 0
14 13 a1i ( 𝜑 → i ≠ 0 )
15 2ne0 2 ≠ 0
16 15 a1i ( 𝜑 → 2 ≠ 0 )
17 pine0 π ≠ 0
18 17 a1i ( 𝜑 → π ≠ 0 )
19 7 9 16 18 mulne0d ( 𝜑 → ( 2 · π ) ≠ 0 )
20 6 10 14 19 mulne0d ( 𝜑 → ( i · ( 2 · π ) ) ≠ 0 )
21 11 12 20 zdivgd ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴𝐵 ) ↔ ( ( 𝐴𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
22 eqcom ( 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 𝐴 )
23 2 adantr ( ( 𝜑𝑛 ∈ ℤ ) → 𝐵 ∈ ℂ )
24 11 adantr ( ( 𝜑𝑛 ∈ ℤ ) → ( i · ( 2 · π ) ) ∈ ℂ )
25 zcn ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
26 25 adantl ( ( 𝜑𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
27 24 26 mulcld ( ( 𝜑𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
28 1 adantr ( ( 𝜑𝑛 ∈ ℤ ) → 𝐴 ∈ ℂ )
29 23 27 28 addrsub ( ( 𝜑𝑛 ∈ ℤ ) → ( ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 𝐴 ↔ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴𝐵 ) ) )
30 22 29 bitrid ( ( 𝜑𝑛 ∈ ℤ ) → ( 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴𝐵 ) ) )
31 30 rexbidva ( 𝜑 → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴𝐵 ) ) )
32 efeq1 ( ( 𝐴𝐵 ) ∈ ℂ → ( ( exp ‘ ( 𝐴𝐵 ) ) = 1 ↔ ( ( 𝐴𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
33 12 32 syl ( 𝜑 → ( ( exp ‘ ( 𝐴𝐵 ) ) = 1 ↔ ( ( 𝐴𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
34 21 31 33 3bitr4rd ( 𝜑 → ( ( exp ‘ ( 𝐴𝐵 ) ) = 1 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
35 1 efcld ( 𝜑 → ( exp ‘ 𝐴 ) ∈ ℂ )
36 2 efcld ( 𝜑 → ( exp ‘ 𝐵 ) ∈ ℂ )
37 2 efne0d ( 𝜑 → ( exp ‘ 𝐵 ) ≠ 0 )
38 35 36 37 diveq1ad ( 𝜑 → ( ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = 1 ↔ ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ) )
39 4 34 38 3bitr3rd ( 𝜑 → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )