Theorem sn-00idlem2

Description: Lemma for sn-00id . (Contributed by SN, 25-Dec-2023)

	Ref	Expression
Assertion	sn-00idlem2	$$⊢0{-}_{ℝ}0\ne 0\to 0{-}_{ℝ}0=1$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		rennncan2	$$⊢\left(0\in ℝ\wedge 0\in ℝ\wedge 0\in ℝ\right)\to \left(0{-}_{ℝ}0\right){-}_{ℝ}\left(0{-}_{ℝ}0\right)=0{-}_{ℝ}0$$
3	1 1 1 2	mp3an	$$⊢\left(0{-}_{ℝ}0\right){-}_{ℝ}\left(0{-}_{ℝ}0\right)=0{-}_{ℝ}0$$
4		re1m1e0m0	$$⊢1{-}_{ℝ}1=0{-}_{ℝ}0$$
5	3 4	eqtr4i	$$⊢\left(0{-}_{ℝ}0\right){-}_{ℝ}\left(0{-}_{ℝ}0\right)=1{-}_{ℝ}1$$
6		rernegcl	$$⊢0\in ℝ\to 0{-}_{ℝ}0\in ℝ$$
7	1 6	ax-mp	$$⊢0{-}_{ℝ}0\in ℝ$$
8		sn-00idlem1	$$⊢0{-}_{ℝ}0\in ℝ\to \left(0{-}_{ℝ}0\right)\left(0{-}_{ℝ}0\right)=\left(0{-}_{ℝ}0\right){-}_{ℝ}\left(0{-}_{ℝ}0\right)$$
9	7 8	ax-mp	$$⊢\left(0{-}_{ℝ}0\right)\left(0{-}_{ℝ}0\right)=\left(0{-}_{ℝ}0\right){-}_{ℝ}\left(0{-}_{ℝ}0\right)$$
10		1re	$$⊢1\in ℝ$$
11		sn-00idlem1	$$⊢1\in ℝ\to 1\left(0{-}_{ℝ}0\right)=1{-}_{ℝ}1$$
12	10 11	ax-mp	$$⊢1\left(0{-}_{ℝ}0\right)=1{-}_{ℝ}1$$
13	5 9 12	3eqtr4i	$$⊢\left(0{-}_{ℝ}0\right)\left(0{-}_{ℝ}0\right)=1\left(0{-}_{ℝ}0\right)$$
14	7	a1i	$$⊢0{-}_{ℝ}0\ne 0\to 0{-}_{ℝ}0\in ℝ$$
15		1red	$$⊢0{-}_{ℝ}0\ne 0\to 1\in ℝ$$
16		id	$$⊢0{-}_{ℝ}0\ne 0\to 0{-}_{ℝ}0\ne 0$$
17	14 15 14 16	remulcan2d	$$⊢0{-}_{ℝ}0\ne 0\to \left(\left(0{-}_{ℝ}0\right)\left(0{-}_{ℝ}0\right)=1\left(0{-}_{ℝ}0\right)\leftrightarrow 0{-}_{ℝ}0=1\right)$$
18	13 17	mpbii	$$⊢0{-}_{ℝ}0\ne 0\to 0{-}_{ℝ}0=1$$