Step | Hyp | Ref
| Expression |
1 | | df-ii 24256 |
. . 3
β’ II =
(MetOpenβ((abs β β ) βΎ ((0[,]1) Γ
(0[,]1)))) |
2 | | cnmet 24151 |
. . . . 5
β’ (abs
β β ) β (Metββ) |
3 | | unitssre 13422 |
. . . . . 6
β’ (0[,]1)
β β |
4 | | ax-resscn 11113 |
. . . . . 6
β’ β
β β |
5 | 3, 4 | sstri 3954 |
. . . . 5
β’ (0[,]1)
β β |
6 | | metres2 23732 |
. . . . 5
β’ (((abs
β β ) β (Metββ) β§ (0[,]1) β β)
β ((abs β β ) βΎ ((0[,]1) Γ (0[,]1))) β
(Metβ(0[,]1))) |
7 | 2, 5, 6 | mp2an 691 |
. . . 4
β’ ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))) β
(Metβ(0[,]1)) |
8 | 7 | a1i 11 |
. . 3
β’ ((π β II β§ (0[,]1) =
βͺ π) β ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))) β (Metβ(0[,]1))) |
9 | | iicmp 24265 |
. . . 4
β’ II β
Comp |
10 | 9 | a1i 11 |
. . 3
β’ ((π β II β§ (0[,]1) =
βͺ π) β II β Comp) |
11 | | simpl 484 |
. . 3
β’ ((π β II β§ (0[,]1) =
βͺ π) β π β II) |
12 | | simpr 486 |
. . 3
β’ ((π β II β§ (0[,]1) =
βͺ π) β (0[,]1) = βͺ π) |
13 | 1, 8, 10, 11, 12 | lebnum 24343 |
. 2
β’ ((π β II β§ (0[,]1) =
βͺ π) β βπ β β+ βπ₯ β (0[,]1)βπ’ β π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’) |
14 | | rpreccl 12946 |
. . . . . . . 8
β’ (π β β+
β (1 / π) β
β+) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β (1 /
π) β
β+) |
16 | 15 | rpred 12962 |
. . . . . 6
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β (1 /
π) β
β) |
17 | 15 | rpge0d 12966 |
. . . . . 6
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β 0 β€ (1
/ π)) |
18 | | flge0nn0 13731 |
. . . . . 6
β’ (((1 /
π) β β β§ 0
β€ (1 / π)) β
(ββ(1 / π))
β β0) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . 5
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β
(ββ(1 / π))
β β0) |
20 | | nn0p1nn 12457 |
. . . . 5
β’
((ββ(1 / π)) β β0 β
((ββ(1 / π)) +
1) β β) |
21 | 19, 20 | syl 17 |
. . . 4
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β
((ββ(1 / π)) +
1) β β) |
22 | | elfznn 13476 |
. . . . . . . . . . . 12
β’ (π β (1...((ββ(1
/ π)) + 1)) β π β
β) |
23 | 22 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β) |
24 | 23 | nnrpd 12960 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β+) |
25 | 21 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
((ββ(1 / π)) +
1) β β) |
26 | 25 | nnrpd 12960 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
((ββ(1 / π)) +
1) β β+) |
27 | 24, 26 | rpdivcld 12979 |
. . . . . . . . 9
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) β
β+) |
28 | 27 | rpred 12962 |
. . . . . . . 8
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) β
β) |
29 | 27 | rpge0d 12966 |
. . . . . . . 8
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0 β€
(π / ((ββ(1 /
π)) + 1))) |
30 | | elfzle2 13451 |
. . . . . . . . . . 11
β’ (π β (1...((ββ(1
/ π)) + 1)) β π β€ ((ββ(1 / π)) + 1)) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β€ ((ββ(1 / π)) + 1)) |
32 | 25 | nnred 12173 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
((ββ(1 / π)) +
1) β β) |
33 | 32 | recnd 11188 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
((ββ(1 / π)) +
1) β β) |
34 | 33 | mulid1d 11177 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((ββ(1 / π)) +
1) Β· 1) = ((ββ(1 / π)) + 1)) |
35 | 31, 34 | breqtrrd 5134 |
. . . . . . . . 9
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β€ (((ββ(1 /
π)) + 1) Β·
1)) |
36 | 23 | nnred 12173 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β) |
37 | | 1red 11161 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 1
β β) |
38 | 25 | nngt0d 12207 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0 <
((ββ(1 / π)) +
1)) |
39 | | ledivmul 12036 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β β§ (((ββ(1 / π)) + 1) β β β§ 0 <
((ββ(1 / π)) +
1))) β ((π /
((ββ(1 / π)) +
1)) β€ 1 β π β€
(((ββ(1 / π)) +
1) Β· 1))) |
40 | 36, 37, 32, 38, 39 | syl112anc 1375 |
. . . . . . . . 9
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β€ 1 β π β€ (((ββ(1 /
π)) + 1) Β·
1))) |
41 | 35, 40 | mpbird 257 |
. . . . . . . 8
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) β€
1) |
42 | | elicc01 13389 |
. . . . . . . 8
β’ ((π / ((ββ(1 / π)) + 1)) β (0[,]1) β
((π / ((ββ(1 /
π)) + 1)) β β
β§ 0 β€ (π /
((ββ(1 / π)) +
1)) β§ (π /
((ββ(1 / π)) +
1)) β€ 1)) |
43 | 28, 29, 41, 42 | syl3anbrc 1344 |
. . . . . . 7
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) β
(0[,]1)) |
44 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π₯ = (π / ((ββ(1 / π)) + 1)) β (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) = ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π)) |
45 | 44 | sseq1d 3976 |
. . . . . . . . 9
β’ (π₯ = (π / ((ββ(1 / π)) + 1)) β ((π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’)) |
46 | 45 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = (π / ((ββ(1 / π)) + 1)) β (βπ’ β π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ’ β π ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’)) |
47 | 46 | rspcv 3576 |
. . . . . . 7
β’ ((π / ((ββ(1 / π)) + 1)) β (0[,]1) β
(βπ₯ β
(0[,]1)βπ’ β
π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ’ β π ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’)) |
48 | 43, 47 | syl 17 |
. . . . . 6
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(βπ₯ β
(0[,]1)βπ’ β
π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ’ β π ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’)) |
49 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β+) |
50 | 49 | rpred 12962 |
. . . . . . . . . . . . 13
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β) |
51 | 28, 50 | resubcld 11588 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β π) β
β) |
52 | 51 | rexrd 11210 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β π) β
β*) |
53 | 28, 50 | readdcld 11189 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) + π) β β) |
54 | 53 | rexrd 11210 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) + π) β
β*) |
55 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β 1) β
β0) |
56 | 23, 55 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π β 1) β
β0) |
57 | 56 | nn0red 12479 |
. . . . . . . . . . . . 13
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π β 1) β
β) |
58 | 57, 25 | nndivred 12212 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π β 1) / ((ββ(1
/ π)) + 1)) β
β) |
59 | 36 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β) |
60 | 57 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π β 1) β
β) |
61 | 25 | nnne0d 12208 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
((ββ(1 / π)) +
1) β 0) |
62 | 59, 60, 33, 61 | divsubdird 11975 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π β (π β 1)) / ((ββ(1 / π)) + 1)) = ((π / ((ββ(1 / π)) + 1)) β ((π β 1) / ((ββ(1 / π)) + 1)))) |
63 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
64 | | nncan 11435 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β (π β
(π β 1)) =
1) |
65 | 59, 63, 64 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π β (π β 1)) = 1) |
66 | 65 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π β (π β 1)) / ((ββ(1 / π)) + 1)) = (1 /
((ββ(1 / π)) +
1))) |
67 | 62, 66 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β ((π β 1) / ((ββ(1
/ π)) + 1))) = (1 /
((ββ(1 / π)) +
1))) |
68 | 49 | rprecred 12973 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (1 /
π) β
β) |
69 | | flltp1 13711 |
. . . . . . . . . . . . . . 15
β’ ((1 /
π) β β β (1
/ π) <
((ββ(1 / π)) +
1)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (1 /
π) < ((ββ(1
/ π)) +
1)) |
71 | | rpgt0 12932 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β 0 < π) |
72 | 71 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0 <
π) |
73 | | ltdiv23 12051 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ (π
β β β§ 0 < π) β§ (((ββ(1 / π)) + 1) β β β§ 0
< ((ββ(1 / π)) + 1))) β ((1 / π) < ((ββ(1 / π)) + 1) β (1 /
((ββ(1 / π)) +
1)) < π)) |
74 | 37, 50, 72, 32, 38, 73 | syl122anc 1380 |
. . . . . . . . . . . . . 14
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((1 /
π) < ((ββ(1
/ π)) + 1) β (1 /
((ββ(1 / π)) +
1)) < π)) |
75 | 70, 74 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (1 /
((ββ(1 / π)) +
1)) < π) |
76 | 67, 75 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β ((π β 1) / ((ββ(1
/ π)) + 1))) < π) |
77 | 28, 58, 50, 76 | ltsub23d 11765 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1)) β π) < ((π β 1) / ((ββ(1 / π)) + 1))) |
78 | 28, 49 | ltaddrpd 12995 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) < ((π / ((ββ(1 / π)) + 1)) + π)) |
79 | | iccssioo 13339 |
. . . . . . . . . . 11
β’
(((((π /
((ββ(1 / π)) +
1)) β π) β
β* β§ ((π / ((ββ(1 / π)) + 1)) + π) β β*) β§ (((π / ((ββ(1 / π)) + 1)) β π) < ((π β 1) / ((ββ(1 / π)) + 1)) β§ (π / ((ββ(1 / π)) + 1)) < ((π / ((ββ(1 / π)) + 1)) + π))) β (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β (((π / ((ββ(1 / π)) + 1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π))) |
80 | 52, 54, 77, 78, 79 | syl22anc 838 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π β 1) /
((ββ(1 / π)) +
1))[,](π /
((ββ(1 / π)) +
1))) β (((π /
((ββ(1 / π)) +
1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π))) |
81 | | 0red 11163 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0
β β) |
82 | 56 | nn0ge0d 12481 |
. . . . . . . . . . . 12
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0 β€
(π β
1)) |
83 | | divge0 12029 |
. . . . . . . . . . . 12
β’ ((((π β 1) β β β§
0 β€ (π β 1)) β§
(((ββ(1 / π)) +
1) β β β§ 0 < ((ββ(1 / π)) + 1))) β 0 β€ ((π β 1) / ((ββ(1 / π)) + 1))) |
84 | 57, 82, 32, 38, 83 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β 0 β€
((π β 1) /
((ββ(1 / π)) +
1))) |
85 | | iccss 13338 |
. . . . . . . . . . 11
β’ (((0
β β β§ 1 β β) β§ (0 β€ ((π β 1) / ((ββ(1 / π)) + 1)) β§ (π / ((ββ(1 / π)) + 1)) β€ 1)) β
(((π β 1) /
((ββ(1 / π)) +
1))[,](π /
((ββ(1 / π)) +
1))) β (0[,]1)) |
86 | 81, 37, 84, 41, 85 | syl22anc 838 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π β 1) /
((ββ(1 / π)) +
1))[,](π /
((ββ(1 / π)) +
1))) β (0[,]1)) |
87 | 80, 86 | ssind 4193 |
. . . . . . . . 9
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π β 1) /
((ββ(1 / π)) +
1))[,](π /
((ββ(1 / π)) +
1))) β ((((π /
((ββ(1 / π)) +
1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π)) β© (0[,]1))) |
88 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
89 | 88 | rexmet 24170 |
. . . . . . . . . . 11
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
90 | | sseqin2 4176 |
. . . . . . . . . . . . 13
β’ ((0[,]1)
β β β (β β© (0[,]1)) = (0[,]1)) |
91 | 3, 90 | mpbi 229 |
. . . . . . . . . . . 12
β’ (β
β© (0[,]1)) = (0[,]1) |
92 | 43, 91 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β (π / ((ββ(1 / π)) + 1)) β (β β©
(0[,]1))) |
93 | | rpxr 12929 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β*) |
94 | 93 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β π β
β*) |
95 | | xpss12 5649 |
. . . . . . . . . . . . . . 15
β’ (((0[,]1)
β β β§ (0[,]1) β β) β ((0[,]1) Γ (0[,]1))
β (β Γ β)) |
96 | 3, 3, 95 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ ((0[,]1)
Γ (0[,]1)) β (β Γ β) |
97 | | resabs1 5968 |
. . . . . . . . . . . . . 14
β’ (((0[,]1)
Γ (0[,]1)) β (β Γ β) β (((abs β
β ) βΎ (β Γ β)) βΎ ((0[,]1) Γ (0[,]1)))
= ((abs β β ) βΎ ((0[,]1) Γ (0[,]1)))) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (((abs
β β ) βΎ (β Γ β)) βΎ ((0[,]1) Γ
(0[,]1))) = ((abs β β ) βΎ ((0[,]1) Γ
(0[,]1))) |
99 | 98 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))) = (((abs β β )
βΎ (β Γ β)) βΎ ((0[,]1) Γ
(0[,]1))) |
100 | 99 | blres 23800 |
. . . . . . . . . . 11
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ (π / ((ββ(1 / π)) + 1)) β (β β© (0[,]1)) β§
π β
β*) β ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) = (((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ (β Γ β)))π) β© (0[,]1))) |
101 | 89, 92, 94, 100 | mp3an2i 1467 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1))(ballβ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))))π) = (((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ (β Γ β)))π) β© (0[,]1))) |
102 | 88 | bl2ioo 24171 |
. . . . . . . . . . . 12
β’ (((π / ((ββ(1 / π)) + 1)) β β β§
π β β) β
((π / ((ββ(1 /
π)) + 1))(ballβ((abs
β β ) βΎ (β Γ β)))π) = (((π / ((ββ(1 / π)) + 1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π))) |
103 | 28, 50, 102 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1))(ballβ((abs
β β ) βΎ (β Γ β)))π) = (((π / ((ββ(1 / π)) + 1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π))) |
104 | 103 | ineq1d 4172 |
. . . . . . . . . 10
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π / ((ββ(1 /
π)) + 1))(ballβ((abs
β β ) βΎ (β Γ β)))π) β© (0[,]1)) = ((((π / ((ββ(1 / π)) + 1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π)) β© (0[,]1))) |
105 | 101, 104 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β ((π / ((ββ(1 / π)) + 1))(ballβ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))))π) = ((((π / ((ββ(1 / π)) + 1)) β π)(,)((π / ((ββ(1 / π)) + 1)) + π)) β© (0[,]1))) |
106 | 87, 105 | sseqtrrd 3986 |
. . . . . . . 8
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π β 1) /
((ββ(1 / π)) +
1))[,](π /
((ββ(1 / π)) +
1))) β ((π /
((ββ(1 / π)) +
1))(ballβ((abs β β ) βΎ ((0[,]1) Γ (0[,]1))))π)) |
107 | | sstr2 3952 |
. . . . . . . 8
β’ ((((π β 1) / ((ββ(1
/ π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β ((π / ((ββ(1 / π)) + 1))(ballβ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))))π) β (((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’ β (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
108 | 106, 107 | syl 17 |
. . . . . . 7
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(((π / ((ββ(1 /
π)) + 1))(ballβ((abs
β β ) βΎ ((0[,]1) Γ (0[,]1))))π) β π’ β (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
109 | 108 | reximdv 3164 |
. . . . . 6
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(βπ’ β π ((π / ((ββ(1 / π)) + 1))(ballβ((abs β β )
βΎ ((0[,]1) Γ (0[,]1))))π) β π’ β βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
110 | 48, 109 | syld 47 |
. . . . 5
β’ ((((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β§ π β (1...((ββ(1
/ π)) + 1))) β
(βπ₯ β
(0[,]1)βπ’ β
π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
111 | 110 | ralrimdva 3148 |
. . . 4
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β
(βπ₯ β
(0[,]1)βπ’ β
π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ β (1...((ββ(1 / π)) + 1))βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
112 | | oveq2 7366 |
. . . . . 6
β’ (π = ((ββ(1 / π)) + 1) β (1...π) = (1...((ββ(1 /
π)) + 1))) |
113 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = ((ββ(1 / π)) + 1) β ((π β 1) / π) = ((π β 1) / ((ββ(1 / π)) + 1))) |
114 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = ((ββ(1 / π)) + 1) β (π / π) = (π / ((ββ(1 / π)) + 1))) |
115 | 113, 114 | oveq12d 7376 |
. . . . . . . 8
β’ (π = ((ββ(1 / π)) + 1) β (((π β 1) / π)[,](π / π)) = (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1)))) |
116 | 115 | sseq1d 3976 |
. . . . . . 7
β’ (π = ((ββ(1 / π)) + 1) β ((((π β 1) / π)[,](π / π)) β π’ β (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
117 | 116 | rexbidv 3172 |
. . . . . 6
β’ (π = ((ββ(1 / π)) + 1) β (βπ’ β π (((π β 1) / π)[,](π / π)) β π’ β βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
118 | 112, 117 | raleqbidv 3318 |
. . . . 5
β’ (π = ((ββ(1 / π)) + 1) β (βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’ β βπ β (1...((ββ(1 / π)) + 1))βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’)) |
119 | 118 | rspcev 3580 |
. . . 4
β’
((((ββ(1 / π)) + 1) β β β§ βπ β (1...((ββ(1
/ π)) + 1))βπ’ β π (((π β 1) / ((ββ(1 / π)) + 1))[,](π / ((ββ(1 / π)) + 1))) β π’) β βπ β β βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’) |
120 | 21, 111, 119 | syl6an 683 |
. . 3
β’ (((π β II β§ (0[,]1) =
βͺ π) β§ π β β+) β
(βπ₯ β
(0[,]1)βπ’ β
π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ β β βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’)) |
121 | 120 | rexlimdva 3149 |
. 2
β’ ((π β II β§ (0[,]1) =
βͺ π) β (βπ β β+ βπ₯ β (0[,]1)βπ’ β π (π₯(ballβ((abs β β ) βΎ
((0[,]1) Γ (0[,]1))))π) β π’ β βπ β β βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’)) |
122 | 13, 121 | mpd 15 |
1
β’ ((π β II β§ (0[,]1) =
βͺ π) β βπ β β βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’) |