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 ∈ ℕ0 | |
| 2 | 1 | nn0cni | ⊢ ; 1 0 ∈ ℂ |
| 3 | 9cn | ⊢ 9 ∈ ℂ | |
| 4 | dec10p | ⊢ ( ; 1 0 + 9 ) = ; 1 9 | |
| 5 | 2 3 4 | addcomli | ⊢ ( 9 + ; 1 0 ) = ; 1 9 |
| 6 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
| 7 | 9nn0 | ⊢ 9 ∈ ℕ0 | |
| 8 | 6 7 | deccl | ⊢ ; 1 9 ∈ ℕ0 |
| 9 | 8 | nn0rei | ⊢ ; 1 9 ∈ ℝ |
| 10 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
| 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 |