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	⊢ 𝑅 = ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) )
Assertion	lambert0	⊢ 0 𝑅 0

Proof

Step	Hyp	Ref	Expression
1		lambert0.1	⊢ 𝑅 = ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) )
2		c0ex	⊢ 0 ∈ V
3		eqcom	⊢ ( 𝑥 = 0 ↔ 0 = 𝑥 )
4	3	biimpi	⊢ ( 𝑥 = 0 → 0 = 𝑥 )
5		0cnd	⊢ ( 𝑥 = 0 → 0 ∈ ℂ )
6	4 5	eqeltrrd	⊢ ( 𝑥 = 0 → 𝑥 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 𝑥 ∈ ℂ )
8		simpr	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 𝑦 = 0 )
9		ef0	⊢ ( exp ‘ 0 ) = 1
10		ax-1cn	⊢ 1 ∈ ℂ
11	9 10	eqeltri	⊢ ( exp ‘ 0 ) ∈ ℂ
12	11	mul02i	⊢ ( 0 · ( exp ‘ 0 ) ) = 0
13	4	fveq2d	⊢ ( 𝑥 = 0 → ( exp ‘ 0 ) = ( exp ‘ 𝑥 ) )
14	4 13	oveq12d	⊢ ( 𝑥 = 0 → ( 0 · ( exp ‘ 0 ) ) = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
15	12 14	eqtr3id	⊢ ( 𝑥 = 0 → 0 = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
16	15	adantr	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 0 = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
17	8 16	eqtrd	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) )
18	7 17	jca	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) )
19		tbtru	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ⊤ ) )
20	18 19	sylib	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) ↔ ⊤ ) )
21		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) }
22	2 2 20 21	braba	⊢ ( 0 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } 0 ↔ ⊤ )
23		tbtru	⊢ ( 0 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } 0 ↔ ( 0 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } 0 ↔ ⊤ ) )
24	22 23	mpbir	⊢ 0 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } 0
25		df-mpt	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) }
26	25	breqi	⊢ ( 0 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0 ↔ 0 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 = ( 𝑥 · ( exp ‘ 𝑥 ) ) ) } 0 )
27	24 26	mpbir	⊢ 0 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0
28	2 2	brcnv	⊢ ( 0 ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0 ↔ 0 ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0 )
29	27 28	mpbir	⊢ 0 ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0
30	1	breqi	⊢ ( 0 𝑅 0 ↔ 0 ◡ ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( exp ‘ 𝑥 ) ) ) 0 )
31	29 30	mpbir	⊢ 0 𝑅 0