Step | Hyp | Ref
| Expression |
1 | | ruc.5 |
. . . . . . 7
β’ πΊ = seq0(π·, πΆ) |
2 | 1 | fveq1i 6848 |
. . . . . 6
β’ (πΊβ0) = (seq0(π·, πΆ)β0) |
3 | | 0z 12517 |
. . . . . . 7
β’ 0 β
β€ |
4 | | seq1 13926 |
. . . . . . 7
β’ (0 β
β€ β (seq0(π·,
πΆ)β0) = (πΆβ0)) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
β’
(seq0(π·, πΆ)β0) = (πΆβ0) |
6 | 2, 5 | eqtri 2765 |
. . . . 5
β’ (πΊβ0) = (πΆβ0) |
7 | | ruc.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
8 | | ruc.2 |
. . . . . 6
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
9 | | ruc.4 |
. . . . . 6
β’ πΆ = ({β¨0, β¨0,
1β©β©} βͺ πΉ) |
10 | 7, 8, 9, 1 | ruclem4 16123 |
. . . . 5
β’ (π β (πΊβ0) = β¨0,
1β©) |
11 | 6, 10 | eqtr3id 2791 |
. . . 4
β’ (π β (πΆβ0) = β¨0,
1β©) |
12 | | 0re 11164 |
. . . . 5
β’ 0 β
β |
13 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
14 | | opelxpi 5675 |
. . . . 5
β’ ((0
β β β§ 1 β β) β β¨0, 1β© β (β
Γ β)) |
15 | 12, 13, 14 | mp2an 691 |
. . . 4
β’ β¨0,
1β© β (β Γ β) |
16 | 11, 15 | eqeltrdi 2846 |
. . 3
β’ (π β (πΆβ0) β (β Γ
β)) |
17 | | 1st2nd2 7965 |
. . . . . 6
β’ (π§ β (β Γ
β) β π§ =
β¨(1st βπ§), (2nd βπ§)β©) |
18 | 17 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β π§ = β¨(1st
βπ§), (2nd
βπ§)β©) |
19 | 18 | oveq1d 7377 |
. . . 4
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β (π§π·π€) = (β¨(1st βπ§), (2nd βπ§)β©π·π€)) |
20 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β πΉ:ββΆβ) |
21 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
22 | | xp1st 7958 |
. . . . . . 7
β’ (π§ β (β Γ
β) β (1st βπ§) β β) |
23 | 22 | ad2antrl 727 |
. . . . . 6
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β
(1st βπ§)
β β) |
24 | | xp2nd 7959 |
. . . . . . 7
β’ (π§ β (β Γ
β) β (2nd βπ§) β β) |
25 | 24 | ad2antrl 727 |
. . . . . 6
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β
(2nd βπ§)
β β) |
26 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β π€ β
β) |
27 | | eqid 2737 |
. . . . . 6
β’
(1st β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) = (1st
β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) |
28 | | eqid 2737 |
. . . . . 6
β’
(2nd β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) = (2nd
β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) |
29 | 20, 21, 23, 25, 26, 27, 28 | ruclem1 16120 |
. . . . 5
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β
((β¨(1st βπ§), (2nd βπ§)β©π·π€) β (β Γ β) β§
(1st β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) = if((((1st βπ§) + (2nd βπ§)) / 2) < π€, (1st βπ§), (((((1st βπ§) + (2nd βπ§)) / 2) + (2nd
βπ§)) / 2)) β§
(2nd β(β¨(1st βπ§), (2nd βπ§)β©π·π€)) = if((((1st βπ§) + (2nd βπ§)) / 2) < π€, (((1st βπ§) + (2nd βπ§)) / 2), (2nd βπ§)))) |
30 | 29 | simp1d 1143 |
. . . 4
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β
(β¨(1st βπ§), (2nd βπ§)β©π·π€) β (β Γ
β)) |
31 | 19, 30 | eqeltrd 2838 |
. . 3
β’ ((π β§ (π§ β (β Γ β) β§ π€ β β)) β (π§π·π€) β (β Γ
β)) |
32 | | nn0uz 12812 |
. . 3
β’
β0 = (β€β₯β0) |
33 | | 0zd 12518 |
. . 3
β’ (π β 0 β
β€) |
34 | | 0p1e1 12282 |
. . . . . . 7
β’ (0 + 1) =
1 |
35 | 34 | fveq2i 6850 |
. . . . . 6
β’
(β€β₯β(0 + 1)) =
(β€β₯β1) |
36 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
37 | 35, 36 | eqtr4i 2768 |
. . . . 5
β’
(β€β₯β(0 + 1)) = β |
38 | 37 | eleq2i 2830 |
. . . 4
β’ (π§ β
(β€β₯β(0 + 1)) β π§ β β) |
39 | 9 | equncomi 4120 |
. . . . . . . 8
β’ πΆ = (πΉ βͺ {β¨0, β¨0,
1β©β©}) |
40 | 39 | fveq1i 6848 |
. . . . . . 7
β’ (πΆβπ§) = ((πΉ βͺ {β¨0, β¨0,
1β©β©})βπ§) |
41 | | nnne0 12194 |
. . . . . . . . 9
β’ (π§ β β β π§ β 0) |
42 | 41 | necomd 3000 |
. . . . . . . 8
β’ (π§ β β β 0 β
π§) |
43 | | fvunsn 7130 |
. . . . . . . 8
β’ (0 β
π§ β ((πΉ βͺ {β¨0, β¨0,
1β©β©})βπ§) =
(πΉβπ§)) |
44 | 42, 43 | syl 17 |
. . . . . . 7
β’ (π§ β β β ((πΉ βͺ {β¨0, β¨0,
1β©β©})βπ§) =
(πΉβπ§)) |
45 | 40, 44 | eqtrid 2789 |
. . . . . 6
β’ (π§ β β β (πΆβπ§) = (πΉβπ§)) |
46 | 45 | adantl 483 |
. . . . 5
β’ ((π β§ π§ β β) β (πΆβπ§) = (πΉβπ§)) |
47 | 7 | ffvelcdmda 7040 |
. . . . 5
β’ ((π β§ π§ β β) β (πΉβπ§) β β) |
48 | 46, 47 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π§ β β) β (πΆβπ§) β β) |
49 | 38, 48 | sylan2b 595 |
. . 3
β’ ((π β§ π§ β (β€β₯β(0 +
1))) β (πΆβπ§) β
β) |
50 | 16, 31, 32, 33, 49 | seqf2 13934 |
. 2
β’ (π β seq0(π·, πΆ):β0βΆ(β
Γ β)) |
51 | 1 | feq1i 6664 |
. 2
β’ (πΊ:β0βΆ(β Γ
β) β seq0(π·,
πΆ):β0βΆ(β
Γ β)) |
52 | 50, 51 | sylibr 233 |
1
β’ (π β πΊ:β0βΆ(β Γ
β)) |