Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . 3
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
2 | | resqrexlemex.a |
. . 3
β’ (π β π΄ β β) |
3 | | resqrexlemex.agt0 |
. . 3
β’ (π β 0 β€ π΄) |
4 | 1, 2, 3 | resqrexlemcalc1 11022 |
. 2
β’ ((π β§ π β β) β (((πΉβ(π + 1))β2) β π΄) = (((((πΉβπ)β2) β π΄)β2) / (4 Β· ((πΉβπ)β2)))) |
5 | 1, 2, 3 | resqrexlemf 11015 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ+) |
6 | 5 | ffvelcdmda 5651 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) β
β+) |
7 | 6 | rpred 9695 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) β β) |
8 | 7 | resqcld 10679 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΉβπ)β2) β β) |
9 | 2 | adantr 276 |
. . . . . . 7
β’ ((π β§ π β β) β π΄ β β) |
10 | 8, 9 | resubcld 8337 |
. . . . . 6
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β β) |
11 | 6 | rpap0d 9701 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) # 0) |
12 | 7, 11 | sqgt0apd 10681 |
. . . . . . 7
β’ ((π β§ π β β) β 0 < ((πΉβπ)β2)) |
13 | 8, 12 | elrpd 9692 |
. . . . . 6
β’ ((π β§ π β β) β ((πΉβπ)β2) β
β+) |
14 | 8, 9 | readdcld 7986 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πΉβπ)β2) + π΄) β β) |
15 | 3 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 β€ π΄) |
16 | 8, 9 | addge01d 8489 |
. . . . . . . . 9
β’ ((π β§ π β β) β (0 β€ π΄ β ((πΉβπ)β2) β€ (((πΉβπ)β2) + π΄))) |
17 | 15, 16 | mpbid 147 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβπ)β2) β€ (((πΉβπ)β2) + π΄)) |
18 | 8, 14, 9, 17 | lesub1dd 8517 |
. . . . . . 7
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β€ ((((πΉβπ)β2) + π΄) β π΄)) |
19 | 8 | recnd 7985 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβπ)β2) β β) |
20 | 9 | recnd 7985 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄ β β) |
21 | 19, 20 | pncand 8268 |
. . . . . . 7
β’ ((π β§ π β β) β ((((πΉβπ)β2) + π΄) β π΄) = ((πΉβπ)β2)) |
22 | 18, 21 | breqtrd 4029 |
. . . . . 6
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β€ ((πΉβπ)β2)) |
23 | 10, 8, 13, 22 | lediv1dd 9754 |
. . . . 5
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) β€ (((πΉβπ)β2) / ((πΉβπ)β2))) |
24 | 8, 12 | gt0ap0d 8585 |
. . . . . 6
β’ ((π β§ π β β) β ((πΉβπ)β2) # 0) |
25 | 19, 24 | dividapd 8742 |
. . . . 5
β’ ((π β§ π β β) β (((πΉβπ)β2) / ((πΉβπ)β2)) = 1) |
26 | 23, 25 | breqtrd 4029 |
. . . 4
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) β€ 1) |
27 | 10, 8, 24 | redivclapd 8791 |
. . . . 5
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) β β) |
28 | | 1red 7971 |
. . . . 5
β’ ((π β§ π β β) β 1 β
β) |
29 | 1, 2, 3 | resqrexlemover 11018 |
. . . . . . 7
β’ ((π β§ π β β) β π΄ < ((πΉβπ)β2)) |
30 | | difrp 9691 |
. . . . . . . 8
β’ ((π΄ β β β§ ((πΉβπ)β2) β β) β (π΄ < ((πΉβπ)β2) β (((πΉβπ)β2) β π΄) β
β+)) |
31 | 9, 8, 30 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄ < ((πΉβπ)β2) β (((πΉβπ)β2) β π΄) β
β+)) |
32 | 29, 31 | mpbid 147 |
. . . . . 6
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β
β+) |
33 | | 4re 8995 |
. . . . . . . 8
β’ 4 β
β |
34 | 33 | a1i 9 |
. . . . . . 7
β’ ((π β§ π β β) β 4 β
β) |
35 | | 4pos 9015 |
. . . . . . . 8
β’ 0 <
4 |
36 | 35 | a1i 9 |
. . . . . . 7
β’ ((π β§ π β β) β 0 <
4) |
37 | 34, 36 | elrpd 9692 |
. . . . . 6
β’ ((π β§ π β β) β 4 β
β+) |
38 | 32, 37 | rpdivcld 9713 |
. . . . 5
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄) / 4) β
β+) |
39 | 27, 28, 38 | lemul1d 9739 |
. . . 4
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) β€ 1 β (((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) Β· ((((πΉβπ)β2) β π΄) / 4)) β€ (1 Β· ((((πΉβπ)β2) β π΄) / 4)))) |
40 | 26, 39 | mpbid 147 |
. . 3
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) Β· ((((πΉβπ)β2) β π΄) / 4)) β€ (1 Β· ((((πΉβπ)β2) β π΄) / 4))) |
41 | 10 | recnd 7985 |
. . . . 5
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β β) |
42 | 34 | recnd 7985 |
. . . . 5
β’ ((π β§ π β β) β 4 β
β) |
43 | 34, 36 | gt0ap0d 8585 |
. . . . 5
β’ ((π β§ π β β) β 4 #
0) |
44 | 41, 19, 41, 42, 24, 43 | divmuldivapd 8788 |
. . . 4
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) Β· ((((πΉβπ)β2) β π΄) / 4)) = (((((πΉβπ)β2) β π΄) Β· (((πΉβπ)β2) β π΄)) / (((πΉβπ)β2) Β· 4))) |
45 | 41 | sqvald 10650 |
. . . . 5
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄)β2) = ((((πΉβπ)β2) β π΄) Β· (((πΉβπ)β2) β π΄))) |
46 | 42, 19 | mulcomd 7978 |
. . . . 5
β’ ((π β§ π β β) β (4 Β· ((πΉβπ)β2)) = (((πΉβπ)β2) Β· 4)) |
47 | 45, 46 | oveq12d 5892 |
. . . 4
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄)β2) / (4 Β· ((πΉβπ)β2))) = (((((πΉβπ)β2) β π΄) Β· (((πΉβπ)β2) β π΄)) / (((πΉβπ)β2) Β· 4))) |
48 | 44, 47 | eqtr4d 2213 |
. . 3
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄) / ((πΉβπ)β2)) Β· ((((πΉβπ)β2) β π΄) / 4)) = (((((πΉβπ)β2) β π΄)β2) / (4 Β· ((πΉβπ)β2)))) |
49 | 38 | rpcnd 9697 |
. . . 4
β’ ((π β§ π β β) β ((((πΉβπ)β2) β π΄) / 4) β β) |
50 | 49 | mulid2d 7975 |
. . 3
β’ ((π β§ π β β) β (1 Β·
((((πΉβπ)β2) β π΄) / 4)) = ((((πΉβπ)β2) β π΄) / 4)) |
51 | 40, 48, 50 | 3brtr3d 4034 |
. 2
β’ ((π β§ π β β) β (((((πΉβπ)β2) β π΄)β2) / (4 Β· ((πΉβπ)β2))) β€ ((((πΉβπ)β2) β π΄) / 4)) |
52 | 4, 51 | eqbrtrd 4025 |
1
β’ ((π β§ π β β) β (((πΉβ(π + 1))β2) β π΄) β€ ((((πΉβπ)β2) β π΄) / 4)) |