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	|- .1. = ( 1r ` R )
	rprmndvdsr1.2	|- .|| = ( ||r ` R )
	rprmndvdsr1.3	|- P = ( RPrime ` R )
	rprmndvdsr1.4	|- ( ph -> R e. CRing )
	rprmndvdsr1.5	|- ( ph -> Q e. P )
Assertion	rprmndvdsr1	|- ( ph -> -. Q .|| .1. )

Proof

Step	Hyp	Ref	Expression
1		rprmndvdsr1.1	|- .1. = ( 1r ` R )
2		rprmndvdsr1.2	|- .|| = ( ||r ` R )
3		rprmndvdsr1.3	|- P = ( RPrime ` R )
4		rprmndvdsr1.4	|- ( ph -> R e. CRing )
5		rprmndvdsr1.5	|- ( ph -> Q e. P )
6		eqid	|- ( Unit ` R ) = ( Unit ` R )
7	3 6 4 5	rprmnunit	|- ( ph -> -. Q e. ( Unit ` R ) )
8	6 1 2	crngunit	|- ( R e. CRing -> ( Q e. ( Unit ` R ) <-> Q .|| .1. ) )
9	4 8	syl	|- ( ph -> ( Q e. ( Unit ` R ) <-> Q .|| .1. ) )
10	7 9	mtbid	|- ( ph -> -. Q .|| .1. )