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

Theorem prmirredlemOLD 18652
 Description: A positive integer is irreducible over iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) Obsolete version of prmirredlem 18649 as of 10-Jun-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
prmirredOLD.1 flds
prmirredOLD.2 Irred
Assertion
Ref Expression
prmirredlemOLD

Proof of Theorem prmirredlemOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zsubrg 18597 . . . . . . 7 SubRingfld
2 prmirredOLD.1 . . . . . . . 8 flds
32subrgring 17558 . . . . . . 7 SubRingfld
41, 3ax-mp 5 . . . . . 6
5 prmirredOLD.2 . . . . . . 7 Irred
6 cnfld1 18569 . . . . . . . . 9 fld
72, 6subrg1 17565 . . . . . . . 8 SubRingfld
81, 7ax-mp 5 . . . . . . 7
95, 8irredn1 17481 . . . . . 6
104, 9mpan 670 . . . . 5
1110anim2i 569 . . . 4
12 eluz2b3 11180 . . . 4
1311, 12sylibr 212 . . 3
14 nnz 10907 . . . . . . . 8
1514ad2antrl 727 . . . . . . 7
16 simprr 757 . . . . . . . 8
17 nnne0 10589 . . . . . . . . . 10
1817ad2antrl 727 . . . . . . . . 9
19 nnz 10907 . . . . . . . . . 10
2019ad2antrr 725 . . . . . . . . 9
21 dvdsval2 14000 . . . . . . . . 9
2215, 18, 20, 21syl3anc 1228 . . . . . . . 8
2316, 22mpbid 210 . . . . . . 7
2420zcnd 10991 . . . . . . . . 9
25 nncn 10564 . . . . . . . . . 10
2625ad2antrl 727 . . . . . . . . 9
2724, 26, 18divcan2d 10343 . . . . . . . 8
28 simplr 755 . . . . . . . 8
2927, 28eqeltrd 2545 . . . . . . 7
302subrgbas 17564 . . . . . . . . 9 SubRingfld
311, 30ax-mp 5 . . . . . . . 8
32 eqid 2457 . . . . . . . 8 Unit Unit
33 zex 10894 . . . . . . . . 9
34 cnfldmul 18552 . . . . . . . . . 10 fld
352, 34ressmulr 14768 . . . . . . . . 9
3633, 35ax-mp 5 . . . . . . . 8
375, 31, 32, 36irredmul 17484 . . . . . . 7 Unit Unit
3815, 23, 29, 37syl3anc 1228 . . . . . 6 Unit Unit
392zrngunit 18647 . . . . . . . . . 10 Unit
4039baib 903 . . . . . . . . 9 Unit
4115, 40syl 16 . . . . . . . 8 Unit
42 nnnn0 10823 . . . . . . . . . . 11
43 nn0re 10825 . . . . . . . . . . . 12
44 nn0ge0 10842 . . . . . . . . . . . 12
4543, 44absidd 13265 . . . . . . . . . . 11
4642, 45syl 16 . . . . . . . . . 10
4746ad2antrl 727 . . . . . . . . 9
4847eqeq1d 2459 . . . . . . . 8
4941, 48bitrd 253 . . . . . . 7 Unit
502zrngunit 18647 . . . . . . . . . 10 Unit
5150baib 903 . . . . . . . . 9 Unit
5223, 51syl 16 . . . . . . . 8 Unit
53 nnre 10563 . . . . . . . . . . . . 13
5453ad2antrr 725 . . . . . . . . . . . 12
55 simprl 756 . . . . . . . . . . . 12
5654, 55nndivred 10605 . . . . . . . . . . 11
57 nnnn0 10823 . . . . . . . . . . . . . 14
58 nn0ge0 10842 . . . . . . . . . . . . . 14
5957, 58syl 16 . . . . . . . . . . . . 13
6059ad2antrr 725 . . . . . . . . . . . 12
6155nnred 10571 . . . . . . . . . . . 12
62 nngt0 10585 . . . . . . . . . . . . 13
6362ad2antrl 727 . . . . . . . . . . . 12
64 divge0 10432 . . . . . . . . . . . 12
6554, 60, 61, 63, 64syl22anc 1229 . . . . . . . . . . 11
6656, 65absidd 13265 . . . . . . . . . 10
6766eqeq1d 2459 . . . . . . . . 9
68 ax-1cn 9567 . . . . . . . . . . 11
6968a1i 11 . . . . . . . . . 10
7024, 26, 69, 18divmuld 10363 . . . . . . . . 9
7126mulid1d 9630 . . . . . . . . . 10
7271eqeq1d 2459 . . . . . . . . 9
7367, 70, 723bitrd 279 . . . . . . . 8
7452, 73bitrd 253 . . . . . . 7 Unit
7549, 74orbi12d 709 . . . . . 6 Unit Unit
7638, 75mpbid 210 . . . . 5
7776expr 615 . . . 4
7877ralrimiva 2871 . . 3
79 isprm2 14236 . . 3
8013, 78, 79sylanbrc 664 . 2
81 prmz 14232 . . . 4
82 1nprm 14233 . . . . 5
832zrngunit 18647 . . . . . 6 Unit
84 prmnn 14231 . . . . . . . . . 10
85 nn0re 10825 . . . . . . . . . . 11
8685, 58absidd 13265 . . . . . . . . . 10
8784, 57, 863syl 20 . . . . . . . . 9
88 id 22 . . . . . . . . 9
8987, 88eqeltrd 2545 . . . . . . . 8
90 eleq1 2529 . . . . . . . 8
9189, 90syl5ibcom 220 . . . . . . 7
9291adantld 467 . . . . . 6
9383, 92syl5bi 217 . . . . 5 Unit
9482, 93mtoi 178 . . . 4 Unit
95 simplrl 761 . . . . . . . . . . . 12
9695zcnd 10991 . . . . . . . . . . 11
9784ad2antrr 725 . . . . . . . . . . . . . 14
9897nnne0d 10601 . . . . . . . . . . . . 13
99 simpr 461 . . . . . . . . . . . . 13
100 simplrr 762 . . . . . . . . . . . . . . 15
101100zcnd 10991 . . . . . . . . . . . . . 14
102101mul02d 9795 . . . . . . . . . . . . 13
10398, 99, 1023netr4d 2762 . . . . . . . . . . . 12
104 oveq1 6303 . . . . . . . . . . . . 13
105104necon3i 2697 . . . . . . . . . . . 12
106103, 105syl 16 . . . . . . . . . . 11
10796, 106absne0d 13289 . . . . . . . . . 10
108107neneqd 2659 . . . . . . . . 9
109 nn0abscl 13156 . . . . . . . . . . . 12
11095, 109syl 16 . . . . . . . . . . 11
111 elnn0 10818 . . . . . . . . . . 11
112110, 111sylib 196 . . . . . . . . . 10
113112ord 377 . . . . . . . . 9
114108, 113mt3d 125 . . . . . . . 8
11579simprbi 464 . . . . . . . . 9
116115ad2antrr 725 . . . . . . . 8
117 dvdsmul1 14016 . . . . . . . . . . 11
118117ad2antlr 726 . . . . . . . . . 10
119118, 99breqtrd 4480 . . . . . . . . 9
12081ad2antrr 725 . . . . . . . . . 10
121 absdvdsb 14013 . . . . . . . . . 10
12295, 120, 121syl2anc 661 . . . . . . . . 9
123119, 122mpbid 210 . . . . . . . 8
124 breq1 4459 . . . . . . . . . 10
125 eqeq1 2461 . . . . . . . . . . 11
126 eqeq1 2461 . . . . . . . . . . 11
127125, 126orbi12d 709 . . . . . . . . . 10
128124, 127imbi12d 320 . . . . . . . . 9
129128rspcv 3206 . . . . . . . 8
130114, 116, 123, 129syl3c 61 . . . . . . 7
1312zrngunit 18647 . . . . . . . . . 10 Unit
132131baib 903 . . . . . . . . 9 Unit
13395, 132syl 16 . . . . . . . 8 Unit
134100, 40syl 16 . . . . . . . . 9 Unit
135101abscld 13278 . . . . . . . . . . 11
136135recnd 9639 . . . . . . . . . 10
13768a1i 11 . . . . . . . . . 10
13896abscld 13278 . . . . . . . . . . 11
139138recnd 9639 . . . . . . . . . 10
140136, 137, 139, 107mulcand 10203 . . . . . . . . 9
14199fveq2d 5876 . . . . . . . . . . . 12
14296, 101absmuld 13296 . . . . . . . . . . . 12
14387ad2antrr 725 . . . . . . . . . . . 12
144141, 142, 1433eqtr3d 2506 . . . . . . . . . . 11
145139mulid1d 9630 . . . . . . . . . . 11
146144, 145eqeq12d 2479 . . . . . . . . . 10
147 eqcom 2466 . . . . . . . . . 10
148146, 147syl6bb 261 . . . . . . . . 9
149134, 140, 1483bitr2d 281 . . . . . . . 8 Unit
150133, 149orbi12d 709 . . . . . . 7 Unit Unit
151130, 150mpbird 232 . . . . . 6 Unit Unit
152151ex 434 . . . . 5 Unit Unit
153152ralrimivva 2878 . . . 4 Unit Unit
15431, 32, 5, 36isirred2 17476 . . . 4 Unit Unit Unit
15581, 94, 153, 154syl3anbrc 1180 . . 3