Step | Hyp | Ref
| Expression |
1 | | peano2nn 12166 |
. . . . . 6
โข (๐ โ โ โ (๐ + 1) โ
โ) |
2 | 1 | nncnd 12170 |
. . . . 5
โข (๐ โ โ โ (๐ + 1) โ
โ) |
3 | | 2cn 12229 |
. . . . . 6
โข 2 โ
โ |
4 | 3 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 2 โ
โ) |
5 | | 2ne0 12258 |
. . . . . 6
โข 2 โ
0 |
6 | 5 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 2 โ
0) |
7 | 2, 4, 6 | divcan2d 11934 |
. . . 4
โข (๐ โ โ โ (2
ยท ((๐ + 1) / 2)) =
(๐ + 1)) |
8 | | nncn 12162 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
9 | 8, 4, 6 | divcan2d 11934 |
. . . . 5
โข (๐ โ โ โ (2
ยท (๐ / 2)) = ๐) |
10 | 9 | oveq1d 7373 |
. . . 4
โข (๐ โ โ โ ((2
ยท (๐ / 2)) + 1) =
(๐ + 1)) |
11 | 7, 10 | eqtr4d 2780 |
. . 3
โข (๐ โ โ โ (2
ยท ((๐ + 1) / 2)) =
((2 ยท (๐ / 2)) +
1)) |
12 | | nnz 12521 |
. . . . . 6
โข (((๐ + 1) / 2) โ โ โ
((๐ + 1) / 2) โ
โค) |
13 | | nnz 12521 |
. . . . . 6
โข ((๐ / 2) โ โ โ
(๐ / 2) โ
โค) |
14 | | zneo 12587 |
. . . . . 6
โข ((((๐ + 1) / 2) โ โค โง
(๐ / 2) โ โค)
โ (2 ยท ((๐ + 1)
/ 2)) โ ((2 ยท (๐
/ 2)) + 1)) |
15 | 12, 13, 14 | syl2an 597 |
. . . . 5
โข ((((๐ + 1) / 2) โ โ โง
(๐ / 2) โ โ)
โ (2 ยท ((๐ + 1)
/ 2)) โ ((2 ยท (๐
/ 2)) + 1)) |
16 | 15 | expcom 415 |
. . . 4
โข ((๐ / 2) โ โ โ
(((๐ + 1) / 2) โ
โ โ (2 ยท ((๐ + 1) / 2)) โ ((2 ยท (๐ / 2)) + 1))) |
17 | 16 | necon2bd 2960 |
. . 3
โข ((๐ / 2) โ โ โ ((2
ยท ((๐ + 1) / 2)) =
((2 ยท (๐ / 2)) + 1)
โ ยฌ ((๐ + 1) / 2)
โ โ)) |
18 | 11, 17 | syl5com 31 |
. 2
โข (๐ โ โ โ ((๐ / 2) โ โ โ
ยฌ ((๐ + 1) / 2) โ
โ)) |
19 | | oveq1 7365 |
. . . . . . 7
โข (๐ = 1 โ (๐ + 1) = (1 + 1)) |
20 | 19 | oveq1d 7373 |
. . . . . 6
โข (๐ = 1 โ ((๐ + 1) / 2) = ((1 + 1) / 2)) |
21 | 20 | eleq1d 2823 |
. . . . 5
โข (๐ = 1 โ (((๐ + 1) / 2) โ โ โ
((1 + 1) / 2) โ โ)) |
22 | | oveq1 7365 |
. . . . . 6
โข (๐ = 1 โ (๐ / 2) = (1 / 2)) |
23 | 22 | eleq1d 2823 |
. . . . 5
โข (๐ = 1 โ ((๐ / 2) โ โ โ (1 / 2) โ
โ)) |
24 | 21, 23 | orbi12d 918 |
. . . 4
โข (๐ = 1 โ ((((๐ + 1) / 2) โ โ โจ
(๐ / 2) โ โ)
โ (((1 + 1) / 2) โ โ โจ (1 / 2) โ
โ))) |
25 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
26 | 25 | oveq1d 7373 |
. . . . . 6
โข (๐ = ๐ โ ((๐ + 1) / 2) = ((๐ + 1) / 2)) |
27 | 26 | eleq1d 2823 |
. . . . 5
โข (๐ = ๐ โ (((๐ + 1) / 2) โ โ โ ((๐ + 1) / 2) โ
โ)) |
28 | | oveq1 7365 |
. . . . . 6
โข (๐ = ๐ โ (๐ / 2) = (๐ / 2)) |
29 | 28 | eleq1d 2823 |
. . . . 5
โข (๐ = ๐ โ ((๐ / 2) โ โ โ (๐ / 2) โ
โ)) |
30 | 27, 29 | orbi12d 918 |
. . . 4
โข (๐ = ๐ โ ((((๐ + 1) / 2) โ โ โจ (๐ / 2) โ โ) โ
(((๐ + 1) / 2) โ
โ โจ (๐ / 2) โ
โ))) |
31 | | oveq1 7365 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ + 1) = ((๐ + 1) + 1)) |
32 | 31 | oveq1d 7373 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ + 1) / 2) = (((๐ + 1) + 1) / 2)) |
33 | 32 | eleq1d 2823 |
. . . . 5
โข (๐ = (๐ + 1) โ (((๐ + 1) / 2) โ โ โ (((๐ + 1) + 1) / 2) โ
โ)) |
34 | | oveq1 7365 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ / 2) = ((๐ + 1) / 2)) |
35 | 34 | eleq1d 2823 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ / 2) โ โ โ ((๐ + 1) / 2) โ
โ)) |
36 | 33, 35 | orbi12d 918 |
. . . 4
โข (๐ = (๐ + 1) โ ((((๐ + 1) / 2) โ โ โจ (๐ / 2) โ โ) โ
((((๐ + 1) + 1) / 2) โ
โ โจ ((๐ + 1) / 2)
โ โ))) |
37 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
38 | 37 | oveq1d 7373 |
. . . . . 6
โข (๐ = ๐ โ ((๐ + 1) / 2) = ((๐ + 1) / 2)) |
39 | 38 | eleq1d 2823 |
. . . . 5
โข (๐ = ๐ โ (((๐ + 1) / 2) โ โ โ ((๐ + 1) / 2) โ
โ)) |
40 | | oveq1 7365 |
. . . . . 6
โข (๐ = ๐ โ (๐ / 2) = (๐ / 2)) |
41 | 40 | eleq1d 2823 |
. . . . 5
โข (๐ = ๐ โ ((๐ / 2) โ โ โ (๐ / 2) โ
โ)) |
42 | 39, 41 | orbi12d 918 |
. . . 4
โข (๐ = ๐ โ ((((๐ + 1) / 2) โ โ โจ (๐ / 2) โ โ) โ
(((๐ + 1) / 2) โ
โ โจ (๐ / 2) โ
โ))) |
43 | | df-2 12217 |
. . . . . . . 8
โข 2 = (1 +
1) |
44 | 43 | oveq1i 7368 |
. . . . . . 7
โข (2 / 2) =
((1 + 1) / 2) |
45 | | 2div2e1 12295 |
. . . . . . 7
โข (2 / 2) =
1 |
46 | 44, 45 | eqtr3i 2767 |
. . . . . 6
โข ((1 + 1)
/ 2) = 1 |
47 | | 1nn 12165 |
. . . . . 6
โข 1 โ
โ |
48 | 46, 47 | eqeltri 2834 |
. . . . 5
โข ((1 + 1)
/ 2) โ โ |
49 | 48 | orci 864 |
. . . 4
โข (((1 + 1)
/ 2) โ โ โจ (1 / 2) โ โ) |
50 | | peano2nn 12166 |
. . . . . . 7
โข ((๐ / 2) โ โ โ
((๐ / 2) + 1) โ
โ) |
51 | | nncn 12162 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
52 | | add1p1 12405 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ + 1) + 1) = (๐ + 2)) |
53 | 52 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1) + 1) / 2) = ((๐ + 2) / 2)) |
54 | | 2cnne0 12364 |
. . . . . . . . . . . 12
โข (2 โ
โ โง 2 โ 0) |
55 | | divdir 11839 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 2 โ
โ โง (2 โ โ โง 2 โ 0)) โ ((๐ + 2) / 2) = ((๐ / 2) + (2 / 2))) |
56 | 3, 54, 55 | mp3an23 1454 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ + 2) / 2) = ((๐ / 2) + (2 /
2))) |
57 | 45 | oveq2i 7369 |
. . . . . . . . . . 11
โข ((๐ / 2) + (2 / 2)) = ((๐ / 2) + 1) |
58 | 56, 57 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 2) / 2) = ((๐ / 2) + 1)) |
59 | 53, 58 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ + 1) + 1) / 2) = ((๐ / 2) + 1)) |
60 | 51, 59 | syl 17 |
. . . . . . . 8
โข (๐ โ โ โ (((๐ + 1) + 1) / 2) = ((๐ / 2) + 1)) |
61 | 60 | eleq1d 2823 |
. . . . . . 7
โข (๐ โ โ โ ((((๐ + 1) + 1) / 2) โ โ
โ ((๐ / 2) + 1) โ
โ)) |
62 | 50, 61 | syl5ibr 246 |
. . . . . 6
โข (๐ โ โ โ ((๐ / 2) โ โ โ
(((๐ + 1) + 1) / 2) โ
โ)) |
63 | 62 | orim2d 966 |
. . . . 5
โข (๐ โ โ โ ((((๐ + 1) / 2) โ โ โจ
(๐ / 2) โ โ)
โ (((๐ + 1) / 2)
โ โ โจ (((๐ +
1) + 1) / 2) โ โ))) |
64 | | orcom 869 |
. . . . 5
โข ((((๐ + 1) / 2) โ โ โจ
(((๐ + 1) + 1) / 2) โ
โ) โ ((((๐ + 1)
+ 1) / 2) โ โ โจ ((๐ + 1) / 2) โ โ)) |
65 | 63, 64 | syl6ib 251 |
. . . 4
โข (๐ โ โ โ ((((๐ + 1) / 2) โ โ โจ
(๐ / 2) โ โ)
โ ((((๐ + 1) + 1) / 2)
โ โ โจ ((๐ +
1) / 2) โ โ))) |
66 | 24, 30, 36, 42, 49, 65 | nnind 12172 |
. . 3
โข (๐ โ โ โ (((๐ + 1) / 2) โ โ โจ
(๐ / 2) โ
โ)) |
67 | 66 | ord 863 |
. 2
โข (๐ โ โ โ (ยฌ
((๐ + 1) / 2) โ
โ โ (๐ / 2)
โ โ)) |
68 | 18, 67 | impbid 211 |
1
โข (๐ โ โ โ ((๐ / 2) โ โ โ
ยฌ ((๐ + 1) / 2) โ
โ)) |