Step | Hyp | Ref
| Expression |
1 | | resqrexlemex.seq |
. . . . . . . . . . 11
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
2 | | resqrexlemex.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
3 | | resqrexlemex.agt0 |
. . . . . . . . . . 11
β’ (π β 0 β€ π΄) |
4 | 1, 2, 3 | resqrexlemf 11016 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ+) |
5 | 4 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β β+) β πΉ:ββΆβ+) |
6 | | 1nn 8930 |
. . . . . . . . . 10
β’ 1 β
β |
7 | 6 | a1i 9 |
. . . . . . . . 9
β’ ((π β§ π β β+) β 1 β
β) |
8 | 5, 7 | ffvelcdmd 5653 |
. . . . . . . 8
β’ ((π β§ π β β+) β (πΉβ1) β
β+) |
9 | | 2z 9281 |
. . . . . . . . 9
β’ 2 β
β€ |
10 | 9 | a1i 9 |
. . . . . . . 8
β’ ((π β§ π β β+) β 2 β
β€) |
11 | 8, 10 | rpexpcld 10678 |
. . . . . . 7
β’ ((π β§ π β β+) β ((πΉβ1)β2) β
β+) |
12 | | simpr 110 |
. . . . . . 7
β’ ((π β§ π β β+) β π β
β+) |
13 | 11, 12 | rpdivcld 9714 |
. . . . . 6
β’ ((π β§ π β β+) β (((πΉβ1)β2) / π) β
β+) |
14 | 13 | rpred 9696 |
. . . . 5
β’ ((π β§ π β β+) β (((πΉβ1)β2) / π) β
β) |
15 | | 1red 7972 |
. . . . 5
β’ ((π β§ π β β+) β 1 β
β) |
16 | 14, 15 | readdcld 7987 |
. . . 4
β’ ((π β§ π β β+) β ((((πΉβ1)β2) / π) + 1) β
β) |
17 | | arch 9173 |
. . . 4
β’
(((((πΉβ1)β2) / π) + 1) β β β βπ β β ((((πΉβ1)β2) / π) + 1) < π) |
18 | 16, 17 | syl 14 |
. . 3
β’ ((π β§ π β β+) β
βπ β β
((((πΉβ1)β2) /
π) + 1) < π) |
19 | | simpllr 534 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β) |
20 | | simpr 110 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
21 | | eluznn 9600 |
. . . . . . . . . 10
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
22 | 19, 20, 21 | syl2anc 411 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β) |
23 | | simplll 533 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ π β β) β§ ((((πΉβ1)β2) / π) + 1) < π) β π) |
24 | 23 | adantr 276 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π) |
25 | 24, 4 | syl 14 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β πΉ:ββΆβ+) |
26 | 25, 22 | ffvelcdmd 5653 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΉβπ) β
β+) |
27 | 9 | a1i 9 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β 2 β
β€) |
28 | 26, 27 | rpexpcld 10678 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΉβπ)β2) β
β+) |
29 | | fveq2 5516 |
. . . . . . . . . . 11
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
30 | 29 | oveq1d 5890 |
. . . . . . . . . 10
β’ (π₯ = π β ((πΉβπ₯)β2) = ((πΉβπ)β2)) |
31 | | resqrexlemsqa.g |
. . . . . . . . . 10
β’ πΊ = (π₯ β β β¦ ((πΉβπ₯)β2)) |
32 | 30, 31 | fvmptg 5593 |
. . . . . . . . 9
β’ ((π β β β§ ((πΉβπ)β2) β β+) β
(πΊβπ) = ((πΉβπ)β2)) |
33 | 22, 28, 32 | syl2anc 411 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΊβπ) = ((πΉβπ)β2)) |
34 | 28 | rpred 9696 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΉβπ)β2) β β) |
35 | 24, 2 | syl 14 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π΄ β β) |
36 | 34, 35 | resubcld 8338 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβπ)β2) β π΄) β β) |
37 | 11 | ad3antrrr 492 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΉβ1)β2) β
β+) |
38 | 37 | rpred 9696 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΉβ1)β2) β
β) |
39 | | 4re 8996 |
. . . . . . . . . . . . . 14
β’ 4 β
β |
40 | | 4pos 9016 |
. . . . . . . . . . . . . 14
β’ 0 <
4 |
41 | 39, 40 | elrpii 9656 |
. . . . . . . . . . . . 13
β’ 4 β
β+ |
42 | 41 | a1i 9 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β 4 β
β+) |
43 | | nnm1nn0 9217 |
. . . . . . . . . . . . . 14
β’ (π β β β (π β 1) β
β0) |
44 | 22, 43 | syl 14 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (π β 1) β
β0) |
45 | 44 | nn0zd 9373 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (π β 1) β β€) |
46 | 42, 45 | rpexpcld 10678 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (4β(π β 1)) β
β+) |
47 | 38, 46 | rerpdivcld 9728 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) / (4β(π β 1))) β
β) |
48 | 12 | ad3antrrr 492 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β+) |
49 | 48 | rpred 9696 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β) |
50 | 1, 2, 3 | resqrexlemcalc3 11025 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β€ (((πΉβ1)β2) / (4β(π β 1)))) |
51 | 24, 22, 50 | syl2anc 411 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβπ)β2) β π΄) β€ (((πΉβ1)β2) / (4β(π β 1)))) |
52 | 14 | ad3antrrr 492 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) / π) β β) |
53 | 22 | nnred 8932 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β) |
54 | | 1red 7972 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β 1 β
β) |
55 | 53, 54 | resubcld 8338 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (π β 1) β β) |
56 | 39 | a1i 9 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β 4 β
β) |
57 | 56, 44 | reexpcld 10671 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (4β(π β 1)) β
β) |
58 | 16 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((((πΉβ1)β2) / π) + 1) β β) |
59 | 19 | nnred 8932 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β β) |
60 | | simplr 528 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((((πΉβ1)β2) / π) + 1) < π) |
61 | | eluzle 9540 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β π β€ π) |
62 | 61 | adantl 277 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π β€ π) |
63 | 58, 59, 53, 60, 62 | ltletrd 8380 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((((πΉβ1)β2) / π) + 1) < π) |
64 | 52, 54, 53 | ltaddsubd 8502 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((((πΉβ1)β2) / π) + 1) < π β (((πΉβ1)β2) / π) < (π β 1))) |
65 | 63, 64 | mpbid 147 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) / π) < (π β 1)) |
66 | | 4z 9283 |
. . . . . . . . . . . . . 14
β’ 4 β
β€ |
67 | | 2re 8989 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
68 | | 2lt4 9092 |
. . . . . . . . . . . . . . 15
β’ 2 <
4 |
69 | 67, 39, 68 | ltleii 8060 |
. . . . . . . . . . . . . 14
β’ 2 β€
4 |
70 | | eluz2 9534 |
. . . . . . . . . . . . . 14
β’ (4 β
(β€β₯β2) β (2 β β€ β§ 4 β
β€ β§ 2 β€ 4)) |
71 | 9, 66, 69, 70 | mpbir3an 1179 |
. . . . . . . . . . . . 13
β’ 4 β
(β€β₯β2) |
72 | | bernneq3 10643 |
. . . . . . . . . . . . 13
β’ ((4
β (β€β₯β2) β§ (π β 1) β β0)
β (π β 1) <
(4β(π β
1))) |
73 | 71, 44, 72 | sylancr 414 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (π β 1) < (4β(π β 1))) |
74 | 52, 55, 57, 65, 73 | lttrd 8083 |
. . . . . . . . . . 11
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) / π) < (4β(π β 1))) |
75 | 38, 48, 46, 74 | ltdiv23d 9757 |
. . . . . . . . . 10
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβ1)β2) / (4β(π β 1))) < π) |
76 | 36, 47, 49, 51, 75 | lelttrd 8082 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (((πΉβπ)β2) β π΄) < π) |
77 | 34, 35, 49 | ltsubadd2d 8500 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((((πΉβπ)β2) β π΄) < π β ((πΉβπ)β2) < (π΄ + π))) |
78 | 76, 77 | mpbid 147 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΉβπ)β2) < (π΄ + π)) |
79 | 33, 78 | eqbrtrd 4026 |
. . . . . . 7
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΊβπ) < (π΄ + π)) |
80 | 33, 28 | eqeltrd 2254 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΊβπ) β
β+) |
81 | 80 | rpred 9696 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
82 | 81, 49 | readdcld 7987 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΊβπ) + π) β β) |
83 | 1, 2, 3 | resqrexlemover 11019 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π΄ < ((πΉβπ)β2)) |
84 | 24, 22, 83 | syl2anc 411 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π΄ < ((πΉβπ)β2)) |
85 | 84, 33 | breqtrrd 4032 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π΄ < (πΊβπ)) |
86 | 81, 48 | ltaddrpd 9730 |
. . . . . . . 8
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β (πΊβπ) < ((πΊβπ) + π)) |
87 | 35, 81, 82, 85, 86 | lttrd 8083 |
. . . . . . 7
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β π΄ < ((πΊβπ) + π)) |
88 | 79, 87 | jca 306 |
. . . . . 6
β’
(((((π β§ π β β+)
β§ π β β)
β§ ((((πΉβ1)β2) / π) + 1) < π) β§ π β (β€β₯βπ)) β ((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π))) |
89 | 88 | ralrimiva 2550 |
. . . . 5
β’ ((((π β§ π β β+) β§ π β β) β§ ((((πΉβ1)β2) / π) + 1) < π) β βπ β (β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π))) |
90 | 89 | ex 115 |
. . . 4
β’ (((π β§ π β β+) β§ π β β) β
(((((πΉβ1)β2) /
π) + 1) < π β βπ β
(β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π)))) |
91 | 90 | reximdva 2579 |
. . 3
β’ ((π β§ π β β+) β
(βπ β β
((((πΉβ1)β2) /
π) + 1) < π β βπ β β βπ β
(β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π)))) |
92 | 18, 91 | mpd 13 |
. 2
β’ ((π β§ π β β+) β
βπ β β
βπ β
(β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π))) |
93 | 92 | ralrimiva 2550 |
1
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π))) |