Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โค) |
2 | | 2nn0 12488 |
. . . . . . 7
โข 2 โ
โ0 |
3 | 2 | numexp1 17009 |
. . . . . 6
โข
(2โ1) = 2 |
4 | | df-2 12274 |
. . . . . 6
โข 2 = (1 +
1) |
5 | 3, 4 | eqtri 2760 |
. . . . 5
โข
(2โ1) = (1 + 1) |
6 | | prmuz2 16632 |
. . . . . . . 8
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ
(โคโฅโ2)) |
7 | 6 | adantl 482 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((2โ๐) โ 1) โ
(โคโฅโ2)) |
8 | | eluz2gt1 12903 |
. . . . . . 7
โข
(((2โ๐) โ
1) โ (โคโฅโ2) โ 1 < ((2โ๐) โ 1)) |
9 | 7, 8 | syl 17 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 < ((2โ๐) โ 1)) |
10 | | 1red 11214 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 โ โ) |
11 | | 2re 12285 |
. . . . . . . . 9
โข 2 โ
โ |
12 | 11 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 2 โ โ) |
13 | | 2ne0 12315 |
. . . . . . . . 9
โข 2 โ
0 |
14 | 13 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 2 โ 0) |
15 | 12, 14, 1 | reexpclzd 14211 |
. . . . . . 7
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ๐) โ โ) |
16 | 10, 10, 15 | ltaddsubd 11813 |
. . . . . 6
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ((1 + 1) < (2โ๐) โ 1 < ((2โ๐) โ 1))) |
17 | 9, 16 | mpbird 256 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 + 1) < (2โ๐)) |
18 | 5, 17 | eqbrtrid 5183 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (2โ1) < (2โ๐)) |
19 | | 1zzd 12592 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 โ โค) |
20 | | 1lt2 12382 |
. . . . . 6
โข 1 <
2 |
21 | 20 | a1i 11 |
. . . . 5
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 < 2) |
22 | 12, 19, 1, 21 | ltexp2d 14213 |
. . . 4
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (1 < ๐ โ (2โ1) < (2โ๐))) |
23 | 18, 22 | mpbird 256 |
. . 3
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ 1 < ๐) |
24 | | eluz2b1 12902 |
. . 3
โข (๐ โ
(โคโฅโ2) โ (๐ โ โค โง 1 < ๐)) |
25 | 1, 23, 24 | sylanbrc 583 |
. 2
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ (โคโฅโ2)) |
26 | | simpllr 774 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
27 | | prmnn 16610 |
. . . . . . . 8
โข
(((2โ๐) โ
1) โ โ โ ((2โ๐) โ 1) โ
โ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
29 | 28 | nncnd 12227 |
. . . . . 6
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
30 | | 2nn 12284 |
. . . . . . . . . . 11
โข 2 โ
โ |
31 | | elfzuz 13496 |
. . . . . . . . . . . . . 14
โข (๐ โ (2...(๐ โ 1)) โ ๐ โ
(โคโฅโ2)) |
32 | 31 | ad2antlr 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ
(โคโฅโ2)) |
33 | | eluz2nn 12867 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โ) |
35 | 34 | nnnn0d 12531 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โ0) |
36 | | nnexpcl 14039 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
37 | 30, 35, 36 | sylancr 587 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โ) |
38 | 37 | nnzd 12584 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โค) |
39 | | peano2zm 12604 |
. . . . . . . . 9
โข
((2โ๐) โ
โค โ ((2โ๐)
โ 1) โ โค) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โค) |
41 | 40 | zred 12665 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
42 | 41 | recnd 11241 |
. . . . . 6
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
43 | | 0red 11216 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 0 โ
โ) |
44 | | 1red 11214 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 โ
โ) |
45 | | 0lt1 11735 |
. . . . . . . . . 10
โข 0 <
1 |
46 | 45 | a1i 11 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 0 <
1) |
47 | | eluz2gt1 12903 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
48 | 32, 47 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 < ๐) |
49 | 11 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 2 โ
โ) |
50 | | 1zzd 12592 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 โ
โค) |
51 | | elfzelz 13500 |
. . . . . . . . . . . . . 14
โข (๐ โ (2...(๐ โ 1)) โ ๐ โ โค) |
52 | 51 | ad2antlr 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โค) |
53 | 20 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 <
2) |
54 | 49, 50, 52, 53 | ltexp2d 14213 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (1 < ๐ โ (2โ1) <
(2โ๐))) |
55 | 48, 54 | mpbid 231 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ1) <
(2โ๐)) |
56 | 5, 55 | eqbrtrrid 5184 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (1 + 1) <
(2โ๐)) |
57 | 37 | nnred 12226 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โ) |
58 | 44, 44, 57 | ltaddsubd 11813 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((1 + 1) <
(2โ๐) โ 1 <
((2โ๐) โ
1))) |
59 | 56, 58 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 < ((2โ๐) โ 1)) |
60 | 43, 44, 41, 46, 59 | lttrd 11374 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 0 < ((2โ๐) โ 1)) |
61 | | elnnz 12567 |
. . . . . . . 8
โข
(((2โ๐) โ
1) โ โ โ (((2โ๐) โ 1) โ โค โง 0 <
((2โ๐) โ
1))) |
62 | 40, 60, 61 | sylanbrc 583 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
63 | 62 | nnne0d 12261 |
. . . . . 6
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
0) |
64 | 29, 42, 63 | divcan2d 11991 |
. . . . 5
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) ยท
(((2โ๐) โ 1) /
((2โ๐) โ 1))) =
((2โ๐) โ
1)) |
65 | 64, 26 | eqeltrd 2833 |
. . . 4
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) ยท
(((2โ๐) โ 1) /
((2โ๐) โ 1)))
โ โ) |
66 | | eluz2b2 12904 |
. . . . . 6
โข
(((2โ๐) โ
1) โ (โคโฅโ2) โ (((2โ๐) โ 1) โ โ โง 1 <
((2โ๐) โ
1))) |
67 | 62, 59, 66 | sylanbrc 583 |
. . . . 5
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
(โคโฅโ2)) |
68 | 37 | nncnd 12227 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โ) |
69 | | ax-1cn 11167 |
. . . . . . . . . . . 12
โข 1 โ
โ |
70 | | subeq0 11485 |
. . . . . . . . . . . 12
โข
(((2โ๐) โ
โ โง 1 โ โ) โ (((2โ๐) โ 1) = 0 โ (2โ๐) = 1)) |
71 | 68, 69, 70 | sylancl 586 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) = 0 โ
(2โ๐) =
1)) |
72 | 71 | necon3bid 2985 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) โ 0 โ
(2โ๐) โ
1)) |
73 | 63, 72 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ 1) |
74 | | simpr 485 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โฅ ๐) |
75 | | eluz2nn 12867 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
76 | 25, 75 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |
77 | 76 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โ) |
78 | | nndivdvds 16205 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
79 | 77, 34, 78 | syl2anc 584 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
80 | 74, 79 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (๐ / ๐) โ โ) |
81 | 80 | nnnn0d 12531 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (๐ / ๐) โ
โ0) |
82 | 68, 73, 81 | geoser 15812 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ฮฃ๐ โ (0...((๐ / ๐) โ 1))((2โ๐)โ๐) = ((1 โ ((2โ๐)โ(๐ / ๐))) / (1 โ (2โ๐)))) |
83 | 15 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โ) |
84 | 83 | recnd 11241 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) โ
โ) |
85 | | negsubdi2 11518 |
. . . . . . . . . . 11
โข
(((2โ๐) โ
โ โง 1 โ โ) โ -((2โ๐) โ 1) = (1 โ (2โ๐))) |
86 | 84, 69, 85 | sylancl 586 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ -((2โ๐) โ 1) = (1 โ
(2โ๐))) |
87 | 77 | nncnd 12227 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โ) |
88 | 34 | nncnd 12227 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โ) |
89 | 34 | nnne0d 12261 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ 0) |
90 | 87, 88, 89 | divcan2d 11991 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (๐ ยท (๐ / ๐)) = ๐) |
91 | 90 | oveq2d 7424 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ(๐ ยท (๐ / ๐))) = (2โ๐)) |
92 | 49 | recnd 11241 |
. . . . . . . . . . . . 13
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 2 โ
โ) |
93 | 92, 81, 35 | expmuld 14113 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ(๐ ยท (๐ / ๐))) = ((2โ๐)โ(๐ / ๐))) |
94 | 91, 93 | eqtr3d 2774 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) = ((2โ๐)โ(๐ / ๐))) |
95 | 94 | oveq2d 7424 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (1 โ
(2โ๐)) = (1 โ
((2โ๐)โ(๐ / ๐)))) |
96 | 86, 95 | eqtrd 2772 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ -((2โ๐) โ 1) = (1 โ
((2โ๐)โ(๐ / ๐)))) |
97 | | negsubdi2 11518 |
. . . . . . . . . 10
โข
(((2โ๐) โ
โ โง 1 โ โ) โ -((2โ๐) โ 1) = (1 โ (2โ๐))) |
98 | 68, 69, 97 | sylancl 586 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ -((2โ๐) โ 1) = (1 โ
(2โ๐))) |
99 | 96, 98 | oveq12d 7426 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (-((2โ๐) โ 1) / -((2โ๐) โ 1)) = ((1 โ
((2โ๐)โ(๐ / ๐))) / (1 โ (2โ๐)))) |
100 | 29, 42, 63 | div2negd 12004 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (-((2โ๐) โ 1) / -((2โ๐) โ 1)) = (((2โ๐) โ 1) / ((2โ๐) โ 1))) |
101 | 82, 99, 100 | 3eqtr2d 2778 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ฮฃ๐ โ (0...((๐ / ๐) โ 1))((2โ๐)โ๐) = (((2โ๐) โ 1) / ((2โ๐) โ 1))) |
102 | | fzfid 13937 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (0...((๐ / ๐) โ 1)) โ Fin) |
103 | | elfznn0 13593 |
. . . . . . . . 9
โข (๐ โ (0...((๐ / ๐) โ 1)) โ ๐ โ โ0) |
104 | | zexpcl 14041 |
. . . . . . . . 9
โข
(((2โ๐) โ
โค โง ๐ โ
โ0) โ ((2โ๐)โ๐) โ โค) |
105 | 38, 103, 104 | syl2an 596 |
. . . . . . . 8
โข
(((((๐ โ
โค โง ((2โ๐)
โ 1) โ โ) โง ๐ โ (2...(๐ โ 1))) โง ๐ โฅ ๐) โง ๐ โ (0...((๐ / ๐) โ 1))) โ ((2โ๐)โ๐) โ โค) |
106 | 102, 105 | fsumzcl 15680 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ฮฃ๐ โ (0...((๐ / ๐) โ 1))((2โ๐)โ๐) โ โค) |
107 | 101, 106 | eqeltrrd 2834 |
. . . . . 6
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) / ((2โ๐) โ 1)) โ
โค) |
108 | 42 | mullidd 11231 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (1 ยท
((2โ๐) โ 1)) =
((2โ๐) โ
1)) |
109 | | 2z 12593 |
. . . . . . . . . . . . . 14
โข 2 โ
โค |
110 | | elfzm11 13571 |
. . . . . . . . . . . . . 14
โข ((2
โ โค โง ๐
โ โค) โ (๐
โ (2...(๐ โ 1))
โ (๐ โ โค
โง 2 โค ๐ โง ๐ < ๐))) |
111 | 109, 1, 110 | sylancr 587 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ (๐
โ (2...(๐ โ 1))
โ (๐ โ โค
โง 2 โค ๐ โง ๐ < ๐))) |
112 | 111 | biimpa 477 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โ (๐ โ โค
โง 2 โค ๐ โง ๐ < ๐)) |
113 | 112 | simp3d 1144 |
. . . . . . . . . . 11
โข (((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โ ๐ < ๐) |
114 | 113 | adantr 481 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ < ๐) |
115 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ๐ โ โค) |
116 | 49, 52, 115, 53 | ltexp2d 14213 |
. . . . . . . . . 10
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (๐ < ๐ โ (2โ๐) < (2โ๐))) |
117 | 114, 116 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (2โ๐) < (2โ๐)) |
118 | 57, 83, 44, 117 | ltsub1dd 11825 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) < ((2โ๐) โ 1)) |
119 | 108, 118 | eqbrtrd 5170 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (1 ยท
((2โ๐) โ 1))
< ((2โ๐) โ
1)) |
120 | 28 | nnred 12226 |
. . . . . . . 8
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((2โ๐) โ 1) โ
โ) |
121 | | ltmuldiv 12086 |
. . . . . . . 8
โข ((1
โ โ โง ((2โ๐) โ 1) โ โ โง
(((2โ๐) โ 1)
โ โ โง 0 < ((2โ๐) โ 1))) โ ((1 ยท
((2โ๐) โ 1))
< ((2โ๐) โ 1)
โ 1 < (((2โ๐)
โ 1) / ((2โ๐)
โ 1)))) |
122 | 44, 120, 41, 60, 121 | syl112anc 1374 |
. . . . . . 7
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ((1 ยท
((2โ๐) โ 1))
< ((2โ๐) โ 1)
โ 1 < (((2โ๐)
โ 1) / ((2โ๐)
โ 1)))) |
123 | 119, 122 | mpbid 231 |
. . . . . 6
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ 1 < (((2โ๐) โ 1) / ((2โ๐) โ 1))) |
124 | | eluz2b1 12902 |
. . . . . 6
โข
((((2โ๐)
โ 1) / ((2โ๐)
โ 1)) โ (โคโฅโ2) โ ((((2โ๐) โ 1) / ((2โ๐) โ 1)) โ โค
โง 1 < (((2โ๐)
โ 1) / ((2โ๐)
โ 1)))) |
125 | 107, 123,
124 | sylanbrc 583 |
. . . . 5
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ (((2โ๐) โ 1) / ((2โ๐) โ 1)) โ
(โคโฅโ2)) |
126 | | nprm 16624 |
. . . . 5
โข
((((2โ๐)
โ 1) โ (โคโฅโ2) โง (((2โ๐) โ 1) / ((2โ๐) โ 1)) โ
(โคโฅโ2)) โ ยฌ (((2โ๐) โ 1) ยท (((2โ๐) โ 1) / ((2โ๐) โ 1))) โ
โ) |
127 | 67, 125, 126 | syl2anc 584 |
. . . 4
โข ((((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โง ๐ โฅ ๐) โ ยฌ (((2โ๐) โ 1) ยท
(((2โ๐) โ 1) /
((2โ๐) โ 1)))
โ โ) |
128 | 65, 127 | pm2.65da 815 |
. . 3
โข (((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โง ๐
โ (2...(๐ โ 1)))
โ ยฌ ๐ โฅ
๐) |
129 | 128 | ralrimiva 3146 |
. 2
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ โ๐ โ (2...(๐ โ 1)) ยฌ ๐ โฅ ๐) |
130 | | isprm3 16619 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ โ (2...(๐ โ 1)) ยฌ ๐ โฅ ๐)) |
131 | 25, 129, 130 | sylanbrc 583 |
1
โข ((๐ โ โค โง
((2โ๐) โ 1)
โ โ) โ ๐
โ โ) |