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