lamberte

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

		Ref	Expression
	Hypothesis	lamberte.1	$⊢ R = {(x \in ℂ ⟼ x e^{x})}^{-1}$
	Assertion	lamberte	$⊢ e R 1$

Proof

Step	Hyp	Ref	Expression
1		lamberte.1	$⊢ R = {(x \in ℂ ⟼ x e^{x})}^{-1}$
2		1ex	$⊢ 1 \in V$
3		epr	$⊢ e \in ℝ^{+}$
4	3	elexi	$⊢ e \in V$
5		eqcom	$⊢ x = 1 \leftrightarrow 1 = x$
6	5	biimpi	$⊢ x = 1 \to 1 = x$
7		ax-1cn	$⊢ 1 \in ℂ$
8	6 7	eqeltrrdi	$⊢ x = 1 \to x \in ℂ$
9	8	adantr	$⊢ (x = 1 \land y = e) \to x \in ℂ$
10		simpr	$⊢ (x = 1 \land y = e) \to y = e$
11		df-e	$⊢ e = e^{1}$
12		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
13		ax-resscn	$⊢ ℝ \subseteq ℂ$
14	12 13	sstri	$⊢ ℝ^{+} \subseteq ℂ$
15	14 3	sselii	$⊢ e \in ℂ$
16	11 15	eqeltrri	$⊢ e^{1} \in ℂ$
17	16	mullidi	$⊢ 1 e^{1} = e^{1}$
18	17 11	eqtr4i	$⊢ 1 e^{1} = e$
19	6	fveq2d	$⊢ x = 1 \to e^{1} = e^{x}$
20	6 19	oveq12d	$⊢ x = 1 \to 1 e^{1} = x e^{x}$
21	18 20	eqtr3id	$⊢ x = 1 \to e = x e^{x}$
22	21	adantr	$⊢ (x = 1 \land y = e) \to e = x e^{x}$
23	10 22	eqtrd	$⊢ (x = 1 \land y = e) \to y = x e^{x}$
24	9 23	jca	$⊢ (x = 1 \land y = e) \to (x \in ℂ \land y = x e^{x})$
25		tbtru	$⊢ (x \in ℂ \land y = x e^{x}) \leftrightarrow ((x \in ℂ \land y = x e^{x}) \leftrightarrow ⊤)$
26	24 25	sylib	$⊢ (x = 1 \land y = e) \to ((x \in ℂ \land y = x e^{x}) \leftrightarrow ⊤)$
27		eqid	$⊢ \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} = \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\}$
28	2 4 26 27	braba	$⊢ 1 \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} e \leftrightarrow ⊤$
29		tbtru	$⊢ 1 \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} e \leftrightarrow (1 \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} e \leftrightarrow ⊤)$
30	28 29	mpbir	$⊢ 1 \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} e$
31		df-mpt	$⊢ (x \in ℂ ⟼ x e^{x}) = \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\}$
32	31	breqi	$⊢ 1 (x \in ℂ ⟼ x e^{x}) e \leftrightarrow 1 \{⟨x, y⟩ \| (x \in ℂ \land y = x e^{x})\} e$
33	30 32	mpbir	$⊢ 1 (x \in ℂ ⟼ x e^{x}) e$
34	4 2	brcnv	$⊢ e {(x \in ℂ ⟼ x e^{x})}^{-1} 1 \leftrightarrow 1 (x \in ℂ ⟼ x e^{x}) e$
35	33 34	mpbir	$⊢ e {(x \in ℂ ⟼ x e^{x})}^{-1} 1$
36	1	breqi	$⊢ e R 1 \leftrightarrow e {(x \in ℂ ⟼ x e^{x})}^{-1} 1$
37	35 36	mpbir	$⊢ e R 1$

Metamath Proof Explorer

Theorem lamberte

Proof