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 ) ) ) )