Theorem 9p10ne21

Description: 9 + 10 is not equal to 21. This disproves a popular meme which asserts that 9 + 10 does equal 21. See https://www.quora.com/Can-someone-try-to-prove-to-me-that-9+10-21 for attempts to prove that 9 + 10 = 21, and see https://tinyurl.com/9p10e21 for the history of the 9 + 10 = 21 meme. (Contributed by BTernaryTau, 25-Aug-2023)

	Ref	Expression
Assertion	9p10ne21	$$⊢9+10\ne 21$$

Proof

Step	Hyp	Ref	Expression
1		10nn0	$$⊢10\in {\mathbb{N}}_0$$
2	1	nn0cni	$$⊢10\in ℂ$$
3		9cn	$$⊢9\in ℂ$$
4		dec10p	$$⊢10+9=19$$
5	2 3 4	addcomli	$$⊢9+10=19$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		9nn0	$$⊢9\in {\mathbb{N}}_0$$
8	6 7	deccl	$$⊢19\in {\mathbb{N}}_0$$
9	8	nn0rei	$$⊢19\in ℝ$$
10		2nn0	$$⊢2\in {\mathbb{N}}_0$$
11		9lt10	$$⊢9<10$$
12		1lt2	$$⊢1<2$$
13	6 10 7 6 11 12	decltc	$$⊢19<21$$
14	9 13	ltneii	$$⊢19\ne 21$$
15	5 14	eqnetri	$$⊢9+10\ne 21$$