Theorem rprmndvdsr1

Description: A ring prime element does not divide the ring multiplicative identity. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmndvdsr1.1	$$⊢\underset{\dot{}}{1}=1_R$$
	rprmndvdsr1.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	rprmndvdsr1.3	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmndvdsr1.4	$$⊢\phi \to R\in \mathrm{CRing}$$
	rprmndvdsr1.5	$$⊢\phi \to Q\in P$$
Assertion	rprmndvdsr1	$$⊢\phi \to \neg Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		rprmndvdsr1.1	$$⊢\underset{\dot{}}{1}=1_R$$
2		rprmndvdsr1.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		rprmndvdsr1.3	$$⊢P=\mathrm{RPrime}\left(R\right)$$
4		rprmndvdsr1.4	$$⊢\phi \to R\in \mathrm{CRing}$$
5		rprmndvdsr1.5	$$⊢\phi \to Q\in P$$
6		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
7	3 6 4 5	rprmnunit	$$⊢\phi \to \neg Q\in \mathrm{Unit}\left(R\right)$$
8	6 1 2	crngunit	$$⊢R\in \mathrm{CRing}\to \left(Q\in \mathrm{Unit}\left(R\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$
9	4 8	syl	$$⊢\phi \to \left(Q\in \mathrm{Unit}\left(R\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$
10	7 9	mtbid	$$⊢\phi \to \neg Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}$$