Description: inelr without ax-mulcom . (Contributed by SN, 1-Jun-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sn-inelr | ⊢ ¬ i ∈ ℝ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reneg1lt0 | ⊢ ( 0 −ℝ 1 ) < 0 | |
| 2 | 1re | ⊢ 1 ∈ ℝ | |
| 3 | rernegcl | ⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ ) | |
| 4 | 2 3 | ax-mp | ⊢ ( 0 −ℝ 1 ) ∈ ℝ |
| 5 | 0re | ⊢ 0 ∈ ℝ | |
| 6 | 4 5 | ltnsymi | ⊢ ( ( 0 −ℝ 1 ) < 0 → ¬ 0 < ( 0 −ℝ 1 ) ) |
| 7 | 1 6 | ax-mp | ⊢ ¬ 0 < ( 0 −ℝ 1 ) |
| 8 | reixi | ⊢ ( i · i ) = ( 0 −ℝ 1 ) | |
| 9 | 8 | breq2i | ⊢ ( 0 < ( i · i ) ↔ 0 < ( 0 −ℝ 1 ) ) |
| 10 | 7 9 | mtbir | ⊢ ¬ 0 < ( i · i ) |
| 11 | id | ⊢ ( i ∈ ℝ → i ∈ ℝ ) | |
| 12 | 0ne1 | ⊢ 0 ≠ 1 | |
| 13 | 12 | a1i | ⊢ ( i ∈ ℝ → 0 ≠ 1 ) |
| 14 | id | ⊢ ( i = 0 → i = 0 ) | |
| 15 | 14 14 | oveq12d | ⊢ ( i = 0 → ( i · i ) = ( 0 · 0 ) ) |
| 16 | 15 | oveq1d | ⊢ ( i = 0 → ( ( i · i ) + 1 ) = ( ( 0 · 0 ) + 1 ) ) |
| 17 | ax-i2m1 | ⊢ ( ( i · i ) + 1 ) = 0 | |
| 18 | remul02 | ⊢ ( 0 ∈ ℝ → ( 0 · 0 ) = 0 ) | |
| 19 | 5 18 | ax-mp | ⊢ ( 0 · 0 ) = 0 |
| 20 | 19 | oveq1i | ⊢ ( ( 0 · 0 ) + 1 ) = ( 0 + 1 ) |
| 21 | readdlid | ⊢ ( 1 ∈ ℝ → ( 0 + 1 ) = 1 ) | |
| 22 | 2 21 | ax-mp | ⊢ ( 0 + 1 ) = 1 |
| 23 | 20 22 | eqtri | ⊢ ( ( 0 · 0 ) + 1 ) = 1 |
| 24 | 16 17 23 | 3eqtr3g | ⊢ ( i = 0 → 0 = 1 ) |
| 25 | 24 | adantl | ⊢ ( ( i ∈ ℝ ∧ i = 0 ) → 0 = 1 ) |
| 26 | 13 25 | mteqand | ⊢ ( i ∈ ℝ → i ≠ 0 ) |
| 27 | 11 26 | sn-msqgt0d | ⊢ ( i ∈ ℝ → 0 < ( i · i ) ) |
| 28 | 10 27 | mto | ⊢ ¬ i ∈ ℝ |