Proof of Theorem isprm3
Step | Hyp | Ref
| Expression |
1 | | isprm2 10499 |
. 2
|
2 | | dvdszrcl 10200 |
. . . . . . . . . . 11
|
3 | 2 | simpld 110 |
. . . . . . . . . 10
|
4 | | 1zzd 8378 |
. . . . . . . . . 10
|
5 | | zdceq 8423 |
. . . . . . . . . 10
DECID |
6 | 3, 4, 5 | syl2an2 558 |
. . . . . . . . 9
DECID
|
7 | 2 | simprd 112 |
. . . . . . . . . . 11
|
8 | 7 | adantl 271 |
. . . . . . . . . 10
|
9 | | zdceq 8423 |
. . . . . . . . . 10
DECID |
10 | 3, 8, 9 | syl2an2 558 |
. . . . . . . . 9
DECID
|
11 | | dcor 876 |
. . . . . . . . 9
DECID
DECID
DECID |
12 | 6, 10, 11 | sylc 61 |
. . . . . . . 8
DECID |
13 | | imandc 819 |
. . . . . . . 8
DECID
|
14 | 12, 13 | syl 14 |
. . . . . . 7
|
15 | | eluz2nn 8657 |
. . . . . . . . . . . . . . . 16
|
16 | | nnz 8370 |
. . . . . . . . . . . . . . . . . 18
|
17 | | dvdsle 10244 |
. . . . . . . . . . . . . . . . . 18
|
18 | 16, 17 | sylan 277 |
. . . . . . . . . . . . . . . . 17
|
19 | | nnge1 8062 |
. . . . . . . . . . . . . . . . . 18
|
20 | 19 | adantr 270 |
. . . . . . . . . . . . . . . . 17
|
21 | 18, 20 | jctild 309 |
. . . . . . . . . . . . . . . 16
|
22 | 15, 21 | sylan2 280 |
. . . . . . . . . . . . . . 15
|
23 | | nnz 8370 |
. . . . . . . . . . . . . . . . . 18
|
24 | | zre 8355 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
25 | | 1re 7118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
26 | | leltap 7724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
# |
27 | 25, 26 | mp3an1 1255 |
. . . . . . . . . . . . . . . . . . . . . . 23
# |
28 | 24, 27 | sylan 277 |
. . . . . . . . . . . . . . . . . . . . . 22
# |
29 | | 1z 8377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
30 | | zapne 8422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
# |
31 | 29, 30 | mpan2 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
#
|
32 | 31 | adantr 270 |
. . . . . . . . . . . . . . . . . . . . . 22
# |
33 | 28, 32 | bitrd 186 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | 3adant2 957 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | 3expia 1140 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | zre 8355 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | | leltap 7724 |
. . . . . . . . . . . . . . . . . . . . . . 23
# |
38 | 24, 37 | syl3an1 1202 |
. . . . . . . . . . . . . . . . . . . . . 22
# |
39 | 36, 38 | syl3an2 1203 |
. . . . . . . . . . . . . . . . . . . . 21
# |
40 | | zapne 8422 |
. . . . . . . . . . . . . . . . . . . . . . 23
#
|
41 | 40 | ancoms 264 |
. . . . . . . . . . . . . . . . . . . . . 22
#
|
42 | 41 | 3adant3 958 |
. . . . . . . . . . . . . . . . . . . . 21
#
|
43 | 39, 42 | bitrd 186 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | 43 | 3expia 1140 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 35, 44 | anim12d 328 |
. . . . . . . . . . . . . . . . . 18
|
46 | 23, 45 | sylan2 280 |
. . . . . . . . . . . . . . . . 17
|
47 | | pm4.38 569 |
. . . . . . . . . . . . . . . . . 18
|
48 | | df-ne 2246 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | | nesym 2290 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | 48, 49 | anbi12i 447 |
. . . . . . . . . . . . . . . . . . 19
|
51 | | ioran 701 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 50, 51 | bitr4i 185 |
. . . . . . . . . . . . . . . . . 18
|
53 | 47, 52 | syl6bb 194 |
. . . . . . . . . . . . . . . . 17
|
54 | 46, 53 | syl6 33 |
. . . . . . . . . . . . . . . 16
|
55 | 16, 15, 54 | syl2an 283 |
. . . . . . . . . . . . . . 15
|
56 | 22, 55 | syld 44 |
. . . . . . . . . . . . . 14
|
57 | 56 | imp 122 |
. . . . . . . . . . . . 13
|
58 | | eluzelz 8628 |
. . . . . . . . . . . . . . 15
|
59 | | zltp1le 8405 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 29, 59 | mpan 414 |
. . . . . . . . . . . . . . . . . . 19
|
61 | | df-2 8098 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 61 | breq1i 3792 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 60, 62 | syl6bbr 196 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | adantr 270 |
. . . . . . . . . . . . . . . . 17
|
65 | | zltlem1 8408 |
. . . . . . . . . . . . . . . . 17
|
66 | 64, 65 | anbi12d 456 |
. . . . . . . . . . . . . . . 16
|
67 | | peano2zm 8389 |
. . . . . . . . . . . . . . . . 17
|
68 | | 2z 8379 |
. . . . . . . . . . . . . . . . . 18
|
69 | | elfz 9035 |
. . . . . . . . . . . . . . . . . 18
|
70 | 68, 69 | mp3an2 1256 |
. . . . . . . . . . . . . . . . 17
|
71 | 67, 70 | sylan2 280 |
. . . . . . . . . . . . . . . 16
|
72 | 66, 71 | bitr4d 189 |
. . . . . . . . . . . . . . 15
|
73 | 16, 58, 72 | syl2an 283 |
. . . . . . . . . . . . . 14
|
74 | 73 | adantr 270 |
. . . . . . . . . . . . 13
|
75 | 57, 74 | bitr3d 188 |
. . . . . . . . . . . 12
|
76 | 75 | anasss 391 |
. . . . . . . . . . 11
|
77 | 76 | expcom 114 |
. . . . . . . . . 10
|
78 | 77 | pm5.32d 437 |
. . . . . . . . 9
|
79 | | fzssuz 9083 |
. . . . . . . . . . . . 13
|
80 | | 2eluzge1 8664 |
. . . . . . . . . . . . . 14
|
81 | | uzss 8639 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | ax-mp 7 |
. . . . . . . . . . . . 13
|
83 | 79, 82 | sstri 3008 |
. . . . . . . . . . . 12
|
84 | | nnuz 8654 |
. . . . . . . . . . . 12
|
85 | 83, 84 | sseqtr4i 3032 |
. . . . . . . . . . 11
|
86 | 85 | sseli 2995 |
. . . . . . . . . 10
|
87 | 86 | pm4.71ri 384 |
. . . . . . . . 9
|
88 | 78, 87 | syl6bbr 196 |
. . . . . . . 8
|
89 | 88 | notbid 624 |
. . . . . . 7
|
90 | 14, 89 | bitrd 186 |
. . . . . 6
|
91 | 90 | pm5.74da 431 |
. . . . 5
|
92 | | bi2.04 246 |
. . . . 5
|
93 | | con2b 625 |
. . . . 5
|
94 | 91, 92, 93 | 3bitr3g 220 |
. . . 4
|
95 | 94 | ralbidv2 2370 |
. . 3
|
96 | 95 | pm5.32i 441 |
. 2
|
97 | 1, 96 | bitri 182 |
1
|