Step | Hyp | Ref
| Expression |
1 | | ovex 7395 |
. 2
β’ (0[,]1)
β V |
2 | | elpwi 4572 |
. . . . 5
β’ (π¦ β π« β β
π¦ β
β) |
3 | | nnuz 12813 |
. . . . . . 7
β’ β =
(β€β₯β1) |
4 | 3 | sumeq1i 15590 |
. . . . . 6
β’
Ξ£π β
β ((πΉβπ¦)βπ) = Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) |
5 | | 1nn 12171 |
. . . . . . 7
β’ 1 β
β |
6 | | rpnnen2.1 |
. . . . . . . 8
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) |
7 | 6 | rpnnen2lem6 16108 |
. . . . . . 7
β’ ((π¦ β β β§ 1 β
β) β Ξ£π
β (β€β₯β1)((πΉβπ¦)βπ) β β) |
8 | 5, 7 | mpan2 690 |
. . . . . 6
β’ (π¦ β β β
Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) β β) |
9 | 4, 8 | eqeltrid 2842 |
. . . . 5
β’ (π¦ β β β
Ξ£π β β
((πΉβπ¦)βπ) β β) |
10 | 2, 9 | syl 17 |
. . . 4
β’ (π¦ β π« β β
Ξ£π β β
((πΉβπ¦)βπ) β β) |
11 | | 1zzd 12541 |
. . . . 5
β’ (π¦ β π« β β
1 β β€) |
12 | | eqidd 2738 |
. . . . 5
β’ ((π¦ β π« β β§
π β β) β
((πΉβπ¦)βπ) = ((πΉβπ¦)βπ)) |
13 | 6 | rpnnen2lem2 16104 |
. . . . . . 7
β’ (π¦ β β β (πΉβπ¦):ββΆβ) |
14 | 2, 13 | syl 17 |
. . . . . 6
β’ (π¦ β π« β β
(πΉβπ¦):ββΆβ) |
15 | 14 | ffvelcdmda 7040 |
. . . . 5
β’ ((π¦ β π« β β§
π β β) β
((πΉβπ¦)βπ) β β) |
16 | 6 | rpnnen2lem5 16107 |
. . . . . 6
β’ ((π¦ β β β§ 1 β
β) β seq1( + , (πΉβπ¦)) β dom β ) |
17 | 2, 5, 16 | sylancl 587 |
. . . . 5
β’ (π¦ β π« β β
seq1( + , (πΉβπ¦)) β dom β
) |
18 | | ssid 3971 |
. . . . . . . 8
β’ β
β β |
19 | 6 | rpnnen2lem4 16106 |
. . . . . . . 8
β’ ((π¦ β β β§ β
β β β§ π
β β) β (0 β€ ((πΉβπ¦)βπ) β§ ((πΉβπ¦)βπ) β€ ((πΉββ)βπ))) |
20 | 18, 19 | mp3an2 1450 |
. . . . . . 7
β’ ((π¦ β β β§ π β β) β (0 β€
((πΉβπ¦)βπ) β§ ((πΉβπ¦)βπ) β€ ((πΉββ)βπ))) |
21 | 20 | simpld 496 |
. . . . . 6
β’ ((π¦ β β β§ π β β) β 0 β€
((πΉβπ¦)βπ)) |
22 | 2, 21 | sylan 581 |
. . . . 5
β’ ((π¦ β π« β β§
π β β) β 0
β€ ((πΉβπ¦)βπ)) |
23 | 3, 11, 12, 15, 17, 22 | isumge0 15658 |
. . . 4
β’ (π¦ β π« β β
0 β€ Ξ£π β
β ((πΉβπ¦)βπ)) |
24 | | halfre 12374 |
. . . . . 6
β’ (1 / 2)
β β |
25 | 24 | a1i 11 |
. . . . 5
β’ (π¦ β π« β β
(1 / 2) β β) |
26 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
27 | 26 | a1i 11 |
. . . . 5
β’ (π¦ β π« β β
1 β β) |
28 | 6 | rpnnen2lem7 16109 |
. . . . . . . . 9
β’ ((π¦ β β β§ β
β β β§ 1 β β) β Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) β€ Ξ£π β
(β€β₯β1)((πΉββ)βπ)) |
29 | 18, 5, 28 | mp3an23 1454 |
. . . . . . . 8
β’ (π¦ β β β
Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) β€ Ξ£π β
(β€β₯β1)((πΉββ)βπ)) |
30 | 2, 29 | syl 17 |
. . . . . . 7
β’ (π¦ β π« β β
Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) β€ Ξ£π β
(β€β₯β1)((πΉββ)βπ)) |
31 | | eqid 2737 |
. . . . . . . 8
β’
(β€β₯β1) =
(β€β₯β1) |
32 | | eqidd 2738 |
. . . . . . . 8
β’ ((π¦ β π« β β§
π β
(β€β₯β1)) β ((πΉββ)βπ) = ((πΉββ)βπ)) |
33 | | elnnuz 12814 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β1)) |
34 | 6 | rpnnen2lem2 16104 |
. . . . . . . . . . . . 13
β’ (β
β β β (πΉββ):ββΆβ) |
35 | 18, 34 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (πΉββ):ββΆβ |
36 | 35 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ (π β β β ((πΉββ)βπ) β
β) |
37 | 36 | recnd 11190 |
. . . . . . . . . 10
β’ (π β β β ((πΉββ)βπ) β
β) |
38 | 33, 37 | sylbir 234 |
. . . . . . . . 9
β’ (π β
(β€β₯β1) β ((πΉββ)βπ) β β) |
39 | 38 | adantl 483 |
. . . . . . . 8
β’ ((π¦ β π« β β§
π β
(β€β₯β1)) β ((πΉββ)βπ) β β) |
40 | 6 | rpnnen2lem3 16105 |
. . . . . . . . 9
β’ seq1( + ,
(πΉββ)) β
(1 / 2) |
41 | 40 | a1i 11 |
. . . . . . . 8
β’ (π¦ β π« β β
seq1( + , (πΉββ)) β (1 /
2)) |
42 | 31, 11, 32, 39, 41 | isumclim 15649 |
. . . . . . 7
β’ (π¦ β π« β β
Ξ£π β
(β€β₯β1)((πΉββ)βπ) = (1 / 2)) |
43 | 30, 42 | breqtrd 5136 |
. . . . . 6
β’ (π¦ β π« β β
Ξ£π β
(β€β₯β1)((πΉβπ¦)βπ) β€ (1 / 2)) |
44 | 4, 43 | eqbrtrid 5145 |
. . . . 5
β’ (π¦ β π« β β
Ξ£π β β
((πΉβπ¦)βπ) β€ (1 / 2)) |
45 | | halflt1 12378 |
. . . . . . 7
β’ (1 / 2)
< 1 |
46 | 24, 26, 45 | ltleii 11285 |
. . . . . 6
β’ (1 / 2)
β€ 1 |
47 | 46 | a1i 11 |
. . . . 5
β’ (π¦ β π« β β
(1 / 2) β€ 1) |
48 | 10, 25, 27, 44, 47 | letrd 11319 |
. . . 4
β’ (π¦ β π« β β
Ξ£π β β
((πΉβπ¦)βπ) β€ 1) |
49 | | elicc01 13390 |
. . . 4
β’
(Ξ£π β
β ((πΉβπ¦)βπ) β (0[,]1) β (Ξ£π β β ((πΉβπ¦)βπ) β β β§ 0 β€ Ξ£π β β ((πΉβπ¦)βπ) β§ Ξ£π β β ((πΉβπ¦)βπ) β€ 1)) |
50 | 10, 23, 48, 49 | syl3anbrc 1344 |
. . 3
β’ (π¦ β π« β β
Ξ£π β β
((πΉβπ¦)βπ) β (0[,]1)) |
51 | | elpwi 4572 |
. . . . . . . . . . 11
β’ (π§ β π« β β
π§ β
β) |
52 | | ssdifss 4100 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ β π§) β β) |
53 | | ssdifss 4100 |
. . . . . . . . . . . 12
β’ (π§ β β β (π§ β π¦) β β) |
54 | | unss 4149 |
. . . . . . . . . . . . 13
β’ (((π¦ β π§) β β β§ (π§ β π¦) β β) β ((π¦ β π§) βͺ (π§ β π¦)) β β) |
55 | 54 | biimpi 215 |
. . . . . . . . . . . 12
β’ (((π¦ β π§) β β β§ (π§ β π¦) β β) β ((π¦ β π§) βͺ (π§ β π¦)) β β) |
56 | 52, 53, 55 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π§ β β) β ((π¦ β π§) βͺ (π§ β π¦)) β β) |
57 | 2, 51, 56 | syl2an 597 |
. . . . . . . . . 10
β’ ((π¦ β π« β β§
π§ β π« β)
β ((π¦ β π§) βͺ (π§ β π¦)) β β) |
58 | | eqss 3964 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (π¦ β π§ β§ π§ β π¦)) |
59 | | ssdif0 4328 |
. . . . . . . . . . . . . 14
β’ (π¦ β π§ β (π¦ β π§) = β
) |
60 | | ssdif0 4328 |
. . . . . . . . . . . . . 14
β’ (π§ β π¦ β (π§ β π¦) = β
) |
61 | 59, 60 | anbi12i 628 |
. . . . . . . . . . . . 13
β’ ((π¦ β π§ β§ π§ β π¦) β ((π¦ β π§) = β
β§ (π§ β π¦) = β
)) |
62 | | un00 4407 |
. . . . . . . . . . . . 13
β’ (((π¦ β π§) = β
β§ (π§ β π¦) = β
) β ((π¦ β π§) βͺ (π§ β π¦)) = β
) |
63 | 58, 61, 62 | 3bitri 297 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β ((π¦ β π§) βͺ (π§ β π¦)) = β
) |
64 | 63 | necon3bii 2997 |
. . . . . . . . . . 11
β’ (π¦ β π§ β ((π¦ β π§) βͺ (π§ β π¦)) β β
) |
65 | 64 | biimpi 215 |
. . . . . . . . . 10
β’ (π¦ β π§ β ((π¦ β π§) βͺ (π§ β π¦)) β β
) |
66 | | nnwo 12845 |
. . . . . . . . . 10
β’ ((((π¦ β π§) βͺ (π§ β π¦)) β β β§ ((π¦ β π§) βͺ (π§ β π¦)) β β
) β βπ β ((π¦ β π§) βͺ (π§ β π¦))βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π) |
67 | 57, 65, 66 | syl2an 597 |
. . . . . . . . 9
β’ (((π¦ β π« β β§
π§ β π« β)
β§ π¦ β π§) β βπ β ((π¦ β π§) βͺ (π§ β π¦))βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π) |
68 | 67 | ex 414 |
. . . . . . . 8
β’ ((π¦ β π« β β§
π§ β π« β)
β (π¦ β π§ β βπ β ((π¦ β π§) βͺ (π§ β π¦))βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π)) |
69 | 57 | sselda 3949 |
. . . . . . . . . 10
β’ (((π¦ β π« β β§
π§ β π« β)
β§ π β ((π¦ β π§) βͺ (π§ β π¦))) β π β β) |
70 | | df-ral 3066 |
. . . . . . . . . . . 12
β’
(βπ β
((π¦ β π§) βͺ (π§ β π¦))π β€ π β βπ(π β ((π¦ β π§) βͺ (π§ β π¦)) β π β€ π)) |
71 | | con34b 316 |
. . . . . . . . . . . . . 14
β’ ((π β ((π¦ β π§) βͺ (π§ β π¦)) β π β€ π) β (Β¬ π β€ π β Β¬ π β ((π¦ β π§) βͺ (π§ β π¦)))) |
72 | | eldif 3925 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π¦ β π§) β (π β π¦ β§ Β¬ π β π§)) |
73 | | eldif 3925 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π§ β π¦) β (π β π§ β§ Β¬ π β π¦)) |
74 | 72, 73 | orbi12i 914 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (π¦ β π§) β¨ π β (π§ β π¦)) β ((π β π¦ β§ Β¬ π β π§) β¨ (π β π§ β§ Β¬ π β π¦))) |
75 | | elun 4113 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π¦ β π§) βͺ (π§ β π¦)) β (π β (π¦ β π§) β¨ π β (π§ β π¦))) |
76 | | xor 1014 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(π β π¦ β π β π§) β ((π β π¦ β§ Β¬ π β π§) β¨ (π β π§ β§ Β¬ π β π¦))) |
77 | 74, 75, 76 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(π β π¦ β π β π§) β π β ((π¦ β π§) βͺ (π§ β π¦))) |
78 | 77 | con1bii 357 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β ((π¦ β π§) βͺ (π§ β π¦)) β (π β π¦ β π β π§)) |
79 | 78 | imbi2i 336 |
. . . . . . . . . . . . . 14
β’ ((Β¬
π β€ π β Β¬ π β ((π¦ β π§) βͺ (π§ β π¦))) β (Β¬ π β€ π β (π β π¦ β π β π§))) |
80 | 71, 79 | bitri 275 |
. . . . . . . . . . . . 13
β’ ((π β ((π¦ β π§) βͺ (π§ β π¦)) β π β€ π) β (Β¬ π β€ π β (π β π¦ β π β π§))) |
81 | 80 | albii 1822 |
. . . . . . . . . . . 12
β’
(βπ(π β ((π¦ β π§) βͺ (π§ β π¦)) β π β€ π) β βπ(Β¬ π β€ π β (π β π¦ β π β π§))) |
82 | 70, 81 | bitri 275 |
. . . . . . . . . . 11
β’
(βπ β
((π¦ β π§) βͺ (π§ β π¦))π β€ π β βπ(Β¬ π β€ π β (π β π¦ β π β π§))) |
83 | | alral 3079 |
. . . . . . . . . . . 12
β’
(βπ(Β¬
π β€ π β (π β π¦ β π β π§)) β βπ β β (Β¬ π β€ π β (π β π¦ β π β π§))) |
84 | | nnre 12167 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
85 | | nnre 12167 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
86 | | ltnle 11241 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π < π β Β¬ π β€ π)) |
87 | 84, 85, 86 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β (π < π β Β¬ π β€ π)) |
88 | 87 | imbi1d 342 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β ((π < π β (π β π¦ β π β π§)) β (Β¬ π β€ π β (π β π¦ β π β π§)))) |
89 | 88 | ralbidva 3173 |
. . . . . . . . . . . 12
β’ (π β β β
(βπ β β
(π < π β (π β π¦ β π β π§)) β βπ β β (Β¬ π β€ π β (π β π¦ β π β π§)))) |
90 | 83, 89 | syl5ibr 246 |
. . . . . . . . . . 11
β’ (π β β β
(βπ(Β¬ π β€ π β (π β π¦ β π β π§)) β βπ β β (π < π β (π β π¦ β π β π§)))) |
91 | 82, 90 | biimtrid 241 |
. . . . . . . . . 10
β’ (π β β β
(βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π β βπ β β (π < π β (π β π¦ β π β π§)))) |
92 | 69, 91 | syl 17 |
. . . . . . . . 9
β’ (((π¦ β π« β β§
π§ β π« β)
β§ π β ((π¦ β π§) βͺ (π§ β π¦))) β (βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π β βπ β β (π < π β (π β π¦ β π β π§)))) |
93 | 92 | reximdva 3166 |
. . . . . . . 8
β’ ((π¦ β π« β β§
π§ β π« β)
β (βπ β
((π¦ β π§) βͺ (π§ β π¦))βπ β ((π¦ β π§) βͺ (π§ β π¦))π β€ π β βπ β ((π¦ β π§) βͺ (π§ β π¦))βπ β β (π < π β (π β π¦ β π β π§)))) |
94 | 68, 93 | syld 47 |
. . . . . . 7
β’ ((π¦ β π« β β§
π§ β π« β)
β (π¦ β π§ β βπ β ((π¦ β π§) βͺ (π§ β π¦))βπ β β (π < π β (π β π¦ β π β π§)))) |
95 | | rexun 4155 |
. . . . . . 7
β’
(βπ β
((π¦ β π§) βͺ (π§ β π¦))βπ β β (π < π β (π β π¦ β π β π§)) β (βπ β (π¦ β π§)βπ β β (π < π β (π β π¦ β π β π§)) β¨ βπ β (π§ β π¦)βπ β β (π < π β (π β π¦ β π β π§)))) |
96 | 94, 95 | syl6ib 251 |
. . . . . 6
β’ ((π¦ β π« β β§
π§ β π« β)
β (π¦ β π§ β (βπ β (π¦ β π§)βπ β β (π < π β (π β π¦ β π β π§)) β¨ βπ β (π§ β π¦)βπ β β (π < π β (π β π¦ β π β π§))))) |
97 | | simpll 766 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π¦ β π§) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π¦ β β) |
98 | | simplr 768 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π¦ β π§) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π§ β β) |
99 | | simprl 770 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π¦ β π§) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π β (π¦ β π§)) |
100 | | simprr 772 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π¦ β π§) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β βπ β β (π < π β (π β π¦ β π β π§))) |
101 | | biid 261 |
. . . . . . . . . 10
β’
(Ξ£π β
β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ) β Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ)) |
102 | 6, 97, 98, 99, 100, 101 | rpnnen2lem11 16113 |
. . . . . . . . 9
β’ (((π¦ β β β§ π§ β β) β§ (π β (π¦ β π§) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ)) |
103 | 102 | rexlimdvaa 3154 |
. . . . . . . 8
β’ ((π¦ β β β§ π§ β β) β
(βπ β (π¦ β π§)βπ β β (π < π β (π β π¦ β π β π§)) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ))) |
104 | | simplr 768 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π§ β β) |
105 | | simpll 766 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π¦ β β) |
106 | | simprl 770 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β π β (π§ β π¦)) |
107 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β βπ β β (π < π β (π β π¦ β π β π§))) |
108 | | bicom 221 |
. . . . . . . . . . . . 13
β’ ((π β π§ β π β π¦) β (π β π¦ β π β π§)) |
109 | 108 | imbi2i 336 |
. . . . . . . . . . . 12
β’ ((π < π β (π β π§ β π β π¦)) β (π < π β (π β π¦ β π β π§))) |
110 | 109 | ralbii 3097 |
. . . . . . . . . . 11
β’
(βπ β
β (π < π β (π β π§ β π β π¦)) β βπ β β (π < π β (π β π¦ β π β π§))) |
111 | 107, 110 | sylibr 233 |
. . . . . . . . . 10
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β βπ β β (π < π β (π β π§ β π β π¦))) |
112 | | eqcom 2744 |
. . . . . . . . . 10
β’
(Ξ£π β
β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ) β Ξ£π β β ((πΉβπ§)βπ) = Ξ£π β β ((πΉβπ¦)βπ)) |
113 | 6, 104, 105, 106, 111, 112 | rpnnen2lem11 16113 |
. . . . . . . . 9
β’ (((π¦ β β β§ π§ β β) β§ (π β (π§ β π¦) β§ βπ β β (π < π β (π β π¦ β π β π§)))) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ)) |
114 | 113 | rexlimdvaa 3154 |
. . . . . . . 8
β’ ((π¦ β β β§ π§ β β) β
(βπ β (π§ β π¦)βπ β β (π < π β (π β π¦ β π β π§)) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ))) |
115 | 103, 114 | jaod 858 |
. . . . . . 7
β’ ((π¦ β β β§ π§ β β) β
((βπ β (π¦ β π§)βπ β β (π < π β (π β π¦ β π β π§)) β¨ βπ β (π§ β π¦)βπ β β (π < π β (π β π¦ β π β π§))) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ))) |
116 | 2, 51, 115 | syl2an 597 |
. . . . . 6
β’ ((π¦ β π« β β§
π§ β π« β)
β ((βπ β
(π¦ β π§)βπ β β (π < π β (π β π¦ β π β π§)) β¨ βπ β (π§ β π¦)βπ β β (π < π β (π β π¦ β π β π§))) β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ))) |
117 | 96, 116 | syld 47 |
. . . . 5
β’ ((π¦ β π« β β§
π§ β π« β)
β (π¦ β π§ β Β¬ Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ))) |
118 | 117 | necon4ad 2963 |
. . . 4
β’ ((π¦ β π« β β§
π§ β π« β)
β (Ξ£π β
β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ) β π¦ = π§)) |
119 | | fveq2 6847 |
. . . . . 6
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
120 | 119 | fveq1d 6849 |
. . . . 5
β’ (π¦ = π§ β ((πΉβπ¦)βπ) = ((πΉβπ§)βπ)) |
121 | 120 | sumeq2sdv 15596 |
. . . 4
β’ (π¦ = π§ β Ξ£π β β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ)) |
122 | 118, 121 | impbid1 224 |
. . 3
β’ ((π¦ β π« β β§
π§ β π« β)
β (Ξ£π β
β ((πΉβπ¦)βπ) = Ξ£π β β ((πΉβπ§)βπ) β π¦ = π§)) |
123 | 50, 122 | dom2 8942 |
. 2
β’ ((0[,]1)
β V β π« β βΌ (0[,]1)) |
124 | 1, 123 | ax-mp 5 |
1
β’ π«
β βΌ (0[,]1) |