| Step | Hyp | Ref
| Expression |
| 1 | | ax-rrecex 11227 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ∃𝑥 ∈ ℝ (𝑅 · 𝑥) = 1) |
| 2 | | sn-inelr 42497 |
. . . . . 6
⊢ ¬ i
∈ ℝ |
| 3 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑅 ∈
ℝ) |
| 4 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑥 ∈
ℝ) |
| 5 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑅 · 𝑥) = 1) |
| 6 | 3, 4, 5 | remulinvcom 42462 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · 𝑅) = 1) |
| 7 | 6 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → ((𝑥 · 𝑅) · i) = (1 ·
i)) |
| 8 | 4 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑥 ∈
ℂ) |
| 9 | 3 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑅 ∈
ℂ) |
| 10 | | ax-icn 11214 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
| 11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → i ∈
ℂ) |
| 12 | 8, 9, 11 | mulassd 11284 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → ((𝑥 · 𝑅) · i) = (𝑥 · (𝑅 · i))) |
| 13 | | sn-1ticom 42464 |
. . . . . . . . . . 11
⊢ (1
· i) = (i · 1) |
| 14 | | sn-it1ei 42466 |
. . . . . . . . . . 11
⊢ (i
· 1) = i |
| 15 | 13, 14 | eqtri 2765 |
. . . . . . . . . 10
⊢ (1
· i) = i |
| 16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (1
· i) = i) |
| 17 | 7, 12, 16 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · (𝑅 · i)) = i) |
| 18 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑅 · i) ∈
ℝ) |
| 19 | 4, 18 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · (𝑅 · i)) ∈
ℝ) |
| 20 | 17, 19 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → i ∈
ℝ) |
| 21 | 20 | ex 412 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ((𝑅 · i) ∈ ℝ → i ∈
ℝ)) |
| 22 | 2, 21 | mtoi 199 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ¬ (𝑅 · i) ∈
ℝ) |
| 23 | 1, 22 | rexlimddv 3161 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ¬ (𝑅 · i) ∈
ℝ) |
| 24 | 23 | ex 412 |
. . 3
⊢ (𝑅 ∈ ℝ → (𝑅 ≠ 0 → ¬ (𝑅 · i) ∈
ℝ)) |
| 25 | 24 | necon4ad 2959 |
. 2
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ
→ 𝑅 =
0)) |
| 26 | | oveq1 7438 |
. . 3
⊢ (𝑅 = 0 → (𝑅 · i) = (0 ·
i)) |
| 27 | | sn-0tie0 42469 |
. . . 4
⊢ (0
· i) = 0 |
| 28 | | 0re 11263 |
. . . 4
⊢ 0 ∈
ℝ |
| 29 | 27, 28 | eqeltri 2837 |
. . 3
⊢ (0
· i) ∈ ℝ |
| 30 | 26, 29 | eqeltrdi 2849 |
. 2
⊢ (𝑅 = 0 → (𝑅 · i) ∈
ℝ) |
| 31 | 25, 30 | impbid1 225 |
1
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ
↔ 𝑅 =
0)) |