Step Hyp Ref
Expression 1 isprm2 14225 . 2
2 iman 424 . . . . . . 7
3 eluz2nn 11148 . . . . . . . . . . . . . . . 16
4 nnz 10911 . . . . . . . . . . . . . . . . . 18
5 dvdsle 14031 . . . . . . . . . . . . . . . . . 18
6 4 , 5 sylan 471 . . . . . . . . . . . . . . . . 17
7 nnge1 10587 . . . . . . . . . . . . . . . . . 18
8 7 adantr 465 . . . . . . . . . . . . . . . . 17
9 6 , 8 jctild 543 . . . . . . . . . . . . . . . 16
10 3 , 9 sylan2 474 . . . . . . . . . . . . . . 15
11 zre 10893 . . . . . . . . . . . . . . . . . 18
12 nnre 10568 . . . . . . . . . . . . . . . . . 18
13 1re 9616 . . . . . . . . . . . . . . . . . . . . . 22
14 leltne 9695 . . . . . . . . . . . . . . . . . . . . . 22
15 13 , 14 mp3an1 1311 . . . . . . . . . . . . . . . . . . . . 21
16 15 3adant2 1015 . . . . . . . . . . . . . . . . . . . 20
17 16 3expia 1198 . . . . . . . . . . . . . . . . . . 19
18 leltne 9695 . . . . . . . . . . . . . . . . . . . 20
19 18 3expia 1198 . . . . . . . . . . . . . . . . . . 19
20 17 , 19 anim12d 563 . . . . . . . . . . . . . . . . . 18
21 11 , 12 , 20 syl2an 477 . . . . . . . . . . . . . . . . 17
22 pm4.38 872 . . . . . . . . . . . . . . . . . 18
23 df-ne 2654 . . . . . . . . . . . . . . . . . . . 20
24 nesym 2729 . . . . . . . . . . . . . . . . . . . 20
25 23 , 24 anbi12i 697 . . . . . . . . . . . . . . . . . . 19
26 ioran 490 . . . . . . . . . . . . . . . . . . 19
27 25 , 26 bitr4i 252 . . . . . . . . . . . . . . . . . 18
28 22 , 27 syl6bb 261 . . . . . . . . . . . . . . . . 17
29 21 , 28 syl6 33 . . . . . . . . . . . . . . . 16
30 4 , 3 , 29 syl2an 477 . . . . . . . . . . . . . . 15
31 10 , 30 syld 44 . . . . . . . . . . . . . 14
32 31 imp 429 . . . . . . . . . . . . 13
33 eluzelz 11119 . . . . . . . . . . . . . . 15
34 1z 10919 . . . . . . . . . . . . . . . . . . . 20
35 zltp1le 10938 . . . . . . . . . . . . . . . . . . . 20
36 34 , 35 mpan 670 . . . . . . . . . . . . . . . . . . 19
37 df-2 10619 . . . . . . . . . . . . . . . . . . . 20
38 37 breq1i 4459 . . . . . . . . . . . . . . . . . . 19
39 36 , 38 syl6bbr 263 . . . . . . . . . . . . . . . . . 18
40 39 adantr 465 . . . . . . . . . . . . . . . . 17
41 zltlem1 10941 . . . . . . . . . . . . . . . . 17
42 40 , 41 anbi12d 710 . . . . . . . . . . . . . . . 16
43 peano2zm 10932 . . . . . . . . . . . . . . . . 17
44 2z 10921 . . . . . . . . . . . . . . . . . 18
45 elfz 11707 . . . . . . . . . . . . . . . . . 18
46 44 , 45 mp3an2 1312 . . . . . . . . . . . . . . . . 17
47 43 , 46 sylan2 474 . . . . . . . . . . . . . . . 16
48 42 , 47 bitr4d 256 . . . . . . . . . . . . . . 15
49 4 , 33 , 48 syl2an 477 . . . . . . . . . . . . . 14
50 49 adantr 465 . . . . . . . . . . . . 13
51 32 , 50 bitr3d 255 . . . . . . . . . . . 12
52 51 anasss 647 . . . . . . . . . . 11
53 52 expcom 435 . . . . . . . . . 10
54 53 pm5.32d 639 . . . . . . . . 9
55 fzssuz 11753 . . . . . . . . . . . . 13
56 2eluzge1 11156 . . . . . . . . . . . . . 14
57 uzss 11130 . . . . . . . . . . . . . 14
58 56 , 57 ax-mp 5 . . . . . . . . . . . . 13
59 55 , 58 sstri 3512 . . . . . . . . . . . 12
60 nnuz 11145 . . . . . . . . . . . 12
61 59 , 60 sseqtr4i 3536 . . . . . . . . . . 11
62 61 sseli 3499 . . . . . . . . . 10
63 62 pm4.71ri 633 . . . . . . . . 9
64 54 , 63 syl6bbr 263 . . . . . . . 8
65 64 notbid 294 . . . . . . 7
66 2 , 65 syl5bb 257 . . . . . 6
67 66 pm5.74da 687 . . . . 5
68 bi2.04 361 . . . . 5
69 con2b 334 . . . . 5
70 67 , 68 , 69 3bitr3g 287 . . . 4
71 70 ralbidv2 2892 . . 3
72 71 pm5.32i 637 . 2
73 1 , 72 bitri 249 1
