Step | Hyp | Ref
| Expression |
1 | | lgseisen.1 |
. . 3
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | | lgseisen.2 |
. . 3
โข (๐ โ ๐ โ (โ โ
{2})) |
3 | | lgseisen.3 |
. . 3
โข (๐ โ ๐ โ ๐) |
4 | 1, 2, 3 | lgseisen 26730 |
. 2
โข (๐ โ (๐ /L ๐) = (-1โฮฃ๐ข โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
5 | | lgsquad.4 |
. . . . . 6
โข ๐ = ((๐ โ 1) / 2) |
6 | 5 | oveq2i 7369 |
. . . . 5
โข
(1...๐) =
(1...((๐ โ 1) /
2)) |
7 | 6 | sumeq1i 15584 |
. . . 4
โข
ฮฃ๐ข โ
(1...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = ฮฃ๐ข โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) |
8 | 1, 5 | gausslemma2dlem0b 26708 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
9 | 8 | nnred 12169 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
10 | 9 | rehalfcld 12401 |
. . . . . . . . 9
โข (๐ โ (๐ / 2) โ โ) |
11 | 10 | flcld 13704 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / 2)) โ
โค) |
12 | 11 | zred 12608 |
. . . . . . 7
โข (๐ โ (โโ(๐ / 2)) โ
โ) |
13 | 12 | ltp1d 12086 |
. . . . . 6
โข (๐ โ (โโ(๐ / 2)) <
((โโ(๐ / 2)) +
1)) |
14 | | fzdisj 13469 |
. . . . . 6
โข
((โโ(๐ /
2)) < ((โโ(๐
/ 2)) + 1) โ ((1...(โโ(๐ / 2))) โฉ (((โโ(๐ / 2)) + 1)...๐)) = โ
) |
15 | 13, 14 | syl 17 |
. . . . 5
โข (๐ โ
((1...(โโ(๐ /
2))) โฉ (((โโ(๐ / 2)) + 1)...๐)) = โ
) |
16 | 8 | nnrpd 12956 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ+) |
17 | 16 | rphalfcld 12970 |
. . . . . . . . . 10
โข (๐ โ (๐ / 2) โ
โ+) |
18 | 17 | rpge0d 12962 |
. . . . . . . . 9
โข (๐ โ 0 โค (๐ / 2)) |
19 | | flge0nn0 13726 |
. . . . . . . . 9
โข (((๐ / 2) โ โ โง 0
โค (๐ / 2)) โ
(โโ(๐ / 2))
โ โ0) |
20 | 10, 18, 19 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / 2)) โ
โ0) |
21 | 8 | nnnn0d 12474 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
22 | | rphalflt 12945 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ / 2) < ๐) |
23 | 16, 22 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ / 2) < ๐) |
24 | 8 | nnzd 12527 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
25 | | fllt 13712 |
. . . . . . . . . . 11
โข (((๐ / 2) โ โ โง ๐ โ โค) โ ((๐ / 2) < ๐ โ (โโ(๐ / 2)) < ๐)) |
26 | 10, 24, 25 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ / 2) < ๐ โ (โโ(๐ / 2)) < ๐)) |
27 | 23, 26 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ / 2)) < ๐) |
28 | 12, 9, 27 | ltled 11304 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / 2)) โค ๐) |
29 | | elfz2nn0 13533 |
. . . . . . . 8
โข
((โโ(๐ /
2)) โ (0...๐) โ
((โโ(๐ / 2))
โ โ0 โง ๐ โ โ0 โง
(โโ(๐ / 2))
โค ๐)) |
30 | 20, 21, 28, 29 | syl3anbrc 1344 |
. . . . . . 7
โข (๐ โ (โโ(๐ / 2)) โ (0...๐)) |
31 | | nn0uz 12806 |
. . . . . . . . 9
โข
โ0 = (โคโฅโ0) |
32 | 21, 31 | eleqtrdi 2848 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ0)) |
33 | | elfzp12 13521 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ0) โ ((โโ(๐ / 2)) โ (0...๐) โ ((โโ(๐ / 2)) = 0 โจ (โโ(๐ / 2)) โ ((0 + 1)...๐)))) |
34 | 32, 33 | syl 17 |
. . . . . . 7
โข (๐ โ ((โโ(๐ / 2)) โ (0...๐) โ ((โโ(๐ / 2)) = 0 โจ
(โโ(๐ / 2))
โ ((0 + 1)...๐)))) |
35 | 30, 34 | mpbid 231 |
. . . . . 6
โข (๐ โ ((โโ(๐ / 2)) = 0 โจ
(โโ(๐ / 2))
โ ((0 + 1)...๐))) |
36 | | un0 4351 |
. . . . . . . . 9
โข
((1...๐) โช
โ
) = (1...๐) |
37 | | uncom 4114 |
. . . . . . . . 9
โข
((1...๐) โช
โ
) = (โ
โช (1...๐)) |
38 | 36, 37 | eqtr3i 2767 |
. . . . . . . 8
โข
(1...๐) = (โ
โช (1...๐)) |
39 | | oveq2 7366 |
. . . . . . . . . 10
โข
((โโ(๐ /
2)) = 0 โ (1...(โโ(๐ / 2))) = (1...0)) |
40 | | fz10 13463 |
. . . . . . . . . 10
โข (1...0) =
โ
|
41 | 39, 40 | eqtrdi 2793 |
. . . . . . . . 9
โข
((โโ(๐ /
2)) = 0 โ (1...(โโ(๐ / 2))) = โ
) |
42 | | oveq1 7365 |
. . . . . . . . . . 11
โข
((โโ(๐ /
2)) = 0 โ ((โโ(๐ / 2)) + 1) = (0 + 1)) |
43 | | 0p1e1 12276 |
. . . . . . . . . . 11
โข (0 + 1) =
1 |
44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . . 10
โข
((โโ(๐ /
2)) = 0 โ ((โโ(๐ / 2)) + 1) = 1) |
45 | 44 | oveq1d 7373 |
. . . . . . . . 9
โข
((โโ(๐ /
2)) = 0 โ (((โโ(๐ / 2)) + 1)...๐) = (1...๐)) |
46 | 41, 45 | uneq12d 4125 |
. . . . . . . 8
โข
((โโ(๐ /
2)) = 0 โ ((1...(โโ(๐ / 2))) โช (((โโ(๐ / 2)) + 1)...๐)) = (โ
โช (1...๐))) |
47 | 38, 46 | eqtr4id 2796 |
. . . . . . 7
โข
((โโ(๐ /
2)) = 0 โ (1...๐) =
((1...(โโ(๐ /
2))) โช (((โโ(๐ / 2)) + 1)...๐))) |
48 | | fzsplit 13468 |
. . . . . . . 8
โข
((โโ(๐ /
2)) โ (1...๐) โ
(1...๐) =
((1...(โโ(๐ /
2))) โช (((โโ(๐ / 2)) + 1)...๐))) |
49 | 43 | oveq1i 7368 |
. . . . . . . 8
โข ((0 +
1)...๐) = (1...๐) |
50 | 48, 49 | eleq2s 2856 |
. . . . . . 7
โข
((โโ(๐ /
2)) โ ((0 + 1)...๐)
โ (1...๐) =
((1...(โโ(๐ /
2))) โช (((โโ(๐ / 2)) + 1)...๐))) |
51 | 47, 50 | jaoi 856 |
. . . . . 6
โข
(((โโ(๐
/ 2)) = 0 โจ (โโ(๐ / 2)) โ ((0 + 1)...๐)) โ (1...๐) = ((1...(โโ(๐ / 2))) โช (((โโ(๐ / 2)) + 1)...๐))) |
52 | 35, 51 | syl 17 |
. . . . 5
โข (๐ โ (1...๐) = ((1...(โโ(๐ / 2))) โช (((โโ(๐ / 2)) + 1)...๐))) |
53 | | fzfid 13879 |
. . . . 5
โข (๐ โ (1...๐) โ Fin) |
54 | 2 | gausslemma2dlem0a 26707 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
55 | 54 | nnred 12169 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
56 | 1 | gausslemma2dlem0a 26707 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
57 | 55, 56 | nndivred 12208 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐) โ โ) |
58 | 57 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (1...๐)) โ (๐ / ๐) โ โ) |
59 | | 2nn 12227 |
. . . . . . . . . 10
โข 2 โ
โ |
60 | | elfznn 13471 |
. . . . . . . . . . 11
โข (๐ข โ (1...๐) โ ๐ข โ โ) |
61 | 60 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ (1...๐)) โ ๐ข โ โ) |
62 | | nnmulcl 12178 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐ข
โ โ) โ (2 ยท ๐ข) โ โ) |
63 | 59, 61, 62 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...๐)) โ (2 ยท ๐ข) โ โ) |
64 | 63 | nnred 12169 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (1...๐)) โ (2 ยท ๐ข) โ โ) |
65 | 58, 64 | remulcld 11186 |
. . . . . . 7
โข ((๐ โง ๐ข โ (1...๐)) โ ((๐ / ๐) ยท (2 ยท ๐ข)) โ โ) |
66 | 54 | nnrpd 12956 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ+) |
67 | 56 | nnrpd 12956 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ+) |
68 | 66, 67 | rpdivcld 12975 |
. . . . . . . . . 10
โข (๐ โ (๐ / ๐) โ
โ+) |
69 | 68 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...๐)) โ (๐ / ๐) โ
โ+) |
70 | 63 | nnrpd 12956 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...๐)) โ (2 ยท ๐ข) โ
โ+) |
71 | 69, 70 | rpmulcld 12974 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (1...๐)) โ ((๐ / ๐) ยท (2 ยท ๐ข)) โ
โ+) |
72 | 71 | rpge0d 12962 |
. . . . . . 7
โข ((๐ โง ๐ข โ (1...๐)) โ 0 โค ((๐ / ๐) ยท (2 ยท ๐ข))) |
73 | | flge0nn0 13726 |
. . . . . . 7
โข ((((๐ / ๐) ยท (2 ยท ๐ข)) โ โ โง 0 โค ((๐ / ๐) ยท (2 ยท ๐ข))) โ (โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
74 | 65, 72, 73 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ข โ (1...๐)) โ (โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
75 | 74 | nn0cnd 12476 |
. . . . 5
โข ((๐ โง ๐ข โ (1...๐)) โ (โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ โ) |
76 | 15, 52, 53, 75 | fsumsplit 15627 |
. . . 4
โข (๐ โ ฮฃ๐ข โ (1...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = (ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) + ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
77 | 7, 76 | eqtr3id 2791 |
. . 3
โข (๐ โ ฮฃ๐ข โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = (ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) + ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
78 | 77 | oveq2d 7374 |
. 2
โข (๐ โ (-1โฮฃ๐ข โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) = (-1โ(ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) + ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
79 | | neg1cn 12268 |
. . . . 5
โข -1 โ
โ |
80 | 79 | a1i 11 |
. . . 4
โข (๐ โ -1 โ
โ) |
81 | | fzfid 13879 |
. . . . 5
โข (๐ โ (((โโ(๐ / 2)) + 1)...๐) โ Fin) |
82 | | ssun2 4134 |
. . . . . . . 8
โข
(((โโ(๐
/ 2)) + 1)...๐) โ
((1...(โโ(๐ /
2))) โช (((โโ(๐ / 2)) + 1)...๐)) |
83 | 82, 52 | sseqtrrid 3998 |
. . . . . . 7
โข (๐ โ (((โโ(๐ / 2)) + 1)...๐) โ (1...๐)) |
84 | 83 | sselda 3945 |
. . . . . 6
โข ((๐ โง ๐ข โ (((โโ(๐ / 2)) + 1)...๐)) โ ๐ข โ (1...๐)) |
85 | 84, 74 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ข โ (((โโ(๐ / 2)) + 1)...๐)) โ (โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
86 | 81, 85 | fsumnn0cl 15622 |
. . . 4
โข (๐ โ ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
87 | | fzfid 13879 |
. . . . 5
โข (๐ โ (1...(โโ(๐ / 2))) โ
Fin) |
88 | | ssun1 4133 |
. . . . . . . 8
โข
(1...(โโ(๐ / 2))) โ ((1...(โโ(๐ / 2))) โช
(((โโ(๐ / 2)) +
1)...๐)) |
89 | 88, 52 | sseqtrrid 3998 |
. . . . . . 7
โข (๐ โ (1...(โโ(๐ / 2))) โ (1...๐)) |
90 | 89 | sselda 3945 |
. . . . . 6
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โ (1...๐)) |
91 | 90, 74 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
92 | 87, 91 | fsumnn0cl 15622 |
. . . 4
โข (๐ โ ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โ0) |
93 | 80, 86, 92 | expaddd 14054 |
. . 3
โข (๐ โ (-1โ(ฮฃ๐ข โ
(1...(โโ(๐ /
2)))(โโ((๐ /
๐) ยท (2 ยท
๐ข))) + ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) = ((-1โฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) ยท (-1โฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
94 | | fzfid 13879 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ Fin) |
95 | | xpfi 9262 |
. . . . . . . . 9
โข
(((1...๐) โ Fin
โง (1...๐) โ Fin)
โ ((1...๐) ร
(1...๐)) โ
Fin) |
96 | 53, 94, 95 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((1...๐) ร (1...๐)) โ Fin) |
97 | | lgsquad.6 |
. . . . . . . . 9
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))} |
98 | | opabssxp 5725 |
. . . . . . . . 9
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))} โ ((1...๐) ร (1...๐)) |
99 | 97, 98 | eqsstri 3979 |
. . . . . . . 8
โข ๐ โ ((1...๐) ร (1...๐)) |
100 | | ssfi 9118 |
. . . . . . . 8
โข
((((1...๐) ร
(1...๐)) โ Fin โง
๐ โ ((1...๐) ร (1...๐))) โ ๐ โ Fin) |
101 | 96, 99, 100 | sylancl 587 |
. . . . . . 7
โข (๐ โ ๐ โ Fin) |
102 | | ssrab2 4038 |
. . . . . . 7
โข {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ ๐ |
103 | | ssfi 9118 |
. . . . . . 7
โข ((๐ โ Fin โง {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ ๐) โ {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ
Fin) |
104 | 101, 102,
103 | sylancl 587 |
. . . . . 6
โข (๐ โ {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ
Fin) |
105 | | hashcl 14257 |
. . . . . 6
โข ({๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ Fin
โ (โฏโ{๐ง
โ ๐ โฃ ยฌ 2
โฅ (1st โ๐ง)}) โ
โ0) |
106 | 104, 105 | syl 17 |
. . . . 5
โข (๐ โ (โฏโ{๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}) โ
โ0) |
107 | | ssrab2 4038 |
. . . . . . 7
โข {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ ๐ |
108 | | ssfi 9118 |
. . . . . . 7
โข ((๐ โ Fin โง {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ ๐) โ {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ
Fin) |
109 | 101, 107,
108 | sylancl 587 |
. . . . . 6
โข (๐ โ {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ
Fin) |
110 | | hashcl 14257 |
. . . . . 6
โข ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ Fin
โ (โฏโ{๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)})
โ โ0) |
111 | 109, 110 | syl 17 |
. . . . 5
โข (๐ โ (โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)}) โ
โ0) |
112 | 80, 106, 111 | expaddd 14054 |
. . . 4
โข (๐ โ
(-1โ((โฏโ{๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)})
+ (โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)}))) = ((-1โ(โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)})) ยท
(-1โ(โฏโ{๐ง
โ ๐ โฃ ยฌ 2
โฅ (1st โ๐ง)})))) |
113 | 90, 63 | syldan 592 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (2 ยท
๐ข) โ
โ) |
114 | | fzfid 13879 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) โ
Fin) |
115 | | xpsnen2g 9010 |
. . . . . . . . . . 11
โข (((2
ยท ๐ข) โ โ
โง (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) โ Fin) โ ({(2 ยท ๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) |
116 | 113, 114,
115 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ({(2 ยท
๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) |
117 | | hasheni 14249 |
. . . . . . . . . 10
โข (({(2
ยท ๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) โ
(โฏโ({(2 ยท ๐ข)} ร (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) =
(โฏโ(1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
118 | 116, 117 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โฏโ({(2 ยท ๐ข)} ร (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) =
(โฏโ(1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
119 | | ssrab2 4038 |
. . . . . . . . . . . . 13
โข {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ ๐ |
120 | 97 | relopabiv 5777 |
. . . . . . . . . . . . 13
โข Rel ๐ |
121 | | relss 5738 |
. . . . . . . . . . . . 13
โข ({๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ ๐ โ (Rel ๐ โ Rel {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) |
122 | 119, 120,
121 | mp2 9 |
. . . . . . . . . . . 12
โข Rel
{๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} |
123 | | relxp 5652 |
. . . . . . . . . . . 12
โข Rel ({(2
ยท ๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) |
124 | 97 | eleq2i 2830 |
. . . . . . . . . . . . . . . 16
โข
(โจ๐ฅ, ๐ฆโฉ โ ๐ โ โจ๐ฅ, ๐ฆโฉ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))}) |
125 | | opabidw 5482 |
. . . . . . . . . . . . . . . 16
โข
(โจ๐ฅ, ๐ฆโฉ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))} โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) |
126 | 124, 125 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โจ๐ฅ, ๐ฆโฉ โ ๐ โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) |
127 | | anass 470 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆ โ โ โง ๐ฆ โค ๐) โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))) โ (๐ฆ โ โ โง (๐ฆ โค ๐ โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))))) |
128 | 113 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) โ
โ) |
129 | 128 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) โ
โ) |
130 | 56 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
131 | 130 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
132 | 131 | rehalfcld 12401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ / 2) โ
โ) |
133 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ โ
โ) |
134 | 133 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
135 | | elfzle2 13446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ข โ
(1...(โโ(๐ /
2))) โ ๐ข โค
(โโ(๐ /
2))) |
136 | 135 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โค (โโ(๐ / 2))) |
137 | 133 | rehalfcld 12401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (๐ / 2) โ
โ) |
138 | | elfzelz 13442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ข โ
(1...(โโ(๐ /
2))) โ ๐ข โ
โค) |
139 | 138 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โ
โค) |
140 | | flge 13711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (((๐ / 2) โ โ โง ๐ข โ โค) โ (๐ข โค (๐ / 2) โ ๐ข โค (โโ(๐ / 2)))) |
141 | 137, 139,
140 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (๐ข โค (๐ / 2) โ ๐ข โค (โโ(๐ / 2)))) |
142 | 136, 141 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โค (๐ / 2)) |
143 | | elfznn 13471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ข โ
(1...(โโ(๐ /
2))) โ ๐ข โ
โ) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โ
โ) |
145 | 144 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โ
โ) |
146 | | 2re 12228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข 2 โ
โ |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ 2 โ
โ) |
148 | | 2pos 12257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข 0 <
2 |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ 0 <
2) |
150 | | lemuldiv2 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ข โ โ โง ๐ โ โ โง (2 โ
โ โง 0 < 2)) โ ((2 ยท ๐ข) โค ๐ โ ๐ข โค (๐ / 2))) |
151 | 145, 133,
147, 149, 150 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((2 ยท
๐ข) โค ๐ โ ๐ข โค (๐ / 2))) |
152 | 142, 151 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (2 ยท
๐ข) โค ๐) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) โค ๐) |
154 | 131 | ltm1d 12088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โ 1) < ๐) |
155 | | peano2rem 11469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
156 | 131, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โ 1) โ
โ) |
157 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 2 โ
โ) |
158 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 0 <
2) |
159 | | ltdiv1 12020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (((๐ โ 1) โ โ โง
๐ โ โ โง (2
โ โ โง 0 < 2)) โ ((๐ โ 1) < ๐ โ ((๐ โ 1) / 2) < (๐ / 2))) |
160 | 156, 131,
157, 158, 159 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ 1) < ๐ โ ((๐ โ 1) / 2) < (๐ / 2))) |
161 | 154, 160 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ 1) / 2) < (๐ / 2)) |
162 | 5, 161 | eqbrtrid 5141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ < (๐ / 2)) |
163 | 129, 134,
132, 153, 162 | lelttrd 11314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) < (๐ / 2)) |
164 | 130 | nnrpd 12956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ+) |
165 | | rphalflt 12945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ+
โ (๐ / 2) < ๐) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ / 2) < ๐) |
167 | 129, 132,
131, 163, 166 | lttrd 11317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) < ๐) |
168 | 129, 131 | ltnled 11303 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((2
ยท ๐ข) < ๐ โ ยฌ ๐ โค (2 ยท ๐ข))) |
169 | 167, 168 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ยฌ
๐ โค (2 ยท ๐ข)) |
170 | 1 | eldifad 3923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ โ โ) |
171 | 170 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
172 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ ๐ โ
โค) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โค) |
174 | | dvdsle 16193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ โค โง (2
ยท ๐ข) โ โ)
โ (๐ โฅ (2
ยท ๐ข) โ ๐ โค (2 ยท ๐ข))) |
175 | 173, 128,
174 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โฅ (2 ยท ๐ข) โ ๐ โค (2 ยท ๐ข))) |
176 | 169, 175 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ยฌ
๐ โฅ (2 ยท ๐ข)) |
177 | 2 | eldifad 3923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ โ โ) |
178 | | prmrp 16589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
179 | 170, 177,
178 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
180 | 3, 179 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐ gcd ๐) = 1) |
181 | 180 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ gcd ๐) = 1) |
182 | 177 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
183 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ ๐ โ
โค) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โค) |
185 | 128 | nnzd 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) โ
โค) |
186 | | coprmdvds 16530 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ โค โง ๐ โ โค โง (2
ยท ๐ข) โ โค)
โ ((๐ โฅ (๐ ยท (2 ยท ๐ข)) โง (๐ gcd ๐) = 1) โ ๐ โฅ (2 ยท ๐ข))) |
187 | 173, 184,
185, 186 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โฅ (๐ ยท (2 ยท ๐ข)) โง (๐ gcd ๐) = 1) โ ๐ โฅ (2 ยท ๐ข))) |
188 | 181, 187 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โฅ (๐ ยท (2 ยท ๐ข)) โ ๐ โฅ (2 ยท ๐ข))) |
189 | 176, 188 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ยฌ
๐ โฅ (๐ ยท (2 ยท ๐ข))) |
190 | | nnz 12521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
191 | 190 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ฆ โ
โค) |
192 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ฆ ยท ๐)) |
193 | 191, 173,
192 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โฅ (๐ฆ ยท ๐)) |
194 | | breq2 5110 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ ยท (2 ยท ๐ข)) = (๐ฆ ยท ๐) โ (๐ โฅ (๐ ยท (2 ยท ๐ข)) โ ๐ โฅ (๐ฆ ยท ๐))) |
195 | 193, 194 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ ยท (2 ยท ๐ข)) = (๐ฆ ยท ๐) โ ๐ โฅ (๐ ยท (2 ยท ๐ข)))) |
196 | 195 | necon3bd 2958 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (ยฌ
๐ โฅ (๐ ยท (2 ยท ๐ข)) โ (๐ ยท (2 ยท ๐ข)) โ (๐ฆ ยท ๐))) |
197 | 189, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (2 ยท ๐ข)) โ (๐ฆ ยท ๐)) |
198 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
199 | 198, 130 | nnmulcld 12207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ ยท ๐) โ โ) |
200 | 199 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ ยท ๐) โ โ) |
201 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ โ
โ) |
202 | 201, 113 | nnmulcld 12207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (๐ ยท (2 ยท ๐ข)) โ
โ) |
203 | 202 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (2 ยท ๐ข)) โ
โ) |
204 | 203 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (2 ยท ๐ข)) โ
โ) |
205 | 200, 204 | ltlend 11301 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ ((๐ฆ ยท ๐) โค (๐ ยท (2 ยท ๐ข)) โง (๐ ยท (2 ยท ๐ข)) โ (๐ฆ ยท ๐)))) |
206 | 197, 205 | mpbiran2d 707 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ (๐ฆ ยท ๐) โค (๐ ยท (2 ยท ๐ข)))) |
207 | | nnre 12161 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
208 | 207 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
209 | 130 | nngt0d 12203 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 0 <
๐) |
210 | | lemuldiv 12036 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง (๐ ยท (2 ยท ๐ข)) โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ฆ ยท ๐) โค (๐ ยท (2 ยท ๐ข)) โ ๐ฆ โค ((๐ ยท (2 ยท ๐ข)) / ๐))) |
211 | 208, 204,
131, 209, 210 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) โค (๐ ยท (2 ยท ๐ข)) โ ๐ฆ โค ((๐ ยท (2 ยท ๐ข)) / ๐))) |
212 | 201 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
213 | 212 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
214 | 128 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (2
ยท ๐ข) โ
โ) |
215 | 130 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
216 | 130 | nnne0d 12204 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ 0) |
217 | 213, 214,
215, 216 | div23d 11969 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ ยท (2 ยท ๐ข)) / ๐) = ((๐ / ๐) ยท (2 ยท ๐ข))) |
218 | 217 | breq2d 5118 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ โค ((๐ ยท (2 ยท ๐ข)) / ๐) โ ๐ฆ โค ((๐ / ๐) ยท (2 ยท ๐ข)))) |
219 | 206, 211,
218 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ ๐ฆ โค ((๐ / ๐) ยท (2 ยท ๐ข)))) |
220 | 212 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
221 | 212 | nngt0d 12203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 0 <
๐) |
222 | | ltmul2 12007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((2
ยท ๐ข) โ โ
โง (๐ / 2) โ
โ โง (๐ โ
โ โง 0 < ๐))
โ ((2 ยท ๐ข) <
(๐ / 2) โ (๐ ยท (2 ยท ๐ข)) < (๐ ยท (๐ / 2)))) |
223 | 129, 132,
220, 221, 222 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((2
ยท ๐ข) < (๐ / 2) โ (๐ ยท (2 ยท ๐ข)) < (๐ ยท (๐ / 2)))) |
224 | 163, 223 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (2 ยท ๐ข)) < (๐ ยท (๐ / 2))) |
225 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 2 โ
โ) |
226 | | 2ne0 12258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข 2 โ
0 |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 2 โ
0) |
228 | | divass 11832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ โง (2 โ
โ โง 2 โ 0)) โ ((๐ ยท ๐) / 2) = (๐ ยท (๐ / 2))) |
229 | | div23 11833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ โง (2 โ
โ โง 2 โ 0)) โ ((๐ ยท ๐) / 2) = ((๐ / 2) ยท ๐)) |
230 | 228, 229 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ โง ๐ โ โ โง (2 โ
โ โง 2 โ 0)) โ (๐ ยท (๐ / 2)) = ((๐ / 2) ยท ๐)) |
231 | 213, 215,
225, 227, 230 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (๐ / 2)) = ((๐ / 2) ยท ๐)) |
232 | 224, 231 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ ยท (2 ยท ๐ข)) < ((๐ / 2) ยท ๐)) |
233 | 220 | rehalfcld 12401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ / 2) โ
โ) |
234 | 233, 131 | remulcld 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ / 2) ยท ๐) โ โ) |
235 | | lttr 11232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ฆ ยท ๐) โ โ โง (๐ ยท (2 ยท ๐ข)) โ โ โง ((๐ / 2) ยท ๐) โ โ) โ (((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โง (๐ ยท (2 ยท ๐ข)) < ((๐ / 2) ยท ๐)) โ (๐ฆ ยท ๐) < ((๐ / 2) ยท ๐))) |
236 | 200, 204,
234, 235 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โง (๐ ยท (2 ยท ๐ข)) < ((๐ / 2) ยท ๐)) โ (๐ฆ ยท ๐) < ((๐ / 2) ยท ๐))) |
237 | 232, 236 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ (๐ฆ ยท ๐) < ((๐ / 2) ยท ๐))) |
238 | | ltmul1 12006 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โ โง (๐ / 2) โ โ โง
(๐ โ โ โง 0
< ๐)) โ (๐ฆ < (๐ / 2) โ (๐ฆ ยท ๐) < ((๐ / 2) ยท ๐))) |
239 | 208, 233,
131, 209, 238 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ < (๐ / 2) โ (๐ฆ ยท ๐) < ((๐ / 2) ยท ๐))) |
240 | 237, 239 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ ๐ฆ < (๐ / 2))) |
241 | | peano2rem 11469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
242 | 220, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โ 1) โ
โ) |
243 | 242 | recnd 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โ 1) โ
โ) |
244 | 213, 243,
225, 227 | divsubdird 11971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ (๐ โ 1)) / 2) = ((๐ / 2) โ ((๐ โ 1) / 2))) |
245 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ๐ = ((๐ โ 1) / 2) |
246 | 245 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ / 2) โ ๐) = ((๐ / 2) โ ((๐ โ 1) / 2)) |
247 | 244, 246 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ (๐ โ 1)) / 2) = ((๐ / 2) โ ๐)) |
248 | | ax-1cn 11110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข 1 โ
โ |
249 | | nncan 11431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
(๐ โ 1)) =
1) |
250 | 213, 248,
249 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ โ (๐ โ 1)) = 1) |
251 | 250 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ (๐ โ 1)) / 2) = (1 /
2)) |
252 | | halflt1 12372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (1 / 2)
< 1 |
253 | 251, 252 | eqbrtrdi 5145 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ โ (๐ โ 1)) / 2) < 1) |
254 | 247, 253 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ / 2) โ ๐) < 1) |
255 | 2, 245 | gausslemma2dlem0b 26708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ โ โ) |
256 | 255 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
257 | 256 | nnred 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ๐ โ
โ) |
258 | | 1red 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ 1 โ
โ) |
259 | 233, 257,
258 | ltsubadd2d 11754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (((๐ / 2) โ ๐) < 1 โ (๐ / 2) < (๐ + 1))) |
260 | 254, 259 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ / 2) < (๐ + 1)) |
261 | | peano2re 11329 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (๐ + 1) โ
โ) |
262 | 257, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ + 1) โ
โ) |
263 | | lttr 11232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โ โง (๐ / 2) โ โ โง
(๐ + 1) โ โ)
โ ((๐ฆ < (๐ / 2) โง (๐ / 2) < (๐ + 1)) โ ๐ฆ < (๐ + 1))) |
264 | 208, 233,
262, 263 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ < (๐ / 2) โง (๐ / 2) < (๐ + 1)) โ ๐ฆ < (๐ + 1))) |
265 | 260, 264 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ < (๐ / 2) โ ๐ฆ < (๐ + 1))) |
266 | 240, 265 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ ๐ฆ < (๐ + 1))) |
267 | | nnleltp1 12559 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ โค ๐ โ ๐ฆ < (๐ + 1))) |
268 | 198, 256,
267 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ โค ๐ โ ๐ฆ < (๐ + 1))) |
269 | 266, 268 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ ๐ฆ โค ๐)) |
270 | 269 | pm4.71rd 564 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)) โ (๐ฆ โค ๐ โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))))) |
271 | 90, 65 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((๐ / ๐) ยท (2 ยท ๐ข)) โ โ) |
272 | | flge 13711 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ / ๐) ยท (2 ยท ๐ข)) โ โ โง ๐ฆ โ โค) โ (๐ฆ โค ((๐ / ๐) ยท (2 ยท ๐ข)) โ ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
273 | 271, 190,
272 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ (๐ฆ โค ((๐ / ๐) ยท (2 ยท ๐ข)) โ ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
274 | 219, 270,
273 | 3bitr3d 309 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฆ โ โ) โ ((๐ฆ โค ๐ โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))) โ ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข))))) |
275 | 274 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((๐ฆ โ โ โง (๐ฆ โค ๐ โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
276 | 127, 275 | bitrid 283 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (((๐ฆ โ โ โง ๐ฆ โค ๐) โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
277 | 276 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (((๐ฆ โ โ โง ๐ฆ โค ๐) โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
278 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ ๐ฅ = (2 ยท ๐ข)) |
279 | | nnuz 12807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข โ =
(โคโฅโ1) |
280 | 113, 279 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (2 ยท
๐ข) โ
(โคโฅโ1)) |
281 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ โ
โค) |
282 | | elfz5 13434 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((2
ยท ๐ข) โ
(โคโฅโ1) โง ๐ โ โค) โ ((2 ยท ๐ข) โ (1...๐) โ (2 ยท ๐ข) โค ๐)) |
283 | 280, 281,
282 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((2 ยท
๐ข) โ (1...๐) โ (2 ยท ๐ข) โค ๐)) |
284 | 152, 283 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (2 ยท
๐ข) โ (1...๐)) |
285 | 284 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (2 ยท ๐ข) โ (1...๐)) |
286 | 278, 285 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ ๐ฅ โ (1...๐)) |
287 | 286 | biantrurd 534 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (๐ฆ โ (1...๐) โ (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)))) |
288 | 255 | nnzd 12527 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ โ โค) |
289 | 288 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ ๐ โ โค) |
290 | | fznn 13510 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (๐ฆ โ (1...๐) โ (๐ฆ โ โ โง ๐ฆ โค ๐))) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (๐ฆ โ (1...๐) โ (๐ฆ โ โ โง ๐ฆ โค ๐))) |
292 | 287, 291 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ (๐ฆ โ โ โง ๐ฆ โค ๐))) |
293 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = (2 ยท ๐ข) โ (๐ฅ ยท ๐) = ((2 ยท ๐ข) ยท ๐)) |
294 | 113 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (2 ยท
๐ข) โ
โ) |
295 | 201 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ โ
โ) |
296 | 294, 295 | mulcomd 11177 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((2 ยท
๐ข) ยท ๐) = (๐ ยท (2 ยท ๐ข))) |
297 | 293, 296 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (๐ฅ ยท ๐) = (๐ ยท (2 ยท ๐ข))) |
298 | 297 | breq2d 5118 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ ((๐ฆ ยท ๐) < (๐ฅ ยท ๐) โ (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข)))) |
299 | 292, 298 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)) โ ((๐ฆ โ โ โง ๐ฆ โค ๐) โง (๐ฆ ยท ๐) < (๐ ยท (2 ยท ๐ข))))) |
300 | 271 | flcld 13704 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โโ((๐ / ๐) ยท (2 ยท ๐ข))) โ
โค) |
301 | | fznn 13510 |
. . . . . . . . . . . . . . . . . 18
โข
((โโ((๐
/ ๐) ยท (2 ยท
๐ข))) โ โค โ
(๐ฆ โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
302 | 300, 301 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (๐ฆ โ
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
303 | 302 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) โ (๐ฆ โ โ โง ๐ฆ โค (โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
304 | 277, 299,
303 | 3bitr4d 311 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)) โ ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
305 | 126, 304 | bitrid 283 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โง ๐ฅ = (2 ยท ๐ข)) โ (โจ๐ฅ, ๐ฆโฉ โ ๐ โ ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
306 | 305 | pm5.32da 580 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ((๐ฅ = (2 ยท ๐ข) โง โจ๐ฅ, ๐ฆโฉ โ ๐) โ (๐ฅ = (2 ยท ๐ข) โง ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข))))))) |
307 | | vex 3450 |
. . . . . . . . . . . . . . . . . 18
โข ๐ฅ โ V |
308 | | vex 3450 |
. . . . . . . . . . . . . . . . . 18
โข ๐ฆ โ V |
309 | 307, 308 | op1std 7932 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ (1st โ๐ง) = ๐ฅ) |
310 | 309 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ((2 ยท ๐ข) = (1st โ๐ง) โ (2 ยท ๐ข) = ๐ฅ)) |
311 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท ๐ข) = ๐ฅ โ ๐ฅ = (2 ยท ๐ข)) |
312 | 310, 311 | bitrdi 287 |
. . . . . . . . . . . . . . 15
โข (๐ง = โจ๐ฅ, ๐ฆโฉ โ ((2 ยท ๐ข) = (1st โ๐ง) โ ๐ฅ = (2 ยท ๐ข))) |
313 | 312 | elrab 3646 |
. . . . . . . . . . . . . 14
โข
(โจ๐ฅ, ๐ฆโฉ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ (โจ๐ฅ, ๐ฆโฉ โ ๐ โง ๐ฅ = (2 ยท ๐ข))) |
314 | 313 | biancomi 464 |
. . . . . . . . . . . . 13
โข
(โจ๐ฅ, ๐ฆโฉ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ (๐ฅ = (2 ยท ๐ข) โง โจ๐ฅ, ๐ฆโฉ โ ๐)) |
315 | | opelxp 5670 |
. . . . . . . . . . . . . 14
โข
(โจ๐ฅ, ๐ฆโฉ โ ({(2 ยท
๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) โ (๐ฅ โ {(2 ยท ๐ข)} โง ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
316 | | velsn 4603 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ {(2 ยท ๐ข)} โ ๐ฅ = (2 ยท ๐ข)) |
317 | 316 | anbi1i 625 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ {(2 ยท ๐ข)} โง ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) โ (๐ฅ = (2 ยท ๐ข) โง ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
318 | 315, 317 | bitri 275 |
. . . . . . . . . . . . 13
โข
(โจ๐ฅ, ๐ฆโฉ โ ({(2 ยท
๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) โ (๐ฅ = (2 ยท ๐ข) โง ๐ฆ โ (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
319 | 306, 314,
318 | 3bitr4g 314 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ (โจ๐ฅ, ๐ฆโฉ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ โจ๐ฅ, ๐ฆโฉ โ ({(2 ยท ๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))))) |
320 | 122, 123,
319 | eqrelrdv 5749 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} = ({(2 ยท ๐ข)} ร (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
321 | 320 | eqcomd 2743 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ({(2 ยท
๐ข)} ร
(1...(โโ((๐ /
๐) ยท (2 ยท
๐ข))))) = {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)}) |
322 | 321 | fveq2d 6847 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โฏโ({(2 ยท ๐ข)} ร (1...(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) = (โฏโ{๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) |
323 | | hashfz1 14247 |
. . . . . . . . . 10
โข
((โโ((๐
/ ๐) ยท (2 ยท
๐ข))) โ
โ0 โ (โฏโ(1...(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) = (โโ((๐ / ๐) ยท (2 ยท ๐ข)))) |
324 | 91, 323 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โฏโ(1...(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) = (โโ((๐ / ๐) ยท (2 ยท ๐ข)))) |
325 | 118, 322,
324 | 3eqtr3rd 2786 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ
(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = (โฏโ{๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) |
326 | 325 | sumeq2dv 15589 |
. . . . . . 7
โข (๐ โ ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โฏโ{๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) |
327 | 101 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ โ Fin) |
328 | | ssfi 9118 |
. . . . . . . . 9
โข ((๐ โ Fin โง {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ ๐) โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ Fin) |
329 | 327, 119,
328 | sylancl 587 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ Fin) |
330 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
โข (๐ง = ๐ฃ โ (1st โ๐ง) = (1st โ๐ฃ)) |
331 | 330 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
โข (๐ง = ๐ฃ โ ((2 ยท ๐ข) = (1st โ๐ง) โ (2 ยท ๐ข) = (1st โ๐ฃ))) |
332 | 331 | elrab 3646 |
. . . . . . . . . . . . . 14
โข (๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ (๐ฃ โ ๐ โง (2 ยท ๐ข) = (1st โ๐ฃ))) |
333 | 332 | simprbi 498 |
. . . . . . . . . . . . 13
โข (๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} โ (2 ยท ๐ข) = (1st โ๐ฃ)) |
334 | 333 | ad2antll 728 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ (2 ยท ๐ข) = (1st โ๐ฃ)) |
335 | 334 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ ((2 ยท ๐ข) / 2) = ((1st โ๐ฃ) / 2)) |
336 | 144 | nncnd 12170 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ (1...(โโ(๐ / 2)))) โ ๐ข โ
โ) |
337 | 336 | adantrr 716 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ ๐ข โ โ) |
338 | | 2cnd 12232 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ 2 โ
โ) |
339 | 226 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ 2 โ 0) |
340 | 337, 338,
339 | divcan3d 11937 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ ((2 ยท ๐ข) / 2) = ๐ข) |
341 | 335, 340 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(โโ(๐ / 2))) โง ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) โ ((1st โ๐ฃ) / 2) = ๐ข) |
342 | 341 | ralrimivva 3198 |
. . . . . . . . 9
โข (๐ โ โ๐ข โ (1...(โโ(๐ / 2)))โ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} ((1st โ๐ฃ) / 2) = ๐ข) |
343 | | invdisj 5090 |
. . . . . . . . 9
โข
(โ๐ข โ
(1...(โโ(๐ /
2)))โ๐ฃ โ {๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} ((1st โ๐ฃ) / 2) = ๐ข โ Disj ๐ข โ (1...(โโ(๐ / 2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)}) |
344 | 342, 343 | syl 17 |
. . . . . . . 8
โข (๐ โ Disj ๐ข โ
(1...(โโ(๐ /
2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)}) |
345 | 87, 329, 344 | hashiun 15708 |
. . . . . . 7
โข (๐ โ (โฏโโช ๐ข โ (1...(โโ(๐ / 2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)}) = ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โฏโ{๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)})) |
346 | | iunrab 5013 |
. . . . . . . . 9
โข โช ๐ข โ (1...(โโ(๐ / 2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} = {๐ง โ ๐ โฃ โ๐ข โ (1...(โโ(๐ / 2)))(2 ยท ๐ข) = (1st โ๐ง)} |
347 | | 2cn 12229 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
348 | | zcn 12505 |
. . . . . . . . . . . . . . 15
โข (๐ข โ โค โ ๐ข โ
โ) |
349 | 348 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ง โ ๐) โง ๐ข โ โค) โ ๐ข โ โ) |
350 | | mulcom 11138 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐ข
โ โ) โ (2 ยท ๐ข) = (๐ข ยท 2)) |
351 | 347, 349,
350 | sylancr 588 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ง โ ๐) โง ๐ข โ โค) โ (2 ยท ๐ข) = (๐ข ยท 2)) |
352 | 351 | eqeq1d 2739 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ง โ ๐) โง ๐ข โ โค) โ ((2 ยท ๐ข) = (1st โ๐ง) โ (๐ข ยท 2) = (1st โ๐ง))) |
353 | 352 | rexbidva 3174 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ ๐) โ (โ๐ข โ โค (2 ยท ๐ข) = (1st โ๐ง) โ โ๐ข โ โค (๐ข ยท 2) = (1st
โ๐ง))) |
354 | 138 | anim1i 616 |
. . . . . . . . . . . . 13
โข ((๐ข โ
(1...(โโ(๐ /
2))) โง (2 ยท ๐ข) =
(1st โ๐ง))
โ (๐ข โ โค
โง (2 ยท ๐ข) =
(1st โ๐ง))) |
355 | 354 | reximi2 3083 |
. . . . . . . . . . . 12
โข
(โ๐ข โ
(1...(โโ(๐ /
2)))(2 ยท ๐ข) =
(1st โ๐ง)
โ โ๐ข โ
โค (2 ยท ๐ข) =
(1st โ๐ง)) |
356 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (2 ยท ๐ข) = (1st โ๐ง)) |
357 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ง โ ๐) โ ๐ง โ ๐) |
358 | 99, 357 | sselid 3943 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ง โ ๐) โ ๐ง โ ((1...๐) ร (1...๐))) |
359 | | xp1st 7954 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ง โ ((1...๐) ร (1...๐)) โ (1st โ๐ง) โ (1...๐)) |
360 | 358, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ง โ ๐) โ (1st โ๐ง) โ (1...๐)) |
361 | 360 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (1st
โ๐ง) โ (1...๐)) |
362 | | elfzle2 13446 |
. . . . . . . . . . . . . . . . . . . 20
โข
((1st โ๐ง) โ (1...๐) โ (1st โ๐ง) โค ๐) |
363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (1st
โ๐ง) โค ๐) |
364 | 356, 363 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (2 ยท ๐ข) โค ๐) |
365 | | zre 12504 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ข โ โค โ ๐ข โ
โ) |
366 | 365 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โ โ) |
367 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ โ โ) |
368 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ 2 โ
โ) |
369 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ 0 <
2) |
370 | 366, 367,
368, 369, 150 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ((2 ยท ๐ข) โค ๐ โ ๐ข โค (๐ / 2))) |
371 | 364, 370 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โค (๐ / 2)) |
372 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (๐ / 2) โ โ) |
373 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โ โค) |
374 | 372, 373,
140 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (๐ข โค (๐ / 2) โ ๐ข โค (โโ(๐ / 2)))) |
375 | 371, 374 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โค (โโ(๐ / 2))) |
376 | | 2t0e0 12323 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 0) = 0 |
377 | | elfznn 13471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((1st โ๐ง) โ (1...๐) โ (1st โ๐ง) โ
โ) |
378 | 361, 377 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (1st
โ๐ง) โ
โ) |
379 | 356, 378 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (2 ยท ๐ข) โ
โ) |
380 | 379 | nngt0d 12203 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ 0 < (2 ยท
๐ข)) |
381 | 376, 380 | eqbrtrid 5141 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (2 ยท 0) <
(2 ยท ๐ข)) |
382 | | 0red 11159 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ 0 โ
โ) |
383 | | ltmul2 12007 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((0
โ โ โง ๐ข
โ โ โง (2 โ โ โง 0 < 2)) โ (0 < ๐ข โ (2 ยท 0) < (2
ยท ๐ข))) |
384 | 382, 366,
368, 369, 383 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (0 < ๐ข โ (2 ยท 0) < (2
ยท ๐ข))) |
385 | 381, 384 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ 0 < ๐ข) |
386 | | elnnz 12510 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ข โ โ โ (๐ข โ โค โง 0 <
๐ข)) |
387 | 373, 385,
386 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โ โ) |
388 | 387, 279 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โ
(โคโฅโ1)) |
389 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (โโ(๐ / 2)) โ
โค) |
390 | | elfz5 13434 |
. . . . . . . . . . . . . . . . 17
โข ((๐ข โ
(โคโฅโ1) โง (โโ(๐ / 2)) โ โค) โ (๐ข โ
(1...(โโ(๐ /
2))) โ ๐ข โค
(โโ(๐ /
2)))) |
391 | 388, 389,
390 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (๐ข โ (1...(โโ(๐ / 2))) โ ๐ข โค (โโ(๐ / 2)))) |
392 | 375, 391 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ ๐ข โ (1...(โโ(๐ / 2)))) |
393 | 392, 356 | jca 513 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ง โ ๐) โง (๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง))) โ (๐ข โ (1...(โโ(๐ / 2))) โง (2 ยท ๐ข) = (1st โ๐ง))) |
394 | 393 | ex 414 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ ๐) โ ((๐ข โ โค โง (2 ยท ๐ข) = (1st โ๐ง)) โ (๐ข โ (1...(โโ(๐ / 2))) โง (2 ยท ๐ข) = (1st โ๐ง)))) |
395 | 394 | reximdv2 3162 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ ๐) โ (โ๐ข โ โค (2 ยท ๐ข) = (1st โ๐ง) โ โ๐ข โ
(1...(โโ(๐ /
2)))(2 ยท ๐ข) =
(1st โ๐ง))) |
396 | 355, 395 | impbid2 225 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ ๐) โ (โ๐ข โ (1...(โโ(๐ / 2)))(2 ยท ๐ข) = (1st โ๐ง) โ โ๐ข โ โค (2 ยท
๐ข) = (1st
โ๐ง))) |
397 | | 2z 12536 |
. . . . . . . . . . . 12
โข 2 โ
โค |
398 | 360 | elfzelzd 13443 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ ๐) โ (1st โ๐ง) โ
โค) |
399 | | divides 16139 |
. . . . . . . . . . . 12
โข ((2
โ โค โง (1st โ๐ง) โ โค) โ (2 โฅ
(1st โ๐ง)
โ โ๐ข โ
โค (๐ข ยท 2) =
(1st โ๐ง))) |
400 | 397, 398,
399 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ ๐) โ (2 โฅ (1st
โ๐ง) โ
โ๐ข โ โค
(๐ข ยท 2) =
(1st โ๐ง))) |
401 | 353, 396,
400 | 3bitr4d 311 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ ๐) โ (โ๐ข โ (1...(โโ(๐ / 2)))(2 ยท ๐ข) = (1st โ๐ง) โ 2 โฅ
(1st โ๐ง))) |
402 | 401 | rabbidva 3415 |
. . . . . . . . 9
โข (๐ โ {๐ง โ ๐ โฃ โ๐ข โ (1...(โโ(๐ / 2)))(2 ยท ๐ข) = (1st โ๐ง)} = {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)}) |
403 | 346, 402 | eqtrid 2789 |
. . . . . . . 8
โข (๐ โ โช ๐ข โ (1...(โโ(๐ / 2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)} = {๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)}) |
404 | 403 | fveq2d 6847 |
. . . . . . 7
โข (๐ โ (โฏโโช ๐ข โ (1...(โโ(๐ / 2))){๐ง โ ๐ โฃ (2 ยท ๐ข) = (1st โ๐ง)}) = (โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)})) |
405 | 326, 345,
404 | 3eqtr2d 2783 |
. . . . . 6
โข (๐ โ ฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข))) = (โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)})) |
406 | 405 | oveq2d 7374 |
. . . . 5
โข (๐ โ (-1โฮฃ๐ข โ
(1...(โโ(๐ /
2)))(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) =
(-1โ(โฏโ{๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)}))) |
407 | 1, 2, 3, 5, 245, 97 | lgsquadlem1 26731 |
. . . . 5
โข (๐ โ (-1โฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) = (-1โ(โฏโ{๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}))) |
408 | 406, 407 | oveq12d 7376 |
. . . 4
โข (๐ โ ((-1โฮฃ๐ข โ
(1...(โโ(๐ /
2)))(โโ((๐ /
๐) ยท (2 ยท
๐ข)))) ยท
(-1โฮฃ๐ข โ
(((โโ(๐ / 2)) +
1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) = ((-1โ(โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)})) ยท
(-1โ(โฏโ{๐ง
โ ๐ โฃ ยฌ 2
โฅ (1st โ๐ง)})))) |
409 | 112, 408 | eqtr4d 2780 |
. . 3
โข (๐ โ
(-1โ((โฏโ{๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)})
+ (โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)}))) = ((-1โฮฃ๐ข โ (1...(โโ(๐ / 2)))(โโ((๐ / ๐) ยท (2 ยท ๐ข)))) ยท (-1โฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข)))))) |
410 | | inrab 4267 |
. . . . . . 7
โข ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โฉ {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}) = {๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โง ยฌ 2
โฅ (1st โ๐ง))} |
411 | | pm3.24 404 |
. . . . . . . . . 10
โข ยฌ (2
โฅ (1st โ๐ง) โง ยฌ 2 โฅ (1st
โ๐ง)) |
412 | 411 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ยฌ (2 โฅ
(1st โ๐ง)
โง ยฌ 2 โฅ (1st โ๐ง))) |
413 | 412 | ralrimivw 3148 |
. . . . . . . 8
โข (๐ โ โ๐ง โ ๐ ยฌ (2 โฅ (1st
โ๐ง) โง ยฌ 2
โฅ (1st โ๐ง))) |
414 | | rabeq0 4345 |
. . . . . . . 8
โข ({๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โง ยฌ 2
โฅ (1st โ๐ง))} = โ
โ โ๐ง โ ๐ ยฌ (2 โฅ (1st
โ๐ง) โง ยฌ 2
โฅ (1st โ๐ง))) |
415 | 413, 414 | sylibr 233 |
. . . . . . 7
โข (๐ โ {๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โง ยฌ 2
โฅ (1st โ๐ง))} = โ
) |
416 | 410, 415 | eqtrid 2789 |
. . . . . 6
โข (๐ โ ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โฉ {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}) =
โ
) |
417 | | hashun 14283 |
. . . . . 6
โข (({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โ Fin โง
{๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)} โ Fin โง
({๐ง โ ๐ โฃ 2 โฅ
(1st โ๐ง)}
โฉ {๐ง โ ๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)})
= โ
) โ (โฏโ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โช {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)})) =
((โฏโ{๐ง โ
๐ โฃ 2 โฅ
(1st โ๐ง)})
+ (โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)}))) |
418 | 109, 104,
416, 417 | syl3anc 1372 |
. . . . 5
โข (๐ โ (โฏโ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โช {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)})) =
((โฏโ{๐ง โ
๐ โฃ 2 โฅ
(1st โ๐ง)})
+ (โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)}))) |
419 | | unrab 4266 |
. . . . . . 7
โข ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โช {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}) = {๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โจ ยฌ 2
โฅ (1st โ๐ง))} |
420 | | exmid 894 |
. . . . . . . . 9
โข (2
โฅ (1st โ๐ง) โจ ยฌ 2 โฅ (1st
โ๐ง)) |
421 | 420 | rgenw 3069 |
. . . . . . . 8
โข
โ๐ง โ
๐ (2 โฅ
(1st โ๐ง)
โจ ยฌ 2 โฅ (1st โ๐ง)) |
422 | | rabid2 3437 |
. . . . . . . 8
โข (๐ = {๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โจ ยฌ 2
โฅ (1st โ๐ง))} โ โ๐ง โ ๐ (2 โฅ (1st โ๐ง) โจ ยฌ 2 โฅ
(1st โ๐ง))) |
423 | 421, 422 | mpbir 230 |
. . . . . . 7
โข ๐ = {๐ง โ ๐ โฃ (2 โฅ (1st
โ๐ง) โจ ยฌ 2
โฅ (1st โ๐ง))} |
424 | 419, 423 | eqtr4i 2768 |
. . . . . 6
โข ({๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)} โช {๐ง โ ๐ โฃ ยฌ 2 โฅ (1st
โ๐ง)}) = ๐ |
425 | 424 | fveq2i 6846 |
. . . . 5
โข
(โฏโ({๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)}
โช {๐ง โ ๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)})) = (โฏโ๐) |
426 | 418, 425 | eqtr3di 2792 |
. . . 4
โข (๐ โ ((โฏโ{๐ง โ ๐ โฃ 2 โฅ (1st
โ๐ง)}) +
(โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)})) = (โฏโ๐)) |
427 | 426 | oveq2d 7374 |
. . 3
โข (๐ โ
(-1โ((โฏโ{๐ง
โ ๐ โฃ 2 โฅ
(1st โ๐ง)})
+ (โฏโ{๐ง โ
๐ โฃ ยฌ 2 โฅ
(1st โ๐ง)}))) = (-1โ(โฏโ๐))) |
428 | 93, 409, 427 | 3eqtr2d 2783 |
. 2
โข (๐ โ (-1โ(ฮฃ๐ข โ
(1...(โโ(๐ /
2)))(โโ((๐ /
๐) ยท (2 ยท
๐ข))) + ฮฃ๐ข โ (((โโ(๐ / 2)) + 1)...๐)(โโ((๐ / ๐) ยท (2 ยท ๐ข))))) = (-1โ(โฏโ๐))) |
429 | 4, 78, 428 | 3eqtrd 2781 |
1
โข (๐ โ (๐ /L ๐) = (-1โ(โฏโ๐))) |