sn-retire

Description: Commuted version of sn-itrere . (Contributed by SN, 27-Jun-2024)

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

Proof

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

Metamath Proof Explorer

Theorem sn-retire

Proof