Step | Hyp | Ref
| Expression |
1 | | nnex 8924 |
. . 3
โข โ
โ V |
2 | 1 | rabex 4147 |
. 2
โข {๐ง โ โ โฃ ยฌ 2
โฅ ๐ง} โ
V |
3 | | elrabi 2890 |
. . . 4
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ ๐ฅ โ โ) |
4 | 3 | peano2nnd 8933 |
. . 3
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ (๐ฅ + 1) โ โ) |
5 | | breq2 4007 |
. . . . . . 7
โข (๐ง = ๐ฅ โ (2 โฅ ๐ง โ 2 โฅ ๐ฅ)) |
6 | 5 | notbid 667 |
. . . . . 6
โข (๐ง = ๐ฅ โ (ยฌ 2 โฅ ๐ง โ ยฌ 2 โฅ ๐ฅ)) |
7 | 6 | elrab 2893 |
. . . . 5
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ (๐ฅ โ โ โง ยฌ 2 โฅ ๐ฅ)) |
8 | 7 | simprbi 275 |
. . . 4
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ ยฌ 2 โฅ ๐ฅ) |
9 | 3 | nnzd 9373 |
. . . . 5
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ ๐ฅ โ โค) |
10 | | oddp1even 11880 |
. . . . 5
โข (๐ฅ โ โค โ (ยฌ 2
โฅ ๐ฅ โ 2 โฅ
(๐ฅ + 1))) |
11 | 9, 10 | syl 14 |
. . . 4
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ (ยฌ 2 โฅ ๐ฅ โ 2 โฅ (๐ฅ + 1))) |
12 | 8, 11 | mpbid 147 |
. . 3
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ 2 โฅ (๐ฅ + 1)) |
13 | | nnehalf 11908 |
. . 3
โข (((๐ฅ + 1) โ โ โง 2
โฅ (๐ฅ + 1)) โ
((๐ฅ + 1) / 2) โ
โ) |
14 | 4, 12, 13 | syl2anc 411 |
. 2
โข (๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โ ((๐ฅ + 1) / 2) โ โ) |
15 | | nnz 9271 |
. . . . . 6
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
16 | | 2z 9280 |
. . . . . . 7
โข 2 โ
โค |
17 | 16 | a1i 9 |
. . . . . 6
โข (๐ฆ โ โ โ 2 โ
โค) |
18 | 15, 17 | zmulcld 9380 |
. . . . 5
โข (๐ฆ โ โ โ (๐ฆ ยท 2) โ
โค) |
19 | | peano2zm 9290 |
. . . . 5
โข ((๐ฆ ยท 2) โ โค
โ ((๐ฆ ยท 2)
โ 1) โ โค) |
20 | 18, 19 | syl 14 |
. . . 4
โข (๐ฆ โ โ โ ((๐ฆ ยท 2) โ 1) โ
โค) |
21 | | 1e2m1 9037 |
. . . . 5
โข 1 = (2
โ 1) |
22 | 17 | zred 9374 |
. . . . . 6
โข (๐ฆ โ โ โ 2 โ
โ) |
23 | | nnre 8925 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
24 | 23, 22 | remulcld 7987 |
. . . . . 6
โข (๐ฆ โ โ โ (๐ฆ ยท 2) โ
โ) |
25 | | 1red 7971 |
. . . . . 6
โข (๐ฆ โ โ โ 1 โ
โ) |
26 | | 0le2 9008 |
. . . . . . . 8
โข 0 โค
2 |
27 | 26 | a1i 9 |
. . . . . . 7
โข (๐ฆ โ โ โ 0 โค
2) |
28 | | nnge1 8941 |
. . . . . . 7
โข (๐ฆ โ โ โ 1 โค
๐ฆ) |
29 | 22, 23, 27, 28 | lemulge12d 8894 |
. . . . . 6
โข (๐ฆ โ โ โ 2 โค
(๐ฆ ยท
2)) |
30 | 22, 24, 25, 29 | lesub1dd 8517 |
. . . . 5
โข (๐ฆ โ โ โ (2
โ 1) โค ((๐ฆ
ยท 2) โ 1)) |
31 | 21, 30 | eqbrtrid 4038 |
. . . 4
โข (๐ฆ โ โ โ 1 โค
((๐ฆ ยท 2) โ
1)) |
32 | | elnnz1 9275 |
. . . 4
โข (((๐ฆ ยท 2) โ 1) โ
โ โ (((๐ฆ
ยท 2) โ 1) โ โค โง 1 โค ((๐ฆ ยท 2) โ 1))) |
33 | 20, 31, 32 | sylanbrc 417 |
. . 3
โข (๐ฆ โ โ โ ((๐ฆ ยท 2) โ 1) โ
โ) |
34 | | dvdsmul2 11820 |
. . . . 5
โข ((๐ฆ โ โค โง 2 โ
โค) โ 2 โฅ (๐ฆ ยท 2)) |
35 | 15, 16, 34 | sylancl 413 |
. . . 4
โข (๐ฆ โ โ โ 2 โฅ
(๐ฆ ยท
2)) |
36 | | oddm1even 11879 |
. . . . . 6
โข ((๐ฆ ยท 2) โ โค
โ (ยฌ 2 โฅ (๐ฆ
ยท 2) โ 2 โฅ ((๐ฆ ยท 2) โ 1))) |
37 | 18, 36 | syl 14 |
. . . . 5
โข (๐ฆ โ โ โ (ยฌ 2
โฅ (๐ฆ ยท 2)
โ 2 โฅ ((๐ฆ
ยท 2) โ 1))) |
38 | 37 | biimprd 158 |
. . . 4
โข (๐ฆ โ โ โ (2
โฅ ((๐ฆ ยท 2)
โ 1) โ ยฌ 2 โฅ (๐ฆ ยท 2))) |
39 | 35, 38 | mt2d 625 |
. . 3
โข (๐ฆ โ โ โ ยฌ 2
โฅ ((๐ฆ ยท 2)
โ 1)) |
40 | | breq2 4007 |
. . . . 5
โข (๐ง = ((๐ฆ ยท 2) โ 1) โ (2 โฅ
๐ง โ 2 โฅ ((๐ฆ ยท 2) โ
1))) |
41 | 40 | notbid 667 |
. . . 4
โข (๐ง = ((๐ฆ ยท 2) โ 1) โ (ยฌ 2
โฅ ๐ง โ ยฌ 2
โฅ ((๐ฆ ยท 2)
โ 1))) |
42 | 41 | elrab 2893 |
. . 3
โข (((๐ฆ ยท 2) โ 1) โ
{๐ง โ โ โฃ
ยฌ 2 โฅ ๐ง} โ
(((๐ฆ ยท 2) โ 1)
โ โ โง ยฌ 2 โฅ ((๐ฆ ยท 2) โ 1))) |
43 | 33, 39, 42 | sylanbrc 417 |
. 2
โข (๐ฆ โ โ โ ((๐ฆ ยท 2) โ 1) โ
{๐ง โ โ โฃ
ยฌ 2 โฅ ๐ง}) |
44 | 3 | adantr 276 |
. . . . . . 7
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฅ โ โ) |
45 | 44 | nncnd 8932 |
. . . . . 6
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฅ โ โ) |
46 | | 1cnd 7972 |
. . . . . 6
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ 1 โ
โ) |
47 | 45, 46 | addcld 7976 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฅ + 1) โ โ) |
48 | | simpr 110 |
. . . . . 6
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
49 | 48 | nncnd 8932 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
50 | | 2cnd 8991 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ 2 โ
โ) |
51 | | 2ap0 9011 |
. . . . . 6
โข 2 #
0 |
52 | 51 | a1i 9 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ 2 #
0) |
53 | 47, 49, 50, 52 | divmulap3d 8781 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (((๐ฅ + 1) / 2) = ๐ฆ โ (๐ฅ + 1) = (๐ฆ ยท 2))) |
54 | 49, 50 | mulcld 7977 |
. . . . 5
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฆ ยท 2) โ โ) |
55 | 45, 46, 54 | addlsub 8326 |
. . . 4
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ ((๐ฅ + 1) = (๐ฆ ยท 2) โ ๐ฅ = ((๐ฆ ยท 2) โ 1))) |
56 | 53, 55 | bitrd 188 |
. . 3
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (((๐ฅ + 1) / 2) = ๐ฆ โ ๐ฅ = ((๐ฆ ยท 2) โ 1))) |
57 | | eqcom 2179 |
. . 3
โข (((๐ฅ + 1) / 2) = ๐ฆ โ ๐ฆ = ((๐ฅ + 1) / 2)) |
58 | 56, 57 | bitr3di 195 |
. 2
โข ((๐ฅ โ {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} โง ๐ฆ โ โ) โ (๐ฅ = ((๐ฆ ยท 2) โ 1) โ ๐ฆ = ((๐ฅ + 1) / 2))) |
59 | 2, 1, 14, 43, 58 | en3i 6770 |
1
โข {๐ง โ โ โฃ ยฌ 2
โฅ ๐ง} โ
โ |