This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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