rprmndvdsru

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

Step	Hyp	Ref	Expression
1		rprmndvdsru.u	$⊢ U = Unit (R)$
2		rprmndvdsru.p	$⊢ P = RPrime (R)$
3		rprmndvdsru.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		rprmndvdsru.r	$⊢ φ \to R \in CRing$
5		rprmndvdsru.q	$⊢ φ \to Q \in P$
6		rprmndvdsru.t	$⊢ φ \to T \in U$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	7 3 2 4 5	rprmndvdsr1	$⊢ φ \to \neg Q \underset{˙}{∥} 1_{R}$
9	4	crngringd	$⊢ φ \to R \in Ring$
10	1 7 3	crngunit	$⊢ R \in CRing \to (T \in U \leftrightarrow T \underset{˙}{∥} 1_{R})$
11	10	biimpa	$⊢ (R \in CRing \land T \in U) \to T \underset{˙}{∥} 1_{R}$
12	4 6 11	syl2anc	$⊢ φ \to T \underset{˙}{∥} 1_{R}$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	13 3	dvdsrtr	$⊢ (R \in Ring \land Q \underset{˙}{∥} T \land T \underset{˙}{∥} 1_{R}) \to Q \underset{˙}{∥} 1_{R}$
15	14	3expa	$⊢ ((R \in Ring \land Q \underset{˙}{∥} T) \land T \underset{˙}{∥} 1_{R}) \to Q \underset{˙}{∥} 1_{R}$
16	15	an32s	$⊢ ((R \in Ring \land T \underset{˙}{∥} 1_{R}) \land Q \underset{˙}{∥} T) \to Q \underset{˙}{∥} 1_{R}$
17	16	ex	$⊢ (R \in Ring \land T \underset{˙}{∥} 1_{R}) \to (Q \underset{˙}{∥} T \to Q \underset{˙}{∥} 1_{R})$
18	9 12 17	syl2anc	$⊢ φ \to (Q \underset{˙}{∥} T \to Q \underset{˙}{∥} 1_{R})$
19	8 18	mtod	$⊢ φ \to \neg Q \underset{˙}{∥} T$

Metamath Proof Explorer