Step | Hyp | Ref
| Expression |
1 | | ser3ge0.1 |
. . 3
β’ (π β π β (β€β₯βπ)) |
2 | | eluzfz2 10031 |
. . 3
β’ (π β
(β€β₯βπ) β π β (π...π)) |
3 | 1, 2 | syl 14 |
. 2
β’ (π β π β (π...π)) |
4 | | fveq2 5515 |
. . . . 5
β’ (π€ = π β (seqπ( + , πΉ)βπ€) = (seqπ( + , πΉ)βπ)) |
5 | 4 | breq2d 4015 |
. . . 4
β’ (π€ = π β (0 β€ (seqπ( + , πΉ)βπ€) β 0 β€ (seqπ( + , πΉ)βπ))) |
6 | 5 | imbi2d 230 |
. . 3
β’ (π€ = π β ((π β 0 β€ (seqπ( + , πΉ)βπ€)) β (π β 0 β€ (seqπ( + , πΉ)βπ)))) |
7 | | fveq2 5515 |
. . . . 5
β’ (π€ = π β (seqπ( + , πΉ)βπ€) = (seqπ( + , πΉ)βπ)) |
8 | 7 | breq2d 4015 |
. . . 4
β’ (π€ = π β (0 β€ (seqπ( + , πΉ)βπ€) β 0 β€ (seqπ( + , πΉ)βπ))) |
9 | 8 | imbi2d 230 |
. . 3
β’ (π€ = π β ((π β 0 β€ (seqπ( + , πΉ)βπ€)) β (π β 0 β€ (seqπ( + , πΉ)βπ)))) |
10 | | fveq2 5515 |
. . . . 5
β’ (π€ = (π + 1) β (seqπ( + , πΉ)βπ€) = (seqπ( + , πΉ)β(π + 1))) |
11 | 10 | breq2d 4015 |
. . . 4
β’ (π€ = (π + 1) β (0 β€ (seqπ( + , πΉ)βπ€) β 0 β€ (seqπ( + , πΉ)β(π + 1)))) |
12 | 11 | imbi2d 230 |
. . 3
β’ (π€ = (π + 1) β ((π β 0 β€ (seqπ( + , πΉ)βπ€)) β (π β 0 β€ (seqπ( + , πΉ)β(π + 1))))) |
13 | | fveq2 5515 |
. . . . 5
β’ (π€ = π β (seqπ( + , πΉ)βπ€) = (seqπ( + , πΉ)βπ)) |
14 | 13 | breq2d 4015 |
. . . 4
β’ (π€ = π β (0 β€ (seqπ( + , πΉ)βπ€) β 0 β€ (seqπ( + , πΉ)βπ))) |
15 | 14 | imbi2d 230 |
. . 3
β’ (π€ = π β ((π β 0 β€ (seqπ( + , πΉ)βπ€)) β (π β 0 β€ (seqπ( + , πΉ)βπ)))) |
16 | | fveq2 5515 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
17 | 16 | breq2d 4015 |
. . . . . 6
β’ (π = π β (0 β€ (πΉβπ) β 0 β€ (πΉβπ))) |
18 | | ser3ge0.3 |
. . . . . . 7
β’ ((π β§ π β (π...π)) β 0 β€ (πΉβπ)) |
19 | 18 | ralrimiva 2550 |
. . . . . 6
β’ (π β βπ β (π...π)0 β€ (πΉβπ)) |
20 | | eluzfz1 10030 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β (π...π)) |
21 | 1, 20 | syl 14 |
. . . . . 6
β’ (π β π β (π...π)) |
22 | 17, 19, 21 | rspcdva 2846 |
. . . . 5
β’ (π β 0 β€ (πΉβπ)) |
23 | | eluzel2 9532 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
24 | 1, 23 | syl 14 |
. . . . . 6
β’ (π β π β β€) |
25 | | ser3ge0.2 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
26 | | readdcl 7936 |
. . . . . . 7
β’ ((π β β β§ π£ β β) β (π + π£) β β) |
27 | 26 | adantl 277 |
. . . . . 6
β’ ((π β§ (π β β β§ π£ β β)) β (π + π£) β β) |
28 | 24, 25, 27 | seq3-1 10459 |
. . . . 5
β’ (π β (seqπ( + , πΉ)βπ) = (πΉβπ)) |
29 | 22, 28 | breqtrrd 4031 |
. . . 4
β’ (π β 0 β€ (seqπ( + , πΉ)βπ)) |
30 | 29 | a1i 9 |
. . 3
β’ (π β
(β€β₯βπ) β (π β 0 β€ (seqπ( + , πΉ)βπ))) |
31 | | eqid 2177 |
. . . . . . . . . . 11
β’
(β€β₯βπ) = (β€β₯βπ) |
32 | 31, 24, 25, 27 | seqf 10460 |
. . . . . . . . . 10
β’ (π β seqπ( + , πΉ):(β€β₯βπ)βΆβ) |
33 | 32 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β seqπ( + , πΉ):(β€β₯βπ)βΆβ) |
34 | | elfzouz 10150 |
. . . . . . . . . 10
β’ (π β (π..^π) β π β (β€β₯βπ)) |
35 | 34 | ad2antlr 489 |
. . . . . . . . 9
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β π β (β€β₯βπ)) |
36 | 33, 35 | ffvelcdmd 5652 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ) β β) |
37 | | fveq2 5515 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
38 | 37 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πΉβπ) β β β (πΉβ(π + 1)) β β)) |
39 | 25 | ralrimiva 2550 |
. . . . . . . . . . 11
β’ (π β βπ β (β€β₯βπ)(πΉβπ) β β) |
40 | 39 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β βπ β (β€β₯βπ)(πΉβπ) β β) |
41 | | peano2uz 9582 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
42 | 34, 41 | syl 14 |
. . . . . . . . . . 11
β’ (π β (π..^π) β (π + 1) β
(β€β₯βπ)) |
43 | 42 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π + 1) β
(β€β₯βπ)) |
44 | 38, 40, 43 | rspcdva 2846 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (πΉβ(π + 1)) β β) |
45 | 44 | adantr 276 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β (πΉβ(π + 1)) β β) |
46 | | simpr 110 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β 0 β€ (seqπ( + , πΉ)βπ)) |
47 | 37 | breq2d 4015 |
. . . . . . . . 9
β’ (π = (π + 1) β (0 β€ (πΉβπ) β 0 β€ (πΉβ(π + 1)))) |
48 | 19 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β βπ β (π...π)0 β€ (πΉβπ)) |
49 | | fzofzp1 10226 |
. . . . . . . . . 10
β’ (π β (π..^π) β (π + 1) β (π...π)) |
50 | 49 | ad2antlr 489 |
. . . . . . . . 9
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β (π + 1) β (π...π)) |
51 | 47, 48, 50 | rspcdva 2846 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β 0 β€ (πΉβ(π + 1))) |
52 | 36, 45, 46, 51 | addge0d 8478 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β 0 β€ ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) |
53 | 25 | adantlr 477 |
. . . . . . . . 9
β’ (((π β§ π β (π..^π)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
54 | 53 | adantlr 477 |
. . . . . . . 8
β’ ((((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
55 | 26 | adantl 277 |
. . . . . . . 8
β’ ((((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β§ (π β β β§ π£ β β)) β (π + π£) β β) |
56 | 35, 54, 55 | seq3p1 10461 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β (seqπ( + , πΉ)β(π + 1)) = ((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))) |
57 | 52, 56 | breqtrrd 4031 |
. . . . . 6
β’ (((π β§ π β (π..^π)) β§ 0 β€ (seqπ( + , πΉ)βπ)) β 0 β€ (seqπ( + , πΉ)β(π + 1))) |
58 | 57 | ex 115 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (0 β€ (seqπ( + , πΉ)βπ) β 0 β€ (seqπ( + , πΉ)β(π + 1)))) |
59 | 58 | expcom 116 |
. . . 4
β’ (π β (π..^π) β (π β (0 β€ (seqπ( + , πΉ)βπ) β 0 β€ (seqπ( + , πΉ)β(π + 1))))) |
60 | 59 | a2d 26 |
. . 3
β’ (π β (π..^π) β ((π β 0 β€ (seqπ( + , πΉ)βπ)) β (π β 0 β€ (seqπ( + , πΉ)β(π + 1))))) |
61 | 6, 9, 12, 15, 30, 60 | fzind2 10238 |
. 2
β’ (π β (π...π) β (π β 0 β€ (seqπ( + , πΉ)βπ))) |
62 | 3, 61 | mpcom 36 |
1
β’ (π β 0 β€ (seqπ( + , πΉ)βπ)) |