Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (1 / π) = (1 / π)) |
2 | 1 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (π β (1 / π)) = (π β (1 / π))) |
3 | | supcvg.3 |
. . . . . . . . . . 11
β’ π
= (π β β β¦ (π β (1 / π))) |
4 | | ovex 7395 |
. . . . . . . . . . 11
β’ (π β (1 / π)) β V |
5 | 2, 3, 4 | fvmpt 6953 |
. . . . . . . . . 10
β’ (π β β β (π
βπ) = (π β (1 / π))) |
6 | 5 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π
βπ) = (π β (1 / π))) |
7 | | supcvg.2 |
. . . . . . . . . . 11
β’ π = sup(π΄, β, < ) |
8 | | supcvg.6 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
9 | | supcvg.4 |
. . . . . . . . . . . . 13
β’ (π β π β β
) |
10 | | supcvg.5 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:πβontoβπ΄) |
11 | | fof 6761 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβontoβπ΄ β πΉ:πβΆπ΄) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβΆπ΄) |
13 | | feq3 6656 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = β
β (πΉ:πβΆπ΄ β πΉ:πβΆβ
)) |
14 | 12, 13 | syl5ibcom 244 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ = β
β πΉ:πβΆβ
)) |
15 | | f00 6729 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβΆβ
β (πΉ = β
β§ π = β
)) |
16 | 15 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’ (πΉ:πβΆβ
β π = β
) |
17 | 14, 16 | syl6 35 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ = β
β π = β
)) |
18 | 17 | necon3d 2965 |
. . . . . . . . . . . . 13
β’ (π β (π β β
β π΄ β β
)) |
19 | 9, 18 | mpd 15 |
. . . . . . . . . . . 12
β’ (π β π΄ β β
) |
20 | | supcvg.7 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) |
21 | 8, 19, 20 | suprcld 12125 |
. . . . . . . . . . 11
β’ (π β sup(π΄, β, < ) β
β) |
22 | 7, 21 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β β) |
23 | | nnrp 12933 |
. . . . . . . . . . 11
β’ (π β β β π β
β+) |
24 | 23 | rpreccld 12974 |
. . . . . . . . . 10
β’ (π β β β (1 /
π) β
β+) |
25 | | ltsubrp 12958 |
. . . . . . . . . 10
β’ ((π β β β§ (1 / π) β β+)
β (π β (1 /
π)) < π) |
26 | 22, 24, 25 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π β (1 / π)) < π) |
27 | 6, 26 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π β§ π β β) β (π
βπ) < π) |
28 | 27, 7 | breqtrdi 5151 |
. . . . . . 7
β’ ((π β§ π β β) β (π
βπ) < sup(π΄, β, < )) |
29 | 8, 19, 20 | 3jca 1129 |
. . . . . . . 8
β’ (π β (π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯)) |
30 | | nnrecre 12202 |
. . . . . . . . . . 11
β’ (π β β β (1 /
π) β
β) |
31 | | resubcl 11472 |
. . . . . . . . . . 11
β’ ((π β β β§ (1 / π) β β) β (π β (1 / π)) β β) |
32 | 22, 30, 31 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π β (1 / π)) β β) |
33 | 32, 3 | fmptd 7067 |
. . . . . . . . 9
β’ (π β π
:ββΆβ) |
34 | 33 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β β) β (π
βπ) β β) |
35 | | suprlub 12126 |
. . . . . . . 8
β’ (((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ (π
βπ) β β) β ((π
βπ) < sup(π΄, β, < ) β βπ§ β π΄ (π
βπ) < π§)) |
36 | 29, 34, 35 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ π β β) β ((π
βπ) < sup(π΄, β, < ) β βπ§ β π΄ (π
βπ) < π§)) |
37 | 28, 36 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β β) β βπ§ β π΄ (π
βπ) < π§) |
38 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π΄ β β) |
39 | 38 | sselda 3949 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π§ β π΄) β π§ β β) |
40 | | ltle 11250 |
. . . . . . . 8
β’ (((π
βπ) β β β§ π§ β β) β ((π
βπ) < π§ β (π
βπ) β€ π§)) |
41 | 34, 39, 40 | syl2an2r 684 |
. . . . . . 7
β’ (((π β§ π β β) β§ π§ β π΄) β ((π
βπ) < π§ β (π
βπ) β€ π§)) |
42 | 41 | reximdva 3166 |
. . . . . 6
β’ ((π β§ π β β) β (βπ§ β π΄ (π
βπ) < π§ β βπ§ β π΄ (π
βπ) β€ π§)) |
43 | 37, 42 | mpd 15 |
. . . . 5
β’ ((π β§ π β β) β βπ§ β π΄ (π
βπ) β€ π§) |
44 | | forn 6764 |
. . . . . . . . 9
β’ (πΉ:πβontoβπ΄ β ran πΉ = π΄) |
45 | 10, 44 | syl 17 |
. . . . . . . 8
β’ (π β ran πΉ = π΄) |
46 | 45 | rexeqdv 3317 |
. . . . . . 7
β’ (π β (βπ§ β ran πΉ(π
βπ) β€ π§ β βπ§ β π΄ (π
βπ) β€ π§)) |
47 | | ffn 6673 |
. . . . . . . 8
β’ (πΉ:πβΆπ΄ β πΉ Fn π) |
48 | | breq2 5114 |
. . . . . . . . 9
β’ (π§ = (πΉβπ₯) β ((π
βπ) β€ π§ β (π
βπ) β€ (πΉβπ₯))) |
49 | 48 | rexrn 7042 |
. . . . . . . 8
β’ (πΉ Fn π β (βπ§ β ran πΉ(π
βπ) β€ π§ β βπ₯ β π (π
βπ) β€ (πΉβπ₯))) |
50 | 12, 47, 49 | 3syl 18 |
. . . . . . 7
β’ (π β (βπ§ β ran πΉ(π
βπ) β€ π§ β βπ₯ β π (π
βπ) β€ (πΉβπ₯))) |
51 | 46, 50 | bitr3d 281 |
. . . . . 6
β’ (π β (βπ§ β π΄ (π
βπ) β€ π§ β βπ₯ β π (π
βπ) β€ (πΉβπ₯))) |
52 | 51 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β (βπ§ β π΄ (π
βπ) β€ π§ β βπ₯ β π (π
βπ) β€ (πΉβπ₯))) |
53 | 43, 52 | mpbid 231 |
. . . 4
β’ ((π β§ π β β) β βπ₯ β π (π
βπ) β€ (πΉβπ₯)) |
54 | 53 | ralrimiva 3144 |
. . 3
β’ (π β βπ β β βπ₯ β π (π
βπ) β€ (πΉβπ₯)) |
55 | | supcvg.1 |
. . . 4
β’ π β V |
56 | | nnenom 13892 |
. . . 4
β’ β
β Ο |
57 | | fveq2 6847 |
. . . . 5
β’ (π₯ = (πβπ) β (πΉβπ₯) = (πΉβ(πβπ))) |
58 | 57 | breq2d 5122 |
. . . 4
β’ (π₯ = (πβπ) β ((π
βπ) β€ (πΉβπ₯) β (π
βπ) β€ (πΉβ(πβπ)))) |
59 | 55, 56, 58 | axcc4 10382 |
. . 3
β’
(βπ β
β βπ₯ β
π (π
βπ) β€ (πΉβπ₯) β βπ(π:ββΆπ β§ βπ β β (π
βπ) β€ (πΉβ(πβπ)))) |
60 | 54, 59 | syl 17 |
. 2
β’ (π β βπ(π:ββΆπ β§ βπ β β (π
βπ) β€ (πΉβ(πβπ)))) |
61 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
62 | | 1zzd 12541 |
. . . . . 6
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β 1 β β€) |
63 | | 1zzd 12541 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
64 | 22 | recnd 11190 |
. . . . . . . . . 10
β’ (π β π β β) |
65 | | 1z 12540 |
. . . . . . . . . 10
β’ 1 β
β€ |
66 | 61 | eqimss2i 4008 |
. . . . . . . . . . 11
β’
(β€β₯β1) β β |
67 | | nnex 12166 |
. . . . . . . . . . 11
β’ β
β V |
68 | 66, 67 | climconst2 15437 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β€) β (β Γ {π}) β π) |
69 | 64, 65, 68 | sylancl 587 |
. . . . . . . . 9
β’ (π β (β Γ {π}) β π) |
70 | 67 | mptex 7178 |
. . . . . . . . . . 11
β’ (π β β β¦ (π β (1 / π))) β V |
71 | 3, 70 | eqeltri 2834 |
. . . . . . . . . 10
β’ π
β V |
72 | 71 | a1i 11 |
. . . . . . . . 9
β’ (π β π
β V) |
73 | | ax-1cn 11116 |
. . . . . . . . . 10
β’ 1 β
β |
74 | | divcnv 15745 |
. . . . . . . . . 10
β’ (1 β
β β (π β
β β¦ (1 / π))
β 0) |
75 | 73, 74 | mp1i 13 |
. . . . . . . . 9
β’ (π β (π β β β¦ (1 / π)) β 0) |
76 | | fvconst2g 7156 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
((β Γ {π})βπ) = π) |
77 | 22, 76 | sylan 581 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((β Γ
{π})βπ) = π) |
78 | 64 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
79 | 77, 78 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((β Γ
{π})βπ) β
β) |
80 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦ (1 /
π)) = (π β β β¦ (1 / π)) |
81 | | ovex 7395 |
. . . . . . . . . . . 12
β’ (1 /
π) β
V |
82 | 1, 80, 81 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ (1 /
π))βπ) = (1 / π)) |
83 | 82 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π β β β¦ (1 / π))βπ) = (1 / π)) |
84 | | nnrecre 12202 |
. . . . . . . . . . . 12
β’ (π β β β (1 /
π) β
β) |
85 | 84 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β β β (1 /
π) β
β) |
86 | 85 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1 / π) β
β) |
87 | 83, 86 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π β β β¦ (1 / π))βπ) β β) |
88 | 77, 83 | oveq12d 7380 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((β Γ
{π})βπ) β ((π β β β¦ (1 / π))βπ)) = (π β (1 / π))) |
89 | 6, 88 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π
βπ) = (((β Γ {π})βπ) β ((π β β β¦ (1 / π))βπ))) |
90 | 61, 63, 69, 72, 75, 79, 87, 89 | climsub 15523 |
. . . . . . . 8
β’ (π β π
β (π β 0)) |
91 | 64 | subid1d 11508 |
. . . . . . . 8
β’ (π β (π β 0) = π) |
92 | 90, 91 | breqtrd 5136 |
. . . . . . 7
β’ (π β π
β π) |
93 | 92 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β π
β π) |
94 | 12 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β πΉ:πβΆπ΄) |
95 | | fex 7181 |
. . . . . . . 8
β’ ((πΉ:πβΆπ΄ β§ π β V) β πΉ β V) |
96 | 94, 55, 95 | sylancl 587 |
. . . . . . 7
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β πΉ β V) |
97 | | vex 3452 |
. . . . . . 7
β’ π β V |
98 | | coexg 7871 |
. . . . . . 7
β’ ((πΉ β V β§ π β V) β (πΉ β π) β V) |
99 | 96, 97, 98 | sylancl 587 |
. . . . . 6
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β (πΉ β π) β V) |
100 | 33 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β π
:ββΆβ) |
101 | 100 | ffvelcdmda 7040 |
. . . . . 6
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (π
βπ) β β) |
102 | 12, 8 | fssd 6691 |
. . . . . . . . 9
β’ (π β πΉ:πβΆβ) |
103 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π:ββΆπ) β (πΉ β π):ββΆβ) |
104 | 102, 103 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π:ββΆπ) β (πΉ β π):ββΆβ) |
105 | 104 | adantr 482 |
. . . . . . 7
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β (πΉ β π):ββΆβ) |
106 | 105 | ffvelcdmda 7040 |
. . . . . 6
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β ((πΉ β π)βπ) β β) |
107 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (π
βπ) = (π
βπ)) |
108 | | 2fveq3 6852 |
. . . . . . . . . 10
β’ (π = π β (πΉβ(πβπ)) = (πΉβ(πβπ))) |
109 | 107, 108 | breq12d 5123 |
. . . . . . . . 9
β’ (π = π β ((π
βπ) β€ (πΉβ(πβπ)) β (π
βπ) β€ (πΉβ(πβπ)))) |
110 | 109 | rspccva 3583 |
. . . . . . . 8
β’
((βπ β
β (π
βπ) β€ (πΉβ(πβπ)) β§ π β β) β (π
βπ) β€ (πΉβ(πβπ))) |
111 | 110 | adantll 713 |
. . . . . . 7
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (π
βπ) β€ (πΉβ(πβπ))) |
112 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β π:ββΆπ) |
113 | | fvco3 6945 |
. . . . . . . 8
β’ ((π:ββΆπ β§ π β β) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
114 | 112, 113 | sylan 581 |
. . . . . . 7
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
115 | 111, 114 | breqtrrd 5138 |
. . . . . 6
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (π
βπ) β€ ((πΉ β π)βπ)) |
116 | 29 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯)) |
117 | 112 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (πβπ) β π) |
118 | 94 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ (πβπ) β π) β (πΉβ(πβπ)) β π΄) |
119 | 117, 118 | syldan 592 |
. . . . . . . . 9
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (πΉβ(πβπ)) β π΄) |
120 | | suprub 12123 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β§ (πΉβ(πβπ)) β π΄) β (πΉβ(πβπ)) β€ sup(π΄, β, < )) |
121 | 116, 119,
120 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (πΉβ(πβπ)) β€ sup(π΄, β, < )) |
122 | 121, 7 | breqtrrdi 5152 |
. . . . . . 7
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β (πΉβ(πβπ)) β€ π) |
123 | 114, 122 | eqbrtrd 5132 |
. . . . . 6
β’ ((((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β§ π β β) β ((πΉ β π)βπ) β€ π) |
124 | 61, 62, 93, 99, 101, 106, 115, 123 | climsqz 15530 |
. . . . 5
β’ (((π β§ π:ββΆπ) β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β (πΉ β π) β π) |
125 | 124 | ex 414 |
. . . 4
β’ ((π β§ π:ββΆπ) β (βπ β β (π
βπ) β€ (πΉβ(πβπ)) β (πΉ β π) β π)) |
126 | 125 | imdistanda 573 |
. . 3
β’ (π β ((π:ββΆπ β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β (π:ββΆπ β§ (πΉ β π) β π))) |
127 | 126 | eximdv 1921 |
. 2
β’ (π β (βπ(π:ββΆπ β§ βπ β β (π
βπ) β€ (πΉβ(πβπ))) β βπ(π:ββΆπ β§ (πΉ β π) β π))) |
128 | 60, 127 | mpd 15 |
1
β’ (π β βπ(π:ββΆπ β§ (πΉ β π) β π)) |