Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . 4
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
2 | | resqrexlemex.a |
. . . 4
β’ (π β π΄ β β) |
3 | | resqrexlemex.agt0 |
. . . 4
β’ (π β 0 β€ π΄) |
4 | 1, 2, 3 | resqrexlemf 11016 |
. . 3
β’ (π β πΉ:ββΆβ+) |
5 | | rpssre 9664 |
. . . 4
β’
β+ β β |
6 | 5 | a1i 9 |
. . 3
β’ (π β β+
β β) |
7 | 4, 6 | fssd 5379 |
. 2
β’ (π β πΉ:ββΆβ) |
8 | | 1nn 8930 |
. . . . . . 7
β’ 1 β
β |
9 | 8 | a1i 9 |
. . . . . 6
β’ (π β 1 β
β) |
10 | 4, 9 | ffvelcdmd 5653 |
. . . . 5
β’ (π β (πΉβ1) β
β+) |
11 | | 2z 9281 |
. . . . . 6
β’ 2 β
β€ |
12 | 11 | a1i 9 |
. . . . 5
β’ (π β 2 β
β€) |
13 | 10, 12 | rpexpcld 10678 |
. . . 4
β’ (π β ((πΉβ1)β2) β
β+) |
14 | | 2rp 9658 |
. . . . 5
β’ 2 β
β+ |
15 | 14 | a1i 9 |
. . . 4
β’ (π β 2 β
β+) |
16 | 13, 15 | rpmulcld 9713 |
. . 3
β’ (π β (((πΉβ1)β2) Β· 2) β
β+) |
17 | 16, 15 | rpmulcld 9713 |
. 2
β’ (π β ((((πΉβ1)β2) Β· 2) Β· 2)
β β+) |
18 | 4 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β πΉ:ββΆβ+) |
19 | | simplr 528 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
20 | 18, 19 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β
β+) |
21 | 20 | rpred 9696 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
22 | | eluznn 9600 |
. . . . . . . . . . 11
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
23 | 22 | adantll 476 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
24 | 18, 23 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β
β+) |
25 | 24 | rpred 9696 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
26 | 21, 25 | resubcld 8338 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (πΉβπ)) β β) |
27 | 17 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((((πΉβ1)β2) Β· 2) Β· 2)
β β+) |
28 | 14 | a1i 9 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 2 β
β+) |
29 | 19 | nnzd 9374 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β€) |
30 | 28, 29 | rpexpcld 10678 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (2βπ) β
β+) |
31 | 27, 30 | rpdivcld 9714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) β
β+) |
32 | 31 | rpred 9696 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) β
β) |
33 | 19 | nnrpd 9694 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β+) |
34 | 27, 33 | rpdivcld 9714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
π) β
β+) |
35 | 34 | rpred 9696 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
π) β
β) |
36 | 2 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π΄ β β) |
37 | 3 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 0 β€ π΄) |
38 | | eluzle 9540 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β€ π) |
39 | 38 | adantl 277 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β€ π) |
40 | 1, 36, 37, 19, 23, 39 | resqrexlemnm 11027 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (πΉβπ)) < ((((πΉβ1)β2) Β· 2) /
(2β(π β
1)))) |
41 | | 2cn 8990 |
. . . . . . . . . . 11
β’ 2 β
β |
42 | | expm1t 10548 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β) β (2βπ) = ((2β(π β 1)) Β· 2)) |
43 | 41, 19, 42 | sylancr 414 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (2βπ) = ((2β(π β 1)) Β· 2)) |
44 | 43 | oveq2d 5891 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) = (((((πΉβ1)β2) Β· 2)
Β· 2) / ((2β(π
β 1)) Β· 2))) |
45 | 8 | a1i 9 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 1 β
β) |
46 | 18, 45 | ffvelcdmd 5653 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβ1) β
β+) |
47 | 11 | a1i 9 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 2 β
β€) |
48 | 46, 47 | rpexpcld 10678 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβ1)β2) β
β+) |
49 | 48, 28 | rpmulcld 9713 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) Β· 2) β
β+) |
50 | 49 | rpcnd 9698 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) Β· 2) β
β) |
51 | 41 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 2 β
β) |
52 | | nnm1nn0 9217 |
. . . . . . . . . . . 12
β’ (π β β β (π β 1) β
β0) |
53 | 19, 52 | syl 14 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (π β 1) β
β0) |
54 | 51, 53 | expcld 10654 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (2β(π β 1)) β
β) |
55 | | 2ap0 9012 |
. . . . . . . . . . . 12
β’ 2 #
0 |
56 | 55 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 2 #
0) |
57 | | 1zzd 9280 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β 1 β
β€) |
58 | 29, 57 | zsubcld 9380 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (π β 1) β β€) |
59 | 51, 56, 58 | expap0d 10660 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (2β(π β 1)) #
0) |
60 | 50, 54, 51, 59, 56 | divcanap5rd 8775 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
((2β(π β 1))
Β· 2)) = ((((πΉβ1)β2) Β· 2) /
(2β(π β
1)))) |
61 | 44, 60 | eqtrd 2210 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) = ((((πΉβ1)β2) Β· 2) /
(2β(π β
1)))) |
62 | 40, 61 | breqtrrd 4032 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (πΉβπ)) < (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ))) |
63 | | uzid 9542 |
. . . . . . . . . 10
β’ (2 β
β€ β 2 β (β€β₯β2)) |
64 | 11, 63 | ax-mp 5 |
. . . . . . . . 9
β’ 2 β
(β€β₯β2) |
65 | 19 | nnnn0d 9229 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β0) |
66 | | bernneq3 10643 |
. . . . . . . . 9
β’ ((2
β (β€β₯β2) β§ π β β0) β π < (2βπ)) |
67 | 64, 65, 66 | sylancr 414 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π < (2βπ)) |
68 | 33, 30, 27 | ltdiv2d 9720 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (π < (2βπ) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) < (((((πΉβ1)β2) Β· 2)
Β· 2) / π))) |
69 | 67, 68 | mpbid 147 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) Β· 2) Β· 2) /
(2βπ)) < (((((πΉβ1)β2) Β· 2)
Β· 2) / π)) |
70 | 26, 32, 35, 62, 69 | lttrd 8083 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (πΉβπ)) < (((((πΉβ1)β2) Β· 2) Β· 2) /
π)) |
71 | 21, 25, 35 | ltsubadd2d 8500 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ) β (πΉβπ)) < (((((πΉβ1)β2) Β· 2) Β· 2) /
π) β (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)))) |
72 | 70, 71 | mpbid 147 |
. . . . 5
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π))) |
73 | 21, 35 | readdcld 7987 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)) β
β) |
74 | 25 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β (πΉβπ) β β) |
75 | 21 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β (πΉβπ) β β) |
76 | 36 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β π΄ β β) |
77 | 37 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β 0 β€ π΄) |
78 | 19 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β π β β) |
79 | 23 | adantr 276 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β π β β) |
80 | | simpr 110 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β π < π) |
81 | 1, 76, 77, 78, 79, 80 | resqrexlemdecn 11021 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β (πΉβπ) < (πΉβπ)) |
82 | 74, 75, 81 | ltled 8076 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π < π) β (πΉβπ) β€ (πΉβπ)) |
83 | | fveq2 5516 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
84 | 83 | eqcomd 2183 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
85 | | eqle 8049 |
. . . . . . . 8
β’ (((πΉβπ) β β β§ (πΉβπ) = (πΉβπ)) β (πΉβπ) β€ (πΉβπ)) |
86 | 25, 84, 85 | syl2an 289 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π β (β€β₯βπ)) β§ π = π) β (πΉβπ) β€ (πΉβπ)) |
87 | 23 | nnzd 9374 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β π β β€) |
88 | | zleloe 9300 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β€) β (π β€ π β (π < π β¨ π = π))) |
89 | 29, 87, 88 | syl2anc 411 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (π β€ π β (π < π β¨ π = π))) |
90 | 39, 89 | mpbid 147 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (π < π β¨ π = π)) |
91 | 82, 86, 90 | mpjaodan 798 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β€ (πΉβπ)) |
92 | 21, 34 | ltaddrpd 9730 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π))) |
93 | 25, 21, 73, 91, 92 | lelttrd 8082 |
. . . . 5
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π))) |
94 | 72, 93 | jca 306 |
. . . 4
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)) β§ (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)))) |
95 | 94 | ralrimiva 2550 |
. . 3
β’ ((π β§ π β β) β βπ β
(β€β₯βπ)((πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)) β§ (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)))) |
96 | 95 | ralrimiva 2550 |
. 2
β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)) β§ (πΉβπ) < ((πΉβπ) + (((((πΉβ1)β2) Β· 2) Β· 2) /
π)))) |
97 | 7, 17, 96 | cvg1n 10995 |
1
β’ (π β βπ β β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) |