Theorem rprmnunit 33755

Description: A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025.)

Hypotheses

Ref	Expression
rprmdvds.2	⊢ 𝑃 = (RPrime‘𝑅)
rprmdvds.3	⊢ 𝑈 = (Unit‘𝑅)
rprmdvds.5	⊢ (𝜑 → 𝑅 ∈ 𝑉)
rprmdvds.6	⊢ (𝜑 → 𝑄 ∈ 𝑃)

Assertion

Ref	Expression
rprmnunit	⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)

Proof of Theorem rprmnunit

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2770	. 2 ⊢ (𝜑 → (𝑈 ∪ {(0g‘𝑅)}) = (𝑈 ∪ {(0g‘𝑅)}))
2		rprmdvds.5	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
3		rprmdvds.6	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
4		rprmdvds.2	. . . . 5 ⊢ 𝑃 = (RPrime‘𝑅)
5	3, 4	eleqtrdi 2879	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (RPrime‘𝑅))
6		eqid 2769	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
7		rprmdvds.3	. . . . . 6 ⊢ 𝑈 = (Unit‘𝑅)
8		eqid 2769	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
9		eqid 2769	. . . . . 6 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
10		eqid 2769	. . . . . 6 ⊢ (.r‘𝑅) = (.r‘𝑅)
11	6, 7, 8, 9, 10	isrprm 33751	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → (𝑄 ∈ (RPrime‘𝑅) ↔ (𝑄 ∈ ((Base‘𝑅) ∖ (𝑈 ∪ {(0g‘𝑅)})) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)(𝑄(∥r‘𝑅)(𝑥(.r‘𝑅)𝑦) → (𝑄(∥r‘𝑅)𝑥 ∨ 𝑄(∥r‘𝑅)𝑦)))))
12	11	simprbda 503	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑄 ∈ (RPrime‘𝑅)) → 𝑄 ∈ ((Base‘𝑅) ∖ (𝑈 ∪ {(0g‘𝑅)})))
13	2, 5, 12	syl2anc 595	. . 3 ⊢ (𝜑 → 𝑄 ∈ ((Base‘𝑅) ∖ (𝑈 ∪ {(0g‘𝑅)})))
14	13	eldifbd 3926	. 2 ⊢ (𝜑 → ¬ 𝑄 ∈ (𝑈 ∪ {(0g‘𝑅)}))
15		nelun 32799	. . 3 ⊢ ((𝑈 ∪ {(0g‘𝑅)}) = (𝑈 ∪ {(0g‘𝑅)}) → (¬ 𝑄 ∈ (𝑈 ∪ {(0g‘𝑅)}) ↔ (¬ 𝑄 ∈ 𝑈 ∧ ¬ 𝑄 ∈ {(0g‘𝑅)})))
16	15	simprbda 503	. 2 ⊢ (((𝑈 ∪ {(0g‘𝑅)}) = (𝑈 ∪ {(0g‘𝑅)}) ∧ ¬ 𝑄 ∈ (𝑈 ∪ {(0g‘𝑅)})) → ¬ 𝑄 ∈ 𝑈)
17	1, 14, 16	syl2anc 595	1 ⊢ (𝜑 → ¬ 𝑄 ∈ 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 860   = wceq 1567   ∈ wcel 2149  ∀wral 3085   ∖ cdif 3910   ∪ cun 3911  {csn 4594   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411  Basecbs 17268  ._rcmulr 17310  0_gc0g 17491  ∥_rcdsr 20435  Unitcui 20436  RPrimecrpm 20513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7414  df-rprm 20514

This theorem is referenced by:  rsprprmprmidl  33756  rprmndvdsr1  33758  rprmirred  33765  1arithidom  33771