Step | Hyp | Ref
| Expression |
1 | | ax-rrecex 10632 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ∃𝑥 ∈ ℝ (𝑅 · 𝑥) = 1) |
2 | | sn-inelr 39917 |
. . . . . 6
⊢ ¬ i
∈ ℝ |
3 | | ax-icn 10619 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
4 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → i ∈
ℂ) |
5 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → 𝑅 ∈ ℝ) |
6 | 5 | recnd 10692 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → 𝑅 ∈ ℂ) |
7 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → 𝑥 ∈ ℝ) |
8 | 7 | recnd 10692 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → 𝑥 ∈ ℂ) |
9 | 4, 6, 8 | mulassd 10687 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → ((i · 𝑅) · 𝑥) = (i · (𝑅 · 𝑥))) |
10 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → (𝑅 · 𝑥) = 1) |
11 | 10 | oveq2d 7159 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → (i · (𝑅 · 𝑥)) = (i · 1)) |
12 | | it1ei 39900 |
. . . . . . . . . 10
⊢ (i
· 1) = i |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → (i · 1) =
i) |
14 | 9, 11, 13 | 3eqtrd 2798 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → ((i · 𝑅) · 𝑥) = i) |
15 | | simpr 489 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → (i · 𝑅) ∈
ℝ) |
16 | 15, 7 | remulcld 10694 |
. . . . . . . 8
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → ((i · 𝑅) · 𝑥) ∈ ℝ) |
17 | 14, 16 | eqeltrrd 2852 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) ∧ (i · 𝑅) ∈ ℝ) → i ∈
ℝ) |
18 | 17 | ex 417 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ((i · 𝑅) ∈ ℝ → i ∈
ℝ)) |
19 | 2, 18 | mtoi 202 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (𝑅 · 𝑥) = 1)) → ¬ (i · 𝑅) ∈
ℝ) |
20 | 1, 19 | rexlimddv 3213 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ≠ 0) → ¬ (i
· 𝑅) ∈
ℝ) |
21 | 20 | ex 417 |
. . 3
⊢ (𝑅 ∈ ℝ → (𝑅 ≠ 0 → ¬ (i ·
𝑅) ∈
ℝ)) |
22 | 21 | necon4ad 2968 |
. 2
⊢ (𝑅 ∈ ℝ → ((i
· 𝑅) ∈ ℝ
→ 𝑅 =
0)) |
23 | | oveq2 7151 |
. . 3
⊢ (𝑅 = 0 → (i · 𝑅) = (i ·
0)) |
24 | | sn-it0e0 39879 |
. . . 4
⊢ (i
· 0) = 0 |
25 | | 0re 10666 |
. . . 4
⊢ 0 ∈
ℝ |
26 | 24, 25 | eqeltri 2847 |
. . 3
⊢ (i
· 0) ∈ ℝ |
27 | 23, 26 | eqeltrdi 2859 |
. 2
⊢ (𝑅 = 0 → (i · 𝑅) ∈
ℝ) |
28 | 22, 27 | impbid1 228 |
1
⊢ (𝑅 ∈ ℝ → ((i
· 𝑅) ∈ ℝ
↔ 𝑅 =
0)) |