Step | Hyp | Ref
| Expression |
1 | | hashnzfzclim.m |
. . . . . 6
β’ (π β π β β) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π½ β 1))) β π β
β) |
3 | | hashnzfzclim.j |
. . . . . 6
β’ (π β π½ β β€) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π½ β 1))) β π½ β
β€) |
5 | | simpr 486 |
. . . . 5
β’ ((π β§ π β (β€β₯β(π½ β 1))) β π β
(β€β₯β(π½ β 1))) |
6 | 2, 4, 5 | hashnzfz 42692 |
. . . 4
β’ ((π β§ π β (β€β₯β(π½ β 1))) β
(β―β(( β₯ β {π}) β© (π½...π))) = ((ββ(π / π)) β (ββ((π½ β 1) / π)))) |
7 | 6 | oveq1d 7376 |
. . 3
β’ ((π β§ π β (β€β₯β(π½ β 1))) β
((β―β(( β₯ β {π}) β© (π½...π))) / π) = (((ββ(π / π)) β (ββ((π½ β 1) / π))) / π)) |
8 | 7 | mpteq2dva 5209 |
. 2
β’ (π β (π β (β€β₯β(π½ β 1)) β¦
((β―β(( β₯ β {π}) β© (π½...π))) / π)) = (π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))) |
9 | | nnuz 12814 |
. . . . 5
β’ β =
(β€β₯β1) |
10 | | 1z 12541 |
. . . . . 6
β’ 1 β
β€ |
11 | 10 | a1i 11 |
. . . . 5
β’ (π β 1 β
β€) |
12 | 1 | nncnd 12177 |
. . . . . . . . . 10
β’ (π β π β β) |
13 | 1 | nnne0d 12211 |
. . . . . . . . . 10
β’ (π β π β 0) |
14 | 12, 13 | reccld 11932 |
. . . . . . . . 9
β’ (π β (1 / π) β β) |
15 | 9 | eqimss2i 4007 |
. . . . . . . . . 10
β’
(β€β₯β1) β β |
16 | | nnex 12167 |
. . . . . . . . . 10
β’ β
β V |
17 | 15, 16 | climconst2 15439 |
. . . . . . . . 9
β’ (((1 /
π) β β β§ 1
β β€) β (β Γ {(1 / π)}) β (1 / π)) |
18 | 14, 10, 17 | sylancl 587 |
. . . . . . . 8
β’ (π β (β Γ {(1 /
π)}) β (1 / π)) |
19 | 16 | mptex 7177 |
. . . . . . . . 9
β’ (π β β β¦ ((1 /
π) β (1 / π))) β V |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β (π β β β¦ ((1 / π) β (1 / π))) β V) |
21 | | ax-1cn 11117 |
. . . . . . . . 9
β’ 1 β
β |
22 | | divcnv 15746 |
. . . . . . . . 9
β’ (1 β
β β (π β
β β¦ (1 / π))
β 0) |
23 | 21, 22 | mp1i 13 |
. . . . . . . 8
β’ (π β (π β β β¦ (1 / π)) β 0) |
24 | | ovex 7394 |
. . . . . . . . . . 11
β’ (1 /
π) β
V |
25 | 24 | fvconst2 7157 |
. . . . . . . . . 10
β’ (π₯ β β β ((β
Γ {(1 / π)})βπ₯) = (1 / π)) |
26 | 25 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((β Γ {(1
/ π)})βπ₯) = (1 / π)) |
27 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (1 / π) β
β) |
28 | 26, 27 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((β Γ {(1
/ π)})βπ₯) β
β) |
29 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π β β β¦ (1 / π)) = (π β β β¦ (1 / π))) |
30 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π = π₯ β (1 / π) = (1 / π₯)) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π = π₯) β (1 / π) = (1 / π₯)) |
32 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β π₯ β β) |
33 | | ovexd 7396 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (1 / π₯) β V) |
34 | 29, 31, 32, 33 | fvmptd 6959 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β ((π β β β¦ (1 / π))βπ₯) = (1 / π₯)) |
35 | 32 | nnrecred 12212 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (1 / π₯) β
β) |
36 | 34, 35 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((π β β β¦ (1 / π))βπ₯) β β) |
37 | 36 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((π β β β¦ (1 / π))βπ₯) β β) |
38 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (π β β β¦ ((1 / π) β (1 / π))) = (π β β β¦ ((1 / π) β (1 / π)))) |
39 | 30 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π = π₯ β ((1 / π) β (1 / π)) = ((1 / π) β (1 / π₯))) |
40 | 39 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π = π₯) β ((1 / π) β (1 / π)) = ((1 / π) β (1 / π₯))) |
41 | | ovexd 7396 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β ((1 / π) β (1 / π₯)) β V) |
42 | 38, 40, 32, 41 | fvmptd 6959 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((π β β β¦ ((1 / π) β (1 / π)))βπ₯) = ((1 / π) β (1 / π₯))) |
43 | 26, 34 | oveq12d 7379 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (((β Γ
{(1 / π)})βπ₯) β ((π β β β¦ (1 / π))βπ₯)) = ((1 / π) β (1 / π₯))) |
44 | 42, 43 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((π β β β¦ ((1 / π) β (1 / π)))βπ₯) = (((β Γ {(1 / π)})βπ₯) β ((π β β β¦ (1 / π))βπ₯))) |
45 | 9, 11, 18, 20, 23, 28, 37, 44 | climsub 15525 |
. . . . . . 7
β’ (π β (π β β β¦ ((1 / π) β (1 / π))) β ((1 / π) β 0)) |
46 | 14 | subid1d 11509 |
. . . . . . 7
β’ (π β ((1 / π) β 0) = (1 / π)) |
47 | 45, 46 | breqtrd 5135 |
. . . . . 6
β’ (π β (π β β β¦ ((1 / π) β (1 / π))) β (1 / π)) |
48 | 16 | mptex 7177 |
. . . . . . 7
β’ (π β β β¦
((ββ(π / π)) / π)) β V |
49 | 48 | a1i 11 |
. . . . . 6
β’ (π β (π β β β¦
((ββ(π / π)) / π)) β V) |
50 | 1 | nnrecred 12212 |
. . . . . . . . 9
β’ (π β (1 / π) β β) |
51 | 50 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (1 / π) β
β) |
52 | | nnre 12168 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β
β) |
53 | 52 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π₯ β β) |
54 | | nnne0 12195 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β 0) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π₯ β 0) |
56 | 53, 55 | rereccld 11990 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (1 / π₯) β
β) |
57 | 51, 56 | resubcld 11591 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((1 / π) β (1 / π₯)) β
β) |
58 | 42, 57 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦ ((1 / π) β (1 / π)))βπ₯) β β) |
59 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π β β β¦
((ββ(π / π)) / π)) = (π β β β¦
((ββ(π / π)) / π))) |
60 | | fvoveq1 7384 |
. . . . . . . . . 10
β’ (π = π₯ β (ββ(π / π)) = (ββ(π₯ / π))) |
61 | | id 22 |
. . . . . . . . . 10
β’ (π = π₯ β π = π₯) |
62 | 60, 61 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = π₯ β ((ββ(π / π)) / π) = ((ββ(π₯ / π)) / π₯)) |
63 | 62 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π = π₯) β ((ββ(π / π)) / π) = ((ββ(π₯ / π)) / π₯)) |
64 | | ovexd 7396 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) / π₯) β V) |
65 | 59, 63, 32, 64 | fvmptd 6959 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ(π / π)) / π))βπ₯) = ((ββ(π₯ / π)) / π₯)) |
66 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π β β) |
67 | 53, 66 | nndivred 12215 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π₯ / π) β β) |
68 | | reflcl 13710 |
. . . . . . . . 9
β’ ((π₯ / π) β β β
(ββ(π₯ / π)) β
β) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (ββ(π₯ / π)) β β) |
70 | 69, 53, 55 | redivcld 11991 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) / π₯) β β) |
71 | 65, 70 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ(π / π)) / π))βπ₯) β β) |
72 | 67 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π₯ / π) β β) |
73 | | 1cnd 11158 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β 1 β
β) |
74 | | nncn 12169 |
. . . . . . . . . . . 12
β’ (π₯ β β β π₯ β
β) |
75 | 74 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β π₯ β β) |
76 | 72, 73, 75, 55 | divsubdird 11978 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (((π₯ / π) β 1) / π₯) = (((π₯ / π) / π₯) β (1 / π₯))) |
77 | 12 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β π β β) |
78 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β π β 0) |
79 | 75, 77, 78 | divrecd 11942 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (π₯ / π) = (π₯ Β· (1 / π))) |
80 | 79 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β ((π₯ / π) / π₯) = ((π₯ Β· (1 / π)) / π₯)) |
81 | 27, 75, 55 | divcan3d 11944 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β ((π₯ Β· (1 / π)) / π₯) = (1 / π)) |
82 | 80, 81 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β ((π₯ / π) / π₯) = (1 / π)) |
83 | 82 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (((π₯ / π) / π₯) β (1 / π₯)) = ((1 / π) β (1 / π₯))) |
84 | 76, 83 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (((π₯ / π) β 1) / π₯) = ((1 / π) β (1 / π₯))) |
85 | | 1red 11164 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β 1 β
β) |
86 | 67, 85 | resubcld 11591 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β ((π₯ / π) β 1) β
β) |
87 | | nnrp 12934 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β
β+) |
88 | 87 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π₯ β β+) |
89 | 69, 85 | readdcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) + 1) β
β) |
90 | | flle 13713 |
. . . . . . . . . . . . . 14
β’ ((π₯ / π) β β β
(ββ(π₯ / π)) β€ (π₯ / π)) |
91 | 67, 90 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (ββ(π₯ / π)) β€ (π₯ / π)) |
92 | | flflp1 13721 |
. . . . . . . . . . . . . 14
β’ (((π₯ / π) β β β§ (π₯ / π) β β) β
((ββ(π₯ / π)) β€ (π₯ / π) β (π₯ / π) < ((ββ(π₯ / π)) + 1))) |
93 | 67, 67, 92 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) β€ (π₯ / π) β (π₯ / π) < ((ββ(π₯ / π)) + 1))) |
94 | 91, 93 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (π₯ / π) < ((ββ(π₯ / π)) + 1)) |
95 | 67, 89, 85, 94 | ltsub1dd 11775 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β ((π₯ / π) β 1) < (((ββ(π₯ / π)) + 1) β 1)) |
96 | 69 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (ββ(π₯ / π)) β β) |
97 | 96, 73 | pncand 11521 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β
(((ββ(π₯ / π)) + 1) β 1) =
(ββ(π₯ / π))) |
98 | 95, 97 | breqtrd 5135 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β ((π₯ / π) β 1) < (ββ(π₯ / π))) |
99 | 86, 69, 88, 98 | ltdiv1dd 13022 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (((π₯ / π) β 1) / π₯) < ((ββ(π₯ / π)) / π₯)) |
100 | 84, 99 | eqbrtrrd 5133 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((1 / π) β (1 / π₯)) < ((ββ(π₯ / π)) / π₯)) |
101 | 57, 70, 100 | ltled 11311 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((1 / π) β (1 / π₯)) β€ ((ββ(π₯ / π)) / π₯)) |
102 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π = π₯) β π = π₯) |
103 | 102 | fvoveq1d 7383 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π = π₯) β (ββ(π / π)) = (ββ(π₯ / π))) |
104 | 103, 102 | oveq12d 7379 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π = π₯) β ((ββ(π / π)) / π) = ((ββ(π₯ / π)) / π₯)) |
105 | 59, 104, 32, 64 | fvmptd 6959 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ(π / π)) / π))βπ₯) = ((ββ(π₯ / π)) / π₯)) |
106 | 101, 42, 105 | 3brtr4d 5141 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦ ((1 / π) β (1 / π)))βπ₯) β€ ((π β β β¦
((ββ(π / π)) / π))βπ₯)) |
107 | 69, 67, 88, 91 | lediv1dd 13023 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) / π₯) β€ ((π₯ / π) / π₯)) |
108 | 107, 82 | breqtrd 5135 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
((ββ(π₯ / π)) / π₯) β€ (1 / π)) |
109 | 105, 108 | eqbrtrd 5131 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ(π / π)) / π))βπ₯) β€ (1 / π)) |
110 | 9, 11, 47, 49, 58, 71, 106, 109 | climsqz 15532 |
. . . . 5
β’ (π β (π β β β¦
((ββ(π / π)) / π)) β (1 / π)) |
111 | 16 | mptex 7177 |
. . . . . 6
β’ (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β V |
112 | 111 | a1i 11 |
. . . . 5
β’ (π β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β V) |
113 | 3 | zred 12615 |
. . . . . . . . . 10
β’ (π β π½ β β) |
114 | | 1red 11164 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
115 | 113, 114 | resubcld 11591 |
. . . . . . . . 9
β’ (π β (π½ β 1) β β) |
116 | 115, 1 | nndivred 12215 |
. . . . . . . 8
β’ (π β ((π½ β 1) / π) β β) |
117 | 116 | flcld 13712 |
. . . . . . 7
β’ (π β (ββ((π½ β 1) / π)) β β€) |
118 | 117 | zcnd 12616 |
. . . . . 6
β’ (π β (ββ((π½ β 1) / π)) β β) |
119 | | divcnv 15746 |
. . . . . 6
β’
((ββ((π½
β 1) / π)) β
β β (π β
β β¦ ((ββ((π½ β 1) / π)) / π)) β 0) |
120 | 118, 119 | syl 17 |
. . . . 5
β’ (π β (π β β β¦
((ββ((π½ β
1) / π)) / π)) β 0) |
121 | 71 | recnd 11191 |
. . . . 5
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ(π / π)) / π))βπ₯) β β) |
122 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β β β¦
((ββ((π½ β
1) / π)) / π)) = (π β β β¦
((ββ((π½ β
1) / π)) / π))) |
123 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π₯ β ((ββ((π½ β 1) / π)) / π) = ((ββ((π½ β 1) / π)) / π₯)) |
124 | 123 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π = π₯) β ((ββ((π½ β 1) / π)) / π) = ((ββ((π½ β 1) / π)) / π₯)) |
125 | | ovexd 7396 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
((ββ((π½ β
1) / π)) / π₯) β V) |
126 | 122, 124,
32, 125 | fvmptd 6959 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ((π½ β
1) / π)) / π))βπ₯) = ((ββ((π½ β 1) / π)) / π₯)) |
127 | 118 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(ββ((π½ β
1) / π)) β
β) |
128 | 127, 75, 55 | divcld 11939 |
. . . . . 6
β’ ((π β§ π₯ β β) β
((ββ((π½ β
1) / π)) / π₯) β
β) |
129 | 126, 128 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π₯ β β) β ((π β β β¦
((ββ((π½ β
1) / π)) / π))βπ₯) β β) |
130 | 96, 127, 75, 55 | divsubdird 11978 |
. . . . . 6
β’ ((π β§ π₯ β β) β
(((ββ(π₯ / π)) β
(ββ((π½ β
1) / π))) / π₯) = (((ββ(π₯ / π)) / π₯) β ((ββ((π½ β 1) / π)) / π₯))) |
131 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) = (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))) |
132 | 60 | oveq1d 7376 |
. . . . . . . . 9
β’ (π = π₯ β ((ββ(π / π)) β (ββ((π½ β 1) / π))) = ((ββ(π₯ / π)) β (ββ((π½ β 1) / π)))) |
133 | 132, 61 | oveq12d 7379 |
. . . . . . . 8
β’ (π = π₯ β (((ββ(π / π)) β (ββ((π½ β 1) / π))) / π) = (((ββ(π₯ / π)) β (ββ((π½ β 1) / π))) / π₯)) |
134 | 133 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π = π₯) β (((ββ(π / π)) β (ββ((π½ β 1) / π))) / π) = (((ββ(π₯ / π)) β (ββ((π½ β 1) / π))) / π₯)) |
135 | | ovexd 7396 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(((ββ(π₯ / π)) β
(ββ((π½ β
1) / π))) / π₯) β V) |
136 | 131, 134,
32, 135 | fvmptd 6959 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))βπ₯) = (((ββ(π₯ / π)) β (ββ((π½ β 1) / π))) / π₯)) |
137 | 65, 126 | oveq12d 7379 |
. . . . . 6
β’ ((π β§ π₯ β β) β (((π β β β¦
((ββ(π / π)) / π))βπ₯) β ((π β β β¦
((ββ((π½ β
1) / π)) / π))βπ₯)) = (((ββ(π₯ / π)) / π₯) β ((ββ((π½ β 1) / π)) / π₯))) |
138 | 130, 136,
137 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ π₯ β β) β ((π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))βπ₯) = (((π β β β¦
((ββ(π / π)) / π))βπ₯) β ((π β β β¦
((ββ((π½ β
1) / π)) / π))βπ₯))) |
139 | 9, 11, 110, 112, 120, 121, 129, 138 | climsub 15525 |
. . . 4
β’ (π β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β ((1 / π) β 0)) |
140 | 139, 46 | breqtrd 5135 |
. . 3
β’ (π β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
141 | | uzssz 12792 |
. . . . . . 7
β’
(β€β₯β(π½ β 1)) β
β€ |
142 | | resmpt 5995 |
. . . . . . 7
β’
((β€β₯β(π½ β 1)) β β€ β ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β(π½ β 1))) = (π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))) |
143 | 141, 142 | ax-mp 5 |
. . . . . 6
β’ ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β(π½ β 1))) = (π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) |
144 | 143 | breq1i 5116 |
. . . . 5
β’ (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β(π½ β 1))) β (1 / π) β (π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
145 | 3, 11 | zsubcld 12620 |
. . . . . 6
β’ (π β (π½ β 1) β β€) |
146 | | zex 12516 |
. . . . . . 7
β’ β€
β V |
147 | 146 | mptex 7177 |
. . . . . 6
β’ (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β V |
148 | | climres 15466 |
. . . . . 6
β’ (((π½ β 1) β β€ β§
(π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β V) β (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β(π½ β 1))) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π))) |
149 | 145, 147,
148 | sylancl 587 |
. . . . 5
β’ (π β (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β(π½ β 1))) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π))) |
150 | 144, 149 | bitr3id 285 |
. . . 4
β’ (π β ((π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π))) |
151 | 9 | reseq2i 5938 |
. . . . . 6
β’ ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ β) = ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β1)) |
152 | 151 | breq1i 5116 |
. . . . 5
β’ (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ β) β (1 /
π) β ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β1)) β (1 / π)) |
153 | | nnssz 12529 |
. . . . . . 7
β’ β
β β€ |
154 | | resmpt 5995 |
. . . . . . 7
β’ (β
β β€ β ((π
β β€ β¦ (((ββ(π / π)) β (ββ((π½ β 1) / π))) / π)) βΎ β) = (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π))) |
155 | 153, 154 | ax-mp 5 |
. . . . . 6
β’ ((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ β) = (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) |
156 | 155 | breq1i 5116 |
. . . . 5
β’ (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ β) β (1 /
π) β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
157 | | climres 15466 |
. . . . . 6
β’ ((1
β β€ β§ (π
β β€ β¦ (((ββ(π / π)) β (ββ((π½ β 1) / π))) / π)) β V) β (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β1)) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π))) |
158 | 10, 147, 157 | mp2an 691 |
. . . . 5
β’ (((π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) βΎ
(β€β₯β1)) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
159 | 152, 156,
158 | 3bitr3i 301 |
. . . 4
β’ ((π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π) β (π β β€ β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
160 | 150, 159 | bitr4di 289 |
. . 3
β’ (π β ((π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π) β (π β β β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π))) |
161 | 140, 160 | mpbird 257 |
. 2
β’ (π β (π β (β€β₯β(π½ β 1)) β¦
(((ββ(π / π)) β
(ββ((π½ β
1) / π))) / π)) β (1 / π)) |
162 | 8, 161 | eqbrtrd 5131 |
1
β’ (π β (π β (β€β₯β(π½ β 1)) β¦
((β―β(( β₯ β {π}) β© (π½...π))) / π)) β (1 / π)) |