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 + ; 1 0 ) =/= ; 2 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 10nn0 | |- ; 1 0 e. NN0 |
|
| 2 | 1 | nn0cni | |- ; 1 0 e. CC |
| 3 | 9cn | |- 9 e. CC |
|
| 4 | dec10p | |- ( ; 1 0 + 9 ) = ; 1 9 |
|
| 5 | 2 3 4 | addcomli | |- ( 9 + ; 1 0 ) = ; 1 9 |
| 6 | 1nn0 | |- 1 e. NN0 |
|
| 7 | 9nn0 | |- 9 e. NN0 |
|
| 8 | 6 7 | deccl | |- ; 1 9 e. NN0 |
| 9 | 8 | nn0rei | |- ; 1 9 e. RR |
| 10 | 2nn0 | |- 2 e. NN0 |
|
| 11 | 9lt10 | |- 9 < ; 1 0 |
|
| 12 | 1lt2 | |- 1 < 2 |
|
| 13 | 6 10 7 6 11 12 | decltc | |- ; 1 9 < ; 2 1 |
| 14 | 9 13 | ltneii | |- ; 1 9 =/= ; 2 1 |
| 15 | 5 14 | eqnetri | |- ( 9 + ; 1 0 ) =/= ; 2 1 |