Step | Hyp | Ref
| Expression |
1 | | iunhoiioolem.K |
. . . . . 6
β’
β²ππ |
2 | | eqid 2733 |
. . . . . 6
β’ (π β π β¦ ((πΉβπ) β π΄)) = (π β π β¦ ((πΉβπ) β π΄)) |
3 | | iunhoiioolem.f |
. . . . . . . . . . 11
β’ (π β πΉ β Xπ β π (π΄(,)π΅)) |
4 | | ixpf 8861 |
. . . . . . . . . . 11
β’ (πΉ β Xπ β
π (π΄(,)π΅) β πΉ:πβΆβͺ
π β π (π΄(,)π΅)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆβͺ
π β π (π΄(,)π΅)) |
6 | | ioossre 13331 |
. . . . . . . . . . . . 13
β’ (π΄(,)π΅) β β |
7 | 6 | rgenw 3065 |
. . . . . . . . . . . 12
β’
βπ β
π (π΄(,)π΅) β β |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
β’ (π β βπ β π (π΄(,)π΅) β β) |
9 | | iunss 5006 |
. . . . . . . . . . 11
β’ (βͺ π β π (π΄(,)π΅) β β β βπ β π (π΄(,)π΅) β β) |
10 | 8, 9 | sylibr 233 |
. . . . . . . . . 10
β’ (π β βͺ π β π (π΄(,)π΅) β β) |
11 | 5, 10 | fssd 6687 |
. . . . . . . . 9
β’ (π β πΉ:πβΆβ) |
12 | 11 | ffvelcdmda 7036 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β β) |
13 | | iunhoiioolem.a |
. . . . . . . 8
β’ ((π β§ π β π) β π΄ β β) |
14 | 12, 13 | resubcld 11588 |
. . . . . . 7
β’ ((π β§ π β π) β ((πΉβπ) β π΄) β β) |
15 | 13 | rexrd 11210 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΄ β
β*) |
16 | | iunhoiioolem.b |
. . . . . . . . 9
β’ ((π β§ π β π) β π΅ β
β*) |
17 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β πΉ β Xπ β π (π΄(,)π΅)) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
19 | | fvixp2 43507 |
. . . . . . . . . 10
β’ ((πΉ β Xπ β
π (π΄(,)π΅) β§ π β π) β (πΉβπ) β (π΄(,)π΅)) |
20 | 17, 18, 19 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β (π΄(,)π΅)) |
21 | | ioogtlb 43819 |
. . . . . . . . 9
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πΉβπ) β (π΄(,)π΅)) β π΄ < (πΉβπ)) |
22 | 15, 16, 20, 21 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β π) β π΄ < (πΉβπ)) |
23 | 13, 12 | posdifd 11747 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΄ < (πΉβπ) β 0 < ((πΉβπ) β π΄))) |
24 | 22, 23 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β π) β 0 < ((πΉβπ) β π΄)) |
25 | 14, 24 | elrpd 12959 |
. . . . . 6
β’ ((π β§ π β π) β ((πΉβπ) β π΄) β
β+) |
26 | 1, 2, 25 | rnmptssd 43504 |
. . . . 5
β’ (π β ran (π β π β¦ ((πΉβπ) β π΄)) β
β+) |
27 | | iunhoiioolem.c |
. . . . . 6
β’ πΆ = inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) |
28 | | ltso 11240 |
. . . . . . . 8
β’ < Or
β |
29 | 28 | a1i 11 |
. . . . . . 7
β’ (π β < Or
β) |
30 | | iunhoiioolem.x |
. . . . . . . 8
β’ (π β π β Fin) |
31 | 2 | rnmptfi 43476 |
. . . . . . . 8
β’ (π β Fin β ran (π β π β¦ ((πΉβπ) β π΄)) β Fin) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ (π β ran (π β π β¦ ((πΉβπ) β π΄)) β Fin) |
33 | | iunhoiioolem.n |
. . . . . . . 8
β’ (π β π β β
) |
34 | 1, 14, 2, 33 | rnmptn0 6197 |
. . . . . . 7
β’ (π β ran (π β π β¦ ((πΉβπ) β π΄)) β β
) |
35 | 1, 2, 14 | rnmptssd 43504 |
. . . . . . 7
β’ (π β ran (π β π β¦ ((πΉβπ) β π΄)) β β) |
36 | | fiinfcl 9442 |
. . . . . . 7
β’ (( <
Or β β§ (ran (π
β π β¦ ((πΉβπ) β π΄)) β Fin β§ ran (π β π β¦ ((πΉβπ) β π΄)) β β
β§ ran (π β π β¦ ((πΉβπ) β π΄)) β β)) β inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) β ran (π β π β¦ ((πΉβπ) β π΄))) |
37 | 29, 32, 34, 35, 36 | syl13anc 1373 |
. . . . . 6
β’ (π β inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) β ran (π β π β¦ ((πΉβπ) β π΄))) |
38 | 27, 37 | eqeltrid 2838 |
. . . . 5
β’ (π β πΆ β ran (π β π β¦ ((πΉβπ) β π΄))) |
39 | 26, 38 | sseldd 3946 |
. . . 4
β’ (π β πΆ β
β+) |
40 | | rpgtrecnn 43701 |
. . . 4
β’ (πΆ β β+
β βπ β
β (1 / π) < πΆ) |
41 | 39, 40 | syl 17 |
. . 3
β’ (π β βπ β β (1 / π) < πΆ) |
42 | 3 | elexd 3464 |
. . . . . . . 8
β’ (π β πΉ β V) |
43 | 42 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β πΉ β V) |
44 | 5 | ffnd 6670 |
. . . . . . . 8
β’ (π β πΉ Fn π) |
45 | 44 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β πΉ Fn π) |
46 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π β β |
47 | 1, 46 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π β§ π β β) |
48 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π(1 /
π) |
49 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π
< |
50 | | nfmpt1 5214 |
. . . . . . . . . . . . 13
β’
β²π(π β π β¦ ((πΉβπ) β π΄)) |
51 | 50 | nfrn 5908 |
. . . . . . . . . . . 12
β’
β²πran
(π β π β¦ ((πΉβπ) β π΄)) |
52 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²πβ |
53 | 51, 52, 49 | nfinf 9423 |
. . . . . . . . . . 11
β’
β²πinf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) |
54 | 27, 53 | nfcxfr 2902 |
. . . . . . . . . 10
β’
β²ππΆ |
55 | 48, 49, 54 | nfbr 5153 |
. . . . . . . . 9
β’
β²π(1 / π) < πΆ |
56 | 47, 55 | nfan 1903 |
. . . . . . . 8
β’
β²π((π β§ π β β) β§ (1 / π) < πΆ) |
57 | 13 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β π΄ β β) |
58 | | nnrecre 12200 |
. . . . . . . . . . . . . 14
β’ (π β β β (1 /
π) β
β) |
59 | 58 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β (1 / π) β β) |
60 | 57, 59 | readdcld 11189 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β (π΄ + (1 / π)) β β) |
61 | 60 | rexrd 11210 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β (π΄ + (1 / π)) β
β*) |
62 | 61 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (π΄ + (1 / π)) β
β*) |
63 | 16 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β π΅ β
β*) |
64 | 63 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β π΅ β
β*) |
65 | | ressxr 11204 |
. . . . . . . . . . . . . 14
β’ β
β β* |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
β*) |
67 | 11, 66 | fssd 6687 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ*) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β πΉ:πβΆβ*) |
69 | 68 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (πΉβπ) β
β*) |
70 | 60 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (π΄ + (1 / π)) β β) |
71 | 12 | ad4ant14 751 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (πΉβπ) β β) |
72 | 59 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (1 / π) β β) |
73 | 35, 38 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β β) |
74 | 73 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β πΆ β β) |
75 | 14 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β ((πΉβπ) β π΄) β β) |
76 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (1 / π) < πΆ) |
77 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β π) β ran (π β π β¦ ((πΉβπ) β π΄)) β β) |
78 | 32 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β π) β ran (π β π β¦ ((πΉβπ) β π΄)) β Fin) |
79 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π β π) |
80 | | ovexd 7393 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β ((πΉβπ) β π΄) β V) |
81 | 2 | elrnmpt1 5914 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ ((πΉβπ) β π΄) β V) β ((πΉβπ) β π΄) β ran (π β π β¦ ((πΉβπ) β π΄))) |
82 | 79, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((πΉβπ) β π΄) β ran (π β π β¦ ((πΉβπ) β π΄))) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β π) β ((πΉβπ) β π΄) β ran (π β π β¦ ((πΉβπ) β π΄))) |
84 | | infrefilb 12146 |
. . . . . . . . . . . . . . . 16
β’ ((ran
(π β π β¦ ((πΉβπ) β π΄)) β β β§ ran (π β π β¦ ((πΉβπ) β π΄)) β Fin β§ ((πΉβπ) β π΄) β ran (π β π β¦ ((πΉβπ) β π΄))) β inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) β€ ((πΉβπ) β π΄)) |
85 | 77, 78, 83, 84 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β π) β inf(ran (π β π β¦ ((πΉβπ) β π΄)), β, < ) β€ ((πΉβπ) β π΄)) |
86 | 27, 85 | eqbrtrid 5141 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β πΆ β€ ((πΉβπ) β π΄)) |
87 | 86 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β πΆ β€ ((πΉβπ) β π΄)) |
88 | 72, 74, 75, 76, 87 | ltletrd 11320 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (1 / π) < ((πΉβπ) β π΄)) |
89 | 57 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β π΄ β β) |
90 | 89, 72, 71 | ltaddsub2d 11761 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β ((π΄ + (1 / π)) < (πΉβπ) β (1 / π) < ((πΉβπ) β π΄))) |
91 | 88, 90 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (π΄ + (1 / π)) < (πΉβπ)) |
92 | 70, 71, 91 | ltled 11308 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (π΄ + (1 / π)) β€ (πΉβπ)) |
93 | | iooltub 43834 |
. . . . . . . . . . . 12
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πΉβπ) β (π΄(,)π΅)) β (πΉβπ) < π΅) |
94 | 15, 16, 20, 93 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) < π΅) |
95 | 94 | ad4ant14 751 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (πΉβπ) < π΅) |
96 | 62, 64, 69, 92, 95 | elicod 13320 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ (1 / π) < πΆ) β§ π β π) β (πΉβπ) β ((π΄ + (1 / π))[,)π΅)) |
97 | 96 | ex 414 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β (π β π β (πΉβπ) β ((π΄ + (1 / π))[,)π΅))) |
98 | 56, 97 | ralrimi 3239 |
. . . . . . 7
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β βπ β π (πΉβπ) β ((π΄ + (1 / π))[,)π΅)) |
99 | 43, 45, 98 | 3jca 1129 |
. . . . . 6
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β ((π΄ + (1 / π))[,)π΅))) |
100 | | elixp2 8842 |
. . . . . 6
β’ (πΉ β Xπ β
π ((π΄ + (1 / π))[,)π΅) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β ((π΄ + (1 / π))[,)π΅))) |
101 | 99, 100 | sylibr 233 |
. . . . 5
β’ (((π β§ π β β) β§ (1 / π) < πΆ) β πΉ β Xπ β π ((π΄ + (1 / π))[,)π΅)) |
102 | 101 | ex 414 |
. . . 4
β’ ((π β§ π β β) β ((1 / π) < πΆ β πΉ β Xπ β π ((π΄ + (1 / π))[,)π΅))) |
103 | 102 | reximdva 3162 |
. . 3
β’ (π β (βπ β β (1 / π) < πΆ β βπ β β πΉ β Xπ β π ((π΄ + (1 / π))[,)π΅))) |
104 | 41, 103 | mpd 15 |
. 2
β’ (π β βπ β β πΉ β Xπ β π ((π΄ + (1 / π))[,)π΅)) |
105 | | eliun 4959 |
. 2
β’ (πΉ β βͺ π β β Xπ β π ((π΄ + (1 / π))[,)π΅) β βπ β β πΉ β Xπ β π ((π΄ + (1 / π))[,)π΅)) |
106 | 104, 105 | sylibr 233 |
1
β’ (π β πΉ β βͺ
π β β Xπ β
π ((π΄ + (1 / π))[,)π΅)) |