Step | Hyp | Ref
| Expression |
1 | | ax-rrecex 10632 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ∃𝑥 ∈ ℝ (𝑅 · 𝑥) = 1) |
2 | | sn-inelr 39917 |
. . . . . 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 39896 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · 𝑅) = 1) |
7 | 6 | oveq1d 7158 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → ((𝑥 · 𝑅) · i) = (1 ·
i)) |
8 | 4 | recnd 10692 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑥 ∈
ℂ) |
9 | 3 | recnd 10692 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → 𝑅 ∈
ℂ) |
10 | | ax-icn 10619 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → i ∈
ℂ) |
12 | 8, 9, 11 | mulassd 10687 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → ((𝑥 · 𝑅) · i) = (𝑥 · (𝑅 · i))) |
13 | | sn-1ticom 39898 |
. . . . . . . . . . 11
⊢ (1
· i) = (i · 1) |
14 | | it1ei 39900 |
. . . . . . . . . . 11
⊢ (i
· 1) = i |
15 | 13, 14 | eqtri 2782 |
. . . . . . . . . 10
⊢ (1
· i) = i |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (1
· i) = i) |
17 | 7, 12, 16 | 3eqtr3d 2802 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · (𝑅 · i)) = i) |
18 | | simpr 489 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑅 · i) ∈
ℝ) |
19 | 4, 18 | remulcld 10694 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → (𝑥 · (𝑅 · i)) ∈
ℝ) |
20 | 17, 19 | eqeltrrd 2852 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (𝑅 · i) ∈ ℝ) → i ∈
ℝ) |
21 | 20 | ex 417 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ((𝑅 · i) ∈ ℝ → i ∈
ℝ)) |
22 | 2, 21 | mtoi 202 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ¬ (𝑅 · i) ∈
ℝ) |
23 | 1, 22 | rexlimddv 3213 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ¬ (𝑅 · i) ∈
ℝ) |
24 | 23 | ex 417 |
. . 3
⊢ (𝑅 ∈ ℝ → (𝑅 ≠ 0 → ¬ (𝑅 · i) ∈
ℝ)) |
25 | 24 | necon4ad 2968 |
. 2
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ
→ 𝑅 =
0)) |
26 | | oveq1 7150 |
. . 3
⊢ (𝑅 = 0 → (𝑅 · i) = (0 ·
i)) |
27 | | sn-0tie0 39903 |
. . . 4
⊢ (0
· i) = 0 |
28 | | 0re 10666 |
. . . 4
⊢ 0 ∈
ℝ |
29 | 27, 28 | eqeltri 2847 |
. . 3
⊢ (0
· i) ∈ ℝ |
30 | 26, 29 | eqeltrdi 2859 |
. 2
⊢ (𝑅 = 0 → (𝑅 · i) ∈
ℝ) |
31 | 25, 30 | impbid1 228 |
1
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ
↔ 𝑅 =
0)) |