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

Theorem prmirredlem 16728
 Description: A natural number is irreducible over iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.)
Hypotheses
Ref Expression
prmirred.1 flds
prmirred.2 Irred
Assertion
Ref Expression
prmirredlem

Proof of Theorem prmirredlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zsubrg 16707 . . . . . . 7 SubRingfld
2 prmirred.1 . . . . . . . 8 flds
32subrgrng 15826 . . . . . . 7 SubRingfld
41, 3ax-mp 8 . . . . . 6
5 prmirred.2 . . . . . . 7 Irred
6 cnfld1 16681 . . . . . . . . 9 fld
72, 6subrg1 15833 . . . . . . . 8 SubRingfld
81, 7ax-mp 8 . . . . . . 7
95, 8irredn1 15766 . . . . . 6
104, 9mpan 652 . . . . 5
1110anim2i 553 . . . 4
12 eluz2b3 10505 . . . 4
1311, 12sylibr 204 . . 3
14 nnz 10259 . . . . . . . 8
1514ad2antrl 709 . . . . . . 7
16 simprr 734 . . . . . . . 8
17 nnne0 9988 . . . . . . . . . 10
1817ad2antrl 709 . . . . . . . . 9
19 nnz 10259 . . . . . . . . . 10
2019ad2antrr 707 . . . . . . . . 9
21 dvdsval2 12810 . . . . . . . . 9
2215, 18, 20, 21syl3anc 1184 . . . . . . . 8
2316, 22mpbid 202 . . . . . . 7
2420zcnd 10332 . . . . . . . . 9
25 nncn 9964 . . . . . . . . . 10
2625ad2antrl 709 . . . . . . . . 9
2724, 26, 18divcan2d 9748 . . . . . . . 8
28 simplr 732 . . . . . . . 8
2927, 28eqeltrd 2478 . . . . . . 7
302subrgbas 15832 . . . . . . . . 9 SubRingfld
311, 30ax-mp 8 . . . . . . . 8
32 eqid 2404 . . . . . . . 8 Unit Unit
33 zex 10247 . . . . . . . . 9
34 cnfldmul 16664 . . . . . . . . . 10 fld
352, 34ressmulr 13537 . . . . . . . . 9
3633, 35ax-mp 8 . . . . . . . 8
375, 31, 32, 36irredmul 15769 . . . . . . 7 Unit Unit
3815, 23, 29, 37syl3anc 1184 . . . . . 6 Unit Unit
392zrngunit 16720 . . . . . . . . . 10 Unit
4039baib 872 . . . . . . . . 9 Unit
4115, 40syl 16 . . . . . . . 8 Unit
42 nnnn0 10184 . . . . . . . . . . 11
43 nn0re 10186 . . . . . . . . . . . 12
44 nn0ge0 10203 . . . . . . . . . . . 12
4543, 44absidd 12180 . . . . . . . . . . 11
4642, 45syl 16 . . . . . . . . . 10
4746ad2antrl 709 . . . . . . . . 9
4847eqeq1d 2412 . . . . . . . 8
4941, 48bitrd 245 . . . . . . 7 Unit
502zrngunit 16720 . . . . . . . . . 10 Unit
5150baib 872 . . . . . . . . 9 Unit
5223, 51syl 16 . . . . . . . 8 Unit
53 nnre 9963 . . . . . . . . . . . . 13
5453ad2antrr 707 . . . . . . . . . . . 12
55 simprl 733 . . . . . . . . . . . 12
5654, 55nndivred 10004 . . . . . . . . . . 11
57 nnnn0 10184 . . . . . . . . . . . . . 14
58 nn0ge0 10203 . . . . . . . . . . . . . 14
5957, 58syl 16 . . . . . . . . . . . . 13
6059ad2antrr 707 . . . . . . . . . . . 12
6155nnred 9971 . . . . . . . . . . . 12
62 nngt0 9985 . . . . . . . . . . . . 13
6362ad2antrl 709 . . . . . . . . . . . 12
64 divge0 9835 . . . . . . . . . . . 12
6554, 60, 61, 63, 64syl22anc 1185 . . . . . . . . . . 11
6656, 65absidd 12180 . . . . . . . . . 10
6766eqeq1d 2412 . . . . . . . . 9
68 ax-1cn 9004 . . . . . . . . . . 11
6968a1i 11 . . . . . . . . . 10
7024, 26, 69, 18divmuld 9768 . . . . . . . . 9
7126mulid1d 9061 . . . . . . . . . 10
7271eqeq1d 2412 . . . . . . . . 9
7367, 70, 723bitrd 271 . . . . . . . 8
7452, 73bitrd 245 . . . . . . 7 Unit
7549, 74orbi12d 691 . . . . . 6 Unit Unit
7638, 75mpbid 202 . . . . 5
7776expr 599 . . . 4
7877ralrimiva 2749 . . 3
79 isprm2 13042 . . 3
8013, 78, 79sylanbrc 646 . 2
81 prmz 13038 . . . 4
82 1nprm 13039 . . . . 5
832zrngunit 16720 . . . . . 6 Unit
84 prmnn 13037 . . . . . . . . . 10
85 nn0re 10186 . . . . . . . . . . 11
8685, 58absidd 12180 . . . . . . . . . 10
8784, 57, 863syl 19 . . . . . . . . 9
88 id 20 . . . . . . . . 9
8987, 88eqeltrd 2478 . . . . . . . 8
90 eleq1 2464 . . . . . . . 8
9189, 90syl5ibcom 212 . . . . . . 7
9291adantld 454 . . . . . 6
9383, 92syl5bi 209 . . . . 5 Unit
9482, 93mtoi 171 . . . 4 Unit
95 simplrl 737 . . . . . . . . . . . 12
9695zcnd 10332 . . . . . . . . . . 11
9784ad2antrr 707 . . . . . . . . . . . . . 14
9897nnne0d 10000 . . . . . . . . . . . . 13
99 simpr 448 . . . . . . . . . . . . 13
100 simplrr 738 . . . . . . . . . . . . . . 15
101100zcnd 10332 . . . . . . . . . . . . . 14
102101mul02d 9220 . . . . . . . . . . . . 13
10398, 99, 1023netr4d 2594 . . . . . . . . . . . 12
104 oveq1 6047 . . . . . . . . . . . . 13
105104necon3i 2606 . . . . . . . . . . . 12
106103, 105syl 16 . . . . . . . . . . 11
10796, 106absne0d 12204 . . . . . . . . . 10
108107neneqd 2583 . . . . . . . . 9
109 nn0abscl 12072 . . . . . . . . . . . 12
11095, 109syl 16 . . . . . . . . . . 11
111 elnn0 10179 . . . . . . . . . . 11
112110, 111sylib 189 . . . . . . . . . 10
113112ord 367 . . . . . . . . 9
114108, 113mt3d 119 . . . . . . . 8
11579simprbi 451 . . . . . . . . 9
116115ad2antrr 707 . . . . . . . 8
117 dvdsmul1 12826 . . . . . . . . . . 11
118117ad2antlr 708 . . . . . . . . . 10
119118, 99breqtrd 4196 . . . . . . . . 9
12081ad2antrr 707 . . . . . . . . . 10
121 absdvdsb 12823 . . . . . . . . . 10
12295, 120, 121syl2anc 643 . . . . . . . . 9
123119, 122mpbid 202 . . . . . . . 8
124 breq1 4175 . . . . . . . . . 10
125 eqeq1 2410 . . . . . . . . . . 11
126 eqeq1 2410 . . . . . . . . . . 11
127125, 126orbi12d 691 . . . . . . . . . 10
128124, 127imbi12d 312 . . . . . . . . 9
129128rspcv 3008 . . . . . . . 8
130114, 116, 123, 129syl3c 59 . . . . . . 7
1312zrngunit 16720 . . . . . . . . . 10 Unit
132131baib 872 . . . . . . . . 9 Unit
13395, 132syl 16 . . . . . . . 8 Unit
134100, 40syl 16 . . . . . . . . 9 Unit
135101abscld 12193 . . . . . . . . . . 11
136135recnd 9070 . . . . . . . . . 10
13768a1i 11 . . . . . . . . . 10
13896abscld 12193 . . . . . . . . . . 11
139138recnd 9070 . . . . . . . . . 10
140136, 137, 139, 107mulcand 9611 . . . . . . . . 9
14199fveq2d 5691 . . . . . . . . . . . 12
14296, 101absmuld 12211 . . . . . . . . . . . 12
14387ad2antrr 707 . . . . . . . . . . . 12
144141, 142, 1433eqtr3d 2444 . . . . . . . . . . 11
145139mulid1d 9061 . . . . . . . . . . 11
146144, 145eqeq12d 2418 . . . . . . . . . 10
147 eqcom 2406 . . . . . . . . . 10
148146, 147syl6bb 253 . . . . . . . . 9
149134, 140, 1483bitr2d 273 . . . . . . . 8 Unit
150133, 149orbi12d 691 . . . . . . 7 Unit Unit
151130, 150mpbird 224 . . . . . 6 Unit Unit
152151ex 424 . . . . 5 Unit Unit
153152ralrimivva 2758 . . . 4 Unit Unit
15431, 32, 5, 36isirred2 15761 . . . 4 Unit Unit Unit
15581, 94, 153, 154syl3anbrc 1138 . . 3