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 ‘ 𝑅 ) | |
| rprmndvdsr1.2 | ⊢ ∥ = ( ∥r ‘ 𝑅 ) | ||
| rprmndvdsr1.3 | ⊢ 𝑃 = ( RPrime ‘ 𝑅 ) | ||
| rprmndvdsr1.4 | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | ||
| rprmndvdsr1.5 | ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 ) | ||
| Assertion | rprmndvdsr1 | ⊢ ( 𝜑 → ¬ 𝑄 ∥ 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rprmndvdsr1.1 | ⊢ 1 = ( 1r ‘ 𝑅 ) | |
| 2 | rprmndvdsr1.2 | ⊢ ∥ = ( ∥r ‘ 𝑅 ) | |
| 3 | rprmndvdsr1.3 | ⊢ 𝑃 = ( RPrime ‘ 𝑅 ) | |
| 4 | rprmndvdsr1.4 | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | |
| 5 | rprmndvdsr1.5 | ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 ) | |
| 6 | eqid | ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 ) | |
| 7 | 3 6 4 5 | rprmnunit | ⊢ ( 𝜑 → ¬ 𝑄 ∈ ( Unit ‘ 𝑅 ) ) |
| 8 | 6 1 2 | crngunit | ⊢ ( 𝑅 ∈ CRing → ( 𝑄 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑄 ∥ 1 ) ) |
| 9 | 4 8 | syl | ⊢ ( 𝜑 → ( 𝑄 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑄 ∥ 1 ) ) |
| 10 | 7 9 | mtbid | ⊢ ( 𝜑 → ¬ 𝑄 ∥ 1 ) |