Description: If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | irredn0.i | |
|
irredmul.b | |
||
irredmul.u | |
||
irredmul.t | |
||
Assertion | irredmul | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | irredn0.i | |
|
2 | irredmul.b | |
|
3 | irredmul.u | |
|
4 | irredmul.t | |
|
5 | 2 3 1 4 | isirred2 | |
6 | 5 | simp3bi | |
7 | eqid | |
|
8 | oveq1 | |
|
9 | 8 | eqeq1d | |
10 | eleq1 | |
|
11 | 10 | orbi1d | |
12 | 9 11 | imbi12d | |
13 | oveq2 | |
|
14 | 13 | eqeq1d | |
15 | eleq1 | |
|
16 | 15 | orbi2d | |
17 | 14 16 | imbi12d | |
18 | 12 17 | rspc2v | |
19 | 7 18 | mpii | |
20 | 6 19 | syl5 | |
21 | 20 | 3impia | |