Proof of Theorem ppiublem1
Step | Hyp | Ref
| Expression |
1 | | ppiublem1.1 |
. . . . . 6
|
2 | 1 | simpli 474 |
. . . . 5
|
3 | | ppiublem1.3 |
. . . . 5
|
4 | | df-6 11083 |
. . . . 5
|
5 | 2, 3, 4 | 3brtr3i 4682 |
. . . 4
|
6 | | ppiublem1.2 |
. . . . . 6
|
7 | 6 | nn0rei 11303 |
. . . . 5
|
8 | | 5re 11099 |
. . . . 5
|
9 | | 1re 10039 |
. . . . 5
|
10 | 7, 8, 9 | leadd1i 10583 |
. . . 4
|
11 | 5, 10 | mpbir 221 |
. . 3
|
12 | | 6re 11101 |
. . . 4
|
13 | | 5lt6 11204 |
. . . 4
|
14 | 8, 12, 13 | ltleii 10160 |
. . 3
|
15 | 7, 8, 12 | letri 10166 |
. . 3
|
16 | 11, 14, 15 | mp2an 708 |
. 2
|
17 | 6 | nn0zi 11402 |
. . . . 5
|
18 | | 5nn 11188 |
. . . . . 6
|
19 | 18 | nnzi 11401 |
. . . . 5
|
20 | | eluz2 11693 |
. . . . 5
|
21 | 17, 19, 11, 20 | mpbir3an 1244 |
. . . 4
|
22 | | elfzp12 12419 |
. . . 4
|
23 | 21, 22 | ax-mp 5 |
. . 3
|
24 | | ppiublem1.4 |
. . . . 5
|
25 | | prmz 15389 |
. . . . . . . . . . . 12
|
26 | 25 | adantr 481 |
. . . . . . . . . . 11
|
27 | | 2nn 11185 |
. . . . . . . . . . . 12
|
28 | | 6nn 11189 |
. . . . . . . . . . . 12
|
29 | | 3z 11410 |
. . . . . . . . . . . . . . 15
|
30 | | 2z 11409 |
. . . . . . . . . . . . . . 15
|
31 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . 15
|
32 | 29, 30, 31 | mp2an 708 |
. . . . . . . . . . . . . 14
|
33 | | 3t2e6 11179 |
. . . . . . . . . . . . . 14
|
34 | 32, 33 | breqtri 4678 |
. . . . . . . . . . . . 13
|
35 | | dvdsmod 15050 |
. . . . . . . . . . . . 13
|
36 | 34, 35 | mpan2 707 |
. . . . . . . . . . . 12
|
37 | 27, 28, 36 | mp3an12 1414 |
. . . . . . . . . . 11
|
38 | 26, 37 | syl 17 |
. . . . . . . . . 10
|
39 | | uzid 11702 |
. . . . . . . . . . . 12
|
40 | 30, 39 | ax-mp 5 |
. . . . . . . . . . 11
|
41 | | simpl 473 |
. . . . . . . . . . 11
|
42 | | dvdsprm 15415 |
. . . . . . . . . . 11
|
43 | 40, 41, 42 | sylancr 695 |
. . . . . . . . . 10
|
44 | 38, 43 | bitrd 268 |
. . . . . . . . 9
|
45 | | simpr 477 |
. . . . . . . . . . 11
|
46 | | breq2 4657 |
. . . . . . . . . . 11
|
47 | 45, 46 | syl5ibrcom 237 |
. . . . . . . . . 10
|
48 | | 2lt4 11198 |
. . . . . . . . . . . 12
|
49 | | 2re 11090 |
. . . . . . . . . . . . 13
|
50 | | 4re 11097 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | ltnlei 10158 |
. . . . . . . . . . . 12
|
52 | 48, 51 | mpbi 220 |
. . . . . . . . . . 11
|
53 | 52 | pm2.21i 116 |
. . . . . . . . . 10
|
54 | 47, 53 | syl6 35 |
. . . . . . . . 9
|
55 | 44, 54 | sylbid 230 |
. . . . . . . 8
|
56 | | breq2 4657 |
. . . . . . . . 9
|
57 | 56 | imbi1d 331 |
. . . . . . . 8
|
58 | 55, 57 | syl5ibcom 235 |
. . . . . . 7
|
59 | 58 | com3r 87 |
. . . . . 6
|
60 | | 3nn 11186 |
. . . . . . . . . . . 12
|
61 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . 15
|
62 | 29, 30, 61 | mp2an 708 |
. . . . . . . . . . . . . 14
|
63 | 62, 33 | breqtri 4678 |
. . . . . . . . . . . . 13
|
64 | | dvdsmod 15050 |
. . . . . . . . . . . . 13
|
65 | 63, 64 | mpan2 707 |
. . . . . . . . . . . 12
|
66 | 60, 28, 65 | mp3an12 1414 |
. . . . . . . . . . 11
|
67 | 26, 66 | syl 17 |
. . . . . . . . . 10
|
68 | | df-3 11080 |
. . . . . . . . . . . 12
|
69 | | peano2uz 11741 |
. . . . . . . . . . . . 13
|
70 | 40, 69 | ax-mp 5 |
. . . . . . . . . . . 12
|
71 | 68, 70 | eqeltri 2697 |
. . . . . . . . . . 11
|
72 | | dvdsprm 15415 |
. . . . . . . . . . 11
|
73 | 71, 41, 72 | sylancr 695 |
. . . . . . . . . 10
|
74 | 67, 73 | bitrd 268 |
. . . . . . . . 9
|
75 | | breq2 4657 |
. . . . . . . . . . 11
|
76 | 45, 75 | syl5ibrcom 237 |
. . . . . . . . . 10
|
77 | | 3lt4 11197 |
. . . . . . . . . . . 12
|
78 | | 3re 11094 |
. . . . . . . . . . . . 13
|
79 | 78, 50 | ltnlei 10158 |
. . . . . . . . . . . 12
|
80 | 77, 79 | mpbi 220 |
. . . . . . . . . . 11
|
81 | 80 | pm2.21i 116 |
. . . . . . . . . 10
|
82 | 76, 81 | syl6 35 |
. . . . . . . . 9
|
83 | 74, 82 | sylbid 230 |
. . . . . . . 8
|
84 | | breq2 4657 |
. . . . . . . . 9
|
85 | 84 | imbi1d 331 |
. . . . . . . 8
|
86 | 83, 85 | syl5ibcom 235 |
. . . . . . 7
|
87 | 86 | com3r 87 |
. . . . . 6
|
88 | | eleq1a 2696 |
. . . . . . 7
|
89 | 88 | a1d 25 |
. . . . . 6
|
90 | 59, 87, 89 | 3jaoi 1391 |
. . . . 5
|
91 | 24, 90 | ax-mp 5 |
. . . 4
|
92 | 3 | oveq1i 6660 |
. . . . . 6
|
93 | 92 | eleq2i 2693 |
. . . . 5
|
94 | 1 | simpri 478 |
. . . . 5
|
95 | 93, 94 | syl5bir 233 |
. . . 4
|
96 | 91, 95 | jaod 395 |
. . 3
|
97 | 23, 96 | syl5bi 232 |
. 2
|
98 | 16, 97 | pm3.2i 471 |
1
|