sn-itrere

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

		Ref	Expression
	Assertion	sn-itrere	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$

Proof

Step	Hyp	Ref	Expression
1		sn-inelr	$⊢ \neg i \in ℝ$
2		ax-icn	$⊢ i \in ℂ$
3	2	a1i	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i \in ℂ$
4		simpll	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \in ℝ$
5	4	recnd	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \in ℂ$
6		simplr	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \neq 0$
7	4 6	sn-rereccld	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. RR ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. RR ) with typecode \|-
8	7	recnd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. CC ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. CC ) with typecode \|-
9	3 5 8	mulassd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = ( _i x. ( R x. ( 1 /R R ) ) ) ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = ( _i x. ( R x. ( 1 /R R ) ) ) ) with typecode \|-
10	4 6	rerecidd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( R x. ( 1 /R R ) ) = 1 ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( R x. ( 1 /R R ) ) = 1 ) with typecode \|-
11	10	oveq2d	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( _i x. ( R x. ( 1 /R R ) ) ) = ( _i x. 1 ) ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( _i x. ( R x. ( 1 /R R ) ) ) = ( _i x. 1 ) ) with typecode \|-
12		sn-it1ei	$⊢ i \cdot 1 = i$
13	12	a1i	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i \cdot 1 = i$
14	9 11 13	3eqtrd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = _i ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = _i ) with typecode \|-
15		simpr	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i R \in ℝ$
16	15 7	remulcld	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) e. RR ) : No typesetting found for \|- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) e. RR ) with typecode \|-
17	14 16	eqeltrrd	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i \in ℝ$
18	17	ex	$⊢ (R \in ℝ \land R \neq 0) \to (i R \in ℝ \to i \in ℝ)$
19	1 18	mtoi	$⊢ (R \in ℝ \land R \neq 0) \to \neg i R \in ℝ$
20	19	ex	$⊢ R \in ℝ \to (R \neq 0 \to \neg i R \in ℝ)$
21	20	necon4ad	$⊢ R \in ℝ \to (i R \in ℝ \to R = 0)$
22		oveq2	$⊢ R = 0 \to i R = i \cdot 0$
23		sn-it0e0	$⊢ i \cdot 0 = 0$
24		0re	$⊢ 0 \in ℝ$
25	23 24	eqeltri	$⊢ i \cdot 0 \in ℝ$
26	22 25	eqeltrdi	$⊢ R = 0 \to i R \in ℝ$
27	21 26	impbid1	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$

Metamath Proof Explorer

Theorem sn-itrere

Proof