Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . 5
β’ (π₯ = 1 β (seq1( + , πΊ)βπ₯) = (seq1( + , πΊ)β1)) |
2 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = 1 β (2βπ₯) = (2β1)) |
3 | | 2cn 12235 |
. . . . . . . . 9
β’ 2 β
β |
4 | | exp1 13980 |
. . . . . . . . 9
β’ (2 β
β β (2β1) = 2) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
β’
(2β1) = 2 |
6 | 2, 5 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = 1 β (2βπ₯) = 2) |
7 | 6 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = 1 β (seq1( + , πΉ)β(2βπ₯)) = (seq1( + , πΉ)β2)) |
8 | 7 | oveq2d 7378 |
. . . . 5
β’ (π₯ = 1 β (2 Β· (seq1( +
, πΉ)β(2βπ₯))) = (2 Β· (seq1( + ,
πΉ)β2))) |
9 | 1, 8 | breq12d 5123 |
. . . 4
β’ (π₯ = 1 β ((seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯))) β (seq1( + , πΊ)β1) β€ (2 Β·
(seq1( + , πΉ)β2)))) |
10 | 9 | imbi2d 341 |
. . 3
β’ (π₯ = 1 β ((π β (seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯)))) β (π β (seq1( + , πΊ)β1) β€ (2 Β· (seq1( + , πΉ)β2))))) |
11 | | fveq2 6847 |
. . . . 5
β’ (π₯ = π β (seq1( + , πΊ)βπ₯) = (seq1( + , πΊ)βπ)) |
12 | | oveq2 7370 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
13 | 12 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = π β (seq1( + , πΉ)β(2βπ₯)) = (seq1( + , πΉ)β(2βπ))) |
14 | 13 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π β (2 Β· (seq1( + , πΉ)β(2βπ₯))) = (2 Β· (seq1( + ,
πΉ)β(2βπ)))) |
15 | 11, 14 | breq12d 5123 |
. . . 4
β’ (π₯ = π β ((seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯))) β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))))) |
16 | 15 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β (seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯)))) β (π β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ)))))) |
17 | | fveq2 6847 |
. . . . 5
β’ (π₯ = (π + 1) β (seq1( + , πΊ)βπ₯) = (seq1( + , πΊ)β(π + 1))) |
18 | | oveq2 7370 |
. . . . . . 7
β’ (π₯ = (π + 1) β (2βπ₯) = (2β(π + 1))) |
19 | 18 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = (π + 1) β (seq1( + , πΉ)β(2βπ₯)) = (seq1( + , πΉ)β(2β(π + 1)))) |
20 | 19 | oveq2d 7378 |
. . . . 5
β’ (π₯ = (π + 1) β (2 Β· (seq1( + , πΉ)β(2βπ₯))) = (2 Β· (seq1( + ,
πΉ)β(2β(π + 1))))) |
21 | 17, 20 | breq12d 5123 |
. . . 4
β’ (π₯ = (π + 1) β ((seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯))) β (seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1)))))) |
22 | 21 | imbi2d 341 |
. . 3
β’ (π₯ = (π + 1) β ((π β (seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯)))) β (π β (seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1))))))) |
23 | | fveq2 6847 |
. . . . 5
β’ (π₯ = π β (seq1( + , πΊ)βπ₯) = (seq1( + , πΊ)βπ)) |
24 | | oveq2 7370 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
25 | 24 | fveq2d 6851 |
. . . . . 6
β’ (π₯ = π β (seq1( + , πΉ)β(2βπ₯)) = (seq1( + , πΉ)β(2βπ))) |
26 | 25 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π β (2 Β· (seq1( + , πΉ)β(2βπ₯))) = (2 Β· (seq1( + ,
πΉ)β(2βπ)))) |
27 | 23, 26 | breq12d 5123 |
. . . 4
β’ (π₯ = π β ((seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯))) β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))))) |
28 | 27 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β (seq1( + , πΊ)βπ₯) β€ (2 Β· (seq1( + , πΉ)β(2βπ₯)))) β (π β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ)))))) |
29 | | fveq2 6847 |
. . . . . . . 8
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
30 | 29 | breq2d 5122 |
. . . . . . 7
β’ (π = 1 β (0 β€ (πΉβπ) β 0 β€ (πΉβ1))) |
31 | | climcnds.2 |
. . . . . . . 8
β’ ((π β§ π β β) β 0 β€ (πΉβπ)) |
32 | 31 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β β 0 β€ (πΉβπ)) |
33 | | 1nn 12171 |
. . . . . . . 8
β’ 1 β
β |
34 | 33 | a1i 11 |
. . . . . . 7
β’ (π β 1 β
β) |
35 | 30, 32, 34 | rspcdva 3585 |
. . . . . 6
β’ (π β 0 β€ (πΉβ1)) |
36 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = 2 β (πΉβπ) = (πΉβ2)) |
37 | 36 | eleq1d 2823 |
. . . . . . . 8
β’ (π = 2 β ((πΉβπ) β β β (πΉβ2) β β)) |
38 | | climcnds.1 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) β β) |
39 | 38 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β β (πΉβπ) β β) |
40 | | 2nn 12233 |
. . . . . . . . 9
β’ 2 β
β |
41 | 40 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β
β) |
42 | 37, 39, 41 | rspcdva 3585 |
. . . . . . 7
β’ (π β (πΉβ2) β β) |
43 | 29 | eleq1d 2823 |
. . . . . . . 8
β’ (π = 1 β ((πΉβπ) β β β (πΉβ1) β β)) |
44 | 43, 39, 34 | rspcdva 3585 |
. . . . . . 7
β’ (π β (πΉβ1) β β) |
45 | 42, 44 | addge02d 11751 |
. . . . . 6
β’ (π β (0 β€ (πΉβ1) β (πΉβ2) β€ ((πΉβ1) + (πΉβ2)))) |
46 | 35, 45 | mpbid 231 |
. . . . 5
β’ (π β (πΉβ2) β€ ((πΉβ1) + (πΉβ2))) |
47 | 44, 42 | readdcld 11191 |
. . . . . 6
β’ (π β ((πΉβ1) + (πΉβ2)) β β) |
48 | 41 | nnrpd 12962 |
. . . . . 6
β’ (π β 2 β
β+) |
49 | 42, 47, 48 | lemul2d 13008 |
. . . . 5
β’ (π β ((πΉβ2) β€ ((πΉβ1) + (πΉβ2)) β (2 Β· (πΉβ2)) β€ (2 Β·
((πΉβ1) + (πΉβ2))))) |
50 | 46, 49 | mpbid 231 |
. . . 4
β’ (π β (2 Β· (πΉβ2)) β€ (2 Β·
((πΉβ1) + (πΉβ2)))) |
51 | | 1z 12540 |
. . . . 5
β’ 1 β
β€ |
52 | | fveq2 6847 |
. . . . . . 7
β’ (π = 1 β (πΊβπ) = (πΊβ1)) |
53 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = 1 β (2βπ) = (2β1)) |
54 | 53, 5 | eqtrdi 2793 |
. . . . . . . 8
β’ (π = 1 β (2βπ) = 2) |
55 | 54 | fveq2d 6851 |
. . . . . . . 8
β’ (π = 1 β (πΉβ(2βπ)) = (πΉβ2)) |
56 | 54, 55 | oveq12d 7380 |
. . . . . . 7
β’ (π = 1 β ((2βπ) Β· (πΉβ(2βπ))) = (2 Β· (πΉβ2))) |
57 | 52, 56 | eqeq12d 2753 |
. . . . . 6
β’ (π = 1 β ((πΊβπ) = ((2βπ) Β· (πΉβ(2βπ))) β (πΊβ1) = (2 Β· (πΉβ2)))) |
58 | | climcnds.4 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) |
59 | 58 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β β0 (πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) |
60 | | 1nn0 12436 |
. . . . . . 7
β’ 1 β
β0 |
61 | 60 | a1i 11 |
. . . . . 6
β’ (π β 1 β
β0) |
62 | 57, 59, 61 | rspcdva 3585 |
. . . . 5
β’ (π β (πΊβ1) = (2 Β· (πΉβ2))) |
63 | 51, 62 | seq1i 13927 |
. . . 4
β’ (π β (seq1( + , πΊ)β1) = (2 Β· (πΉβ2))) |
64 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
65 | | df-2 12223 |
. . . . . 6
β’ 2 = (1 +
1) |
66 | | eqidd 2738 |
. . . . . . 7
β’ (π β (πΉβ1) = (πΉβ1)) |
67 | 51, 66 | seq1i 13927 |
. . . . . 6
β’ (π β (seq1( + , πΉ)β1) = (πΉβ1)) |
68 | | eqidd 2738 |
. . . . . 6
β’ (π β (πΉβ2) = (πΉβ2)) |
69 | 64, 34, 65, 67, 68 | seqp1d 13930 |
. . . . 5
β’ (π β (seq1( + , πΉ)β2) = ((πΉβ1) + (πΉβ2))) |
70 | 69 | oveq2d 7378 |
. . . 4
β’ (π β (2 Β· (seq1( + ,
πΉ)β2)) = (2 Β·
((πΉβ1) + (πΉβ2)))) |
71 | 50, 63, 70 | 3brtr4d 5142 |
. . 3
β’ (π β (seq1( + , πΊ)β1) β€ (2 Β·
(seq1( + , πΉ)β2))) |
72 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πΊβπ) = (πΊβ(π + 1))) |
73 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (2βπ) = (2β(π + 1))) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (πΉβ(2βπ)) = (πΉβ(2β(π + 1)))) |
75 | 73, 74 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((2βπ) Β· (πΉβ(2βπ))) = ((2β(π + 1)) Β· (πΉβ(2β(π + 1))))) |
76 | 72, 75 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πΊβπ) = ((2βπ) Β· (πΉβ(2βπ))) β (πΊβ(π + 1)) = ((2β(π + 1)) Β· (πΉβ(2β(π + 1)))))) |
77 | 59 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β βπ β β0
(πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) |
78 | | peano2nn 12172 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
79 | 78 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π + 1) β β) |
80 | 79 | nnnn0d 12480 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π + 1) β
β0) |
81 | 76, 77, 80 | rspcdva 3585 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΊβ(π + 1)) = ((2β(π + 1)) Β· (πΉβ(2β(π + 1))))) |
82 | | nnnn0 12427 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
83 | 82 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β0) |
84 | | expp1 13981 |
. . . . . . . . . . . 12
β’ ((2
β β β§ π
β β0) β (2β(π + 1)) = ((2βπ) Β· 2)) |
85 | 3, 83, 84 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (2β(π + 1)) = ((2βπ) Β· 2)) |
86 | | nnexpcl 13987 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
87 | 40, 82, 86 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β β β
(2βπ) β
β) |
88 | 87 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (2βπ) β
β) |
89 | 88 | nncnd 12176 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (2βπ) β
β) |
90 | | mulcom 11144 |
. . . . . . . . . . . 12
β’
(((2βπ) β
β β§ 2 β β) β ((2βπ) Β· 2) = (2 Β· (2βπ))) |
91 | 89, 3, 90 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((2βπ) Β· 2) = (2 Β·
(2βπ))) |
92 | 85, 91 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (2β(π + 1)) = (2 Β·
(2βπ))) |
93 | 92 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((2β(π + 1)) Β· (πΉβ(2β(π + 1)))) = ((2 Β·
(2βπ)) Β· (πΉβ(2β(π + 1))))) |
94 | 3 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 2 β
β) |
95 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = (2β(π + 1)) β (πΉβπ) = (πΉβ(2β(π + 1)))) |
96 | 95 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ (π = (2β(π + 1)) β ((πΉβπ) β β β (πΉβ(2β(π + 1))) β β)) |
97 | 39 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β βπ β β (πΉβπ) β β) |
98 | | nnexpcl 13987 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ (π +
1) β β0) β (2β(π + 1)) β β) |
99 | 40, 80, 98 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (2β(π + 1)) β
β) |
100 | 96, 97, 99 | rspcdva 3585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβ(2β(π + 1))) β β) |
101 | 100 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβ(2β(π + 1))) β β) |
102 | 94, 89, 101 | mulassd 11185 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((2 Β·
(2βπ)) Β· (πΉβ(2β(π + 1)))) = (2 Β·
((2βπ) Β· (πΉβ(2β(π + 1)))))) |
103 | 81, 93, 102 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβ(π + 1)) = (2 Β· ((2βπ) Β· (πΉβ(2β(π + 1)))))) |
104 | 88 | nnnn0d 12480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (2βπ) β
β0) |
105 | | hashfz1 14253 |
. . . . . . . . . . . . . . 15
β’
((2βπ) β
β0 β (β―β(1...(2βπ))) = (2βπ)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(β―β(1...(2βπ))) = (2βπ)) |
107 | 106, 89 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β
(β―β(1...(2βπ))) β β) |
108 | | fzfid 13885 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (((2βπ) + 1)...(2β(π + 1))) β
Fin) |
109 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’
((((2βπ) +
1)...(2β(π + 1)))
β Fin β (β―β(((2βπ) + 1)...(2β(π + 1)))) β
β0) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(β―β(((2βπ)
+ 1)...(2β(π + 1))))
β β0) |
111 | 110 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β
(β―β(((2βπ)
+ 1)...(2β(π + 1))))
β β) |
112 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π β β) |
113 | 112 | nnzd 12533 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β€) |
114 | | uzid 12785 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β€ β π β
(β€β₯βπ)) |
115 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
116 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β |
117 | | 1le2 12369 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β€
2 |
118 | | leexp2a 14084 |
. . . . . . . . . . . . . . . . . . 19
β’ ((2
β β β§ 1 β€ 2 β§ (π + 1) β
(β€β₯βπ)) β (2βπ) β€ (2β(π + 1))) |
119 | 116, 117,
118 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β
(β€β₯βπ) β (2βπ) β€ (2β(π + 1))) |
120 | 113, 114,
115, 119 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (2βπ) β€ (2β(π + 1))) |
121 | 88, 64 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (2βπ) β
(β€β₯β1)) |
122 | 99 | nnzd 12533 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (2β(π + 1)) β
β€) |
123 | | elfz5 13440 |
. . . . . . . . . . . . . . . . . 18
β’
(((2βπ) β
(β€β₯β1) β§ (2β(π + 1)) β β€) β ((2βπ) β (1...(2β(π + 1))) β (2βπ) β€ (2β(π + 1)))) |
124 | 121, 122,
123 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((2βπ) β (1...(2β(π + 1))) β (2βπ) β€ (2β(π + 1)))) |
125 | 120, 124 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2βπ) β (1...(2β(π + 1)))) |
126 | | fzsplit 13474 |
. . . . . . . . . . . . . . . 16
β’
((2βπ) β
(1...(2β(π + 1)))
β (1...(2β(π +
1))) = ((1...(2βπ))
βͺ (((2βπ) +
1)...(2β(π +
1))))) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (1...(2β(π + 1))) = ((1...(2βπ)) βͺ (((2βπ) + 1)...(2β(π + 1))))) |
128 | 127 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(β―β(1...(2β(π + 1)))) = (β―β((1...(2βπ)) βͺ (((2βπ) + 1)...(2β(π + 1)))))) |
129 | 89 | times2d 12404 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((2βπ) Β· 2) = ((2βπ) + (2βπ))) |
130 | 85, 129 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (2β(π + 1)) = ((2βπ) + (2βπ))) |
131 | 99 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2β(π + 1)) β
β0) |
132 | | hashfz1 14253 |
. . . . . . . . . . . . . . . 16
β’
((2β(π + 1))
β β0 β (β―β(1...(2β(π + 1)))) = (2β(π + 1))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β
(β―β(1...(2β(π + 1)))) = (2β(π + 1))) |
134 | 106 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β
((β―β(1...(2βπ))) + (2βπ)) = ((2βπ) + (2βπ))) |
135 | 130, 133,
134 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(β―β(1...(2β(π + 1)))) = ((β―β(1...(2βπ))) + (2βπ))) |
136 | | fzfid 13885 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (1...(2βπ)) β Fin) |
137 | 88 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (2βπ) β
β) |
138 | 137 | ltp1d 12092 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2βπ) < ((2βπ) + 1)) |
139 | | fzdisj 13475 |
. . . . . . . . . . . . . . . 16
β’
((2βπ) <
((2βπ) + 1) β
((1...(2βπ)) β©
(((2βπ) +
1)...(2β(π + 1)))) =
β
) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((1...(2βπ)) β© (((2βπ) + 1)...(2β(π + 1)))) =
β
) |
141 | | hashun 14289 |
. . . . . . . . . . . . . . 15
β’
(((1...(2βπ))
β Fin β§ (((2βπ) + 1)...(2β(π + 1))) β Fin β§ ((1...(2βπ)) β© (((2βπ) + 1)...(2β(π + 1)))) = β
) β
(β―β((1...(2βπ)) βͺ (((2βπ) + 1)...(2β(π + 1))))) =
((β―β(1...(2βπ))) + (β―β(((2βπ) + 1)...(2β(π + 1)))))) |
142 | 136, 108,
140, 141 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β
(β―β((1...(2βπ)) βͺ (((2βπ) + 1)...(2β(π + 1))))) =
((β―β(1...(2βπ))) + (β―β(((2βπ) + 1)...(2β(π + 1)))))) |
143 | 128, 135,
142 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β
((β―β(1...(2βπ))) + (2βπ)) = ((β―β(1...(2βπ))) +
(β―β(((2βπ)
+ 1)...(2β(π +
1)))))) |
144 | 107, 89, 111, 143 | addcanad 11367 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (2βπ) =
(β―β(((2βπ)
+ 1)...(2β(π +
1))))) |
145 | 144 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((2βπ) Β· (πΉβ(2β(π + 1)))) = ((β―β(((2βπ) + 1)...(2β(π + 1)))) Β· (πΉβ(2β(π + 1))))) |
146 | | fsumconst 15682 |
. . . . . . . . . . . 12
β’
(((((2βπ) +
1)...(2β(π + 1)))
β Fin β§ (πΉβ(2β(π + 1))) β β) β Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβ(2β(π + 1))) = ((β―β(((2βπ) + 1)...(2β(π + 1)))) Β· (πΉβ(2β(π + 1))))) |
147 | 108, 101,
146 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβ(2β(π + 1))) = ((β―β(((2βπ) + 1)...(2β(π + 1)))) Β· (πΉβ(2β(π + 1))))) |
148 | 145, 147 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((2βπ) Β· (πΉβ(2β(π + 1)))) = Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβ(2β(π + 1)))) |
149 | 100 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (πΉβ(2β(π + 1))) β β) |
150 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π) |
151 | | peano2nn 12172 |
. . . . . . . . . . . . . 14
β’
((2βπ) β
β β ((2βπ)
+ 1) β β) |
152 | 88, 151 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((2βπ) + 1) β
β) |
153 | | elfzuz 13444 |
. . . . . . . . . . . . 13
β’ (π β (((2βπ) + 1)...(2β(π + 1))) β π β
(β€β₯β((2βπ) + 1))) |
154 | | eluznn 12850 |
. . . . . . . . . . . . 13
β’
((((2βπ) + 1)
β β β§ π
β (β€β₯β((2βπ) + 1))) β π β β) |
155 | 152, 153,
154 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β π β β) |
156 | 150, 155,
38 | syl2an2r 684 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (πΉβπ) β β) |
157 | | elfzuz3 13445 |
. . . . . . . . . . . . . . 15
β’ (π β (((2βπ) + 1)...(2β(π + 1))) β (2β(π + 1)) β
(β€β₯βπ)) |
158 | 157 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (2β(π + 1)) β
(β€β₯βπ)) |
159 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...(2β(π + 1)))) β π) |
160 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((2βπ) + 1)...(2β(π + 1))) β π β
(β€β₯β((2βπ) + 1))) |
161 | | eluznn 12850 |
. . . . . . . . . . . . . . . . 17
β’
((((2βπ) + 1)
β β β§ π
β (β€β₯β((2βπ) + 1))) β π β β) |
162 | 152, 160,
161 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β π β β) |
163 | | elfzuz 13444 |
. . . . . . . . . . . . . . . 16
β’ (π β (π...(2β(π + 1))) β π β (β€β₯βπ)) |
164 | | eluznn 12850 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
165 | 162, 163,
164 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...(2β(π + 1)))) β π β β) |
166 | 159, 165,
38 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...(2β(π + 1)))) β (πΉβπ) β β) |
167 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...((2β(π + 1)) β 1))) β π) |
168 | | elfzuz 13444 |
. . . . . . . . . . . . . . . 16
β’ (π β (π...((2β(π + 1)) β 1)) β π β (β€β₯βπ)) |
169 | 162, 168,
164 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...((2β(π + 1)) β 1))) β π β β) |
170 | | climcnds.3 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβ(π + 1)) β€ (πΉβπ)) |
171 | 167, 169,
170 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β§ π β (π...((2β(π + 1)) β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
172 | 158, 166,
171 | monoord2 13946 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (πΉβ(2β(π + 1))) β€ (πΉβπ)) |
173 | 172 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β βπ β (((2βπ) + 1)...(2β(π + 1)))(πΉβ(2β(π + 1))) β€ (πΉβπ)) |
174 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
175 | 174 | breq2d 5122 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβ(2β(π + 1))) β€ (πΉβπ) β (πΉβ(2β(π + 1))) β€ (πΉβπ))) |
176 | 175 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ β
(((2βπ) +
1)...(2β(π +
1)))(πΉβ(2β(π + 1))) β€ (πΉβπ) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (πΉβ(2β(π + 1))) β€ (πΉβπ)) |
177 | 173, 176 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (((2βπ) + 1)...(2β(π + 1)))) β (πΉβ(2β(π + 1))) β€ (πΉβπ)) |
178 | 108, 149,
156, 177 | fsumle 15691 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβ(2β(π + 1))) β€ Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)) |
179 | 148, 178 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((2βπ) Β· (πΉβ(2β(π + 1)))) β€ Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)) |
180 | 137, 100 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((2βπ) Β· (πΉβ(2β(π + 1)))) β β) |
181 | 108, 156 | fsumrecl 15626 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ) β β) |
182 | | 2rp 12927 |
. . . . . . . . . . 11
β’ 2 β
β+ |
183 | 182 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 2 β
β+) |
184 | 180, 181,
183 | lemul2d 13008 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((2βπ) Β· (πΉβ(2β(π + 1)))) β€ Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ) β (2 Β· ((2βπ) Β· (πΉβ(2β(π + 1))))) β€ (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)))) |
185 | 179, 184 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β (2 Β·
((2βπ) Β· (πΉβ(2β(π + 1))))) β€ (2 Β·
Ξ£π β
(((2βπ) +
1)...(2β(π +
1)))(πΉβπ))) |
186 | 103, 185 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ π β β) β (πΊβ(π + 1)) β€ (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) |
187 | | 1zzd 12541 |
. . . . . . . . . 10
β’ (π β 1 β
β€) |
188 | | nnnn0 12427 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
189 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β0) |
190 | | nnexpcl 13987 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
191 | 40, 189, 190 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
(2βπ) β
β) |
192 | 191 | nnred 12175 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
(2βπ) β
β) |
193 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = (2βπ) β (πΉβπ) = (πΉβ(2βπ))) |
194 | 193 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = (2βπ) β ((πΉβπ) β β β (πΉβ(2βπ)) β β)) |
195 | 39 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
βπ β β
(πΉβπ) β β) |
196 | 194, 195,
191 | rspcdva 3585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (πΉβ(2βπ)) β
β) |
197 | 192, 196 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β
((2βπ) Β· (πΉβ(2βπ))) β
β) |
198 | 58, 197 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πΊβπ) β β) |
199 | 188, 198 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΊβπ) β β) |
200 | 64, 187, 199 | serfre 13944 |
. . . . . . . . 9
β’ (π β seq1( + , πΊ):ββΆβ) |
201 | 200 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β β) β (seq1( + , πΊ)βπ) β β) |
202 | 72 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = (π + 1) β ((πΊβπ) β β β (πΊβ(π + 1)) β β)) |
203 | 199 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ β β (πΊβπ) β β) |
204 | 203 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β βπ β β (πΊβπ) β β) |
205 | 202, 204,
79 | rspcdva 3585 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβ(π + 1)) β β) |
206 | 64, 187, 38 | serfre 13944 |
. . . . . . . . . 10
β’ (π β seq1( + , πΉ):ββΆβ) |
207 | | ffvelcdm 7037 |
. . . . . . . . . 10
β’ ((seq1( +
, πΉ):ββΆβ
β§ (2βπ) β
β) β (seq1( + , πΉ)β(2βπ)) β β) |
208 | 206, 87, 207 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β β) β (seq1( + , πΉ)β(2βπ)) β
β) |
209 | | remulcl 11143 |
. . . . . . . . 9
β’ ((2
β β β§ (seq1( + , πΉ)β(2βπ)) β β) β (2 Β· (seq1(
+ , πΉ)β(2βπ))) β
β) |
210 | 116, 208,
209 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π β β) β (2 Β· (seq1( +
, πΉ)β(2βπ))) β
β) |
211 | | remulcl 11143 |
. . . . . . . . 9
β’ ((2
β β β§ Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ) β β) β (2 Β·
Ξ£π β
(((2βπ) +
1)...(2β(π +
1)))(πΉβπ)) β
β) |
212 | 116, 181,
211 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π β β) β (2 Β·
Ξ£π β
(((2βπ) +
1)...(2β(π +
1)))(πΉβπ)) β
β) |
213 | | le2add 11644 |
. . . . . . . 8
β’ ((((seq1(
+ , πΊ)βπ) β β β§ (πΊβ(π + 1)) β β) β§ ((2 Β·
(seq1( + , πΉ)β(2βπ))) β β β§ (2 Β·
Ξ£π β
(((2βπ) +
1)...(2β(π +
1)))(πΉβπ)) β β)) β
(((seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + ,
πΉ)β(2βπ))) β§ (πΊβ(π + 1)) β€ (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) β ((seq1( + , πΊ)βπ) + (πΊβ(π + 1))) β€ ((2 Β· (seq1( + , πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))))) |
214 | 201, 205,
210, 212, 213 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ π β β) β (((seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))) β§ (πΊβ(π + 1)) β€ (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) β ((seq1( + , πΊ)βπ) + (πΊβ(π + 1))) β€ ((2 Β· (seq1( + , πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))))) |
215 | 186, 214 | mpan2d 693 |
. . . . . 6
β’ ((π β§ π β β) β ((seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))) β ((seq1( + , πΊ)βπ) + (πΊβ(π + 1))) β€ ((2 Β· (seq1( + , πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))))) |
216 | 112, 64 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
217 | | seqp1 13928 |
. . . . . . . 8
β’ (π β
(β€β₯β1) β (seq1( + , πΊ)β(π + 1)) = ((seq1( + , πΊ)βπ) + (πΊβ(π + 1)))) |
218 | 216, 217 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (seq1( + , πΊ)β(π + 1)) = ((seq1( + , πΊ)βπ) + (πΊβ(π + 1)))) |
219 | | fzfid 13885 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (1...(2β(π + 1))) β
Fin) |
220 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β (1...(2β(π + 1))) β π β
β) |
221 | 38 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβπ) β β) |
222 | 150, 220,
221 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...(2β(π + 1)))) β (πΉβπ) β β) |
223 | 140, 127,
219, 222 | fsumsplit 15633 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Ξ£π β (1...(2β(π + 1)))(πΉβπ) = (Ξ£π β (1...(2βπ))(πΉβπ) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) |
224 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...(2β(π + 1)))) β (πΉβπ) = (πΉβπ)) |
225 | 99, 64 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (2β(π + 1)) β
(β€β₯β1)) |
226 | 224, 225,
222 | fsumser 15622 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Ξ£π β (1...(2β(π + 1)))(πΉβπ) = (seq1( + , πΉ)β(2β(π + 1)))) |
227 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...(2βπ))) β (πΉβπ) = (πΉβπ)) |
228 | | elfznn 13477 |
. . . . . . . . . . . . 13
β’ (π β (1...(2βπ)) β π β β) |
229 | 150, 228,
221 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...(2βπ))) β (πΉβπ) β β) |
230 | 227, 121,
229 | fsumser 15622 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β Ξ£π β (1...(2βπ))(πΉβπ) = (seq1( + , πΉ)β(2βπ))) |
231 | 230 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (Ξ£π β (1...(2βπ))(πΉβπ) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)) = ((seq1( + , πΉ)β(2βπ)) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) |
232 | 223, 226,
231 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ ((π β§ π β β) β (seq1( + , πΉ)β(2β(π + 1))) = ((seq1( + , πΉ)β(2βπ)) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) |
233 | 232 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ π β β) β (2 Β· (seq1( +
, πΉ)β(2β(π + 1)))) = (2 Β· ((seq1( +
, πΉ)β(2βπ)) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)))) |
234 | 208 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β β) β (seq1( + , πΉ)β(2βπ)) β
β) |
235 | 181 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ) β β) |
236 | 94, 234, 235 | adddid 11186 |
. . . . . . . 8
β’ ((π β§ π β β) β (2 Β· ((seq1( +
, πΉ)β(2βπ)) + Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))) = ((2 Β· (seq1( + , πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)))) |
237 | 233, 236 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π β β) β (2 Β· (seq1( +
, πΉ)β(2β(π + 1)))) = ((2 Β· (seq1( +
, πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ)))) |
238 | 218, 237 | breq12d 5123 |
. . . . . 6
β’ ((π β§ π β β) β ((seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1)))) β ((seq1( + ,
πΊ)βπ) + (πΊβ(π + 1))) β€ ((2 Β· (seq1( + , πΉ)β(2βπ))) + (2 Β· Ξ£π β (((2βπ) + 1)...(2β(π + 1)))(πΉβπ))))) |
239 | 215, 238 | sylibrd 259 |
. . . . 5
β’ ((π β§ π β β) β ((seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))) β (seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1)))))) |
240 | 239 | expcom 415 |
. . . 4
β’ (π β β β (π β ((seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))) β (seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1))))))) |
241 | 240 | a2d 29 |
. . 3
β’ (π β β β ((π β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ)))) β (π β (seq1( + , πΊ)β(π + 1)) β€ (2 Β· (seq1( + , πΉ)β(2β(π + 1))))))) |
242 | 10, 16, 22, 28, 71, 241 | nnind 12178 |
. 2
β’ (π β β β (π β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ))))) |
243 | 242 | impcom 409 |
1
β’ ((π β§ π β β) β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ)))) |