Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6852 |
. . . . 5
β’ (π = 0 β (1st
β(πΊβπ)) = (1st
β(πΊβ0))) |
2 | | 2fveq3 6852 |
. . . . 5
β’ (π = 0 β (2nd
β(πΊβπ)) = (2nd
β(πΊβ0))) |
3 | 1, 2 | breq12d 5123 |
. . . 4
β’ (π = 0 β ((1st
β(πΊβπ)) < (2nd
β(πΊβπ)) β (1st
β(πΊβ0)) <
(2nd β(πΊβ0)))) |
4 | 3 | imbi2d 341 |
. . 3
β’ (π = 0 β ((π β (1st β(πΊβπ)) < (2nd β(πΊβπ))) β (π β (1st β(πΊβ0)) < (2nd
β(πΊβ0))))) |
5 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (1st β(πΊβπ)) = (1st β(πΊβπ))) |
6 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (2nd β(πΊβπ)) = (2nd β(πΊβπ))) |
7 | 5, 6 | breq12d 5123 |
. . . 4
β’ (π = π β ((1st β(πΊβπ)) < (2nd β(πΊβπ)) β (1st β(πΊβπ)) < (2nd β(πΊβπ)))) |
8 | 7 | imbi2d 341 |
. . 3
β’ (π = π β ((π β (1st β(πΊβπ)) < (2nd β(πΊβπ))) β (π β (1st β(πΊβπ)) < (2nd β(πΊβπ))))) |
9 | | 2fveq3 6852 |
. . . . 5
β’ (π = (π + 1) β (1st β(πΊβπ)) = (1st β(πΊβ(π + 1)))) |
10 | | 2fveq3 6852 |
. . . . 5
β’ (π = (π + 1) β (2nd β(πΊβπ)) = (2nd β(πΊβ(π + 1)))) |
11 | 9, 10 | breq12d 5123 |
. . . 4
β’ (π = (π + 1) β ((1st β(πΊβπ)) < (2nd β(πΊβπ)) β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1))))) |
12 | 11 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π β (1st β(πΊβπ)) < (2nd β(πΊβπ))) β (π β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1)))))) |
13 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (1st β(πΊβπ)) = (1st β(πΊβπ))) |
14 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (2nd β(πΊβπ)) = (2nd β(πΊβπ))) |
15 | 13, 14 | breq12d 5123 |
. . . 4
β’ (π = π β ((1st β(πΊβπ)) < (2nd β(πΊβπ)) β (1st β(πΊβπ)) < (2nd β(πΊβπ)))) |
16 | 15 | imbi2d 341 |
. . 3
β’ (π = π β ((π β (1st β(πΊβπ)) < (2nd β(πΊβπ))) β (π β (1st β(πΊβπ)) < (2nd β(πΊβπ))))) |
17 | | 0lt1 11684 |
. . . . 5
β’ 0 <
1 |
18 | 17 | a1i 11 |
. . . 4
β’ (π β 0 < 1) |
19 | | ruc.1 |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
20 | | ruc.2 |
. . . . . . 7
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
21 | | ruc.4 |
. . . . . . 7
β’ πΆ = ({β¨0, β¨0,
1β©β©} βͺ πΉ) |
22 | | ruc.5 |
. . . . . . 7
β’ πΊ = seq0(π·, πΆ) |
23 | 19, 20, 21, 22 | ruclem4 16123 |
. . . . . 6
β’ (π β (πΊβ0) = β¨0,
1β©) |
24 | 23 | fveq2d 6851 |
. . . . 5
β’ (π β (1st
β(πΊβ0)) =
(1st ββ¨0, 1β©)) |
25 | | c0ex 11156 |
. . . . . 6
β’ 0 β
V |
26 | | 1ex 11158 |
. . . . . 6
β’ 1 β
V |
27 | 25, 26 | op1st 7934 |
. . . . 5
β’
(1st ββ¨0, 1β©) = 0 |
28 | 24, 27 | eqtrdi 2793 |
. . . 4
β’ (π β (1st
β(πΊβ0)) =
0) |
29 | 23 | fveq2d 6851 |
. . . . 5
β’ (π β (2nd
β(πΊβ0)) =
(2nd ββ¨0, 1β©)) |
30 | 25, 26 | op2nd 7935 |
. . . . 5
β’
(2nd ββ¨0, 1β©) = 1 |
31 | 29, 30 | eqtrdi 2793 |
. . . 4
β’ (π β (2nd
β(πΊβ0)) =
1) |
32 | 18, 28, 31 | 3brtr4d 5142 |
. . 3
β’ (π β (1st
β(πΊβ0)) <
(2nd β(πΊβ0))) |
33 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β πΉ:ββΆβ) |
34 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
35 | 19, 20, 21, 22 | ruclem6 16124 |
. . . . . . . . . . . 12
β’ (π β πΊ:β0βΆ(β Γ
β)) |
36 | 35 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πΊβπ) β (β Γ
β)) |
37 | 36 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (πΊβπ) β (β Γ
β)) |
38 | | xp1st 7958 |
. . . . . . . . . 10
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (1st β(πΊβπ)) β β) |
40 | | xp2nd 7959 |
. . . . . . . . . 10
β’ ((πΊβπ) β (β Γ β) β
(2nd β(πΊβπ)) β β) |
41 | 37, 40 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (2nd β(πΊβπ)) β β) |
42 | | nn0p1nn 12459 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
β) |
43 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
44 | 19, 42, 43 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (πΉβ(π + 1)) β β) |
45 | 44 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (πΉβ(π + 1)) β β) |
46 | | eqid 2737 |
. . . . . . . . 9
β’
(1st β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) = (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
47 | | eqid 2737 |
. . . . . . . . 9
β’
(2nd β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) = (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
48 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (1st β(πΊβπ)) < (2nd β(πΊβπ))) |
49 | 33, 34, 39, 41, 45, 46, 47, 48 | ruclem2 16121 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β ((1st β(πΊβπ)) β€ (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β§ (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) < (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β§ (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β€ (2nd β(πΊβπ)))) |
50 | 49 | simp2d 1144 |
. . . . . . 7
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) < (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
51 | 19, 20, 21, 22 | ruclem7 16125 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (πΊβ(π + 1)) = ((πΊβπ)π·(πΉβ(π + 1)))) |
52 | 51 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (πΊβ(π + 1)) = ((πΊβπ)π·(πΉβ(π + 1)))) |
53 | | 1st2nd2 7965 |
. . . . . . . . . . 11
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
54 | 37, 53 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
55 | 54 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β ((πΊβπ)π·(πΉβ(π + 1))) = (β¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©π·(πΉβ(π + 1)))) |
56 | 52, 55 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (πΊβ(π + 1)) = (β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
57 | 56 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (1st β(πΊβ(π + 1))) = (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
58 | 56 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (2nd β(πΊβ(π + 1))) = (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
59 | 50, 57, 58 | 3brtr4d 5142 |
. . . . . 6
β’ ((π β§ (π β β0 β§
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1)))) |
60 | 59 | expr 458 |
. . . . 5
β’ ((π β§ π β β0) β
((1st β(πΊβπ)) < (2nd β(πΊβπ)) β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1))))) |
61 | 60 | expcom 415 |
. . . 4
β’ (π β β0
β (π β
((1st β(πΊβπ)) < (2nd β(πΊβπ)) β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1)))))) |
62 | 61 | a2d 29 |
. . 3
β’ (π β β0
β ((π β
(1st β(πΊβπ)) < (2nd β(πΊβπ))) β (π β (1st β(πΊβ(π + 1))) < (2nd β(πΊβ(π + 1)))))) |
63 | 4, 8, 12, 16, 32, 62 | nn0ind 12605 |
. 2
β’ (π β β0
β (π β
(1st β(πΊβπ)) < (2nd β(πΊβπ)))) |
64 | 63 | impcom 409 |
1
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) < (2nd β(πΊβπ))) |