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 11015 |
. . . . . 6
β’ (π β πΉ:ββΆβ+) |
5 | | resqrexlemnmsq.n |
. . . . . 6
β’ (π β π β β) |
6 | 4, 5 | ffvelcdmd 5652 |
. . . . 5
β’ (π β (πΉβπ) β
β+) |
7 | 6 | rpred 9695 |
. . . 4
β’ (π β (πΉβπ) β β) |
8 | | resqrexlemnmsq.m |
. . . . . 6
β’ (π β π β β) |
9 | 4, 8 | ffvelcdmd 5652 |
. . . . 5
β’ (π β (πΉβπ) β
β+) |
10 | 9 | rpred 9695 |
. . . 4
β’ (π β (πΉβπ) β β) |
11 | 7, 10 | resubcld 8337 |
. . 3
β’ (π β ((πΉβπ) β (πΉβπ)) β β) |
12 | 7 | resqcld 10679 |
. . . . 5
β’ (π β ((πΉβπ)β2) β β) |
13 | 10 | resqcld 10679 |
. . . . 5
β’ (π β ((πΉβπ)β2) β β) |
14 | 12, 13 | resubcld 8337 |
. . . 4
β’ (π β (((πΉβπ)β2) β ((πΉβπ)β2)) β β) |
15 | | 2cn 8989 |
. . . . . . 7
β’ 2 β
β |
16 | | expm1t 10547 |
. . . . . . 7
β’ ((2
β β β§ π
β β) β (2βπ) = ((2β(π β 1)) Β· 2)) |
17 | 15, 5, 16 | sylancr 414 |
. . . . . 6
β’ (π β (2βπ) = ((2β(π β 1)) Β· 2)) |
18 | | 2nn 9079 |
. . . . . . . . 9
β’ 2 β
β |
19 | 18 | a1i 9 |
. . . . . . . 8
β’ (π β 2 β
β) |
20 | 5 | nnnn0d 9228 |
. . . . . . . 8
β’ (π β π β
β0) |
21 | 19, 20 | nnexpcld 10675 |
. . . . . . 7
β’ (π β (2βπ) β β) |
22 | 21 | nnrpd 9693 |
. . . . . 6
β’ (π β (2βπ) β
β+) |
23 | 17, 22 | eqeltrrd 2255 |
. . . . 5
β’ (π β ((2β(π β 1)) Β· 2) β
β+) |
24 | 23 | rpred 9695 |
. . . 4
β’ (π β ((2β(π β 1)) Β· 2) β
β) |
25 | 14, 24 | remulcld 7987 |
. . 3
β’ (π β ((((πΉβπ)β2) β ((πΉβπ)β2)) Β· ((2β(π β 1)) Β· 2)) β
β) |
26 | | 1nn 8929 |
. . . . . . . . 9
β’ 1 β
β |
27 | 26 | a1i 9 |
. . . . . . . 8
β’ (π β 1 β
β) |
28 | 4, 27 | ffvelcdmd 5652 |
. . . . . . 7
β’ (π β (πΉβ1) β
β+) |
29 | 19 | nnzd 9373 |
. . . . . . 7
β’ (π β 2 β
β€) |
30 | 28, 29 | rpexpcld 10677 |
. . . . . 6
β’ (π β ((πΉβ1)β2) β
β+) |
31 | | 4re 8995 |
. . . . . . . . 9
β’ 4 β
β |
32 | | 4pos 9015 |
. . . . . . . . 9
β’ 0 <
4 |
33 | 31, 32 | elrpii 9655 |
. . . . . . . 8
β’ 4 β
β+ |
34 | 33 | a1i 9 |
. . . . . . 7
β’ (π β 4 β
β+) |
35 | 5 | nnzd 9373 |
. . . . . . . 8
β’ (π β π β β€) |
36 | | peano2zm 9290 |
. . . . . . . 8
β’ (π β β€ β (π β 1) β
β€) |
37 | 35, 36 | syl 14 |
. . . . . . 7
β’ (π β (π β 1) β β€) |
38 | 34, 37 | rpexpcld 10677 |
. . . . . 6
β’ (π β (4β(π β 1)) β
β+) |
39 | 30, 38 | rpdivcld 9713 |
. . . . 5
β’ (π β (((πΉβ1)β2) / (4β(π β 1))) β
β+) |
40 | 39 | rpred 9695 |
. . . 4
β’ (π β (((πΉβ1)β2) / (4β(π β 1))) β
β) |
41 | 40, 24 | remulcld 7987 |
. . 3
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2)) β β) |
42 | 6, 9 | rpaddcld 9711 |
. . . . . . 7
β’ (π β ((πΉβπ) + (πΉβπ)) β
β+) |
43 | 42, 23 | rpmulcld 9712 |
. . . . . 6
β’ (π β (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2)) β
β+) |
44 | 43 | rpred 9695 |
. . . . 5
β’ (π β (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2)) β
β) |
45 | 2 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β π΄ β β) |
46 | 3 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β 0 β€ π΄) |
47 | 5 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β π β β) |
48 | 8 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β π β β) |
49 | | simpr 110 |
. . . . . . . . 9
β’ ((π β§ π < π) β π < π) |
50 | 1, 45, 46, 47, 48, 49 | resqrexlemdecn 11020 |
. . . . . . . 8
β’ ((π β§ π < π) β (πΉβπ) < (πΉβπ)) |
51 | 10 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β (πΉβπ) β β) |
52 | 7 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π < π) β (πΉβπ) β β) |
53 | | difrp 9691 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β ((πΉβπ) < (πΉβπ) β ((πΉβπ) β (πΉβπ)) β
β+)) |
54 | 51, 52, 53 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ π < π) β ((πΉβπ) < (πΉβπ) β ((πΉβπ) β (πΉβπ)) β
β+)) |
55 | 50, 54 | mpbid 147 |
. . . . . . 7
β’ ((π β§ π < π) β ((πΉβπ) β (πΉβπ)) β
β+) |
56 | 55 | rpge0d 9699 |
. . . . . 6
β’ ((π β§ π < π) β 0 β€ ((πΉβπ) β (πΉβπ))) |
57 | 7 | recnd 7985 |
. . . . . . . . 9
β’ (π β (πΉβπ) β β) |
58 | 57 | subidd 8255 |
. . . . . . . 8
β’ (π β ((πΉβπ) β (πΉβπ)) = 0) |
59 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
60 | 59 | oveq2d 5890 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) β (πΉβπ)) = ((πΉβπ) β (πΉβπ))) |
61 | 58, 60 | sylan9req 2231 |
. . . . . . 7
β’ ((π β§ π = π) β 0 = ((πΉβπ) β (πΉβπ))) |
62 | | 0re 7956 |
. . . . . . . 8
β’ 0 β
β |
63 | 62 | eqlei 8050 |
. . . . . . 7
β’ (0 =
((πΉβπ) β (πΉβπ)) β 0 β€ ((πΉβπ) β (πΉβπ))) |
64 | 61, 63 | syl 14 |
. . . . . 6
β’ ((π β§ π = π) β 0 β€ ((πΉβπ) β (πΉβπ))) |
65 | | resqrexlemnmsq.nm |
. . . . . . 7
β’ (π β π β€ π) |
66 | 8 | nnzd 9373 |
. . . . . . . 8
β’ (π β π β β€) |
67 | | zleloe 9299 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€) β (π β€ π β (π < π β¨ π = π))) |
68 | 35, 66, 67 | syl2anc 411 |
. . . . . . 7
β’ (π β (π β€ π β (π < π β¨ π = π))) |
69 | 65, 68 | mpbid 147 |
. . . . . 6
β’ (π β (π < π β¨ π = π)) |
70 | 56, 64, 69 | mpjaodan 798 |
. . . . 5
β’ (π β 0 β€ ((πΉβπ) β (πΉβπ))) |
71 | | 1red 7971 |
. . . . . 6
β’ (π β 1 β
β) |
72 | 21 | nnrecred 8965 |
. . . . . . . . . . 11
β’ (π β (1 / (2βπ)) β
β) |
73 | 72 | recnd 7985 |
. . . . . . . . . 10
β’ (π β (1 / (2βπ)) β
β) |
74 | 73 | addid1d 8105 |
. . . . . . . . 9
β’ (π β ((1 / (2βπ)) + 0) = (1 / (2βπ))) |
75 | | 0red 7957 |
. . . . . . . . . 10
β’ (π β 0 β
β) |
76 | 1, 2, 3 | resqrexlemlo 11021 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (1 / (2βπ)) < (πΉβπ)) |
77 | 5, 76 | mpdan 421 |
. . . . . . . . . 10
β’ (π β (1 / (2βπ)) < (πΉβπ)) |
78 | 9 | rpgt0d 9698 |
. . . . . . . . . 10
β’ (π β 0 < (πΉβπ)) |
79 | 72, 75, 7, 10, 77, 78 | lt2addd 8523 |
. . . . . . . . 9
β’ (π β ((1 / (2βπ)) + 0) < ((πΉβπ) + (πΉβπ))) |
80 | 74, 79 | eqbrtrrd 4027 |
. . . . . . . 8
β’ (π β (1 / (2βπ)) < ((πΉβπ) + (πΉβπ))) |
81 | 7, 10 | readdcld 7986 |
. . . . . . . . 9
β’ (π β ((πΉβπ) + (πΉβπ)) β β) |
82 | 71, 81, 22 | ltdivmul2d 9748 |
. . . . . . . 8
β’ (π β ((1 / (2βπ)) < ((πΉβπ) + (πΉβπ)) β 1 < (((πΉβπ) + (πΉβπ)) Β· (2βπ)))) |
83 | 80, 82 | mpbid 147 |
. . . . . . 7
β’ (π β 1 < (((πΉβπ) + (πΉβπ)) Β· (2βπ))) |
84 | 17 | oveq2d 5890 |
. . . . . . 7
β’ (π β (((πΉβπ) + (πΉβπ)) Β· (2βπ)) = (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2))) |
85 | 83, 84 | breqtrd 4029 |
. . . . . 6
β’ (π β 1 < (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2))) |
86 | 71, 44, 85 | ltled 8075 |
. . . . 5
β’ (π β 1 β€ (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2))) |
87 | 11, 44, 70, 86 | lemulge11d 8893 |
. . . 4
β’ (π β ((πΉβπ) β (πΉβπ)) β€ (((πΉβπ) β (πΉβπ)) Β· (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2)))) |
88 | 11 | recnd 7985 |
. . . . . 6
β’ (π β ((πΉβπ) β (πΉβπ)) β β) |
89 | 81 | recnd 7985 |
. . . . . 6
β’ (π β ((πΉβπ) + (πΉβπ)) β β) |
90 | 23 | rpcnd 9697 |
. . . . . 6
β’ (π β ((2β(π β 1)) Β· 2) β
β) |
91 | 88, 89, 90 | mulassd 7980 |
. . . . 5
β’ (π β ((((πΉβπ) β (πΉβπ)) Β· ((πΉβπ) + (πΉβπ))) Β· ((2β(π β 1)) Β· 2)) = (((πΉβπ) β (πΉβπ)) Β· (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2)))) |
92 | 88, 89 | mulcomd 7978 |
. . . . . . 7
β’ (π β (((πΉβπ) β (πΉβπ)) Β· ((πΉβπ) + (πΉβπ))) = (((πΉβπ) + (πΉβπ)) Β· ((πΉβπ) β (πΉβπ)))) |
93 | 10 | recnd 7985 |
. . . . . . . 8
β’ (π β (πΉβπ) β β) |
94 | | subsq 10626 |
. . . . . . . 8
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (((πΉβπ)β2) β ((πΉβπ)β2)) = (((πΉβπ) + (πΉβπ)) Β· ((πΉβπ) β (πΉβπ)))) |
95 | 57, 93, 94 | syl2anc 411 |
. . . . . . 7
β’ (π β (((πΉβπ)β2) β ((πΉβπ)β2)) = (((πΉβπ) + (πΉβπ)) Β· ((πΉβπ) β (πΉβπ)))) |
96 | 92, 95 | eqtr4d 2213 |
. . . . . 6
β’ (π β (((πΉβπ) β (πΉβπ)) Β· ((πΉβπ) + (πΉβπ))) = (((πΉβπ)β2) β ((πΉβπ)β2))) |
97 | 96 | oveq1d 5889 |
. . . . 5
β’ (π β ((((πΉβπ) β (πΉβπ)) Β· ((πΉβπ) + (πΉβπ))) Β· ((2β(π β 1)) Β· 2)) = ((((πΉβπ)β2) β ((πΉβπ)β2)) Β· ((2β(π β 1)) Β·
2))) |
98 | 91, 97 | eqtr3d 2212 |
. . . 4
β’ (π β (((πΉβπ) β (πΉβπ)) Β· (((πΉβπ) + (πΉβπ)) Β· ((2β(π β 1)) Β· 2))) = ((((πΉβπ)β2) β ((πΉβπ)β2)) Β· ((2β(π β 1)) Β·
2))) |
99 | 87, 98 | breqtrd 4029 |
. . 3
β’ (π β ((πΉβπ) β (πΉβπ)) β€ ((((πΉβπ)β2) β ((πΉβπ)β2)) Β· ((2β(π β 1)) Β·
2))) |
100 | 1, 2, 3, 5, 8, 65 | resqrexlemnmsq 11025 |
. . . 4
β’ (π β (((πΉβπ)β2) β ((πΉβπ)β2)) < (((πΉβ1)β2) / (4β(π β 1)))) |
101 | 14, 40, 23, 100 | ltmul1dd 9751 |
. . 3
β’ (π β ((((πΉβπ)β2) β ((πΉβπ)β2)) Β· ((2β(π β 1)) Β· 2)) <
((((πΉβ1)β2) /
(4β(π β 1)))
Β· ((2β(π
β 1)) Β· 2))) |
102 | 11, 25, 41, 99, 101 | lelttrd 8081 |
. 2
β’ (π β ((πΉβπ) β (πΉβπ)) < ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2))) |
103 | 40 | recnd 7985 |
. . . . . 6
β’ (π β (((πΉβ1)β2) / (4β(π β 1))) β
β) |
104 | 19 | nnrpd 9693 |
. . . . . . . 8
β’ (π β 2 β
β+) |
105 | 104, 37 | rpexpcld 10677 |
. . . . . . 7
β’ (π β (2β(π β 1)) β
β+) |
106 | 105 | rpcnd 9697 |
. . . . . 6
β’ (π β (2β(π β 1)) β
β) |
107 | | 2cnd 8991 |
. . . . . 6
β’ (π β 2 β
β) |
108 | 103, 106,
107 | mulassd 7980 |
. . . . 5
β’ (π β (((((πΉβ1)β2) / (4β(π β 1))) Β·
(2β(π β 1)))
Β· 2) = ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2))) |
109 | 30 | rpcnd 9697 |
. . . . . . . 8
β’ (π β ((πΉβ1)β2) β
β) |
110 | 38 | rpcnd 9697 |
. . . . . . . 8
β’ (π β (4β(π β 1)) β
β) |
111 | 38 | rpap0d 9701 |
. . . . . . . 8
β’ (π β (4β(π β 1)) # 0) |
112 | 109, 110,
106, 111 | div32apd 8770 |
. . . . . . 7
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
(2β(π β 1))) =
(((πΉβ1)β2)
Β· ((2β(π
β 1)) / (4β(π
β 1))))) |
113 | | 4d2e2 9078 |
. . . . . . . . . . . 12
β’ (4 / 2) =
2 |
114 | 113 | oveq1i 5884 |
. . . . . . . . . . 11
β’ ((4 /
2)β(π β 1)) =
(2β(π β
1)) |
115 | 34 | rpcnd 9697 |
. . . . . . . . . . . 12
β’ (π β 4 β
β) |
116 | 104 | rpap0d 9701 |
. . . . . . . . . . . 12
β’ (π β 2 # 0) |
117 | | nnm1nn0 9216 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
118 | 5, 117 | syl 14 |
. . . . . . . . . . . 12
β’ (π β (π β 1) β
β0) |
119 | 115, 107,
116, 118 | expdivapd 10667 |
. . . . . . . . . . 11
β’ (π β ((4 / 2)β(π β 1)) = ((4β(π β 1)) / (2β(π β 1)))) |
120 | 114, 119 | eqtr3id 2224 |
. . . . . . . . . 10
β’ (π β (2β(π β 1)) = ((4β(π β 1)) / (2β(π β 1)))) |
121 | 120 | oveq2d 5890 |
. . . . . . . . 9
β’ (π β (1 / (2β(π β 1))) = (1 /
((4β(π β 1)) /
(2β(π β
1))))) |
122 | 105 | rpap0d 9701 |
. . . . . . . . . 10
β’ (π β (2β(π β 1)) # 0) |
123 | 110, 106,
111, 122 | recdivapd 8763 |
. . . . . . . . 9
β’ (π β (1 / ((4β(π β 1)) / (2β(π β 1)))) = ((2β(π β 1)) / (4β(π β 1)))) |
124 | 121, 123 | eqtrd 2210 |
. . . . . . . 8
β’ (π β (1 / (2β(π β 1))) = ((2β(π β 1)) / (4β(π β 1)))) |
125 | 124 | oveq2d 5890 |
. . . . . . 7
β’ (π β (((πΉβ1)β2) Β· (1 /
(2β(π β 1)))) =
(((πΉβ1)β2)
Β· ((2β(π
β 1)) / (4β(π
β 1))))) |
126 | 112, 125 | eqtr4d 2213 |
. . . . . 6
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
(2β(π β 1))) =
(((πΉβ1)β2)
Β· (1 / (2β(π
β 1))))) |
127 | 126 | oveq1d 5889 |
. . . . 5
β’ (π β (((((πΉβ1)β2) / (4β(π β 1))) Β·
(2β(π β 1)))
Β· 2) = ((((πΉβ1)β2) Β· (1 /
(2β(π β 1))))
Β· 2)) |
128 | 108, 127 | eqtr3d 2212 |
. . . 4
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2)) = ((((πΉβ1)β2) Β· (1 /
(2β(π β 1))))
Β· 2)) |
129 | 106, 122 | recclapd 8737 |
. . . . 5
β’ (π β (1 / (2β(π β 1))) β
β) |
130 | 109, 129,
107 | mul32d 8109 |
. . . 4
β’ (π β ((((πΉβ1)β2) Β· (1 /
(2β(π β 1))))
Β· 2) = ((((πΉβ1)β2) Β· 2) Β· (1 /
(2β(π β
1))))) |
131 | 128, 130 | eqtrd 2210 |
. . 3
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2)) = ((((πΉβ1)β2) Β· 2) Β· (1 /
(2β(π β
1))))) |
132 | 109, 107 | mulcld 7977 |
. . . 4
β’ (π β (((πΉβ1)β2) Β· 2) β
β) |
133 | 132, 106,
122 | divrecapd 8749 |
. . 3
β’ (π β ((((πΉβ1)β2) Β· 2) /
(2β(π β 1))) =
((((πΉβ1)β2)
Β· 2) Β· (1 / (2β(π β 1))))) |
134 | 131, 133 | eqtr4d 2213 |
. 2
β’ (π β ((((πΉβ1)β2) / (4β(π β 1))) Β·
((2β(π β 1))
Β· 2)) = ((((πΉβ1)β2) Β· 2) /
(2β(π β
1)))) |
135 | 102, 134 | breqtrd 4029 |
1
β’ (π β ((πΉβπ) β (πΉβπ)) < ((((πΉβ1)β2) Β· 2) /
(2β(π β
1)))) |