Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = 0 β (2 Β· π₯) = (2 Β·
0)) |
2 | | 2t0e0 12327 |
. . . . . . . . . 10
β’ (2
Β· 0) = 0 |
3 | 1, 2 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π₯ = 0 β (2 Β· π₯) = 0) |
4 | 3 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = 0 β (π + (2 Β· π₯)) = (π + 0)) |
5 | 4 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = 0 β (seqπ( + , πΉ)β(π + (2 Β· π₯))) = (seqπ( + , πΉ)β(π + 0))) |
6 | 5 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = 0 β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + 0)))) |
7 | 6 | breq1d 5116 |
. . . . 5
β’ (π₯ = 0 β (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + 0))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
8 | 7 | imbi2d 341 |
. . . 4
β’ (π₯ = 0 β (((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + 0))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
9 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = π β (2 Β· π₯) = (2 Β· π)) |
10 | 9 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = π β (π + (2 Β· π₯)) = (π + (2 Β· π))) |
11 | 10 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (seqπ( + , πΉ)β(π + (2 Β· π₯))) = (seqπ( + , πΉ)β(π + (2 Β· π)))) |
12 | 11 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = π β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π))))) |
13 | 12 | breq1d 5116 |
. . . . 5
β’ (π₯ = π β (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
14 | 13 | imbi2d 341 |
. . . 4
β’ (π₯ = π β (((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
15 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (2 Β· π₯) = (2 Β· (π + 1))) |
16 | 15 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (π + (2 Β· π₯)) = (π + (2 Β· (π + 1)))) |
17 | 16 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = (π + 1) β (seqπ( + , πΉ)β(π + (2 Β· π₯))) = (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) |
18 | 17 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = (π + 1) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1)))))) |
19 | 18 | breq1d 5116 |
. . . . 5
β’ (π₯ = (π + 1) β (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
20 | 19 | imbi2d 341 |
. . . 4
β’ (π₯ = (π + 1) β (((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
21 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = πΎ β (2 Β· π₯) = (2 Β· πΎ)) |
22 | 21 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = πΎ β (π + (2 Β· π₯)) = (π + (2 Β· πΎ))) |
23 | 22 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = πΎ β (seqπ( + , πΉ)β(π + (2 Β· π₯))) = (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) |
24 | 23 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = πΎ β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ))))) |
25 | 24 | breq1d 5116 |
. . . . 5
β’ (π₯ = πΎ β (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
26 | 25 | imbi2d 341 |
. . . 4
β’ (π₯ = πΎ β (((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π₯)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
27 | | iseralt.1 |
. . . . . . . . . . . 12
β’ π =
(β€β₯βπ) |
28 | | uzssz 12789 |
. . . . . . . . . . . 12
β’
(β€β₯βπ) β β€ |
29 | 27, 28 | eqsstri 3979 |
. . . . . . . . . . 11
β’ π β
β€ |
30 | 29 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β β€) |
31 | 30 | sselda 3945 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β β€) |
32 | 31 | zcnd 12613 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β) |
33 | 32 | addid1d 11360 |
. . . . . . 7
β’ ((π β§ π β π) β (π + 0) = π) |
34 | 33 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π β π) β (seqπ( + , πΉ)β(π + 0)) = (seqπ( + , πΉ)βπ)) |
35 | 34 | oveq2d 7374 |
. . . . 5
β’ ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + 0))) = ((-1βπ) Β· (seqπ( + , πΉ)βπ))) |
36 | | neg1rr 12273 |
. . . . . . . 8
β’ -1 β
β |
37 | | neg1ne0 12274 |
. . . . . . . 8
β’ -1 β
0 |
38 | | reexpclz 13994 |
. . . . . . . 8
β’ ((-1
β β β§ -1 β 0 β§ π β β€) β (-1βπ) β
β) |
39 | 36, 37, 31, 38 | mp3an12i 1466 |
. . . . . . 7
β’ ((π β§ π β π) β (-1βπ) β β) |
40 | | iseralt.2 |
. . . . . . . . 9
β’ (π β π β β€) |
41 | | iseralt.6 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) |
42 | 30 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β β€) |
43 | | reexpclz 13994 |
. . . . . . . . . . . 12
β’ ((-1
β β β§ -1 β 0 β§ π β β€) β (-1βπ) β
β) |
44 | 36, 37, 42, 43 | mp3an12i 1466 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (-1βπ) β β) |
45 | | iseralt.3 |
. . . . . . . . . . . 12
β’ (π β πΊ:πβΆβ) |
46 | 45 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΊβπ) β β) |
47 | 44, 46 | remulcld 11190 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((-1βπ) Β· (πΊβπ)) β β) |
48 | 41, 47 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β β) |
49 | 27, 40, 48 | serfre 13943 |
. . . . . . . 8
β’ (π β seqπ( + , πΉ):πβΆβ) |
50 | 49 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
51 | 39, 50 | remulcld 11190 |
. . . . . 6
β’ ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β β) |
52 | 51 | leidd 11726 |
. . . . 5
β’ ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) |
53 | 35, 52 | eqbrtrd 5128 |
. . . 4
β’ ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + 0))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) |
54 | 45 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β πΊ:πβΆβ) |
55 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
56 | 55 | 2timesi 12296 |
. . . . . . . . . . . . . . 15
β’ (2
Β· 1) = (1 + 1) |
57 | 56 | oveq2i 7369 |
. . . . . . . . . . . . . 14
β’ ((π + (2 Β· π)) + (2 Β· 1)) = ((π + (2 Β· π)) + (1 + 1)) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β π β π) |
59 | 58, 27 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β π β
(β€β₯βπ)) |
61 | | eluzelz 12778 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ) β π β β€) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β π β
β€) |
63 | 62 | zcnd 12613 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β π β
β) |
64 | | 2cn 12233 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
65 | | nn0cn 12428 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
66 | 65 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β π β
β) |
67 | | mulcl 11140 |
. . . . . . . . . . . . . . . 16
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
68 | 64, 66, 67 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (2
Β· π) β
β) |
69 | 64, 55 | mulcli 11167 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· 1) β β |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (2
Β· 1) β β) |
71 | 63, 68, 70 | addassd 11182 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β ((π + (2 Β· π)) + (2 Β· 1)) = (π + ((2 Β· π) + (2 Β·
1)))) |
72 | 57, 71 | eqtr3id 2787 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β ((π + (2 Β· π)) + (1 + 1)) = (π + ((2 Β· π) + (2 Β·
1)))) |
73 | | 2nn0 12435 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β0 |
74 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β π β
β0) |
75 | | nn0mulcl 12454 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
76 | 73, 74, 75 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β (2
Β· π) β
β0) |
77 | | uzaddcl 12834 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯βπ) β§ (2 Β· π) β β0) β (π + (2 Β· π)) β
(β€β₯βπ)) |
78 | 60, 76, 77 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· π)) β
(β€β₯βπ)) |
79 | 28, 78 | sselid 3943 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· π)) β
β€) |
80 | 79 | zcnd 12613 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· π)) β
β) |
81 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β 1 β
β) |
82 | 80, 81, 81 | addassd 11182 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (((π + (2 Β· π)) + 1) + 1) = ((π + (2 Β· π)) + (1 + 1))) |
83 | | 2cnd 12236 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β 2 β
β) |
84 | 83, 66, 81 | adddid 11184 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β (2
Β· (π + 1)) = ((2
Β· π) + (2 Β·
1))) |
85 | 84 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· (π + 1))) = (π + ((2 Β· π) + (2 Β· 1)))) |
86 | 72, 82, 85 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (((π + (2 Β· π)) + 1) + 1) = (π + (2 Β· (π + 1)))) |
87 | | peano2nn0 12458 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
88 | 87 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (π + 1) β
β0) |
89 | | nn0mulcl 12454 |
. . . . . . . . . . . . . . 15
β’ ((2
β β0 β§ (π + 1) β β0) β (2
Β· (π + 1)) β
β0) |
90 | 73, 88, 89 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β (2
Β· (π + 1)) β
β0) |
91 | | uzaddcl 12834 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯βπ) β§ (2 Β· (π + 1)) β β0) β
(π + (2 Β· (π + 1))) β
(β€β₯βπ)) |
92 | 60, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· (π + 1))) β
(β€β₯βπ)) |
93 | 92, 27 | eleqtrrdi 2845 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· (π + 1))) β π) |
94 | 86, 93 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β (((π + (2 Β· π)) + 1) + 1) β π) |
95 | 54, 94 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (πΊβ(((π + (2 Β· π)) + 1) + 1)) β
β) |
96 | | peano2uz 12831 |
. . . . . . . . . . . . 13
β’ ((π + (2 Β· π)) β
(β€β₯βπ) β ((π + (2 Β· π)) + 1) β
(β€β₯βπ)) |
97 | 78, 96 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β ((π + (2 Β· π)) + 1) β
(β€β₯βπ)) |
98 | 97, 27 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β ((π + (2 Β· π)) + 1) β π) |
99 | 54, 98 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (πΊβ((π + (2 Β· π)) + 1)) β β) |
100 | 95, 99 | resubcld 11588 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1))) β β) |
101 | | 0red 11163 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β 0 β
β) |
102 | 39 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β
(-1βπ) β
β) |
103 | 49 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β seqπ( + , πΉ):πβΆβ) |
104 | 78, 27 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β (π + (2 Β· π)) β π) |
105 | 103, 104 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(π + (2 Β· π))) β β) |
106 | 102, 105 | remulcld 11190 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) β β) |
107 | | fvoveq1 7381 |
. . . . . . . . . . . 12
β’ (π = ((π + (2 Β· π)) + 1) β (πΊβ(π + 1)) = (πΊβ(((π + (2 Β· π)) + 1) + 1))) |
108 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = ((π + (2 Β· π)) + 1) β (πΊβπ) = (πΊβ((π + (2 Β· π)) + 1))) |
109 | 107, 108 | breq12d 5119 |
. . . . . . . . . . 11
β’ (π = ((π + (2 Β· π)) + 1) β ((πΊβ(π + 1)) β€ (πΊβπ) β (πΊβ(((π + (2 Β· π)) + 1) + 1)) β€ (πΊβ((π + (2 Β· π)) + 1)))) |
110 | | iseralt.4 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) |
111 | 110 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β βπ β π (πΊβ(π + 1)) β€ (πΊβπ)) |
112 | 111 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β
βπ β π (πΊβ(π + 1)) β€ (πΊβπ)) |
113 | 109, 112,
98 | rspcdva 3581 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (πΊβ(((π + (2 Β· π)) + 1) + 1)) β€ (πΊβ((π + (2 Β· π)) + 1))) |
114 | 95, 99 | suble0d 11751 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1))) β€ 0 β (πΊβ(((π + (2 Β· π)) + 1) + 1)) β€ (πΊβ((π + (2 Β· π)) + 1)))) |
115 | 113, 114 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1))) β€ 0) |
116 | 100, 101,
106, 115 | leadd2dd 11775 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) + ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1)))) β€ (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) + 0)) |
117 | | seqp1 13927 |
. . . . . . . . . . . . 13
β’ (((π + (2 Β· π)) + 1) β
(β€β₯βπ) β (seqπ( + , πΉ)β(((π + (2 Β· π)) + 1) + 1)) = ((seqπ( + , πΉ)β((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) |
118 | 97, 117 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(((π + (2 Β· π)) + 1) + 1)) = ((seqπ( + , πΉ)β((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) |
119 | | seqp1 13927 |
. . . . . . . . . . . . . 14
β’ ((π + (2 Β· π)) β
(β€β₯βπ) β (seqπ( + , πΉ)β((π + (2 Β· π)) + 1)) = ((seqπ( + , πΉ)β(π + (2 Β· π))) + (πΉβ((π + (2 Β· π)) + 1)))) |
120 | 78, 119 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β((π + (2 Β· π)) + 1)) = ((seqπ( + , πΉ)β(π + (2 Β· π))) + (πΉβ((π + (2 Β· π)) + 1)))) |
121 | 120 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β
((seqπ( + , πΉ)β((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))) = (((seqπ( + , πΉ)β(π + (2 Β· π))) + (πΉβ((π + (2 Β· π)) + 1))) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) |
122 | 118, 121 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(((π + (2 Β· π)) + 1) + 1)) = (((seqπ( + , πΉ)β(π + (2 Β· π))) + (πΉβ((π + (2 Β· π)) + 1))) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) |
123 | 86 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(((π + (2 Β· π)) + 1) + 1)) = (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) |
124 | 105 | recnd 11188 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(π + (2 Β· π))) β β) |
125 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((π + (2 Β· π)) + 1) β (πΉβπ) = (πΉβ((π + (2 Β· π)) + 1))) |
126 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((π + (2 Β· π)) + 1) β (-1βπ) = (-1β((π + (2 Β· π)) + 1))) |
127 | 126, 108 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((π + (2 Β· π)) + 1) β ((-1βπ) Β· (πΊβπ)) = ((-1β((π + (2 Β· π)) + 1)) Β· (πΊβ((π + (2 Β· π)) + 1)))) |
128 | 125, 127 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π = ((π + (2 Β· π)) + 1) β ((πΉβπ) = ((-1βπ) Β· (πΊβπ)) β (πΉβ((π + (2 Β· π)) + 1)) = ((-1β((π + (2 Β· π)) + 1)) Β· (πΊβ((π + (2 Β· π)) + 1))))) |
129 | 41 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β π (πΉβπ) = ((-1βπ) Β· (πΊβπ))) |
130 | 129 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β
βπ β π (πΉβπ) = ((-1βπ) Β· (πΊβπ))) |
131 | 128, 130,
98 | rspcdva 3581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (πΉβ((π + (2 Β· π)) + 1)) = ((-1β((π + (2 Β· π)) + 1)) Β· (πΊβ((π + (2 Β· π)) + 1)))) |
132 | | neg1cn 12272 |
. . . . . . . . . . . . . . . . . . 19
β’ -1 β
β |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β -1 β
β) |
134 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β -1 β
0) |
135 | 133, 134,
79 | expp1zd 14066 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
(-1β((π + (2 Β·
π)) + 1)) =
((-1β(π + (2 Β·
π))) Β·
-1)) |
136 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π) β§ π β β0) β -1 β
β) |
137 | 136, 134,
79 | reexpclzd 14158 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π) β§ π β β0) β
(-1β(π + (2 Β·
π))) β
β) |
138 | 137 | recnd 11188 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β
(-1β(π + (2 Β·
π))) β
β) |
139 | | mulcom 11142 |
. . . . . . . . . . . . . . . . . 18
β’
(((-1β(π + (2
Β· π))) β
β β§ -1 β β) β ((-1β(π + (2 Β· π))) Β· -1) = (-1 Β·
(-1β(π + (2 Β·
π))))) |
140 | 138, 132,
139 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
((-1β(π + (2 Β·
π))) Β· -1) = (-1
Β· (-1β(π + (2
Β· π))))) |
141 | 138 | mulm1d 11612 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β (-1
Β· (-1β(π + (2
Β· π)))) =
-(-1β(π + (2 Β·
π)))) |
142 | 135, 140,
141 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β
(-1β((π + (2 Β·
π)) + 1)) =
-(-1β(π + (2 Β·
π)))) |
143 | 142 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
((-1β((π + (2 Β·
π)) + 1)) Β· (πΊβ((π + (2 Β· π)) + 1))) = (-(-1β(π + (2 Β· π))) Β· (πΊβ((π + (2 Β· π)) + 1)))) |
144 | 99 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β (πΊβ((π + (2 Β· π)) + 1)) β β) |
145 | | mulneg12 11598 |
. . . . . . . . . . . . . . . 16
β’
(((-1β(π + (2
Β· π))) β
β β§ (πΊβ((π + (2 Β· π)) + 1)) β β) β
(-(-1β(π + (2 Β·
π))) Β· (πΊβ((π + (2 Β· π)) + 1))) = ((-1β(π + (2 Β· π))) Β· -(πΊβ((π + (2 Β· π)) + 1)))) |
146 | 138, 144,
145 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
(-(-1β(π + (2 Β·
π))) Β· (πΊβ((π + (2 Β· π)) + 1))) = ((-1β(π + (2 Β· π))) Β· -(πΊβ((π + (2 Β· π)) + 1)))) |
147 | 131, 143,
146 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β (πΉβ((π + (2 Β· π)) + 1)) = ((-1β(π + (2 Β· π))) Β· -(πΊβ((π + (2 Β· π)) + 1)))) |
148 | 99 | renegcld 11587 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β -(πΊβ((π + (2 Β· π)) + 1)) β β) |
149 | 137, 148 | remulcld 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
((-1β(π + (2 Β·
π))) Β· -(πΊβ((π + (2 Β· π)) + 1))) β β) |
150 | 147, 149 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (πΉβ((π + (2 Β· π)) + 1)) β β) |
151 | 150 | recnd 11188 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (πΉβ((π + (2 Β· π)) + 1)) β β) |
152 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = (((π + (2 Β· π)) + 1) + 1) β (πΉβπ) = (πΉβ(((π + (2 Β· π)) + 1) + 1))) |
153 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (((π + (2 Β· π)) + 1) + 1) β (-1βπ) = (-1β(((π + (2 Β· π)) + 1) + 1))) |
154 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (((π + (2 Β· π)) + 1) + 1) β (πΊβπ) = (πΊβ(((π + (2 Β· π)) + 1) + 1))) |
155 | 153, 154 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π = (((π + (2 Β· π)) + 1) + 1) β ((-1βπ) Β· (πΊβπ)) = ((-1β(((π + (2 Β· π)) + 1) + 1)) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
156 | 152, 155 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π = (((π + (2 Β· π)) + 1) + 1) β ((πΉβπ) = ((-1βπ) Β· (πΊβπ)) β (πΉβ(((π + (2 Β· π)) + 1) + 1)) = ((-1β(((π + (2 Β· π)) + 1) + 1)) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))))) |
157 | 156, 130,
94 | rspcdva 3581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (πΉβ(((π + (2 Β· π)) + 1) + 1)) = ((-1β(((π + (2 Β· π)) + 1) + 1)) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
158 | 79 | peano2zd 12615 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β ((π + (2 Β· π)) + 1) β
β€) |
159 | 133, 134,
158 | expp1zd 14066 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
(-1β(((π + (2 Β·
π)) + 1) + 1)) =
((-1β((π + (2 Β·
π)) + 1)) Β·
-1)) |
160 | 142 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
((-1β((π + (2 Β·
π)) + 1)) Β· -1) =
(-(-1β(π + (2 Β·
π))) Β·
-1)) |
161 | | mul2neg 11599 |
. . . . . . . . . . . . . . . . . . 19
β’
(((-1β(π + (2
Β· π))) β
β β§ 1 β β) β (-(-1β(π + (2 Β· π))) Β· -1) = ((-1β(π + (2 Β· π))) Β·
1)) |
162 | 138, 55, 161 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β
(-(-1β(π + (2 Β·
π))) Β· -1) =
((-1β(π + (2 Β·
π))) Β·
1)) |
163 | 138 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β
((-1β(π + (2 Β·
π))) Β· 1) =
(-1β(π + (2 Β·
π)))) |
164 | 162, 163 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
(-(-1β(π + (2 Β·
π))) Β· -1) =
(-1β(π + (2 Β·
π)))) |
165 | 159, 160,
164 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β
(-1β(((π + (2 Β·
π)) + 1) + 1)) =
(-1β(π + (2 Β·
π)))) |
166 | 165 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
((-1β(((π + (2
Β· π)) + 1) + 1))
Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))) =
((-1β(π + (2 Β·
π))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
167 | 157, 166 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β (πΉβ(((π + (2 Β· π)) + 1) + 1)) = ((-1β(π + (2 Β· π))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
168 | 137, 95 | remulcld 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
((-1β(π + (2 Β·
π))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))) β
β) |
169 | 167, 168 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (πΉβ(((π + (2 Β· π)) + 1) + 1)) β
β) |
170 | 169 | recnd 11188 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (πΉβ(((π + (2 Β· π)) + 1) + 1)) β
β) |
171 | 124, 151,
170 | addassd 11182 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β
(((seqπ( + , πΉ)β(π + (2 Β· π))) + (πΉβ((π + (2 Β· π)) + 1))) + (πΉβ(((π + (2 Β· π)) + 1) + 1))) = ((seqπ( + , πΉ)β(π + (2 Β· π))) + ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))))) |
172 | 122, 123,
171 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(π + (2 Β· (π + 1)))) = ((seqπ( + , πΉ)β(π + (2 Β· π))) + ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))))) |
173 | 172 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) = ((-1βπ) Β· ((seqπ( + , πΉ)β(π + (2 Β· π))) + ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))))) |
174 | 102 | recnd 11188 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β
(-1βπ) β
β) |
175 | 150, 169 | readdcld 11189 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))) β
β) |
176 | 175 | recnd 11188 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))) β
β) |
177 | 174, 124,
176 | adddid 11184 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
((seqπ( + , πΉ)β(π + (2 Β· π))) + ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))))) = (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) + ((-1βπ) Β· ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))))) |
178 | 174, 151,
170 | adddid 11184 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) = (((-1βπ) Β· (πΉβ((π + (2 Β· π)) + 1))) + ((-1βπ) Β· (πΉβ(((π + (2 Β· π)) + 1) + 1))))) |
179 | 147 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ((π + (2 Β· π)) + 1))) = ((-1βπ) Β· ((-1β(π + (2 Β· π))) Β· -(πΊβ((π + (2 Β· π)) + 1))))) |
180 | 148 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β -(πΊβ((π + (2 Β· π)) + 1)) β β) |
181 | 174, 138,
180 | mulassd 11183 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(-1β(π + (2 Β·
π)))) Β· -(πΊβ((π + (2 Β· π)) + 1))) = ((-1βπ) Β· ((-1β(π + (2 Β· π))) Β· -(πΊβ((π + (2 Β· π)) + 1))))) |
182 | 179, 181 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ((π + (2 Β· π)) + 1))) = (((-1βπ) Β· (-1β(π + (2 Β· π)))) Β· -(πΊβ((π + (2 Β· π)) + 1)))) |
183 | 83, 63, 66 | adddid 11184 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β (2
Β· (π + π)) = ((2 Β· π) + (2 Β· π))) |
184 | 63 | 2timesd 12401 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π β β0) β (2
Β· π) = (π + π)) |
185 | 184 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β ((2
Β· π) + (2 Β·
π)) = ((π + π) + (2 Β· π))) |
186 | 63, 63, 68 | addassd 11182 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β ((π + π) + (2 Β· π)) = (π + (π + (2 Β· π)))) |
187 | 183, 185,
186 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β (π + (π + (2 Β· π))) = (2 Β· (π + π))) |
188 | 187 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
(-1β(π + (π + (2 Β· π)))) = (-1β(2 Β·
(π + π)))) |
189 | | expaddz 14018 |
. . . . . . . . . . . . . . . 16
β’ (((-1
β β β§ -1 β 0) β§ (π β β€ β§ (π + (2 Β· π)) β β€)) β (-1β(π + (π + (2 Β· π)))) = ((-1βπ) Β· (-1β(π + (2 Β· π))))) |
190 | 133, 134,
62, 79, 189 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
(-1β(π + (π + (2 Β· π)))) = ((-1βπ) Β· (-1β(π + (2 Β· π))))) |
191 | | 2z 12540 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β€ |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β 2 β
β€) |
193 | | nn0z 12529 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β π β
β€) |
194 | | zaddcl 12548 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β€) β (π + π) β β€) |
195 | 31, 193, 194 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β (π + π) β β€) |
196 | | expmulz 14020 |
. . . . . . . . . . . . . . . . 17
β’ (((-1
β β β§ -1 β 0) β§ (2 β β€ β§ (π + π) β β€)) β (-1β(2
Β· (π + π))) = ((-1β2)β(π + π))) |
197 | 133, 134,
192, 195, 196 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β
(-1β(2 Β· (π +
π))) =
((-1β2)β(π +
π))) |
198 | | neg1sqe1 14106 |
. . . . . . . . . . . . . . . . . 18
β’
(-1β2) = 1 |
199 | 198 | oveq1i 7368 |
. . . . . . . . . . . . . . . . 17
β’
((-1β2)β(π
+ π)) = (1β(π + π)) |
200 | | 1exp 14003 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + π) β β€ β (1β(π + π)) = 1) |
201 | 195, 200 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β β0) β
(1β(π + π)) = 1) |
202 | 199, 201 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β β0) β
((-1β2)β(π +
π)) = 1) |
203 | 197, 202 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β
(-1β(2 Β· (π +
π))) = 1) |
204 | 188, 190,
203 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(-1β(π + (2 Β·
π)))) = 1) |
205 | 204 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(-1β(π + (2 Β·
π)))) Β· -(πΊβ((π + (2 Β· π)) + 1))) = (1 Β· -(πΊβ((π + (2 Β· π)) + 1)))) |
206 | 180 | mulid2d 11178 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (1
Β· -(πΊβ((π + (2 Β· π)) + 1))) = -(πΊβ((π + (2 Β· π)) + 1))) |
207 | 182, 205,
206 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ((π + (2 Β· π)) + 1))) = -(πΊβ((π + (2 Β· π)) + 1))) |
208 | 167 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ(((π + (2 Β· π)) + 1) + 1))) = ((-1βπ) Β· ((-1β(π + (2 Β· π))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))))) |
209 | 95 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β β0) β (πΊβ(((π + (2 Β· π)) + 1) + 1)) β
β) |
210 | 174, 138,
209 | mulassd 11183 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(-1β(π + (2 Β·
π)))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))) = ((-1βπ) Β· ((-1β(π + (2 Β· π))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))))) |
211 | 208, 210 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ(((π + (2 Β· π)) + 1) + 1))) =
(((-1βπ) Β·
(-1β(π + (2 Β·
π)))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
212 | 204 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(-1β(π + (2 Β·
π)))) Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))) = (1 Β· (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
213 | 209 | mulid2d 11178 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β (1
Β· (πΊβ(((π + (2 Β· π)) + 1) + 1))) = (πΊβ(((π + (2 Β· π)) + 1) + 1))) |
214 | 211, 212,
213 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(πΉβ(((π + (2 Β· π)) + 1) + 1))) = (πΊβ(((π + (2 Β· π)) + 1) + 1))) |
215 | 207, 214 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(πΉβ((π + (2 Β· π)) + 1))) + ((-1βπ) Β· (πΉβ(((π + (2 Β· π)) + 1) + 1)))) = (-(πΊβ((π + (2 Β· π)) + 1)) + (πΊβ(((π + (2 Β· π)) + 1) + 1)))) |
216 | 144 | negcld 11504 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β β0) β -(πΊβ((π + (2 Β· π)) + 1)) β β) |
217 | 216, 209 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β (-(πΊβ((π + (2 Β· π)) + 1)) + (πΊβ(((π + (2 Β· π)) + 1) + 1))) = ((πΊβ(((π + (2 Β· π)) + 1) + 1)) + -(πΊβ((π + (2 Β· π)) + 1)))) |
218 | 209, 144 | negsubd 11523 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β β0) β ((πΊβ(((π + (2 Β· π)) + 1) + 1)) + -(πΊβ((π + (2 Β· π)) + 1))) = ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1)))) |
219 | 217, 218 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β β0) β (-(πΊβ((π + (2 Β· π)) + 1)) + (πΊβ(((π + (2 Β· π)) + 1) + 1))) = ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1)))) |
220 | 178, 215,
219 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1)))) = ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1)))) |
221 | 220 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) + ((-1βπ) Β· ((πΉβ((π + (2 Β· π)) + 1)) + (πΉβ(((π + (2 Β· π)) + 1) + 1))))) = (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) + ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1))))) |
222 | 173, 177,
221 | 3eqtrrd 2778 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) + ((πΊβ(((π + (2 Β· π)) + 1) + 1)) β (πΊβ((π + (2 Β· π)) + 1)))) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1)))))) |
223 | 106 | recnd 11188 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) β β) |
224 | 223 | addid1d 11360 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) + 0) = ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π))))) |
225 | 116, 222,
224 | 3brtr3d 5137 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π))))) |
226 | 103, 93 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β0) β (seqπ( + , πΉ)β(π + (2 Β· (π + 1)))) β β) |
227 | 102, 226 | remulcld 11190 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β β) |
228 | 51 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)βπ)) β β) |
229 | | letr 11254 |
. . . . . . . 8
β’
((((-1βπ)
Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β β β§
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) β β β§ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β β) β ((((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β§ ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
230 | 227, 106,
228, 229 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β β0) β
((((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β§ ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
231 | 225, 230 | mpand 694 |
. . . . . 6
β’ (((π β§ π β π) β§ π β β0) β
(((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
232 | 231 | expcom 415 |
. . . . 5
β’ (π β β0
β ((π β§ π β π) β (((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
233 | 232 | a2d 29 |
. . . 4
β’ (π β β0
β (((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· π)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· (π + 1))))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))))) |
234 | 8, 14, 20, 26, 53, 233 | nn0ind 12603 |
. . 3
β’ (πΎ β β0
β ((π β§ π β π) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
235 | 234 | com12 32 |
. 2
β’ ((π β§ π β π) β (πΎ β β0 β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ)))) |
236 | 235 | 3impia 1118 |
1
β’ ((π β§ π β π β§ πΎ β β0) β
((-1βπ) Β·
(seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) |