Step | Hyp | Ref
| Expression |
1 | | oveq2 5882 |
. . . . . 6
β’ (π€ = 1 β (2βπ€) = (2β1)) |
2 | 1 | oveq2d 5890 |
. . . . 5
β’ (π€ = 1 β (1 / (2βπ€)) = (1 /
(2β1))) |
3 | | fveq2 5515 |
. . . . 5
β’ (π€ = 1 β (πΉβπ€) = (πΉβ1)) |
4 | 2, 3 | breq12d 4016 |
. . . 4
β’ (π€ = 1 β ((1 / (2βπ€)) < (πΉβπ€) β (1 / (2β1)) < (πΉβ1))) |
5 | 4 | imbi2d 230 |
. . 3
β’ (π€ = 1 β ((π β (1 / (2βπ€)) < (πΉβπ€)) β (π β (1 / (2β1)) < (πΉβ1)))) |
6 | | oveq2 5882 |
. . . . . 6
β’ (π€ = π β (2βπ€) = (2βπ)) |
7 | 6 | oveq2d 5890 |
. . . . 5
β’ (π€ = π β (1 / (2βπ€)) = (1 / (2βπ))) |
8 | | fveq2 5515 |
. . . . 5
β’ (π€ = π β (πΉβπ€) = (πΉβπ)) |
9 | 7, 8 | breq12d 4016 |
. . . 4
β’ (π€ = π β ((1 / (2βπ€)) < (πΉβπ€) β (1 / (2βπ)) < (πΉβπ))) |
10 | 9 | imbi2d 230 |
. . 3
β’ (π€ = π β ((π β (1 / (2βπ€)) < (πΉβπ€)) β (π β (1 / (2βπ)) < (πΉβπ)))) |
11 | | oveq2 5882 |
. . . . . 6
β’ (π€ = (π + 1) β (2βπ€) = (2β(π + 1))) |
12 | 11 | oveq2d 5890 |
. . . . 5
β’ (π€ = (π + 1) β (1 / (2βπ€)) = (1 / (2β(π + 1)))) |
13 | | fveq2 5515 |
. . . . 5
β’ (π€ = (π + 1) β (πΉβπ€) = (πΉβ(π + 1))) |
14 | 12, 13 | breq12d 4016 |
. . . 4
β’ (π€ = (π + 1) β ((1 / (2βπ€)) < (πΉβπ€) β (1 / (2β(π + 1))) < (πΉβ(π + 1)))) |
15 | 14 | imbi2d 230 |
. . 3
β’ (π€ = (π + 1) β ((π β (1 / (2βπ€)) < (πΉβπ€)) β (π β (1 / (2β(π + 1))) < (πΉβ(π + 1))))) |
16 | | oveq2 5882 |
. . . . . 6
β’ (π€ = π β (2βπ€) = (2βπ)) |
17 | 16 | oveq2d 5890 |
. . . . 5
β’ (π€ = π β (1 / (2βπ€)) = (1 / (2βπ))) |
18 | | fveq2 5515 |
. . . . 5
β’ (π€ = π β (πΉβπ€) = (πΉβπ)) |
19 | 17, 18 | breq12d 4016 |
. . . 4
β’ (π€ = π β ((1 / (2βπ€)) < (πΉβπ€) β (1 / (2βπ)) < (πΉβπ))) |
20 | 19 | imbi2d 230 |
. . 3
β’ (π€ = π β ((π β (1 / (2βπ€)) < (πΉβπ€)) β (π β (1 / (2βπ)) < (πΉβπ)))) |
21 | | 2cnd 8991 |
. . . . . . . 8
β’ (π β 2 β
β) |
22 | 21 | exp1d 10648 |
. . . . . . 7
β’ (π β (2β1) =
2) |
23 | | 2rp 9657 |
. . . . . . 7
β’ 2 β
β+ |
24 | 22, 23 | eqeltrdi 2268 |
. . . . . 6
β’ (π β (2β1) β
β+) |
25 | 24 | rprecred 9707 |
. . . . 5
β’ (π β (1 / (2β1)) β
β) |
26 | | 1red 7971 |
. . . . 5
β’ (π β 1 β
β) |
27 | | resqrexlemex.a |
. . . . . 6
β’ (π β π΄ β β) |
28 | 26, 27 | readdcld 7986 |
. . . . 5
β’ (π β (1 + π΄) β β) |
29 | 22 | oveq2d 5890 |
. . . . . 6
β’ (π β (1 / (2β1)) = (1 /
2)) |
30 | | halflt1 9135 |
. . . . . 6
β’ (1 / 2)
< 1 |
31 | 29, 30 | eqbrtrdi 4042 |
. . . . 5
β’ (π β (1 / (2β1)) <
1) |
32 | | resqrexlemex.agt0 |
. . . . . 6
β’ (π β 0 β€ π΄) |
33 | 26, 27 | addge01d 8489 |
. . . . . 6
β’ (π β (0 β€ π΄ β 1 β€ (1 + π΄))) |
34 | 32, 33 | mpbid 147 |
. . . . 5
β’ (π β 1 β€ (1 + π΄)) |
35 | 25, 26, 28, 31, 34 | ltletrd 8379 |
. . . 4
β’ (π β (1 / (2β1)) < (1 +
π΄)) |
36 | | resqrexlemex.seq |
. . . . 5
β’ πΉ = seq1((π¦ β β+, π§ β β+
β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) |
37 | 36, 27, 32 | resqrexlemf1 11016 |
. . . 4
β’ (π β (πΉβ1) = (1 + π΄)) |
38 | 35, 37 | breqtrrd 4031 |
. . 3
β’ (π β (1 / (2β1)) <
(πΉβ1)) |
39 | 23 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β 2 β
β+) |
40 | | nnz 9271 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
41 | 40 | ad2antlr 489 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β π β β€) |
42 | 39, 41 | rpexpcld 10677 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (2βπ) β
β+) |
43 | 42 | rpcnd 9697 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (2βπ) β β) |
44 | | 2cnd 8991 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β 2 β β) |
45 | 42 | rpap0d 9701 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (2βπ) # 0) |
46 | 39 | rpap0d 9701 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β 2 # 0) |
47 | 43, 44, 45, 46 | recdivap2d 8764 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β ((1 / (2βπ)) / 2) = (1 / ((2βπ) Β· 2))) |
48 | | nnnn0 9182 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
49 | 48 | ad2antlr 489 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β π β β0) |
50 | 44, 49 | expp1d 10654 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (2β(π + 1)) = ((2βπ) Β· 2)) |
51 | 50 | oveq2d 5890 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (1 / (2β(π + 1))) = (1 / ((2βπ) Β· 2))) |
52 | 47, 51 | eqtr4d 2213 |
. . . . . . 7
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β ((1 / (2βπ)) / 2) = (1 / (2β(π + 1)))) |
53 | 42 | rprecred 9707 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (1 / (2βπ)) β β) |
54 | 36, 27, 32 | resqrexlemf 11015 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆβ+) |
55 | 54 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβπ) β
β+) |
56 | 55 | rpred 9695 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβπ) β β) |
57 | 56 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (πΉβπ) β β) |
58 | 27 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π΄ β β) |
59 | 58, 55 | rerpdivcld 9727 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π΄ / (πΉβπ)) β β) |
60 | 59 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (π΄ / (πΉβπ)) β β) |
61 | 57, 60 | readdcld 7986 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β ((πΉβπ) + (π΄ / (πΉβπ))) β β) |
62 | | simpr 110 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (1 / (2βπ)) < (πΉβπ)) |
63 | 32 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β 0 β€ π΄) |
64 | 58, 55, 63 | divge0d 9736 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 β€ (π΄ / (πΉβπ))) |
65 | 56, 59 | addge01d 8489 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (0 β€ (π΄ / (πΉβπ)) β (πΉβπ) β€ ((πΉβπ) + (π΄ / (πΉβπ))))) |
66 | 64, 65 | mpbid 147 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβπ) β€ ((πΉβπ) + (π΄ / (πΉβπ)))) |
67 | 66 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (πΉβπ) β€ ((πΉβπ) + (π΄ / (πΉβπ)))) |
68 | 53, 57, 61, 62, 67 | ltletrd 8379 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (1 / (2βπ)) < ((πΉβπ) + (π΄ / (πΉβπ)))) |
69 | 53, 61, 39, 68 | ltdiv1dd 9753 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β ((1 / (2βπ)) / 2) < (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
70 | 36, 27, 32 | resqrexlemfp1 11017 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβ(π + 1)) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
71 | 70 | adantr 276 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (πΉβ(π + 1)) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) |
72 | 69, 71 | breqtrrd 4031 |
. . . . . . 7
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β ((1 / (2βπ)) / 2) < (πΉβ(π + 1))) |
73 | 52, 72 | eqbrtrrd 4027 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 / (2βπ)) < (πΉβπ)) β (1 / (2β(π + 1))) < (πΉβ(π + 1))) |
74 | 73 | ex 115 |
. . . . 5
β’ ((π β§ π β β) β ((1 / (2βπ)) < (πΉβπ) β (1 / (2β(π + 1))) < (πΉβ(π + 1)))) |
75 | 74 | expcom 116 |
. . . 4
β’ (π β β β (π β ((1 / (2βπ)) < (πΉβπ) β (1 / (2β(π + 1))) < (πΉβ(π + 1))))) |
76 | 75 | a2d 26 |
. . 3
β’ (π β β β ((π β (1 / (2βπ)) < (πΉβπ)) β (π β (1 / (2β(π + 1))) < (πΉβ(π + 1))))) |
77 | 5, 10, 15, 20, 38, 76 | nnind 8934 |
. 2
β’ (π β β β (π β (1 / (2βπ)) < (πΉβπ))) |
78 | 77 | impcom 125 |
1
β’ ((π β§ π β β) β (1 / (2βπ)) < (πΉβπ)) |