Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rprm Structured version   Unicode version

Definition df-rprm 21770
 Description: Define the set of prime elements in a ring. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 13109. (Contributed by Mario Carneiro, 17-Feb-2015.)
Assertion
Ref Expression
df-rprm RPrime Unit r
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-rprm
StepHypRef Expression
1 crpm 21769 . 2 RPrime
2 vw . . 3
3 cvv 2957 . . 3
4 vb . . . 4
52cv 1652 . . . . 5
6 cbs 13470 . . . . 5
75, 6cfv 5455 . . . 4
8 vp . . . . . . . . . . 11
98cv 1652 . . . . . . . . . 10
10 vx . . . . . . . . . . . 12
1110cv 1652 . . . . . . . . . . 11
12 vy . . . . . . . . . . . 12
1312cv 1652 . . . . . . . . . . 11
14 cmulr 13531 . . . . . . . . . . . 12
155, 14cfv 5455 . . . . . . . . . . 11
1611, 13, 15co 6082 . . . . . . . . . 10
17 vd . . . . . . . . . . 11
1817cv 1652 . . . . . . . . . 10
199, 16, 18wbr 4213 . . . . . . . . 9
209, 11, 18wbr 4213 . . . . . . . . . 10
219, 13, 18wbr 4213 . . . . . . . . . 10
2220, 21wo 359 . . . . . . . . 9
2319, 22wi 4 . . . . . . . 8
24 cdsr 15744 . . . . . . . . 9 r
255, 24cfv 5455 . . . . . . . 8 r
2623, 17, 25wsbc 3162 . . . . . . 7 r
274cv 1652 . . . . . . 7
2826, 12, 27wral 2706 . . . . . 6 r
2928, 10, 27wral 2706 . . . . 5 r
30 cui 15745 . . . . . . . 8 Unit
315, 30cfv 5455 . . . . . . 7 Unit
32 c0g 13724 . . . . . . . . 9
335, 32cfv 5455 . . . . . . . 8
3433csn 3815 . . . . . . 7
3531, 34cun 3319 . . . . . 6 Unit
3627, 35cdif 3318 . . . . 5 Unit
3729, 8, 36crab 2710 . . . 4 Unit r
384, 7, 37csb 3252 . . 3 Unit r
392, 3, 38cmpt 4267 . 2 Unit r
401, 39wceq 1653 1 RPrime Unit r
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator