Theorem rprmndvdsru

Description: A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	rprmndvdsru.u	|- U = ( Unit ` R )
	rprmndvdsru.p	|- P = ( RPrime ` R )
	rprmndvdsru.d	|- .|| = ( ||r ` R )
	rprmndvdsru.r	|- ( ph -> R e. CRing )
	rprmndvdsru.q	|- ( ph -> Q e. P )
	rprmndvdsru.t	|- ( ph -> T e. U )
Assertion	rprmndvdsru	|- ( ph -> -. Q .|| T )

Proof

Step	Hyp	Ref	Expression
1		rprmndvdsru.u	|- U = ( Unit ` R )
2		rprmndvdsru.p	|- P = ( RPrime ` R )
3		rprmndvdsru.d	|- .|| = ( ||r ` R )
4		rprmndvdsru.r	|- ( ph -> R e. CRing )
5		rprmndvdsru.q	|- ( ph -> Q e. P )
6		rprmndvdsru.t	|- ( ph -> T e. U )
7		eqid	|- ( 1r ` R ) = ( 1r ` R )
8	7 3 2 4 5	rprmndvdsr1	|- ( ph -> -. Q .|| ( 1r ` R ) )
9	4	crngringd	|- ( ph -> R e. Ring )
10	1 7 3	crngunit	|- ( R e. CRing -> ( T e. U <-> T .|| ( 1r ` R ) ) )
11	10	biimpa	|- ( ( R e. CRing /\ T e. U ) -> T .|| ( 1r ` R ) )
12	4 6 11	syl2anc	|- ( ph -> T .|| ( 1r ` R ) )
13		eqid	|- ( Base ` R ) = ( Base ` R )
14	13 3	dvdsrtr	|- ( ( R e. Ring /\ Q .|| T /\ T .|| ( 1r ` R ) ) -> Q .|| ( 1r ` R ) )
15	14	3expa	|- ( ( ( R e. Ring /\ Q .|| T ) /\ T .|| ( 1r ` R ) ) -> Q .|| ( 1r ` R ) )
16	15	an32s	|- ( ( ( R e. Ring /\ T .|| ( 1r ` R ) ) /\ Q .|| T ) -> Q .|| ( 1r ` R ) )
17	16	ex	|- ( ( R e. Ring /\ T .|| ( 1r ` R ) ) -> ( Q .|| T -> Q .|| ( 1r ` R ) ) )
18	9 12 17	syl2anc	|- ( ph -> ( Q .|| T -> Q .|| ( 1r ` R ) ) )
19	8 18	mtod	|- ( ph -> -. Q .|| T )