Step | Hyp | Ref
| Expression |
1 | | nnrp 12927 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ+) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ
โ+) |
3 | | elfzelz 13442 |
. . . . . 6
โข (๐ โ (1...((๐ โ 1) / 2)) โ ๐ โ โค) |
4 | | zre 12504 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
5 | | 2re 12228 |
. . . . . . . 8
โข 2 โ
โ |
6 | 5 | a1i 11 |
. . . . . . 7
โข (๐ โ โค โ 2 โ
โ) |
7 | 4, 6 | remulcld 11186 |
. . . . . 6
โข (๐ โ โค โ (๐ ยท 2) โ
โ) |
8 | 3, 7 | syl 17 |
. . . . 5
โข (๐ โ (1...((๐ โ 1) / 2)) โ (๐ ยท 2) โ โ) |
9 | 2, 8 | anim12ci 615 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ ยท 2) โ โ
โง ๐ โ
โ+)) |
10 | | elfznn 13471 |
. . . . . 6
โข (๐ โ (1...((๐ โ 1) / 2)) โ ๐ โ โ) |
11 | | nnre 12161 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
12 | | nnnn0 12421 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
13 | 12 | nn0ge0d 12477 |
. . . . . . 7
โข (๐ โ โ โ 0 โค
๐) |
14 | | 0le2 12256 |
. . . . . . . . 9
โข 0 โค
2 |
15 | 5, 14 | pm3.2i 472 |
. . . . . . . 8
โข (2 โ
โ โง 0 โค 2) |
16 | 15 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ (2 โ
โ โง 0 โค 2)) |
17 | | mulge0 11674 |
. . . . . . 7
โข (((๐ โ โ โง 0 โค
๐) โง (2 โ โ
โง 0 โค 2)) โ 0 โค (๐ ยท 2)) |
18 | 11, 13, 16, 17 | syl21anc 837 |
. . . . . 6
โข (๐ โ โ โ 0 โค
(๐ ยท
2)) |
19 | 10, 18 | syl 17 |
. . . . 5
โข (๐ โ (1...((๐ โ 1) / 2)) โ 0 โค (๐ ยท 2)) |
20 | 19 | adantl 483 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ 0 โค (๐ ยท 2)) |
21 | | elfz2 13432 |
. . . . . 6
โข (๐ โ (1...((๐ โ 1) / 2)) โ ((1 โ โค
โง ((๐ โ 1) / 2)
โ โค โง ๐
โ โค) โง (1 โค ๐ โง ๐ โค ((๐ โ 1) / 2)))) |
22 | 4 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ ๐ โ โ) |
23 | | zre 12504 |
. . . . . . . . . . 11
โข (((๐ โ 1) / 2) โ โค
โ ((๐ โ 1) / 2)
โ โ) |
24 | 23 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ ((๐ โ 1) / 2) โ
โ) |
25 | | 2pos 12257 |
. . . . . . . . . . . 12
โข 0 <
2 |
26 | 5, 25 | pm3.2i 472 |
. . . . . . . . . . 11
โข (2 โ
โ โง 0 < 2) |
27 | 26 | a1i 11 |
. . . . . . . . . 10
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ (2 โ โ
โง 0 < 2)) |
28 | | lemul1 12008 |
. . . . . . . . . 10
โข ((๐ โ โ โง ((๐ โ 1) / 2) โ โ
โง (2 โ โ โง 0 < 2)) โ (๐ โค ((๐ โ 1) / 2) โ (๐ ยท 2) โค (((๐ โ 1) / 2) ยท
2))) |
29 | 22, 24, 27, 28 | syl3anc 1372 |
. . . . . . . . 9
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ (๐ โค ((๐ โ 1) / 2) โ (๐ ยท 2) โค (((๐ โ 1) / 2) ยท
2))) |
30 | | nncn 12162 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
31 | | peano2cnm 11468 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
33 | | 2cnd 12232 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ) |
34 | | 2ne0 12258 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
0 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
0) |
36 | 32, 33, 35 | divcan1d 11933 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (((๐ โ 1) / 2) ยท 2) =
(๐ โ
1)) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (((๐ โ 1) / 2) ยท 2) =
(๐ โ
1)) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ (((๐ โ 1) / 2) ยท 2) = (๐ โ 1)) |
39 | 38 | breq2d 5118 |
. . . . . . . . . . . 12
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ ((๐ ยท 2) โค (((๐ โ 1) / 2) ยท 2) โ (๐ ยท 2) โค (๐ โ 1))) |
40 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โค) |
41 | | 2z 12536 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โค |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ 2 โ
โค) |
43 | 40, 42 | zmulcld 12614 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (๐ ยท 2) โ
โค) |
44 | 43 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ (๐ ยท 2) โ โค) |
45 | | nnz 12521 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โค) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ
โค) |
47 | | zltlem1 12557 |
. . . . . . . . . . . . . 14
โข (((๐ ยท 2) โ โค
โง ๐ โ โค)
โ ((๐ ยท 2) <
๐ โ (๐ ยท 2) โค (๐ โ 1))) |
48 | 44, 46, 47 | syl2an 597 |
. . . . . . . . . . . . 13
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ ((๐ ยท 2) < ๐ โ (๐ ยท 2) โค (๐ โ 1))) |
49 | 48 | biimprd 248 |
. . . . . . . . . . . 12
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ ((๐ ยท 2) โค (๐ โ 1) โ (๐ ยท 2) < ๐)) |
50 | 39, 49 | sylbid 239 |
. . . . . . . . . . 11
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (๐ โ โ โง ยฌ 2 โฅ ๐)) โ ((๐ ยท 2) โค (((๐ โ 1) / 2) ยท 2) โ (๐ ยท 2) < ๐)) |
51 | 50 | ex 414 |
. . . . . . . . . 10
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ ((๐ โ โ โง ยฌ 2 โฅ ๐) โ ((๐ ยท 2) โค (((๐ โ 1) / 2) ยท 2) โ (๐ ยท 2) < ๐))) |
52 | 51 | com23 86 |
. . . . . . . . 9
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ ((๐ ยท 2) โค (((๐ โ 1) / 2) ยท 2) โ ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (๐ ยท 2) < ๐))) |
53 | 29, 52 | sylbid 239 |
. . . . . . . 8
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ (๐ โค ((๐ โ 1) / 2) โ ((๐ โ โ โง ยฌ 2 โฅ ๐) โ (๐ ยท 2) < ๐))) |
54 | 53 | a1d 25 |
. . . . . . 7
โข ((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โ (1 โค ๐ โ (๐ โค ((๐ โ 1) / 2) โ ((๐ โ โ โง ยฌ 2 โฅ ๐) โ (๐ ยท 2) < ๐)))) |
55 | 54 | imp32 420 |
. . . . . 6
โข (((1
โ โค โง ((๐
โ 1) / 2) โ โค โง ๐ โ โค) โง (1 โค ๐ โง ๐ โค ((๐ โ 1) / 2))) โ ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (๐ ยท 2) < ๐)) |
56 | 21, 55 | sylbi 216 |
. . . . 5
โข (๐ โ (1...((๐ โ 1) / 2)) โ ((๐ โ โ โง ยฌ 2 โฅ ๐) โ (๐ ยท 2) < ๐)) |
57 | 56 | impcom 409 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ ยท 2) < ๐) |
58 | | modid 13802 |
. . . 4
โข ((((๐ ยท 2) โ โ
โง ๐ โ
โ+) โง (0 โค (๐ ยท 2) โง (๐ ยท 2) < ๐)) โ ((๐ ยท 2) mod ๐) = (๐ ยท 2)) |
59 | 9, 20, 57, 58 | syl12anc 836 |
. . 3
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ ((๐ ยท 2) mod ๐) = (๐ ยท 2)) |
60 | 59 | eqcomd 2743 |
. 2
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ (1...((๐ โ 1) / 2))) โ (๐ ยท 2) = ((๐ ยท 2) mod ๐)) |
61 | 60 | ralrimiva 3144 |
1
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ
(1...((๐ โ 1) /
2))(๐ ยท 2) = ((๐ ยท 2) mod ๐)) |