Step | Hyp | Ref
| Expression |
1 | | ruclem9.7 |
. 2
β’ (π β π β (β€β₯βπ)) |
2 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (1st β(πΊβπ)) = (1st β(πΊβπ))) |
3 | 2 | breq2d 5122 |
. . . . 5
β’ (π = π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β (1st β(πΊβπ)) β€ (1st β(πΊβπ)))) |
4 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (2nd β(πΊβπ)) = (2nd β(πΊβπ))) |
5 | 4 | breq1d 5120 |
. . . . 5
β’ (π = π β ((2nd β(πΊβπ)) β€ (2nd β(πΊβπ)) β (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
6 | 3, 5 | anbi12d 632 |
. . . 4
β’ (π = π β (((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))) β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))))) |
7 | 6 | imbi2d 341 |
. . 3
β’ (π = π β ((π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))))) |
8 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (1st β(πΊβπ)) = (1st β(πΊβπ))) |
9 | 8 | breq2d 5122 |
. . . . 5
β’ (π = π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β (1st β(πΊβπ)) β€ (1st β(πΊβπ)))) |
10 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (2nd β(πΊβπ)) = (2nd β(πΊβπ))) |
11 | 10 | breq1d 5120 |
. . . . 5
β’ (π = π β ((2nd β(πΊβπ)) β€ (2nd β(πΊβπ)) β (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
12 | 9, 11 | anbi12d 632 |
. . . 4
β’ (π = π β (((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))) β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))))) |
13 | 12 | imbi2d 341 |
. . 3
β’ (π = π β ((π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))))) |
14 | | 2fveq3 6852 |
. . . . . 6
β’ (π = (π + 1) β (1st β(πΊβπ)) = (1st β(πΊβ(π + 1)))) |
15 | 14 | breq2d 5122 |
. . . . 5
β’ (π = (π + 1) β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β (1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))))) |
16 | | 2fveq3 6852 |
. . . . . 6
β’ (π = (π + 1) β (2nd β(πΊβπ)) = (2nd β(πΊβ(π + 1)))) |
17 | 16 | breq1d 5120 |
. . . . 5
β’ (π = (π + 1) β ((2nd β(πΊβπ)) β€ (2nd β(πΊβπ)) β (2nd β(πΊβ(π + 1))) β€ (2nd β(πΊβπ)))) |
18 | 15, 17 | anbi12d 632 |
. . . 4
β’ (π = (π + 1) β (((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))) β ((1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))) β§ (2nd β(πΊβ(π + 1))) β€ (2nd β(πΊβπ))))) |
19 | 18 | imbi2d 341 |
. . 3
β’ (π = (π + 1) β ((π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))) β§ (2nd β(πΊβ(π + 1))) β€ (2nd β(πΊβπ)))))) |
20 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (1st β(πΊβπ)) = (1st β(πΊβπ))) |
21 | 20 | breq2d 5122 |
. . . . 5
β’ (π = π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β (1st β(πΊβπ)) β€ (1st β(πΊβπ)))) |
22 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (2nd β(πΊβπ)) = (2nd β(πΊβπ))) |
23 | 22 | breq1d 5120 |
. . . . 5
β’ (π = π β ((2nd β(πΊβπ)) β€ (2nd β(πΊβπ)) β (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
24 | 21, 23 | anbi12d 632 |
. . . 4
β’ (π = π β (((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))) β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))))) |
25 | 24 | imbi2d 341 |
. . 3
β’ (π = π β ((π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))))) |
26 | | ruc.1 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
27 | | ruc.2 |
. . . . . . . 8
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
28 | | ruc.4 |
. . . . . . . 8
β’ πΆ = ({β¨0, β¨0,
1β©β©} βͺ πΉ) |
29 | | ruc.5 |
. . . . . . . 8
β’ πΊ = seq0(π·, πΆ) |
30 | 26, 27, 28, 29 | ruclem6 16124 |
. . . . . . 7
β’ (π β πΊ:β0βΆ(β Γ
β)) |
31 | | ruclem9.6 |
. . . . . . 7
β’ (π β π β
β0) |
32 | 30, 31 | ffvelcdmd 7041 |
. . . . . 6
β’ (π β (πΊβπ) β (β Γ
β)) |
33 | | xp1st 7958 |
. . . . . 6
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
34 | 32, 33 | syl 17 |
. . . . 5
β’ (π β (1st
β(πΊβπ)) β
β) |
35 | 34 | leidd 11728 |
. . . 4
β’ (π β (1st
β(πΊβπ)) β€ (1st
β(πΊβπ))) |
36 | | xp2nd 7959 |
. . . . . 6
β’ ((πΊβπ) β (β Γ β) β
(2nd β(πΊβπ)) β β) |
37 | 32, 36 | syl 17 |
. . . . 5
β’ (π β (2nd
β(πΊβπ)) β
β) |
38 | 37 | leidd 11728 |
. . . 4
β’ (π β (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ))) |
39 | 35, 38 | jca 513 |
. . 3
β’ (π β ((1st
β(πΊβπ)) β€ (1st
β(πΊβπ)) β§ (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |
40 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β πΉ:ββΆβ) |
41 | 27 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
42 | 30 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β πΊ:β0βΆ(β Γ
β)) |
43 | | eluznn0 12849 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β
(β€β₯βπ)) β π β β0) |
44 | 31, 43 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β π β β0) |
45 | 42, 44 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β (β Γ
β)) |
46 | | xp1st 7958 |
. . . . . . . . . . 11
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβπ)) β
β) |
48 | | xp2nd 7959 |
. . . . . . . . . . 11
β’ ((πΊβπ) β (β Γ β) β
(2nd β(πΊβπ)) β β) |
49 | 45, 48 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(πΊβπ)) β
β) |
50 | | nn0p1nn 12459 |
. . . . . . . . . . . 12
β’ (π β β0
β (π + 1) β
β) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (π + 1) β β) |
52 | 40, 51 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (πΉβ(π + 1)) β β) |
53 | | eqid 2737 |
. . . . . . . . . 10
β’
(1st β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) = (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
54 | | eqid 2737 |
. . . . . . . . . 10
β’
(2nd β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) = (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
55 | 26, 27, 28, 29 | ruclem8 16126 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β
(1st β(πΊβπ)) < (2nd β(πΊβπ))) |
56 | 44, 55 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβπ)) < (2nd
β(πΊβπ))) |
57 | 40, 41, 47, 49, 52, 53, 54, 56 | ruclem2 16121 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β ((1st
β(πΊβπ)) β€ (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β§ (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) < (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β§ (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β€ (2nd β(πΊβπ)))) |
58 | 57 | simp1d 1143 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβπ)) β€ (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
59 | 26, 27, 28, 29 | ruclem7 16125 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πΊβ(π + 1)) = ((πΊβπ)π·(πΉβ(π + 1)))) |
60 | 44, 59 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (πΊβ(π + 1)) = ((πΊβπ)π·(πΉβ(π + 1)))) |
61 | | 1st2nd2 7965 |
. . . . . . . . . . . 12
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
62 | 45, 61 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
63 | 62 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β ((πΊβπ)π·(πΉβ(π + 1))) = (β¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©π·(πΉβ(π + 1)))) |
64 | 60, 63 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (πΊβ(π + 1)) = (β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) |
65 | 64 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβ(π + 1))) = (1st
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
66 | 58, 65 | breqtrrd 5138 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβπ)) β€ (1st
β(πΊβ(π + 1)))) |
67 | 34 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβπ)) β
β) |
68 | | peano2nn0 12460 |
. . . . . . . . . . 11
β’ (π β β0
β (π + 1) β
β0) |
69 | 44, 68 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (π + 1) β
β0) |
70 | 42, 69 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (πΊβ(π + 1)) β (β Γ
β)) |
71 | | xp1st 7958 |
. . . . . . . . 9
β’ ((πΊβ(π + 1)) β (β Γ β)
β (1st β(πΊβ(π + 1))) β β) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1st
β(πΊβ(π + 1))) β
β) |
73 | | letr 11256 |
. . . . . . . 8
β’
(((1st β(πΊβπ)) β β β§ (1st
β(πΊβπ)) β β β§
(1st β(πΊβ(π + 1))) β β) β
(((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1)))) β (1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))))) |
74 | 67, 47, 72, 73 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (((1st
β(πΊβπ)) β€ (1st
β(πΊβπ)) β§ (1st
β(πΊβπ)) β€ (1st
β(πΊβ(π + 1)))) β (1st
β(πΊβπ)) β€ (1st
β(πΊβ(π + 1))))) |
75 | 66, 74 | mpan2d 693 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((1st
β(πΊβπ)) β€ (1st
β(πΊβπ)) β (1st
β(πΊβπ)) β€ (1st
β(πΊβ(π + 1))))) |
76 | 64 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(πΊβ(π + 1))) = (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1))))) |
77 | 57 | simp3d 1145 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©π·(πΉβ(π + 1)))) β€ (2nd β(πΊβπ))) |
78 | 76, 77 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ))) |
79 | | xp2nd 7959 |
. . . . . . . . 9
β’ ((πΊβ(π + 1)) β (β Γ β)
β (2nd β(πΊβ(π + 1))) β β) |
80 | 70, 79 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(πΊβ(π + 1))) β
β) |
81 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (2nd
β(πΊβπ)) β
β) |
82 | | letr 11256 |
. . . . . . . 8
β’
(((2nd β(πΊβ(π + 1))) β β β§ (2nd
β(πΊβπ)) β β β§
(2nd β(πΊβπ)) β β) β (((2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ)) β§ (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ))) β (2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ)))) |
83 | 80, 49, 81, 82 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (((2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ)) β§ (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ))) β (2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ)))) |
84 | 78, 83 | mpand 694 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ)) β (2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ)))) |
85 | 75, 84 | anim12d 610 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (((1st
β(πΊβπ)) β€ (1st
β(πΊβπ)) β§ (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ))) β ((1st
β(πΊβπ)) β€ (1st
β(πΊβ(π + 1))) β§ (2nd
β(πΊβ(π + 1))) β€ (2nd
β(πΊβπ))))) |
86 | 85 | expcom 415 |
. . . 4
β’ (π β
(β€β₯βπ) β (π β (((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))) β ((1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))) β§ (2nd β(πΊβ(π + 1))) β€ (2nd β(πΊβπ)))))) |
87 | 86 | a2d 29 |
. . 3
β’ (π β
(β€β₯βπ) β ((π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβ(π + 1))) β§ (2nd β(πΊβ(π + 1))) β€ (2nd β(πΊβπ)))))) |
88 | 7, 13, 19, 25, 39, 87 | uzind4i 12842 |
. 2
β’ (π β
(β€β₯βπ) β (π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ))))) |
89 | 1, 88 | mpcom 38 |
1
β’ (π β ((1st
β(πΊβπ)) β€ (1st
β(πΊβπ)) β§ (2nd
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |