Theorem helloworld

Description: The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://helloworldcollection.de . However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able to put it to rest with a remarkably short proof only four lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	helloworld	⊢ ¬ ( ℎ ∈ ( 𝐿 𝐿 0 ) ∧ 𝑊 ∅ ( R 1 𝑑 ) )

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ ⟨ 𝑊 , ( R 1 𝑑 ) ⟩ ∈ ∅
2		df-br	⊢ ( 𝑊 ∅ ( R 1 𝑑 ) ↔ ⟨ 𝑊 , ( R 1 𝑑 ) ⟩ ∈ ∅ )
3	1 2	mtbir	⊢ ¬ 𝑊 ∅ ( R 1 𝑑 )
4	3	intnan	⊢ ¬ ( ℎ ∈ ( 𝐿 𝐿 0 ) ∧ 𝑊 ∅ ( R 1 𝑑 ) )