Step | Hyp | Ref
| Expression |
1 | | bgoldbtbnd.i |
. . . . 5
β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) |
2 | | elfzoelz 13581 |
. . . . . . 7
β’ (πΌ β (1..^π·) β πΌ β β€) |
3 | | elfzoel2 13580 |
. . . . . . 7
β’ (πΌ β (1..^π·) β π· β β€) |
4 | | elfzom1b 13680 |
. . . . . . . . 9
β’ ((πΌ β β€ β§ π· β β€) β (πΌ β (1..^π·) β (πΌ β 1) β (0..^(π· β 1)))) |
5 | | fzossrbm1 13610 |
. . . . . . . . . . 11
β’ (π· β β€ β
(0..^(π· β 1)) β
(0..^π·)) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((πΌ β β€ β§ π· β β€) β
(0..^(π· β 1)) β
(0..^π·)) |
7 | 6 | sseld 3947 |
. . . . . . . . 9
β’ ((πΌ β β€ β§ π· β β€) β ((πΌ β 1) β (0..^(π· β 1)) β (πΌ β 1) β (0..^π·))) |
8 | 4, 7 | sylbid 239 |
. . . . . . . 8
β’ ((πΌ β β€ β§ π· β β€) β (πΌ β (1..^π·) β (πΌ β 1) β (0..^π·))) |
9 | 8 | com12 32 |
. . . . . . 7
β’ (πΌ β (1..^π·) β ((πΌ β β€ β§ π· β β€) β (πΌ β 1) β (0..^π·))) |
10 | 2, 3, 9 | mp2and 698 |
. . . . . 6
β’ (πΌ β (1..^π·) β (πΌ β 1) β (0..^π·)) |
11 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (πΌ β 1) β (πΉβπ) = (πΉβ(πΌ β 1))) |
12 | 11 | eleq1d 2819 |
. . . . . . . 8
β’ (π = (πΌ β 1) β ((πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β (β β
{2}))) |
13 | | fvoveq1 7384 |
. . . . . . . . . 10
β’ (π = (πΌ β 1) β (πΉβ(π + 1)) = (πΉβ((πΌ β 1) + 1))) |
14 | 13, 11 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = (πΌ β 1) β ((πΉβ(π + 1)) β (πΉβπ)) = ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))) |
15 | 14 | breq1d 5119 |
. . . . . . . 8
β’ (π = (πΌ β 1) β (((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4))) |
16 | 14 | breq2d 5121 |
. . . . . . . 8
β’ (π = (πΌ β 1) β (4 < ((πΉβ(π + 1)) β (πΉβπ)) β 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) |
17 | 12, 15, 16 | 3anbi123d 1437 |
. . . . . . 7
β’ (π = (πΌ β 1) β (((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))))) |
18 | 17 | rspcv 3579 |
. . . . . 6
β’ ((πΌ β 1) β (0..^π·) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))))) |
19 | 10, 18 | syl 17 |
. . . . 5
β’ (πΌ β (1..^π·) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))))) |
20 | 1, 19 | syl5com 31 |
. . . 4
β’ (π β (πΌ β (1..^π·) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))))) |
21 | 20 | a1d 25 |
. . 3
β’ (π β (π β Odd β (πΌ β (1..^π·) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))))) |
22 | 21 | 3imp 1112 |
. 2
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) |
23 | | bgoldbtbndlem2.s |
. . . . 5
β’ π = (π β (πΉβ(πΌ β 1))) |
24 | | simp2 1138 |
. . . . . . . 8
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β π β Odd ) |
25 | | oddprmALTV 45969 |
. . . . . . . . 9
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β Odd
) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . 8
β’ (((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))) β (πΉβ(πΌ β 1)) β Odd ) |
27 | 24, 26 | anim12i 614 |
. . . . . . 7
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β (π β Odd β§ (πΉβ(πΌ β 1)) β Odd )) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (π β Odd β§ (πΉβ(πΌ β 1)) β Odd )) |
29 | | omoeALTV 45967 |
. . . . . 6
β’ ((π β Odd β§ (πΉβ(πΌ β 1)) β Odd ) β (π β (πΉβ(πΌ β 1))) β Even ) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (π β (πΉβ(πΌ β 1))) β Even ) |
31 | 23, 30 | eqeltrid 2838 |
. . . 4
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β π β Even ) |
32 | 2 | zcnd 12616 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΌ β (1..^π·) β πΌ β β) |
33 | 32 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β πΌ β β) |
34 | | npcan1 11588 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΌ β β β ((πΌ β 1) + 1) = πΌ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΌ β 1) + 1) = πΌ) |
36 | 35 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (πΉβ((πΌ β 1) + 1)) = (πΉβπΌ)) |
37 | 36 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) = ((πΉβπΌ) β (πΉβ(πΌ β 1)))) |
38 | 37 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ (πΉβ(πΌ β 1)) β (β β {2}))
β (((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) |
40 | | eldifi 4090 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β
β) |
41 | | prmz 16559 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβ(πΌ β 1)) β β β (πΉβ(πΌ β 1)) β
β€) |
42 | | zre 12511 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβ(πΌ β 1)) β β€ β (πΉβ(πΌ β 1)) β
β) |
43 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (πΉβπ) β (β β
{2})) |
44 | 43 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β βπ β (0..^π·)(πΉβπ) β (β β
{2})) |
45 | | fzo0ss1 13611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(1..^π·) β
(0..^π·) |
46 | 45 | sseli 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΌ β (1..^π·) β πΌ β (0..^π·)) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ πΌ β (1..^π·)) β πΌ β (0..^π·)) |
48 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = πΌ β (πΉβπ) = (πΉβπΌ)) |
49 | 48 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = πΌ β ((πΉβπ) β (β β {2}) β (πΉβπΌ) β (β β
{2}))) |
50 | 49 | rspcv 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΌ β (0..^π·) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβπΌ) β (β β
{2}))) |
51 | 47, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβπΌ) β (β β
{2}))) |
52 | 51 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΌ β (1..^π·) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβπΌ) β (β β
{2})))) |
53 | 52 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΌ β (1..^π·) β (πΉβπΌ) β (β β
{2})))) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Odd β (π β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΌ β (1..^π·) β (πΉβπΌ) β (β β
{2}))))) |
55 | 54 | com13 88 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
(0..^π·)(πΉβπ) β (β β {2}) β (π β (π β Odd β (πΌ β (1..^π·) β (πΉβπΌ) β (β β
{2}))))) |
56 | 44, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (π β (π β Odd β (πΌ β (1..^π·) β (πΉβπΌ) β (β β
{2}))))) |
57 | 1, 56 | mpcom 38 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β Odd β (πΌ β (1..^π·) β (πΉβπΌ) β (β β
{2})))) |
58 | 57 | 3imp 1112 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (πΉβπΌ) β (β β
{2})) |
59 | | eldifi 4090 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπΌ) β (β β {2}) β (πΉβπΌ) β β) |
60 | | prmz 16559 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπΌ) β β β (πΉβπΌ) β β€) |
61 | | zre 12511 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβπΌ) β β€ β (πΉβπΌ) β β) |
62 | | bgoldbtbnd.n |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β (β€β₯β;11)) |
63 | | eluzelz 12781 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β;11)
β π β
β€) |
64 | | zre 12511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β€ β π β
β) |
65 | | oddz 45913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β Odd β π β
β€) |
66 | 65 | zred 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β Odd β π β
β) |
67 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β π β
β) |
68 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (πΉβπΌ) β β) |
69 | | 4re 12245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 4 β
β |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β 4
β β) |
71 | 67, 68, 70 | lesubaddd 11760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β ((π β (πΉβπΌ)) β€ 4 β π β€ (4 + (πΉβπΌ)))) |
72 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β π β β) |
73 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (πΉβ(πΌ β 1)) β
β) |
74 | 72, 73 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (π β (πΉβ(πΌ β 1))) β
β) |
75 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β 4 β
β) |
76 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (πΉβπΌ) β β) |
77 | 75, 76 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (4 + (πΉβπΌ)) β β) |
78 | 77, 73 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β ((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1))) β
β) |
79 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β π β β) |
80 | 70, 68 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (4 +
(πΉβπΌ)) β β) |
81 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (πΉβ(πΌ β 1)) β
β) |
82 | 67, 80, 81 | lesub1d 11770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (π β€ (4 + (πΉβπΌ)) β (π β (πΉβ(πΌ β 1))) β€ ((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1))))) |
83 | 82 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ π β€ (4 + (πΉβπΌ))) β (π β (πΉβ(πΌ β 1))) β€ ((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1)))) |
84 | 83 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (π β (πΉβ(πΌ β 1))) β€ ((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1)))) |
85 | | resubcl 11473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) β
β) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) β
β) |
87 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β π β
β) |
88 | | ltaddsub2 11638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((4
β β β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) β β β§ π β β) β ((4 +
((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π β ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) |
89 | 88 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((4
β β β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) β β β§ π β β) β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
90 | 70, 86, 87, 89 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β
(((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
91 | 90 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β
(((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
92 | 91 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β ((π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4)) β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
93 | 92 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π) |
94 | | 4cn 12246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ 4 β
β |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β 4
β β) |
96 | 68 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (πΉβπΌ) β β) |
97 | | recn 11149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΉβ(πΌ β 1)) β β β (πΉβ(πΌ β 1)) β
β) |
98 | 97 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β) β (πΉβ(πΌ β 1)) β
β) |
99 | 98 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (πΉβ(πΌ β 1)) β
β) |
100 | 95, 96, 99 | addsubassd 11540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β ((4 +
(πΉβπΌ)) β (πΉβ(πΌ β 1))) = (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1))))) |
101 | 100 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (((4 +
(πΉβπΌ)) β (πΉβ(πΌ β 1))) < π β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1))) < π β (4 + ((πΉβπΌ) β (πΉβ(πΌ β 1)))) < π)) |
103 | 93, 102 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β ((4 + (πΉβπΌ)) β (πΉβ(πΌ β 1))) < π) |
104 | 74, 78, 79, 84, 103 | lelttrd 11321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β§ (π β€ (4 + (πΉβπΌ)) β§ ((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4))) β (π β (πΉβ(πΌ β 1))) < π) |
105 | 104 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β (π β€ (4 + (πΉβπΌ)) β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β (π β (πΉβ(πΌ β 1))) < π))) |
106 | 71, 105 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β ((π β (πΉβπΌ)) β€ 4 β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β (π β (πΉβ(πΌ β 1))) < π))) |
107 | 106 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β β β§ π β β) β§ ((πΉβπΌ) β β β§ (πΉβ(πΌ β 1)) β β)) β
(((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))) |
108 | 107 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β β§ π β β) β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
109 | 66, 108 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β β§ π β Odd ) β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
110 | 109 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (π β Odd β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))))) |
111 | 64, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β (π β Odd β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))))) |
112 | 62, 63, 111 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π β Odd β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))))) |
113 | 112 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β Odd ) β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
114 | 113 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβπΌ) β β β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
115 | 61, 114 | syl5com 31 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπΌ) β β€ β ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
116 | 59, 60, 115 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπΌ) β (β β {2}) β
((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))))) |
117 | 58, 116 | mpcom 38 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ(πΌ β 1)) β β β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))) |
118 | 42, 117 | syl5com 31 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβ(πΌ β 1)) β β€ β ((π β§ π β Odd β§ πΌ β (1..^π·)) β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))) |
119 | 40, 41, 118 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β ((π β§ π β Odd β§ πΌ β (1..^π·)) β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))) |
120 | 119 | impcom 409 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ (πΉβ(πΌ β 1)) β (β β {2}))
β (((πΉβπΌ) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))) |
121 | 39, 120 | sylbid 239 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ (πΉβ(πΌ β 1)) β (β β {2}))
β (((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))) |
122 | 121 | expcom 415 |
. . . . . . . . . . . 12
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β ((π β§ π β Odd β§ πΌ β (1..^π·)) β (((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))) |
123 | 122 | com23 86 |
. . . . . . . . . . 11
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)))) |
124 | 123 | imp 408 |
. . . . . . . . . 10
β’ (((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4)) β ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))) |
125 | 124 | 3adant3 1133 |
. . . . . . . . 9
β’ (((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))) β ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π))) |
126 | 125 | impcom 409 |
. . . . . . . 8
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β ((π β (πΉβπΌ)) β€ 4 β (π β (πΉβ(πΌ β 1))) < π)) |
127 | 126 | com12 32 |
. . . . . . 7
β’ ((π β (πΉβπΌ)) β€ 4 β (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β (π β (πΉβ(πΌ β 1))) < π)) |
128 | 127 | adantl 483 |
. . . . . 6
β’ ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β (π β (πΉβ(πΌ β 1))) < π)) |
129 | 128 | impcom 409 |
. . . . 5
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (π β (πΉβ(πΌ β 1))) < π) |
130 | 23, 129 | eqbrtrid 5144 |
. . . 4
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β π < π) |
131 | 69 | a1i 11 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β 4 β
β) |
132 | | 1eluzge0 12825 |
. . . . . . . . . . . . . . . 16
β’ 1 β
(β€β₯β0) |
133 | | fzoss1 13608 |
. . . . . . . . . . . . . . . 16
β’ (1 β
(β€β₯β0) β (1..^π·) β (0..^π·)) |
134 | 132, 133 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ (π β (1..^π·) β (0..^π·)) |
135 | 134 | sselda 3948 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΌ β (1..^π·)) β πΌ β (0..^π·)) |
136 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . 18
β’ (π = πΌ β (πΉβ(π + 1)) = (πΉβ(πΌ + 1))) |
137 | 136, 48 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΌ β ((πΉβ(π + 1)) β (πΉβπ)) = ((πΉβ(πΌ + 1)) β (πΉβπΌ))) |
138 | 137 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
β’ (π = πΌ β (((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β ((πΉβ(πΌ + 1)) β (πΉβπΌ)) < (π β 4))) |
139 | 137 | breq2d 5121 |
. . . . . . . . . . . . . . . 16
β’ (π = πΌ β (4 < ((πΉβ(π + 1)) β (πΉβπ)) β 4 < ((πΉβ(πΌ + 1)) β (πΉβπΌ)))) |
140 | 49, 138, 139 | 3anbi123d 1437 |
. . . . . . . . . . . . . . 15
β’ (π = πΌ β (((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβπΌ) β (β β {2}) β§ ((πΉβ(πΌ + 1)) β (πΉβπΌ)) < (π β 4) β§ 4 < ((πΉβ(πΌ + 1)) β (πΉβπΌ))))) |
141 | 140 | rspcv 3579 |
. . . . . . . . . . . . . 14
β’ (πΌ β (0..^π·) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβπΌ) β (β β {2}) β§ ((πΉβ(πΌ + 1)) β (πΉβπΌ)) < (π β 4) β§ 4 < ((πΉβ(πΌ + 1)) β (πΉβπΌ))))) |
142 | 135, 141 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β ((πΉβπΌ) β (β β {2}) β§ ((πΉβ(πΌ + 1)) β (πΉβπΌ)) < (π β 4) β§ 4 < ((πΉβ(πΌ + 1)) β (πΉβπΌ))))) |
143 | 60 | zred 12615 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπΌ) β β β (πΉβπΌ) β β) |
144 | 59, 143 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((πΉβπΌ) β (β β {2}) β (πΉβπΌ) β β) |
145 | 144 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ (((πΉβπΌ) β (β β {2}) β§ ((πΉβ(πΌ + 1)) β (πΉβπΌ)) < (π β 4) β§ 4 < ((πΉβ(πΌ + 1)) β (πΉβπΌ))) β (πΉβπΌ) β β) |
146 | 142, 145 | syl6 35 |
. . . . . . . . . . . 12
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (πΉβπΌ) β β)) |
147 | 146 | ex 414 |
. . . . . . . . . . 11
β’ (π β (πΌ β (1..^π·) β (βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (πΉβπΌ) β β))) |
148 | 1, 147 | mpid 44 |
. . . . . . . . . 10
β’ (π β (πΌ β (1..^π·) β (πΉβπΌ) β β)) |
149 | 148 | imp 408 |
. . . . . . . . 9
β’ ((π β§ πΌ β (1..^π·)) β (πΉβπΌ) β β) |
150 | 149 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (πΉβπΌ) β β) |
151 | 150 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (πΉβπΌ) β β) |
152 | 41 | zred 12615 |
. . . . . . . . . 10
β’ ((πΉβ(πΌ β 1)) β β β (πΉβ(πΌ β 1)) β
β) |
153 | 40, 152 | syl 17 |
. . . . . . . . 9
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β
β) |
154 | 153 | 3ad2ant1 1134 |
. . . . . . . 8
β’ (((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))) β (πΉβ(πΌ β 1)) β
β) |
155 | 154 | ad2antlr 726 |
. . . . . . 7
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (πΉβ(πΌ β 1)) β
β) |
156 | 151, 155 | resubcld 11591 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) β
β) |
157 | 66 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β π β β) |
158 | | resubcl 11473 |
. . . . . . . 8
β’ ((π β β β§ (πΉβ(πΌ β 1)) β β) β (π β (πΉβ(πΌ β 1))) β
β) |
159 | 157, 154,
158 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β (π β (πΉβ(πΌ β 1))) β
β) |
160 | 159 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (π β (πΉβ(πΌ β 1))) β
β) |
161 | 32, 34 | syl 17 |
. . . . . . . . . . . . . 14
β’ (πΌ β (1..^π·) β ((πΌ β 1) + 1) = πΌ) |
162 | 161 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΌ β 1) + 1) = πΌ) |
163 | 162 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (πΉβ((πΌ β 1) + 1)) = (πΉβπΌ)) |
164 | 163 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) = ((πΉβπΌ) β (πΉβ(πΌ β 1)))) |
165 | 164 | breq2d 5121 |
. . . . . . . . . 10
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) β 4 < ((πΉβπΌ) β (πΉβ(πΌ β 1))))) |
166 | 165 | biimpcd 249 |
. . . . . . . . 9
β’ (4 <
((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) β ((π β§ π β Odd β§ πΌ β (1..^π·)) β 4 < ((πΉβπΌ) β (πΉβ(πΌ β 1))))) |
167 | 166 | 3ad2ant3 1136 |
. . . . . . . 8
β’ (((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1)))) β ((π β§ π β Odd β§ πΌ β (1..^π·)) β 4 < ((πΉβπΌ) β (πΉβ(πΌ β 1))))) |
168 | 167 | impcom 409 |
. . . . . . 7
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β 4 < ((πΉβπΌ) β (πΉβ(πΌ β 1)))) |
169 | 168 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β 4 < ((πΉβπΌ) β (πΉβ(πΌ β 1)))) |
170 | 157 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β π β β) |
171 | | bgoldbtbnd.d |
. . . . . . . . . . . . . . . . 17
β’ (π β π· β
(β€β₯β3)) |
172 | | eluzge3nn 12823 |
. . . . . . . . . . . . . . . . 17
β’ (π· β
(β€β₯β3) β π· β β) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β β) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΌ β (1..^π·)) β π· β β) |
175 | | bgoldbtbnd.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ β (RePartβπ·)) |
176 | 175 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΌ β (1..^π·)) β πΉ β (RePartβπ·)) |
177 | 132, 133 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
β’ (π· β
(β€β₯β3) β (1..^π·) β (0..^π·)) |
178 | | fzossfz 13600 |
. . . . . . . . . . . . . . . . . 18
β’
(0..^π·) β
(0...π·) |
179 | 177, 178 | sstrdi 3960 |
. . . . . . . . . . . . . . . . 17
β’ (π· β
(β€β₯β3) β (1..^π·) β (0...π·)) |
180 | 171, 179 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (1..^π·) β (0...π·)) |
181 | 180 | sselda 3948 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΌ β (1..^π·)) β πΌ β (0...π·)) |
182 | 174, 176,
181 | iccpartxr 45701 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΌ β (1..^π·)) β (πΉβπΌ) β
β*) |
183 | | fzofzp1 13678 |
. . . . . . . . . . . . . . . 16
β’ (πΌ β (0..^π·) β (πΌ + 1) β (0...π·)) |
184 | 135, 183 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΌ β (1..^π·)) β (πΌ + 1) β (0...π·)) |
185 | 174, 176,
184 | iccpartxr 45701 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΌ β (1..^π·)) β (πΉβ(πΌ + 1)) β
β*) |
186 | 182, 185 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ πΌ β (1..^π·)) β ((πΉβπΌ) β β* β§ (πΉβ(πΌ + 1)) β
β*)) |
187 | 186 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((πΉβπΌ) β β* β§ (πΉβ(πΌ + 1)) β
β*)) |
188 | | elico1 13316 |
. . . . . . . . . . . 12
β’ (((πΉβπΌ) β β* β§ (πΉβ(πΌ + 1)) β β*) β
(π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β (π β β* β§ (πΉβπΌ) β€ π β§ π < (πΉβ(πΌ + 1))))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β (π β β* β§ (πΉβπΌ) β€ π β§ π < (πΉβ(πΌ + 1))))) |
190 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (πΉβπΌ) β€ π β§ π < (πΉβ(πΌ + 1))) β (πΉβπΌ) β€ π) |
191 | 189, 190 | syl6bi 253 |
. . . . . . . . . 10
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β (πΉβπΌ) β€ π)) |
192 | 191 | adantrd 493 |
. . . . . . . . 9
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (πΉβπΌ) β€ π)) |
193 | 192 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (πΉβπΌ) β€ π)) |
194 | 193 | imp 408 |
. . . . . . 7
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (πΉβπΌ) β€ π) |
195 | 151, 170,
155, 194 | lesub1dd 11779 |
. . . . . 6
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β ((πΉβπΌ) β (πΉβ(πΌ β 1))) β€ (π β (πΉβ(πΌ β 1)))) |
196 | 131, 156,
160, 169, 195 | ltletrd 11323 |
. . . . 5
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β 4 < (π β (πΉβ(πΌ β 1)))) |
197 | 196, 23 | breqtrrdi 5151 |
. . . 4
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β 4 < π) |
198 | 31, 130, 197 | 3jca 1129 |
. . 3
β’ ((((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β§ (π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4)) β (π β Even β§ π < π β§ 4 < π)) |
199 | 198 | ex 414 |
. 2
β’ (((π β§ π β Odd β§ πΌ β (1..^π·)) β§ ((πΉβ(πΌ β 1)) β (β β {2})
β§ ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))) < (π β 4) β§ 4 < ((πΉβ((πΌ β 1) + 1)) β (πΉβ(πΌ β 1))))) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (π β Even β§ π < π β§ 4 < π))) |
200 | 22, 199 | mpdan 686 |
1
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (π β Even β§ π < π β§ 4 < π))) |