Theorem lamberte

Description: A value of Lambert W (product logarithm) function at _e . (Contributed by Ender Ting, 13-Nov-2025)

	Ref	Expression
Hypothesis	lamberte.1	⊢ 𝑅 = ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) )
Assertion	lamberte	⊢ e 𝑅 1

Proof

Step	Hyp	Ref	Expression
1		lamberte.1	⊢ 𝑅 = ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) )
2		1ex	⊢ 1 ∈ V
3		epr	⊢ e ∈ ℝ+
4	3	elexi	⊢ e ∈ V
5		eqcom	⊢ ( 𝑥 = 1 ↔ 1 = 𝑥 )
6	5	biimpi	⊢ ( 𝑥 = 1 → 1 = 𝑥 )
7		ax-1cn	⊢ 1 ∈ ℂ
8	6 7	eqeltrrdi	⊢ ( 𝑥 = 1 → 𝑥 ∈ ℂ )
9	8	adantr	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → 𝑥 ∈ ℂ )
10		simpr	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → 𝑦 = e )
11		df-e	⊢ e = ( exp ‘ 1 )
12		rpssre	⊢ ℝ+ ⊆ ℝ
13		ax-resscn	⊢ ℝ ⊆ ℂ
14	12 13	sstri	⊢ ℝ+ ⊆ ℂ
15	14 3	sselii	⊢ e ∈ ℂ
16	11 15	eqeltrri	⊢ ( exp ‘ 1 ) ∈ ℂ
17	16	mullidi	⊢ ( 1 · ( exp ‘ 1 ) ) = ( exp ‘ 1 )
18	17 11	eqtr4i	⊢ ( 1 · ( exp ‘ 1 ) ) = e
19	6	fveq2d	⊢ ( 𝑥 = 1 → ( exp ‘ 1 ) = ( exp ‘ 𝑥 ) )
20	6 19	oveq12d	⊢ ( 𝑥 = 1 → ( 1 · ( exp ‘ 1 ) ) = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
21	18 20	eqtr3id	⊢ ( 𝑥 = 1 → e = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
22	21	adantr	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → e = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
23	10 22	eqtrd	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
24	9 23	jca	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) )
25		tbtru	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ⊤ ) )
26	24 25	sylib	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = e ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ⊤ ) )
27		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) }
28	2 4 26 27	braba	⊢ ( 1 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } e ↔ ⊤ )
29		tbtru	⊢ ( 1 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } e ↔ ( 1 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } e ↔ ⊤ ) )
30	28 29	mpbir	⊢ 1 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } e
31		df-mpt	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) }
32	31	breqi	⊢ ( 1 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) e ↔ 1 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } e )
33	30 32	mpbir	⊢ 1 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) e
34	4 2	brcnv	⊢ ( e ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 1 ↔ 1 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) e )
35	33 34	mpbir	⊢ e ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 1
36	1	breqi	⊢ ( e 𝑅 1 ↔ e ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 1 )
37	35 36	mpbir	⊢ e 𝑅 1