Description: 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | n2dvdsm1 | ⊢ ¬ 2 ∥ - 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | z0even | ⊢ 2 ∥ 0 | |
2 | ax-1cn | ⊢ 1 ∈ ℂ | |
3 | neg1cn | ⊢ - 1 ∈ ℂ | |
4 | 1pneg1e0 | ⊢ ( 1 + - 1 ) = 0 | |
5 | 2 3 4 | addcomli | ⊢ ( - 1 + 1 ) = 0 |
6 | 1 5 | breqtrri | ⊢ 2 ∥ ( - 1 + 1 ) |
7 | neg1z | ⊢ - 1 ∈ ℤ | |
8 | oddp1even | ⊢ ( - 1 ∈ ℤ → ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) ) ) | |
9 | 7 8 | ax-mp | ⊢ ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) ) |
10 | 6 9 | mpbir | ⊢ ¬ 2 ∥ - 1 |