Step | Hyp | Ref
| Expression |
1 | | resqrexlemdecn.n |
. . . . 5
β’ (π β π β β) |
2 | 1 | nnzd 9374 |
. . . 4
β’ (π β π β β€) |
3 | 2 | peano2zd 9378 |
. . 3
β’ (π β (π + 1) β β€) |
4 | | resqrexlemdecn.m |
. . . 4
β’ (π β π β β) |
5 | 4 | nnzd 9374 |
. . 3
β’ (π β π β β€) |
6 | | resqrexlemdecn.nm |
. . . 4
β’ (π β π < π) |
7 | | nnltp1le 9313 |
. . . . 5
β’ ((π β β β§ π β β) β (π < π β (π + 1) β€ π)) |
8 | 1, 4, 7 | syl2anc 411 |
. . . 4
β’ (π β (π < π β (π + 1) β€ π)) |
9 | 6, 8 | mpbid 147 |
. . 3
β’ (π β (π + 1) β€ π) |
10 | | fveq2 5516 |
. . . . . 6
β’ (π€ = (π + 1) β (πΉβπ€) = (πΉβ(π + 1))) |
11 | 10 | breq1d 4014 |
. . . . 5
β’ (π€ = (π + 1) β ((πΉβπ€) < (πΉβπ) β (πΉβ(π + 1)) < (πΉβπ))) |
12 | 11 | imbi2d 230 |
. . . 4
β’ (π€ = (π + 1) β ((π β (πΉβπ€) < (πΉβπ)) β (π β (πΉβ(π + 1)) < (πΉβπ)))) |
13 | | fveq2 5516 |
. . . . . 6
β’ (π€ = π β (πΉβπ€) = (πΉβπ)) |
14 | 13 | breq1d 4014 |
. . . . 5
β’ (π€ = π β ((πΉβπ€) < (πΉβπ) β (πΉβπ) < (πΉβπ))) |
15 | 14 | imbi2d 230 |
. . . 4
β’ (π€ = π β ((π β (πΉβπ€) < (πΉβπ)) β (π β (πΉβπ) < (πΉβπ)))) |
16 | | fveq2 5516 |
. . . . . 6
β’ (π€ = (π + 1) β (πΉβπ€) = (πΉβ(π + 1))) |
17 | 16 | breq1d 4014 |
. . . . 5
β’ (π€ = (π + 1) β ((πΉβπ€) < (πΉβπ) β (πΉβ(π + 1)) < (πΉβπ))) |
18 | 17 | imbi2d 230 |
. . . 4
β’ (π€ = (π + 1) β ((π β (πΉβπ€) < (πΉβπ)) β (π β (πΉβ(π + 1)) < (πΉβπ)))) |
19 | | fveq2 5516 |
. . . . . 6
β’ (π€ = π β (πΉβπ€) = (πΉβπ)) |
20 | 19 | breq1d 4014 |
. . . . 5
β’ (π€ = π β ((πΉβπ€) < (πΉβπ) β (πΉβπ) < (πΉβπ))) |
21 | 20 | imbi2d 230 |
. . . 4
β’ (π€ = π β ((π β (πΉβπ€) < (πΉβπ)) β (π β (πΉβπ) < (πΉβπ)))) |
22 | | resqrexlemex.seq |
. . . . . . 7
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
23 | | resqrexlemex.a |
. . . . . . 7
β’ (π β π΄ β β) |
24 | | resqrexlemex.agt0 |
. . . . . . 7
β’ (π β 0 β€ π΄) |
25 | 22, 23, 24 | resqrexlemdec 11020 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβ(π + 1)) < (πΉβπ)) |
26 | 1, 25 | mpdan 421 |
. . . . 5
β’ (π β (πΉβ(π + 1)) < (πΉβπ)) |
27 | 26 | a1i 9 |
. . . 4
β’ ((π + 1) β β€ β
(π β (πΉβ(π + 1)) < (πΉβπ))) |
28 | 22, 23, 24 | resqrexlemf 11016 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ+) |
29 | 28 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β πΉ:ββΆβ+) |
30 | | simplr2 1040 |
. . . . . . . . . . . 12
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β π β β€) |
31 | | 1red 7972 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β 1 β β) |
32 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (π + 1) β β€) |
33 | 32 | zred 9375 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (π + 1) β β) |
34 | 30 | zred 9375 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β π β β) |
35 | 1 | nnred 8932 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
36 | 1 | nngt0d 8963 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 < π) |
37 | | 0re 7957 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
β |
38 | | ltle 8045 |
. . . . . . . . . . . . . . . . 17
β’ ((0
β β β§ π
β β) β (0 < π β 0 β€ π)) |
39 | 37, 38 | mpan 424 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (0 <
π β 0 β€ π)) |
40 | 35, 36, 39 | sylc 62 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ π) |
41 | | 1red 7972 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 β
β) |
42 | 41, 35 | addge02d 8491 |
. . . . . . . . . . . . . . 15
β’ (π β (0 β€ π β 1 β€ (π + 1))) |
43 | 40, 42 | mpbid 147 |
. . . . . . . . . . . . . 14
β’ (π β 1 β€ (π + 1)) |
44 | 43 | ad2antrr 488 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β 1 β€ (π + 1)) |
45 | | simplr3 1041 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (π + 1) β€ π) |
46 | 31, 33, 34, 44, 45 | letrd 8081 |
. . . . . . . . . . . 12
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β 1 β€ π) |
47 | | elnnz1 9276 |
. . . . . . . . . . . 12
β’ (π β β β (π β β€ β§ 1 β€
π)) |
48 | 30, 46, 47 | sylanbrc 417 |
. . . . . . . . . . 11
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β π β β) |
49 | 48 | peano2nnd 8934 |
. . . . . . . . . 10
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (π + 1) β β) |
50 | 29, 49 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβ(π + 1)) β
β+) |
51 | 50 | rpred 9696 |
. . . . . . . 8
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβ(π + 1)) β β) |
52 | 29, 48 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβπ) β
β+) |
53 | 52 | rpred 9696 |
. . . . . . . 8
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβπ) β β) |
54 | 1 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β π β β) |
55 | 29, 54 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβπ) β
β+) |
56 | 55 | rpred 9696 |
. . . . . . . 8
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβπ) β β) |
57 | | simpll 527 |
. . . . . . . . 9
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β π) |
58 | 22, 23, 24 | resqrexlemdec 11020 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβ(π + 1)) < (πΉβπ)) |
59 | 57, 48, 58 | syl2anc 411 |
. . . . . . . 8
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβ(π + 1)) < (πΉβπ)) |
60 | | simpr 110 |
. . . . . . . 8
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβπ) < (πΉβπ)) |
61 | 51, 53, 56, 59, 60 | lttrd 8083 |
. . . . . . 7
β’ (((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β§ (πΉβπ) < (πΉβπ)) β (πΉβ(π + 1)) < (πΉβπ)) |
62 | 61 | ex 115 |
. . . . . 6
β’ ((π β§ ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) β ((πΉβπ) < (πΉβπ) β (πΉβ(π + 1)) < (πΉβπ))) |
63 | 62 | expcom 116 |
. . . . 5
β’ (((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π) β (π β ((πΉβπ) < (πΉβπ) β (πΉβ(π + 1)) < (πΉβπ)))) |
64 | 63 | a2d 26 |
. . . 4
β’ (((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π) β ((π β (πΉβπ) < (πΉβπ)) β (π β (πΉβ(π + 1)) < (πΉβπ)))) |
65 | 12, 15, 18, 21, 27, 64 | uzind 9364 |
. . 3
β’ (((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π) β (π β (πΉβπ) < (πΉβπ))) |
66 | 3, 5, 9, 65 | syl3anc 1238 |
. 2
β’ (π β (π β (πΉβπ) < (πΉβπ))) |
67 | 66 | pm2.43i 49 |
1
β’ (π β (πΉβπ) < (πΉβπ)) |