Step | Hyp | Ref
| Expression |
1 | | ruc.6 |
. . 3
β’ π = sup(ran (1st
β πΊ), β, <
) |
2 | | ruc.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
3 | | ruc.2 |
. . . . . 6
β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
4 | | ruc.4 |
. . . . . 6
β’ πΆ = ({β¨0, β¨0,
1β©β©} βͺ πΉ) |
5 | | ruc.5 |
. . . . . 6
β’ πΊ = seq0(π·, πΆ) |
6 | 2, 3, 4, 5 | ruclem11 16129 |
. . . . 5
β’ (π β (ran (1st
β πΊ) β β
β§ ran (1st β πΊ) β β
β§ βπ§ β ran (1st
β πΊ)π§ β€ 1)) |
7 | 6 | simp1d 1143 |
. . . 4
β’ (π β ran (1st
β πΊ) β
β) |
8 | 6 | simp2d 1144 |
. . . 4
β’ (π β ran (1st
β πΊ) β
β
) |
9 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
10 | 6 | simp3d 1145 |
. . . . 5
β’ (π β βπ§ β ran (1st β πΊ)π§ β€ 1) |
11 | | brralrspcev 5170 |
. . . . 5
β’ ((1
β β β§ βπ§ β ran (1st β πΊ)π§ β€ 1) β βπ β β βπ§ β ran (1st β πΊ)π§ β€ π) |
12 | 9, 10, 11 | sylancr 588 |
. . . 4
β’ (π β βπ β β βπ§ β ran (1st β πΊ)π§ β€ π) |
13 | 7, 8, 12 | suprcld 12125 |
. . 3
β’ (π β sup(ran (1st
β πΊ), β, < )
β β) |
14 | 1, 13 | eqeltrid 2842 |
. 2
β’ (π β π β β) |
15 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ:ββΆβ) |
16 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
17 | 2, 3, 4, 5 | ruclem6 16124 |
. . . . . . . . . . 11
β’ (π β πΊ:β0βΆ(β Γ
β)) |
18 | | nnm1nn0 12461 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β0) |
19 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((πΊ:β0βΆ(β Γ
β) β§ (π β
1) β β0) β (πΊβ(π β 1)) β (β Γ
β)) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΊβ(π β 1)) β (β Γ
β)) |
21 | | xp1st 7958 |
. . . . . . . . . 10
β’ ((πΊβ(π β 1)) β (β Γ β)
β (1st β(πΊβ(π β 1))) β
β) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1st
β(πΊβ(π β 1))) β
β) |
23 | | xp2nd 7959 |
. . . . . . . . . 10
β’ ((πΊβ(π β 1)) β (β Γ β)
β (2nd β(πΊβ(π β 1))) β
β) |
24 | 20, 23 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (2nd
β(πΊβ(π β 1))) β
β) |
25 | 2 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) β β) |
26 | | eqid 2737 |
. . . . . . . . 9
β’
(1st β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) = (1st
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) |
27 | | eqid 2737 |
. . . . . . . . 9
β’
(2nd β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) = (2nd
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) |
28 | 2, 3, 4, 5 | ruclem8 16126 |
. . . . . . . . . 10
β’ ((π β§ (π β 1) β β0)
β (1st β(πΊβ(π β 1))) < (2nd
β(πΊβ(π β 1)))) |
29 | 18, 28 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1st
β(πΊβ(π β 1))) <
(2nd β(πΊβ(π β 1)))) |
30 | 15, 16, 22, 24, 25, 26, 27, 29 | ruclem3 16122 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβπ) < (1st
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) β¨ (2nd
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) < (πΉβπ))) |
31 | 2, 3, 4, 5 | ruclem7 16125 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β 1) β β0)
β (πΊβ((π β 1) + 1)) = ((πΊβ(π β 1))π·(πΉβ((π β 1) + 1)))) |
32 | 18, 31 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΊβ((π β 1) + 1)) = ((πΊβ(π β 1))π·(πΉβ((π β 1) + 1)))) |
33 | | nncn 12168 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
34 | 33 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
35 | | ax-1cn 11116 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
36 | | npcan 11417 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
37 | 34, 35, 36 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π β 1) + 1) = π) |
38 | 37 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΊβ((π β 1) + 1)) = (πΊβπ)) |
39 | | 1st2nd2 7965 |
. . . . . . . . . . . . . 14
β’ ((πΊβ(π β 1)) β (β Γ β)
β (πΊβ(π β 1)) =
β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©) |
40 | 20, 39 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΊβ(π β 1)) = β¨(1st
β(πΊβ(π β 1))), (2nd
β(πΊβ(π β
1)))β©) |
41 | 37 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβ((π β 1) + 1)) = (πΉβπ)) |
42 | 40, 41 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΊβ(π β 1))π·(πΉβ((π β 1) + 1))) = (β¨(1st
β(πΊβ(π β 1))), (2nd
β(πΊβ(π β 1)))β©π·(πΉβπ))) |
43 | 32, 38, 42 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΊβπ) = (β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) |
44 | 43 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1st
β(πΊβπ)) = (1st
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ)))) |
45 | 44 | breq2d 5122 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΉβπ) < (1st β(πΊβπ)) β (πΉβπ) < (1st
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))))) |
46 | 43 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (2nd
β(πΊβπ)) = (2nd
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ)))) |
47 | 46 | breq1d 5120 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((2nd
β(πΊβπ)) < (πΉβπ) β (2nd
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) < (πΉβπ))) |
48 | 45, 47 | orbi12d 918 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πΉβπ) < (1st β(πΊβπ)) β¨ (2nd β(πΊβπ)) < (πΉβπ)) β ((πΉβπ) < (1st
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) β¨ (2nd
β(β¨(1st β(πΊβ(π β 1))), (2nd β(πΊβ(π β 1)))β©π·(πΉβπ))) < (πΉβπ)))) |
49 | 30, 48 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΉβπ) < (1st β(πΊβπ)) β¨ (2nd β(πΊβπ)) < (πΉβπ))) |
50 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ran (1st
β πΊ) β
β) |
51 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ran (1st
β πΊ) β
β
) |
52 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β βπ β β βπ§ β ran (1st
β πΊ)π§ β€ π) |
53 | | nnnn0 12427 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
54 | | fvco3 6945 |
. . . . . . . . . . . . 13
β’ ((πΊ:β0βΆ(β Γ
β) β§ π β
β0) β ((1st β πΊ)βπ) = (1st β(πΊβπ))) |
55 | 17, 53, 54 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((1st
β πΊ)βπ) = (1st
β(πΊβπ))) |
56 | 17 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β πΊ:β0βΆ(β Γ
β)) |
57 | | 1stcof 7956 |
. . . . . . . . . . . . . 14
β’ (πΊ:β0βΆ(β Γ
β) β (1st β πΊ):β0βΆβ) |
58 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’
((1st β πΊ):β0βΆβ β
(1st β πΊ)
Fn β0) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (1st
β πΊ) Fn
β0) |
60 | 53 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β0) |
61 | | fnfvelrn 7036 |
. . . . . . . . . . . . 13
β’
(((1st β πΊ) Fn β0 β§ π β β0)
β ((1st β πΊ)βπ) β ran (1st β πΊ)) |
62 | 59, 60, 61 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((1st
β πΊ)βπ) β ran (1st
β πΊ)) |
63 | 55, 62 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (1st
β(πΊβπ)) β ran (1st
β πΊ)) |
64 | 50, 51, 52, 63 | suprubd 12124 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1st
β(πΊβπ)) β€ sup(ran (1st
β πΊ), β, <
)) |
65 | 64, 1 | breqtrrdi 5152 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1st
β(πΊβπ)) β€ π) |
66 | | ffvelcdm 7037 |
. . . . . . . . . . . 12
β’ ((πΊ:β0βΆ(β Γ
β) β§ π β
β0) β (πΊβπ) β (β Γ
β)) |
67 | 17, 53, 66 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΊβπ) β (β Γ
β)) |
68 | | xp1st 7958 |
. . . . . . . . . . 11
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1st
β(πΊβπ)) β
β) |
70 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
71 | | ltletr 11254 |
. . . . . . . . . 10
β’ (((πΉβπ) β β β§ (1st
β(πΊβπ)) β β β§ π β β) β (((πΉβπ) < (1st β(πΊβπ)) β§ (1st β(πΊβπ)) β€ π) β (πΉβπ) < π)) |
72 | 25, 69, 70, 71 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((πΉβπ) < (1st β(πΊβπ)) β§ (1st β(πΊβπ)) β€ π) β (πΉβπ) < π)) |
73 | 65, 72 | mpan2d 693 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβπ) < (1st β(πΊβπ)) β (πΉβπ) < π)) |
74 | | fvco3 6945 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:β0βΆ(β Γ
β) β§ π β
β0) β ((1st β πΊ)βπ) = (1st β(πΊβπ))) |
75 | 56, 74 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β β0) β
((1st β πΊ)βπ) = (1st β(πΊβπ))) |
76 | 56 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β (πΊβπ) β (β Γ
β)) |
77 | | xp1st 7958 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπ) β (β Γ β) β
(1st β(πΊβπ)) β β) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β0) β
(1st β(πΊβπ)) β β) |
79 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊβπ) β (β Γ β) β
(2nd β(πΊβπ)) β β) |
80 | 67, 79 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2nd
β(πΊβπ)) β
β) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β0) β
(2nd β(πΊβπ)) β β) |
82 | 15 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β πΉ:ββΆβ) |
83 | 16 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β π· = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
84 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β π β
β0) |
85 | 60 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β β0) β π β
β0) |
86 | 82, 83, 4, 5, 84, 85 | ruclem10 16128 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β0) β
(1st β(πΊβπ)) < (2nd β(πΊβπ))) |
87 | 78, 81, 86 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β β0) β
(1st β(πΊβπ)) β€ (2nd β(πΊβπ))) |
88 | 75, 87 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β β0) β
((1st β πΊ)βπ) β€ (2nd β(πΊβπ))) |
89 | 88 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β βπ β β0
((1st β πΊ)βπ) β€ (2nd β(πΊβπ))) |
90 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π§ = ((1st β
πΊ)βπ) β (π§ β€ (2nd β(πΊβπ)) β ((1st β πΊ)βπ) β€ (2nd β(πΊβπ)))) |
91 | 90 | ralrn 7043 |
. . . . . . . . . . . . 13
β’
((1st β πΊ) Fn β0 β
(βπ§ β ran
(1st β πΊ)π§ β€ (2nd β(πΊβπ)) β βπ β β0 ((1st
β πΊ)βπ) β€ (2nd
β(πΊβπ)))) |
92 | 59, 91 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (βπ§ β ran (1st
β πΊ)π§ β€ (2nd
β(πΊβπ)) β βπ β β0
((1st β πΊ)βπ) β€ (2nd β(πΊβπ)))) |
93 | 89, 92 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β βπ§ β ran (1st
β πΊ)π§ β€ (2nd
β(πΊβπ))) |
94 | | suprleub 12128 |
. . . . . . . . . . . 12
β’ (((ran
(1st β πΊ)
β β β§ ran (1st β πΊ) β β
β§ βπ β β βπ§ β ran (1st
β πΊ)π§ β€ π) β§ (2nd β(πΊβπ)) β β) β (sup(ran
(1st β πΊ),
β, < ) β€ (2nd β(πΊβπ)) β βπ§ β ran (1st β πΊ)π§ β€ (2nd β(πΊβπ)))) |
95 | 50, 51, 52, 80, 94 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (sup(ran
(1st β πΊ),
β, < ) β€ (2nd β(πΊβπ)) β βπ§ β ran (1st β πΊ)π§ β€ (2nd β(πΊβπ)))) |
96 | 93, 95 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π β β) β sup(ran
(1st β πΊ),
β, < ) β€ (2nd β(πΊβπ))) |
97 | 1, 96 | eqbrtrid 5145 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β€ (2nd β(πΊβπ))) |
98 | | lelttr 11252 |
. . . . . . . . . 10
β’ ((π β β β§
(2nd β(πΊβπ)) β β β§ (πΉβπ) β β) β ((π β€ (2nd β(πΊβπ)) β§ (2nd β(πΊβπ)) < (πΉβπ)) β π < (πΉβπ))) |
99 | 70, 80, 25, 98 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π β€ (2nd β(πΊβπ)) β§ (2nd β(πΊβπ)) < (πΉβπ)) β π < (πΉβπ))) |
100 | 97, 99 | mpand 694 |
. . . . . . . 8
β’ ((π β§ π β β) β ((2nd
β(πΊβπ)) < (πΉβπ) β π < (πΉβπ))) |
101 | 73, 100 | orim12d 964 |
. . . . . . 7
β’ ((π β§ π β β) β (((πΉβπ) < (1st β(πΊβπ)) β¨ (2nd β(πΊβπ)) < (πΉβπ)) β ((πΉβπ) < π β¨ π < (πΉβπ)))) |
102 | 49, 101 | mpd 15 |
. . . . . 6
β’ ((π β§ π β β) β ((πΉβπ) < π β¨ π < (πΉβπ))) |
103 | 25, 70 | lttri2d 11301 |
. . . . . 6
β’ ((π β§ π β β) β ((πΉβπ) β π β ((πΉβπ) < π β¨ π < (πΉβπ)))) |
104 | 102, 103 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) β π) |
105 | 104 | neneqd 2949 |
. . . 4
β’ ((π β§ π β β) β Β¬ (πΉβπ) = π) |
106 | 105 | nrexdv 3147 |
. . 3
β’ (π β Β¬ βπ β β (πΉβπ) = π) |
107 | | risset 3224 |
. . . 4
β’ (π β ran πΉ β βπ§ β ran πΉ π§ = π) |
108 | | ffn 6673 |
. . . . 5
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
109 | | eqeq1 2741 |
. . . . . 6
β’ (π§ = (πΉβπ) β (π§ = π β (πΉβπ) = π)) |
110 | 109 | rexrn 7042 |
. . . . 5
β’ (πΉ Fn β β (βπ§ β ran πΉ π§ = π β βπ β β (πΉβπ) = π)) |
111 | 2, 108, 110 | 3syl 18 |
. . . 4
β’ (π β (βπ§ β ran πΉ π§ = π β βπ β β (πΉβπ) = π)) |
112 | 107, 111 | bitrid 283 |
. . 3
β’ (π β (π β ran πΉ β βπ β β (πΉβπ) = π)) |
113 | 106, 112 | mtbird 325 |
. 2
β’ (π β Β¬ π β ran πΉ) |
114 | 14, 113 | eldifd 3926 |
1
β’ (π β π β (β β ran πΉ)) |