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

Theorem irredn0 15810
 Description: The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
Hypotheses
Ref Expression
irredn0.i Irred
irredn0.z
Assertion
Ref Expression
irredn0

Proof of Theorem irredn0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2438 . . . . . . . . . 10
2 irredn0.z . . . . . . . . . 10
31, 2rng0cl 15687 . . . . . . . . 9
43anim1i 553 . . . . . . . 8 Unit Unit
5 eldif 3332 . . . . . . . 8 Unit Unit
64, 5sylibr 205 . . . . . . 7 Unit Unit
7 eqid 2438 . . . . . . . . . 10
81, 7, 2rnglz 15702 . . . . . . . . 9
93, 8mpdan 651 . . . . . . . 8
109adantr 453 . . . . . . 7 Unit
11 oveq1 6090 . . . . . . . . 9
1211eqeq1d 2446 . . . . . . . 8
13 oveq2 6091 . . . . . . . . 9
1413eqeq1d 2446 . . . . . . . 8
1512, 14rspc2ev 3062 . . . . . . 7 Unit Unit Unit Unit
166, 6, 10, 15syl3anc 1185 . . . . . 6 Unit Unit Unit
1716ex 425 . . . . 5 Unit Unit Unit
1817orrd 369 . . . 4 Unit Unit Unit
19 eqid 2438 . . . . . 6 Unit Unit
20 irredn0.i . . . . . 6 Irred
21 eqid 2438 . . . . . 6 Unit Unit
221, 19, 20, 21, 7isnirred 15807 . . . . 5 Unit Unit Unit
233, 22syl 16 . . . 4 Unit Unit Unit
2418, 23mpbird 225 . . 3