Step | Hyp | Ref
| Expression |
1 | | ppiublem1.1 |
. . . . . 6
โข (๐ โค 6 โง ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) โ (๐...5) โ (๐ mod 6) โ {1, 5}))) |
2 | 1 | simpli 485 |
. . . . 5
โข ๐ โค 6 |
3 | | ppiublem1.3 |
. . . . 5
โข ๐ = (๐ + 1) |
4 | | df-6 12227 |
. . . . 5
โข 6 = (5 +
1) |
5 | 2, 3, 4 | 3brtr3i 5139 |
. . . 4
โข (๐ + 1) โค (5 +
1) |
6 | | ppiublem1.2 |
. . . . . 6
โข ๐ โ
โ0 |
7 | 6 | nn0rei 12431 |
. . . . 5
โข ๐ โ โ |
8 | | 5re 12247 |
. . . . 5
โข 5 โ
โ |
9 | | 1re 11162 |
. . . . 5
โข 1 โ
โ |
10 | 7, 8, 9 | leadd1i 11717 |
. . . 4
โข (๐ โค 5 โ (๐ + 1) โค (5 +
1)) |
11 | 5, 10 | mpbir 230 |
. . 3
โข ๐ โค 5 |
12 | | 6re 12250 |
. . . 4
โข 6 โ
โ |
13 | | 5lt6 12341 |
. . . 4
โข 5 <
6 |
14 | 8, 12, 13 | ltleii 11285 |
. . 3
โข 5 โค
6 |
15 | 7, 8, 12 | letri 11291 |
. . 3
โข ((๐ โค 5 โง 5 โค 6) โ
๐ โค 6) |
16 | 11, 14, 15 | mp2an 691 |
. 2
โข ๐ โค 6 |
17 | 6 | nn0zi 12535 |
. . . . 5
โข ๐ โ โค |
18 | | 5nn 12246 |
. . . . . 6
โข 5 โ
โ |
19 | 18 | nnzi 12534 |
. . . . 5
โข 5 โ
โค |
20 | | eluz2 12776 |
. . . . 5
โข (5 โ
(โคโฅโ๐) โ (๐ โ โค โง 5 โ โค โง
๐ โค 5)) |
21 | 17, 19, 11, 20 | mpbir3an 1342 |
. . . 4
โข 5 โ
(โคโฅโ๐) |
22 | | elfzp12 13527 |
. . . 4
โข (5 โ
(โคโฅโ๐) โ ((๐ mod 6) โ (๐...5) โ ((๐ mod 6) = ๐ โจ (๐ mod 6) โ ((๐ + 1)...5)))) |
23 | 21, 22 | ax-mp 5 |
. . 3
โข ((๐ mod 6) โ (๐...5) โ ((๐ mod 6) = ๐ โจ (๐ mod 6) โ ((๐ + 1)...5))) |
24 | | ppiublem1.4 |
. . . . 5
โข (2
โฅ ๐ โจ 3 โฅ
๐ โจ ๐ โ {1, 5}) |
25 | | 2nn 12233 |
. . . . . . . . . . 11
โข 2 โ
โ |
26 | | 6nn 12249 |
. . . . . . . . . . 11
โข 6 โ
โ |
27 | | prmz 16558 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
28 | 27 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 4 โค
๐) โ ๐ โ โค) |
29 | | 3z 12543 |
. . . . . . . . . . . . . 14
โข 3 โ
โค |
30 | | 2z 12542 |
. . . . . . . . . . . . . 14
โข 2 โ
โค |
31 | | dvdsmul2 16168 |
. . . . . . . . . . . . . 14
โข ((3
โ โค โง 2 โ โค) โ 2 โฅ (3 ยท
2)) |
32 | 29, 30, 31 | mp2an 691 |
. . . . . . . . . . . . 13
โข 2 โฅ
(3 ยท 2) |
33 | | 3t2e6 12326 |
. . . . . . . . . . . . 13
โข (3
ยท 2) = 6 |
34 | 32, 33 | breqtri 5135 |
. . . . . . . . . . . 12
โข 2 โฅ
6 |
35 | | dvdsmod 16218 |
. . . . . . . . . . . 12
โข (((2
โ โ โง 6 โ โ โง ๐ โ โค) โง 2 โฅ 6) โ
(2 โฅ (๐ mod 6) โ
2 โฅ ๐)) |
36 | 34, 35 | mpan2 690 |
. . . . . . . . . . 11
โข ((2
โ โ โง 6 โ โ โง ๐ โ โค) โ (2 โฅ (๐ mod 6) โ 2 โฅ ๐)) |
37 | 25, 26, 28, 36 | mp3an12i 1466 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (2 โฅ (๐ mod 6) โ 2 โฅ ๐)) |
38 | | uzid 12785 |
. . . . . . . . . . . 12
โข (2 โ
โค โ 2 โ (โคโฅโ2)) |
39 | 30, 38 | ax-mp 5 |
. . . . . . . . . . 11
โข 2 โ
(โคโฅโ2) |
40 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 4 โค
๐) โ ๐ โ โ) |
41 | | dvdsprm 16586 |
. . . . . . . . . . 11
โข ((2
โ (โคโฅโ2) โง ๐ โ โ) โ (2 โฅ ๐ โ 2 = ๐)) |
42 | 39, 40, 41 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (2 โฅ ๐ โ 2 = ๐)) |
43 | 37, 42 | bitrd 279 |
. . . . . . . . 9
โข ((๐ โ โ โง 4 โค
๐) โ (2 โฅ (๐ mod 6) โ 2 = ๐)) |
44 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 4 โค
๐) โ 4 โค ๐) |
45 | | breq2 5114 |
. . . . . . . . . . 11
โข (2 =
๐ โ (4 โค 2 โ 4
โค ๐)) |
46 | 44, 45 | syl5ibrcom 247 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (2 = ๐ โ 4 โค
2)) |
47 | | 2lt4 12335 |
. . . . . . . . . . . 12
โข 2 <
4 |
48 | | 2re 12234 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
49 | | 4re 12244 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
50 | 48, 49 | ltnlei 11283 |
. . . . . . . . . . . 12
โข (2 < 4
โ ยฌ 4 โค 2) |
51 | 47, 50 | mpbi 229 |
. . . . . . . . . . 11
โข ยฌ 4
โค 2 |
52 | 51 | pm2.21i 119 |
. . . . . . . . . 10
โข (4 โค 2
โ (๐ mod 6) โ {1,
5}) |
53 | 46, 52 | syl6 35 |
. . . . . . . . 9
โข ((๐ โ โ โง 4 โค
๐) โ (2 = ๐ โ (๐ mod 6) โ {1, 5})) |
54 | 43, 53 | sylbid 239 |
. . . . . . . 8
โข ((๐ โ โ โง 4 โค
๐) โ (2 โฅ (๐ mod 6) โ (๐ mod 6) โ {1,
5})) |
55 | | breq2 5114 |
. . . . . . . . 9
โข ((๐ mod 6) = ๐ โ (2 โฅ (๐ mod 6) โ 2 โฅ ๐)) |
56 | 55 | imbi1d 342 |
. . . . . . . 8
โข ((๐ mod 6) = ๐ โ ((2 โฅ (๐ mod 6) โ (๐ mod 6) โ {1, 5}) โ (2 โฅ
๐ โ (๐ mod 6) โ {1, 5}))) |
57 | 54, 56 | syl5ibcom 244 |
. . . . . . 7
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (2 โฅ ๐ โ (๐ mod 6) โ {1, 5}))) |
58 | 57 | com3r 87 |
. . . . . 6
โข (2
โฅ ๐ โ ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5}))) |
59 | | 3nn 12239 |
. . . . . . . . . . 11
โข 3 โ
โ |
60 | | dvdsmul1 16167 |
. . . . . . . . . . . . . 14
โข ((3
โ โค โง 2 โ โค) โ 3 โฅ (3 ยท
2)) |
61 | 29, 30, 60 | mp2an 691 |
. . . . . . . . . . . . 13
โข 3 โฅ
(3 ยท 2) |
62 | 61, 33 | breqtri 5135 |
. . . . . . . . . . . 12
โข 3 โฅ
6 |
63 | | dvdsmod 16218 |
. . . . . . . . . . . 12
โข (((3
โ โ โง 6 โ โ โง ๐ โ โค) โง 3 โฅ 6) โ
(3 โฅ (๐ mod 6) โ
3 โฅ ๐)) |
64 | 62, 63 | mpan2 690 |
. . . . . . . . . . 11
โข ((3
โ โ โง 6 โ โ โง ๐ โ โค) โ (3 โฅ (๐ mod 6) โ 3 โฅ ๐)) |
65 | 59, 26, 28, 64 | mp3an12i 1466 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (3 โฅ (๐ mod 6) โ 3 โฅ ๐)) |
66 | | df-3 12224 |
. . . . . . . . . . . 12
โข 3 = (2 +
1) |
67 | | peano2uz 12833 |
. . . . . . . . . . . . 13
โข (2 โ
(โคโฅโ2) โ (2 + 1) โ
(โคโฅโ2)) |
68 | 39, 67 | ax-mp 5 |
. . . . . . . . . . . 12
โข (2 + 1)
โ (โคโฅโ2) |
69 | 66, 68 | eqeltri 2834 |
. . . . . . . . . . 11
โข 3 โ
(โคโฅโ2) |
70 | | dvdsprm 16586 |
. . . . . . . . . . 11
โข ((3
โ (โคโฅโ2) โง ๐ โ โ) โ (3 โฅ ๐ โ 3 = ๐)) |
71 | 69, 40, 70 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (3 โฅ ๐ โ 3 = ๐)) |
72 | 65, 71 | bitrd 279 |
. . . . . . . . 9
โข ((๐ โ โ โง 4 โค
๐) โ (3 โฅ (๐ mod 6) โ 3 = ๐)) |
73 | | breq2 5114 |
. . . . . . . . . . 11
โข (3 =
๐ โ (4 โค 3 โ 4
โค ๐)) |
74 | 44, 73 | syl5ibrcom 247 |
. . . . . . . . . 10
โข ((๐ โ โ โง 4 โค
๐) โ (3 = ๐ โ 4 โค
3)) |
75 | | 3lt4 12334 |
. . . . . . . . . . . 12
โข 3 <
4 |
76 | | 3re 12240 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
77 | 76, 49 | ltnlei 11283 |
. . . . . . . . . . . 12
โข (3 < 4
โ ยฌ 4 โค 3) |
78 | 75, 77 | mpbi 229 |
. . . . . . . . . . 11
โข ยฌ 4
โค 3 |
79 | 78 | pm2.21i 119 |
. . . . . . . . . 10
โข (4 โค 3
โ (๐ mod 6) โ {1,
5}) |
80 | 74, 79 | syl6 35 |
. . . . . . . . 9
โข ((๐ โ โ โง 4 โค
๐) โ (3 = ๐ โ (๐ mod 6) โ {1, 5})) |
81 | 72, 80 | sylbid 239 |
. . . . . . . 8
โข ((๐ โ โ โง 4 โค
๐) โ (3 โฅ (๐ mod 6) โ (๐ mod 6) โ {1,
5})) |
82 | | breq2 5114 |
. . . . . . . . 9
โข ((๐ mod 6) = ๐ โ (3 โฅ (๐ mod 6) โ 3 โฅ ๐)) |
83 | 82 | imbi1d 342 |
. . . . . . . 8
โข ((๐ mod 6) = ๐ โ ((3 โฅ (๐ mod 6) โ (๐ mod 6) โ {1, 5}) โ (3 โฅ
๐ โ (๐ mod 6) โ {1, 5}))) |
84 | 81, 83 | syl5ibcom 244 |
. . . . . . 7
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (3 โฅ ๐ โ (๐ mod 6) โ {1, 5}))) |
85 | 84 | com3r 87 |
. . . . . 6
โข (3
โฅ ๐ โ ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5}))) |
86 | | eleq1a 2833 |
. . . . . . 7
โข (๐ โ {1, 5} โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5})) |
87 | 86 | a1d 25 |
. . . . . 6
โข (๐ โ {1, 5} โ ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5}))) |
88 | 58, 85, 87 | 3jaoi 1428 |
. . . . 5
โข ((2
โฅ ๐ โจ 3 โฅ
๐ โจ ๐ โ {1, 5}) โ ((๐ โ โ โง 4 โค ๐) โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5}))) |
89 | 24, 88 | ax-mp 5 |
. . . 4
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) = ๐ โ (๐ mod 6) โ {1, 5})) |
90 | 3 | oveq1i 7372 |
. . . . . 6
โข (๐...5) = ((๐ + 1)...5) |
91 | 90 | eleq2i 2830 |
. . . . 5
โข ((๐ mod 6) โ (๐...5) โ (๐ mod 6) โ ((๐ + 1)...5)) |
92 | 1 | simpri 487 |
. . . . 5
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) โ (๐...5) โ (๐ mod 6) โ {1, 5})) |
93 | 91, 92 | biimtrrid 242 |
. . . 4
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) โ ((๐ + 1)...5) โ (๐ mod 6) โ {1,
5})) |
94 | 89, 93 | jaod 858 |
. . 3
โข ((๐ โ โ โง 4 โค
๐) โ (((๐ mod 6) = ๐ โจ (๐ mod 6) โ ((๐ + 1)...5)) โ (๐ mod 6) โ {1, 5})) |
95 | 23, 94 | biimtrid 241 |
. 2
โข ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) โ (๐...5) โ (๐ mod 6) โ {1, 5})) |
96 | 16, 95 | pm3.2i 472 |
1
โข (๐ โค 6 โง ((๐ โ โ โง 4 โค
๐) โ ((๐ mod 6) โ (๐...5) โ (๐ mod 6) โ {1, 5}))) |