Proof of Theorem ppiublem1
Step | Hyp | Ref
| Expression |
1 | | ppiublem1.1 |
. . . . . 6
  
                 |
2 | 1 | simpli 458 |
. . . . 5
 |
3 | | ppiublem1.3 |
. . . . 5
   |
4 | | df-6 10490 |
. . . . 5
   |
5 | 2, 3, 4 | 3brtr3i 4422 |
. . . 4
     |
6 | | ppiublem1.2 |
. . . . . 6
 |
7 | 6 | nn0rei 10696 |
. . . . 5
 |
8 | | 5re 10506 |
. . . . 5
 |
9 | | 1re 9491 |
. . . . 5
 |
10 | 7, 8, 9 | leadd1i 10001 |
. . . 4

      |
11 | 5, 10 | mpbir 209 |
. . 3
 |
12 | | 6re 10508 |
. . . 4
 |
13 | | 5lt6 10604 |
. . . 4
 |
14 | 8, 12, 13 | ltleii 9603 |
. . 3
 |
15 | 7, 8, 12 | letri 9609 |
. . 3
 
   |
16 | 11, 14, 15 | mp2an 672 |
. 2
 |
17 | 6 | nn0zi 10777 |
. . . . 5
 |
18 | | 5nn 10588 |
. . . . . 6
 |
19 | 18 | nnzi 10776 |
. . . . 5
 |
20 | | eluz2 10973 |
. . . . 5
         |
21 | 17, 19, 11, 20 | mpbir3an 1170 |
. . . 4
     |
22 | | elfzp12 11651 |
. . . 4
    
                      |
23 | 21, 22 | ax-mp 5 |
. . 3
      
              |
24 | | ppiublem1.4 |
. . . . 5
      |
25 | | prmz 13880 |
. . . . . . . . . . . 12

  |
26 | 25 | adantr 465 |
. . . . . . . . . . 11
     |
27 | | 2nn 10585 |
. . . . . . . . . . . 12
 |
28 | | 6nn 10589 |
. . . . . . . . . . . 12
 |
29 | | 3z 10785 |
. . . . . . . . . . . . . . 15
 |
30 | | 2z 10784 |
. . . . . . . . . . . . . . 15
 |
31 | | dvdsmul2 13668 |
. . . . . . . . . . . . . . 15
 
     |
32 | 29, 30, 31 | mp2an 672 |
. . . . . . . . . . . . . 14
   |
33 | | 3t2e6 10579 |
. . . . . . . . . . . . . 14
   |
34 | 32, 33 | breqtri 4418 |
. . . . . . . . . . . . 13
 |
35 | | dvdsmod 13703 |
. . . . . . . . . . . . 13
  

  
    |
36 | 34, 35 | mpan2 671 |
. . . . . . . . . . . 12
 
 
 
   |
37 | 27, 28, 36 | mp3an12 1305 |
. . . . . . . . . . 11
 
 
   |
38 | 26, 37 | syl 16 |
. . . . . . . . . 10
   
 
   |
39 | | uzid 10981 |
. . . . . . . . . . . 12
       |
40 | 30, 39 | ax-mp 5 |
. . . . . . . . . . 11
     |
41 | | simpl 457 |
. . . . . . . . . . 11
     |
42 | | dvdsprm 13898 |
. . . . . . . . . . 11
       
   |
43 | 40, 41, 42 | sylancr 663 |
. . . . . . . . . 10
   
   |
44 | 38, 43 | bitrd 253 |
. . . . . . . . 9
   
 
   |
45 | | simpr 461 |
. . . . . . . . . . 11
     |
46 | | breq2 4399 |
. . . . . . . . . . 11
 
   |
47 | 45, 46 | syl5ibrcom 222 |
. . . . . . . . . 10
   
   |
48 | | 2lt4 10598 |
. . . . . . . . . . . 12
 |
49 | | 2re 10497 |
. . . . . . . . . . . . 13
 |
50 | | 4re 10504 |
. . . . . . . . . . . . 13
 |
51 | 49, 50 | ltnlei 9601 |
. . . . . . . . . . . 12

  |
52 | 48, 51 | mpbi 208 |
. . . . . . . . . . 11
 |
53 | 52 | pm2.21i 131 |
. . . . . . . . . 10
        |
54 | 47, 53 | syl6 33 |
. . . . . . . . 9
            |
55 | 44, 54 | sylbid 215 |
. . . . . . . 8
   
          |
56 | | breq2 4399 |
. . . . . . . . 9
   
 
   |
57 | 56 | imbi1d 317 |
. . . . . . . 8
                       |
58 | 55, 57 | syl5ibcom 220 |
. . . . . . 7
                |
59 | 58 | com3r 79 |
. . . . . 6
  
             |
60 | | 3nn 10586 |
. . . . . . . . . . . 12
 |
61 | | dvdsmul1 13667 |
. . . . . . . . . . . . . . 15
 
     |
62 | 29, 30, 61 | mp2an 672 |
. . . . . . . . . . . . . 14
   |
63 | 62, 33 | breqtri 4418 |
. . . . . . . . . . . . 13
 |
64 | | dvdsmod 13703 |
. . . . . . . . . . . . 13
  

  
    |
65 | 63, 64 | mpan2 671 |
. . . . . . . . . . . 12
 
 
 
   |
66 | 60, 28, 65 | mp3an12 1305 |
. . . . . . . . . . 11
 
 
   |
67 | 26, 66 | syl 16 |
. . . . . . . . . 10
   
 
   |
68 | | df-3 10487 |
. . . . . . . . . . . 12
   |
69 | | peano2uz 11014 |
. . . . . . . . . . . . 13
    
        |
70 | 40, 69 | ax-mp 5 |
. . . . . . . . . . . 12
       |
71 | 68, 70 | eqeltri 2536 |
. . . . . . . . . . 11
     |
72 | | dvdsprm 13898 |
. . . . . . . . . . 11
       
   |
73 | 71, 41, 72 | sylancr 663 |
. . . . . . . . . 10
   
   |
74 | 67, 73 | bitrd 253 |
. . . . . . . . 9
   
 
   |
75 | | breq2 4399 |
. . . . . . . . . . 11
 
   |
76 | 45, 75 | syl5ibrcom 222 |
. . . . . . . . . 10
   
   |
77 | | 3lt4 10597 |
. . . . . . . . . . . 12
 |
78 | | 3re 10501 |
. . . . . . . . . . . . 13
 |
79 | 78, 50 | ltnlei 9601 |
. . . . . . . . . . . 12

  |
80 | 77, 79 | mpbi 208 |
. . . . . . . . . . 11
 |
81 | 80 | pm2.21i 131 |
. . . . . . . . . 10
        |
82 | 76, 81 | syl6 33 |
. . . . . . . . 9
            |
83 | 74, 82 | sylbid 215 |
. . . . . . . 8
   
          |
84 | | breq2 4399 |
. . . . . . . . 9
   
 
   |
85 | 84 | imbi1d 317 |
. . . . . . . 8
                       |
86 | 83, 85 | syl5ibcom 220 |
. . . . . . 7
                |
87 | 86 | com3r 79 |
. . . . . 6
  
             |
88 | | eleq1a 2535 |
. . . . . . 7
               |
89 | 88 | a1d 25 |
. . . . . 6
     
             |
90 | 59, 87, 89 | 3jaoi 1282 |
. . . . 5
       
             |
91 | 24, 90 | ax-mp 5 |
. . . 4
              |
92 | 3 | oveq1i 6205 |
. . . . . 6
           |
93 | 92 | eleq2i 2530 |
. . . . 5
      
          |
94 | 1 | simpri 462 |
. . . . 5
                  |
95 | 93, 94 | syl5bir 218 |
. . . 4
                    |
96 | 91, 95 | jaod 380 |
. . 3
               
        |
97 | 23, 96 | syl5bi 217 |
. 2
                  |
98 | 16, 97 | pm3.2i 455 |
1
  
                 |