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 ⊢ φ → A ∈ ℂ
ef11d.b ⊢ φ → B ∈ ℂ
Assertion ef11d ⊢ φ → e A = e B ↔ ∃ n ∈ ℤ A = B + i ⁢ 2 ⁢ π ⁢ n

Proof

Step Hyp Ref Expression
1 ef11d.a ⊢ φ → A ∈ ℂ
2 ef11d.b ⊢ φ → B ∈ ℂ
3 1 2 efsubd ⊢ φ → e A − B = e A e B
4 3 eqeq1d ⊢ φ → e A − B = 1 ↔ e A e B = 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 ⊢ φ → A − B ∈ ℂ
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 ⊢ φ → ∃ n ∈ ℤ i ⁢ 2 ⁢ π ⁢ n = A − B ↔ A − B i ⁢ 2 ⁢ π ∈ ℤ
22 eqcom ⊢ A = B + i ⁢ 2 ⁢ π ⁢ n ↔ B + i ⁢ 2 ⁢ π ⁢ n = A
23 2 adantr ⊢ φ ∧ n ∈ ℤ → B ∈ ℂ
24 11 adantr ⊢ φ ∧ n ∈ ℤ → i ⁢ 2 ⁢ π ∈ ℂ
25 zcn ⊢ n ∈ ℤ → n ∈ ℂ
26 25 adantl ⊢ φ ∧ n ∈ ℤ → n ∈ ℂ
27 24 26 mulcld ⊢ φ ∧ n ∈ ℤ → i ⁢ 2 ⁢ π ⁢ n ∈ ℂ
28 1 adantr ⊢ φ ∧ n ∈ ℤ → A ∈ ℂ
29 23 27 28 addrsub ⊢ φ ∧ n ∈ ℤ → B + i ⁢ 2 ⁢ π ⁢ n = A ↔ i ⁢ 2 ⁢ π ⁢ n = A − B
30 22 29 bitrid ⊢ φ ∧ n ∈ ℤ → A = B + i ⁢ 2 ⁢ π ⁢ n ↔ i ⁢ 2 ⁢ π ⁢ n = A − B
31 30 rexbidva ⊢ φ → ∃ n ∈ ℤ A = B + i ⁢ 2 ⁢ π ⁢ n ↔ ∃ n ∈ ℤ i ⁢ 2 ⁢ π ⁢ n = A − B
32 efeq1 ⊢ A − B ∈ ℂ → e A − B = 1 ↔ A − B i ⁢ 2 ⁢ π ∈ ℤ
33 12 32 syl ⊢ φ → e A − B = 1 ↔ A − B i ⁢ 2 ⁢ π ∈ ℤ
34 21 31 33 3bitr4rd ⊢ φ → e A − B = 1 ↔ ∃ n ∈ ℤ A = B + i ⁢ 2 ⁢ π ⁢ n
35 1 efcld ⊢ φ → e A ∈ ℂ
36 2 efcld ⊢ φ → e B ∈ ℂ
37 2 efne0d ⊢ φ → e B ≠ 0
38 35 36 37 diveq1ad ⊢ φ → e A e B = 1 ↔ e A = e B
39 4 34 38 3bitr3rd ⊢ φ → e A = e B ↔ ∃ n ∈ ℤ A = B + i ⁢ 2 ⁢ π ⁢ n