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
|- ( ph -> A e. CC )
ef11d.b
|- ( ph -> B e. CC )
Assertion ef11d
|- ( ph -> ( ( exp ` A ) = ( exp ` B ) <-> E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )

Proof

Step Hyp Ref Expression
1 ef11d.a
 |-  ( ph -> A e. CC )
2 ef11d.b
 |-  ( ph -> B e. CC )
3 1 2 efsubd
 |-  ( ph -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )
4 3 eqeq1d
 |-  ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( exp ` A ) / ( exp ` B ) ) = 1 ) )
5 ax-icn
 |-  _i e. CC
6 5 a1i
 |-  ( ph -> _i e. CC )
7 2cnd
 |-  ( ph -> 2 e. CC )
8 picn
 |-  _pi e. CC
9 8 a1i
 |-  ( ph -> _pi e. CC )
10 7 9 mulcld
 |-  ( ph -> ( 2 x. _pi ) e. CC )
11 6 10 mulcld
 |-  ( ph -> ( _i x. ( 2 x. _pi ) ) e. CC )
12 1 2 subcld
 |-  ( ph -> ( A - B ) e. CC )
13 ine0
 |-  _i =/= 0
14 13 a1i
 |-  ( ph -> _i =/= 0 )
15 2ne0
 |-  2 =/= 0
16 15 a1i
 |-  ( ph -> 2 =/= 0 )
17 pine0
 |-  _pi =/= 0
18 17 a1i
 |-  ( ph -> _pi =/= 0 )
19 7 9 16 18 mulne0d
 |-  ( ph -> ( 2 x. _pi ) =/= 0 )
20 6 10 14 19 mulne0d
 |-  ( ph -> ( _i x. ( 2 x. _pi ) ) =/= 0 )
21 11 12 20 zdivgd
 |-  ( ph -> ( E. n e. ZZ ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
22 eqcom
 |-  ( A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = A )
23 2 adantr
 |-  ( ( ph /\ n e. ZZ ) -> B e. CC )
24 11 adantr
 |-  ( ( ph /\ n e. ZZ ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
25 zcn
 |-  ( n e. ZZ -> n e. CC )
26 25 adantl
 |-  ( ( ph /\ n e. ZZ ) -> n e. CC )
27 24 26 mulcld
 |-  ( ( ph /\ n e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) x. n ) e. CC )
28 1 adantr
 |-  ( ( ph /\ n e. ZZ ) -> A e. CC )
29 23 27 28 addrsub
 |-  ( ( ph /\ n e. ZZ ) -> ( ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) = A <-> ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) )
30 22 29 bitrid
 |-  ( ( ph /\ n e. ZZ ) -> ( A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) )
31 30 rexbidva
 |-  ( ph -> ( E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) <-> E. n e. ZZ ( ( _i x. ( 2 x. _pi ) ) x. n ) = ( A - B ) ) )
32 efeq1
 |-  ( ( A - B ) e. CC -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
33 12 32 syl
 |-  ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> ( ( A - B ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
34 21 31 33 3bitr4rd
 |-  ( ph -> ( ( exp ` ( A - B ) ) = 1 <-> E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )
35 1 efcld
 |-  ( ph -> ( exp ` A ) e. CC )
36 2 efcld
 |-  ( ph -> ( exp ` B ) e. CC )
37 2 efne0d
 |-  ( ph -> ( exp ` B ) =/= 0 )
38 35 36 37 diveq1ad
 |-  ( ph -> ( ( ( exp ` A ) / ( exp ` B ) ) = 1 <-> ( exp ` A ) = ( exp ` B ) ) )
39 4 34 38 3bitr3rd
 |-  ( ph -> ( ( exp ` A ) = ( exp ` B ) <-> E. n e. ZZ A = ( B + ( ( _i x. ( 2 x. _pi ) ) x. n ) ) ) )