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