Step | Hyp | Ref
| Expression |
1 | | zre 12508 |
. . . . . . . . 9
โข (๐พ โ โค โ ๐พ โ
โ) |
2 | | 1red 11161 |
. . . . . . . . 9
โข (๐พ โ โค โ 1 โ
โ) |
3 | 1, 2 | resubcld 11588 |
. . . . . . . 8
โข (๐พ โ โค โ (๐พ โ 1) โ
โ) |
4 | | 2rp 12925 |
. . . . . . . . 9
โข 2 โ
โ+ |
5 | 4 | a1i 11 |
. . . . . . . 8
โข (๐พ โ โค โ 2 โ
โ+) |
6 | 1 | lem1d 12093 |
. . . . . . . 8
โข (๐พ โ โค โ (๐พ โ 1) โค ๐พ) |
7 | 3, 1, 5, 6 | lediv1dd 13020 |
. . . . . . 7
โข (๐พ โ โค โ ((๐พ โ 1) / 2) โค (๐พ / 2)) |
8 | 1 | rehalfcld 12405 |
. . . . . . . . 9
โข (๐พ โ โค โ (๐พ / 2) โ
โ) |
9 | 5 | rpreccld 12972 |
. . . . . . . . 9
โข (๐พ โ โค โ (1 / 2)
โ โ+) |
10 | 8, 9 | ltaddrpd 12995 |
. . . . . . . 8
โข (๐พ โ โค โ (๐พ / 2) < ((๐พ / 2) + (1 / 2))) |
11 | | zcn 12509 |
. . . . . . . . . . 11
โข (๐พ โ โค โ ๐พ โ
โ) |
12 | 2 | recnd 11188 |
. . . . . . . . . . 11
โข (๐พ โ โค โ 1 โ
โ) |
13 | | 2cnd 12236 |
. . . . . . . . . . 11
โข (๐พ โ โค โ 2 โ
โ) |
14 | 5 | rpne0d 12967 |
. . . . . . . . . . 11
โข (๐พ โ โค โ 2 โ
0) |
15 | 11, 12, 13, 14 | divsubdird 11975 |
. . . . . . . . . 10
โข (๐พ โ โค โ ((๐พ โ 1) / 2) = ((๐พ / 2) โ (1 /
2))) |
16 | 15 | oveq1d 7373 |
. . . . . . . . 9
โข (๐พ โ โค โ (((๐พ โ 1) / 2) + 1) = (((๐พ / 2) โ (1 / 2)) +
1)) |
17 | 11 | halfcld 12403 |
. . . . . . . . . 10
โข (๐พ โ โค โ (๐พ / 2) โ
โ) |
18 | 13, 14 | reccld 11929 |
. . . . . . . . . 10
โข (๐พ โ โค โ (1 / 2)
โ โ) |
19 | 17, 18, 12 | subadd23d 11539 |
. . . . . . . . 9
โข (๐พ โ โค โ (((๐พ / 2) โ (1 / 2)) + 1) =
((๐พ / 2) + (1 โ (1 /
2)))) |
20 | | 1mhlfehlf 12377 |
. . . . . . . . . . 11
โข (1
โ (1 / 2)) = (1 / 2) |
21 | 20 | oveq2i 7369 |
. . . . . . . . . 10
โข ((๐พ / 2) + (1 โ (1 / 2))) =
((๐พ / 2) + (1 /
2)) |
22 | 21 | a1i 11 |
. . . . . . . . 9
โข (๐พ โ โค โ ((๐พ / 2) + (1 โ (1 / 2))) =
((๐พ / 2) + (1 /
2))) |
23 | 16, 19, 22 | 3eqtrrd 2778 |
. . . . . . . 8
โข (๐พ โ โค โ ((๐พ / 2) + (1 / 2)) = (((๐พ โ 1) / 2) +
1)) |
24 | 10, 23 | breqtrd 5132 |
. . . . . . 7
โข (๐พ โ โค โ (๐พ / 2) < (((๐พ โ 1) / 2) + 1)) |
25 | 7, 24 | jca 513 |
. . . . . 6
โข (๐พ โ โค โ (((๐พ โ 1) / 2) โค (๐พ / 2) โง (๐พ / 2) < (((๐พ โ 1) / 2) + 1))) |
26 | 25 | adantr 482 |
. . . . 5
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (((๐พ โ 1) / 2) โค (๐พ / 2) โง (๐พ / 2) < (((๐พ โ 1) / 2) + 1))) |
27 | 1 | adantr 482 |
. . . . . . 7
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ๐พ โ
โ) |
28 | 27 | rehalfcld 12405 |
. . . . . 6
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (๐พ / 2) โ
โ) |
29 | 11, 12 | npcand 11521 |
. . . . . . . . . 10
โข (๐พ โ โค โ ((๐พ โ 1) + 1) = ๐พ) |
30 | 29 | oveq1d 7373 |
. . . . . . . . 9
โข (๐พ โ โค โ (((๐พ โ 1) + 1) / 2) = (๐พ / 2)) |
31 | 30 | adantr 482 |
. . . . . . . 8
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (((๐พ โ 1) + 1) / 2) = (๐พ / 2)) |
32 | | simpr 486 |
. . . . . . . . . 10
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (๐พ mod 2) โ 0) |
33 | 32 | neneqd 2945 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ยฌ
(๐พ mod 2) =
0) |
34 | | mod0 13787 |
. . . . . . . . . . 11
โข ((๐พ โ โ โง 2 โ
โ+) โ ((๐พ mod 2) = 0 โ (๐พ / 2) โ โค)) |
35 | 1, 5, 34 | syl2anc 585 |
. . . . . . . . . 10
โข (๐พ โ โค โ ((๐พ mod 2) = 0 โ (๐พ / 2) โ
โค)) |
36 | 35 | adantr 482 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ((๐พ mod 2) = 0 โ (๐พ / 2) โ
โค)) |
37 | 33, 36 | mtbid 324 |
. . . . . . . 8
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ยฌ
(๐พ / 2) โ
โค) |
38 | 31, 37 | eqneltrd 2854 |
. . . . . . 7
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ยฌ
(((๐พ โ 1) + 1) / 2)
โ โค) |
39 | | simpl 484 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ๐พ โ
โค) |
40 | | 1zzd 12539 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ 1 โ
โค) |
41 | 39, 40 | zsubcld 12617 |
. . . . . . . 8
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (๐พ โ 1) โ
โค) |
42 | | zeo2 12595 |
. . . . . . . 8
โข ((๐พ โ 1) โ โค
โ (((๐พ โ 1) / 2)
โ โค โ ยฌ (((๐พ โ 1) + 1) / 2) โ
โค)) |
43 | 41, 42 | syl 17 |
. . . . . . 7
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (((๐พ โ 1) / 2) โ โค
โ ยฌ (((๐พ โ
1) + 1) / 2) โ โค)) |
44 | 38, 43 | mpbird 257 |
. . . . . 6
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ((๐พ โ 1) / 2) โ
โค) |
45 | | flbi 13727 |
. . . . . 6
โข (((๐พ / 2) โ โ โง
((๐พ โ 1) / 2) โ
โค) โ ((โโ(๐พ / 2)) = ((๐พ โ 1) / 2) โ (((๐พ โ 1) / 2) โค (๐พ / 2) โง (๐พ / 2) < (((๐พ โ 1) / 2) + 1)))) |
46 | 28, 44, 45 | syl2anc 585 |
. . . . 5
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ
((โโ(๐พ / 2)) =
((๐พ โ 1) / 2) โ
(((๐พ โ 1) / 2) โค
(๐พ / 2) โง (๐พ / 2) < (((๐พ โ 1) / 2) + 1)))) |
47 | 26, 46 | mpbird 257 |
. . . 4
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ
(โโ(๐พ / 2)) =
((๐พ โ 1) /
2)) |
48 | 47 | oveq2d 7374 |
. . 3
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ (2
ยท (โโ(๐พ
/ 2))) = (2 ยท ((๐พ
โ 1) / 2))) |
49 | 48 | oveq1d 7373 |
. 2
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ((2
ยท (โโ(๐พ
/ 2))) + 1) = ((2 ยท ((๐พ โ 1) / 2)) + 1)) |
50 | 11, 12 | subcld 11517 |
. . . . 5
โข (๐พ โ โค โ (๐พ โ 1) โ
โ) |
51 | 50, 13, 14 | divcan2d 11938 |
. . . 4
โข (๐พ โ โค โ (2
ยท ((๐พ โ 1) /
2)) = (๐พ โ
1)) |
52 | 51 | oveq1d 7373 |
. . 3
โข (๐พ โ โค โ ((2
ยท ((๐พ โ 1) /
2)) + 1) = ((๐พ โ 1) +
1)) |
53 | 52 | adantr 482 |
. 2
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ((2
ยท ((๐พ โ 1) /
2)) + 1) = ((๐พ โ 1) +
1)) |
54 | 29 | adantr 482 |
. 2
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ((๐พ โ 1) + 1) = ๐พ) |
55 | 49, 53, 54 | 3eqtrrd 2778 |
1
โข ((๐พ โ โค โง (๐พ mod 2) โ 0) โ ๐พ = ((2 ยท
(โโ(๐พ / 2))) +
1)) |