Metamath Proof Explorer

Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024)

Ref Expression
Assertion itrere ⊢ R ∈ ℝ → i ⁢ R ∈ ℝ ↔ R = 0

Proof

Step Hyp Ref Expression
1 ax-rrecex ⊢ R ∈ ℝ ∧ R ≠ 0 → ∃ x ∈ ℝ R ⁢ x = 1
2 sn-inelr ⊢ ¬ i ∈ ℝ
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ∈ ℂ
5 simplll ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → R ∈ ℝ
6 5 recnd ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → R ∈ ℂ
7 simplrl ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → x ∈ ℝ
8 7 recnd ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → x ∈ ℂ
9 4 6 8 mulassd ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⁢ R ⁢ x = i ⁢ R ⁢ x
10 simplrr ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → R ⁢ x = 1
11 10 oveq2d ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⁢ R ⁢ x = i ⋅ 1
12 it1ei ⊢ i ⋅ 1 = i
13 12 a1i ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⋅ 1 = i
14 9 11 13 3eqtrd ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⁢ R ⁢ x = i
15 simpr ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⁢ R ∈ ℝ
16 15 7 remulcld ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ⁢ R ⁢ x ∈ ℝ
17 14 16 eqeltrrd ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 ∧ i ⁢ R ∈ ℝ → i ∈ ℝ
18 17 ex ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 → i ⁢ R ∈ ℝ → i ∈ ℝ
19 2 18 mtoi ⊢ R ∈ ℝ ∧ R ≠ 0 ∧ x ∈ ℝ ∧ R ⁢ x = 1 → ¬ i ⁢ R ∈ ℝ
20 1 19 rexlimddv ⊢ R ∈ ℝ ∧ R ≠ 0 → ¬ i ⁢ R ∈ ℝ
21 20 ex ⊢ R ∈ ℝ → R ≠ 0 → ¬ i ⁢ R ∈ ℝ
22 21 necon4ad ⊢ R ∈ ℝ → i ⁢ R ∈ ℝ → R = 0
23 oveq2 ⊢ R = 0 → i ⁢ R = i ⋅ 0
24 sn-it0e0 ⊢ i ⋅ 0 = 0
25 0re ⊢ 0 ∈ ℝ
26 24 25 eqeltri ⊢ i ⋅ 0 ∈ ℝ
27 23 26 eqeltrdi ⊢ R = 0 → i ⁢ R ∈ ℝ
28 22 27 impbid1 ⊢ R ∈ ℝ → i ⁢ R ∈ ℝ ↔ R = 0