Step | Hyp | Ref
| Expression |
1 | | elnnuz 9564 |
. . . . . 6
β’ (π β β β π β
(β€β₯β1)) |
2 | 1 | biimpi 120 |
. . . . 5
β’ (π β β β π β
(β€β₯β1)) |
3 | 2 | adantl 277 |
. . . 4
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
4 | | elnnuz 9564 |
. . . . . 6
β’ (π β β β π β
(β€β₯β1)) |
5 | | resqrexlemex.a |
. . . . . . 7
β’ (π β π΄ β β) |
6 | | resqrexlemex.agt0 |
. . . . . . 7
β’ (π β 0 β€ π΄) |
7 | 5, 6 | resqrexlem1arp 11014 |
. . . . . 6
β’ ((π β§ π β β) β ((β Γ {(1
+ π΄)})βπ) β
β+) |
8 | 4, 7 | sylan2br 288 |
. . . . 5
β’ ((π β§ π β (β€β₯β1))
β ((β Γ {(1 + π΄)})βπ) β
β+) |
9 | 8 | adantlr 477 |
. . . 4
β’ (((π β§ π β β) β§ π β (β€β₯β1))
β ((β Γ {(1 + π΄)})βπ) β
β+) |
10 | 5, 6 | resqrexlemp1rp 11015 |
. . . . 5
β’ ((π β§ (π β β+ β§ π β β+))
β (π(π¦ β β+,
π§ β
β+ β¦ ((π¦ + (π΄ / π¦)) / 2))π) β
β+) |
11 | 10 | adantlr 477 |
. . . 4
β’ (((π β§ π β β) β§ (π β β+ β§ π β β+))
β (π(π¦ β β+,
π§ β
β+ β¦ ((π¦ + (π΄ / π¦)) / 2))π) β
β+) |
12 | 3, 9, 11 | seq3p1 10462 |
. . 3
β’ ((π β§ π β β) β (seq1((π¦ β β+,
π§ β
β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)}))β(π + 1)) = ((seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)}))βπ)(π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2))((β Γ {(1 + π΄)})β(π + 1)))) |
13 | | resqrexlemex.seq |
. . . 4
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
14 | 13 | fveq1i 5517 |
. . 3
β’ (πΉβ(π + 1)) = (seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)}))β(π + 1)) |
15 | 13 | fveq1i 5517 |
. . . 4
β’ (πΉβπ) = (seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)}))βπ) |
16 | 15 | oveq1i 5885 |
. . 3
β’ ((πΉβπ)(π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2))((β Γ {(1 + π΄)})β(π + 1))) = ((seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)}))βπ)(π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2))((β Γ {(1 + π΄)})β(π + 1))) |
17 | 12, 14, 16 | 3eqtr4g 2235 |
. 2
β’ ((π β§ π β β) β (πΉβ(π + 1)) = ((πΉβπ)(π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2))((β Γ {(1 + π΄)})β(π + 1)))) |
18 | | id 19 |
. . . . . . 7
β’ (π¦ = π β π¦ = π) |
19 | | oveq2 5883 |
. . . . . . 7
β’ (π¦ = π β (π΄ / π¦) = (π΄ / π)) |
20 | 18, 19 | oveq12d 5893 |
. . . . . 6
β’ (π¦ = π β (π¦ + (π΄ / π¦)) = (π + (π΄ / π))) |
21 | 20 | oveq1d 5890 |
. . . . 5
β’ (π¦ = π β ((π¦ + (π΄ / π¦)) / 2) = ((π + (π΄ / π)) / 2)) |
22 | | eqidd 2178 |
. . . . 5
β’ (π§ = π β ((π + (π΄ / π)) / 2) = ((π + (π΄ / π)) / 2)) |
23 | 21, 22 | cbvmpov 5955 |
. . . 4
β’ (π¦ β β+,
π§ β
β+ β¦ ((π¦ + (π΄ / π¦)) / 2)) = (π β β+, π β β+
β¦ ((π + (π΄ / π)) / 2)) |
24 | 23 | a1i 9 |
. . 3
β’ ((π β§ π β β) β (π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)) = (π β β+, π β β+
β¦ ((π + (π΄ / π)) / 2))) |
25 | | id 19 |
. . . . . 6
β’ (π = (πΉβπ) β π = (πΉβπ)) |
26 | | oveq2 5883 |
. . . . . 6
β’ (π = (πΉβπ) β (π΄ / π) = (π΄ / (πΉβπ))) |
27 | 25, 26 | oveq12d 5893 |
. . . . 5
β’ (π = (πΉβπ) β (π + (π΄ / π)) = ((πΉβπ) + (π΄ / (πΉβπ)))) |
28 | 27 | oveq1d 5890 |
. . . 4
β’ (π = (πΉβπ) β ((π + (π΄ / π)) / 2) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
29 | 28 | ad2antrl 490 |
. . 3
β’ (((π β§ π β β) β§ (π = (πΉβπ) β§ π = ((β Γ {(1 + π΄)})β(π + 1)))) β ((π + (π΄ / π)) / 2) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
30 | 13, 5, 6 | resqrexlemf 11016 |
. . . 4
β’ (π β πΉ:ββΆβ+) |
31 | 30 | ffvelcdmda 5652 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) β
β+) |
32 | | peano2nn 8931 |
. . . 4
β’ (π β β β (π + 1) β
β) |
33 | 5, 6 | resqrexlem1arp 11014 |
. . . 4
β’ ((π β§ (π + 1) β β) β ((β
Γ {(1 + π΄)})β(π + 1)) β
β+) |
34 | 32, 33 | sylan2 286 |
. . 3
β’ ((π β§ π β β) β ((β Γ
{(1 + π΄)})β(π + 1)) β
β+) |
35 | 31 | rpred 9696 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) β β) |
36 | 5 | adantr 276 |
. . . . . 6
β’ ((π β§ π β β) β π΄ β β) |
37 | 36, 31 | rerpdivcld 9728 |
. . . . 5
β’ ((π β§ π β β) β (π΄ / (πΉβπ)) β β) |
38 | 35, 37 | readdcld 7987 |
. . . 4
β’ ((π β§ π β β) β ((πΉβπ) + (π΄ / (πΉβπ))) β β) |
39 | 38 | rehalfcld 9165 |
. . 3
β’ ((π β§ π β β) β (((πΉβπ) + (π΄ / (πΉβπ))) / 2) β β) |
40 | 24, 29, 31, 34, 39 | ovmpod 6002 |
. 2
β’ ((π β§ π β β) β ((πΉβπ)(π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2))((β Γ {(1 + π΄)})β(π + 1))) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
41 | 17, 40 | eqtrd 2210 |
1
β’ ((π β§ π β β) β (πΉβ(π + 1)) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |