Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . . . . 7
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
2 | | resqrexlemex.a |
. . . . . . 7
β’ (π β π΄ β β) |
3 | | resqrexlemex.agt0 |
. . . . . . 7
β’ (π β 0 β€ π΄) |
4 | 1, 2, 3 | resqrexlemf 11029 |
. . . . . 6
β’ (π β πΉ:ββΆβ+) |
5 | 4 | ffvelcdmda 5664 |
. . . . 5
β’ ((π β§ π₯ β β) β (πΉβπ₯) β
β+) |
6 | | 2z 9294 |
. . . . . 6
β’ 2 β
β€ |
7 | 6 | a1i 9 |
. . . . 5
β’ ((π β§ π₯ β β) β 2 β
β€) |
8 | 5, 7 | rpexpcld 10691 |
. . . 4
β’ ((π β§ π₯ β β) β ((πΉβπ₯)β2) β
β+) |
9 | | eqid 2187 |
. . . 4
β’ (π₯ β β β¦ ((πΉβπ₯)β2)) = (π₯ β β β¦ ((πΉβπ₯)β2)) |
10 | 8, 9 | fmptd 5683 |
. . 3
β’ (π β (π₯ β β β¦ ((πΉβπ₯)β2)):ββΆβ+) |
11 | | rpssre 9677 |
. . . 4
β’
β+ β β |
12 | 11 | a1i 9 |
. . 3
β’ (π β β+
β β) |
13 | 10, 12 | fssd 5390 |
. 2
β’ (π β (π₯ β β β¦ ((πΉβπ₯)β2)):ββΆβ) |
14 | | resqrexlemgt0.rr |
. . 3
β’ (π β πΏ β β) |
15 | 14 | resqcld 10693 |
. 2
β’ (π β (πΏβ2) β β) |
16 | | resqrexlemgt0.lim |
. . . 4
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
17 | | oveq2 5896 |
. . . . . . . . 9
β’ (π = π β (πΏ + π) = (πΏ + π)) |
18 | 17 | breq2d 4027 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) < (πΏ + π) β (πΉβπ) < (πΏ + π))) |
19 | | oveq2 5896 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) + π) = ((πΉβπ) + π)) |
20 | 19 | breq2d 4027 |
. . . . . . . 8
β’ (π = π β (πΏ < ((πΉβπ) + π) β πΏ < ((πΉβπ) + π))) |
21 | 18, 20 | anbi12d 473 |
. . . . . . 7
β’ (π = π β (((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β ((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)))) |
22 | 21 | rexralbidv 2513 |
. . . . . 6
β’ (π = π β (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)))) |
23 | 22 | cbvralv 2715 |
. . . . 5
β’
(βπ β
β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
24 | | fveq2 5527 |
. . . . . . . 8
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
25 | 24 | raleqdv 2689 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)))) |
26 | 25 | cbvrexv 2716 |
. . . . . 6
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
27 | 26 | ralbii 2493 |
. . . . 5
β’
(βπ β
β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
28 | | fveq2 5527 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
29 | 28 | breq1d 4025 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) < (πΏ + π) β (πΉβπ) < (πΏ + π))) |
30 | 28 | oveq1d 5903 |
. . . . . . . . . 10
β’ (π = π β ((πΉβπ) + π) = ((πΉβπ) + π)) |
31 | 30 | breq2d 4027 |
. . . . . . . . 9
β’ (π = π β (πΏ < ((πΉβπ) + π) β πΏ < ((πΉβπ) + π))) |
32 | 29, 31 | anbi12d 473 |
. . . . . . . 8
β’ (π = π β (((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β ((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)))) |
33 | 32 | cbvralv 2715 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
34 | 33 | rexbii 2494 |
. . . . . 6
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
35 | 34 | ralbii 2493 |
. . . . 5
β’
(βπ β
β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
36 | 23, 27, 35 | 3bitri 206 |
. . . 4
β’
(βπ β
β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π)) β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
37 | 16, 36 | sylib 122 |
. . 3
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) |
38 | 1, 2, 3, 14, 37, 9 | resqrexlemglsq 11044 |
. 2
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)(((π₯ β β β¦ ((πΉβπ₯)β2))βπ) < ((πΏβ2) + π) β§ (πΏβ2) < (((π₯ β β β¦ ((πΉβπ₯)β2))βπ) + π))) |
39 | 1, 2, 3, 14, 37, 9 | resqrexlemga 11045 |
. 2
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)(((π₯ β β β¦ ((πΉβπ₯)β2))βπ) < (π΄ + π) β§ π΄ < (((π₯ β β β¦ ((πΉβπ₯)β2))βπ) + π))) |
40 | 13, 15, 38, 2, 39 | recvguniq 11017 |
1
β’ (π β (πΏβ2) = π΄) |