Theorem lambert0

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

	Ref	Expression
Hypothesis	lambert0.1	$$⊢R={\left(x\in ℂ⟼x{\mathrm{e}}^x\right)}^{-1}$$
Assertion	lambert0	$$⊢0R0$$

Proof

Step	Hyp	Ref	Expression
1		lambert0.1	$$⊢R={\left(x\in ℂ⟼x{\mathrm{e}}^x\right)}^{-1}$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3		eqcom	$$⊢x=0\leftrightarrow 0=x$$
4	3	biimpi	$$⊢x=0\to 0=x$$
5		0cnd	$$⊢x=0\to 0\in ℂ$$
6	4 5	eqeltrrd	$$⊢x=0\to x\in ℂ$$
7	6	adantr	$$⊢\left(x=0\wedge y=0\right)\to x\in ℂ$$
8		simpr	$$⊢\left(x=0\wedge y=0\right)\to y=0$$
9		ef0	$$⊢{\mathrm{e}}^0=1$$
10		ax-1cn	$$⊢1\in ℂ$$
11	9 10	eqeltri	$$⊢{\mathrm{e}}^0\in ℂ$$
12	11	mul02i	$$⊢0\cdot {\mathrm{e}}^0=0$$
13	4	fveq2d	$$⊢x=0\to {\mathrm{e}}^0={\mathrm{e}}^x$$
14	4 13	oveq12d	$$⊢x=0\to 0\cdot {\mathrm{e}}^0=x{\mathrm{e}}^x$$
15	12 14	eqtr3id	$$⊢x=0\to 0=x{\mathrm{e}}^x$$
16	15	adantr	$$⊢\left(x=0\wedge y=0\right)\to 0=x{\mathrm{e}}^x$$
17	8 16	eqtrd	$$⊢\left(x=0\wedge y=0\right)\to y=x{\mathrm{e}}^x$$
18	7 17	jca	$$⊢\left(x=0\wedge y=0\right)\to \left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)$$
19		tbtru	$$⊢\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\leftrightarrow \left(\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\leftrightarrow \top \right)$$
20	18 19	sylib	$$⊢\left(x=0\wedge y=0\right)\to \left(\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\leftrightarrow \top \right)$$
21		eqid	$$⊢\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}=\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}$$
22	2 2 20 21	braba	$$⊢0\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}0\leftrightarrow \top$$
23		tbtru	$$⊢0\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}0\leftrightarrow \left(0\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}0\leftrightarrow \top \right)$$
24	22 23	mpbir	$$⊢0\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}0$$
25		df-mpt	$$⊢\left(x\in ℂ⟼x{\mathrm{e}}^x\right)=\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}$$
26	25	breqi	$$⊢0\left(x\in ℂ⟼x{\mathrm{e}}^x\right)0\leftrightarrow 0\left\{⟨x,y⟩|\left(x\in ℂ\wedge y=x{\mathrm{e}}^x\right)\right\}0$$
27	24 26	mpbir	$$⊢0\left(x\in ℂ⟼x{\mathrm{e}}^x\right)0$$
28	2 2	brcnv	$$⊢0{\left(x\in ℂ⟼x{\mathrm{e}}^x\right)}^{-1}0\leftrightarrow 0\left(x\in ℂ⟼x{\mathrm{e}}^x\right)0$$
29	27 28	mpbir	$$⊢0{\left(x\in ℂ⟼x{\mathrm{e}}^x\right)}^{-1}0$$
30	1	breqi	$$⊢0R0\leftrightarrow 0{\left(x\in ℂ⟼x{\mathrm{e}}^x\right)}^{-1}0$$
31	29 30	mpbir	$$⊢0R0$$