Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . 3
β’
((βfld βΎs β)
βs πΌ) = ((βfld
βΎs β) βs πΌ) |
2 | | eqid 2736 |
. . 3
β’
(distβ((βfld βΎs β)
βs πΌ)) = (distβ((βfld
βΎs β) βs πΌ)) |
3 | | rrntotbnd.1 |
. . 3
β’ π = (β βm
πΌ) |
4 | 1, 2, 3 | repwsmet 36033 |
. 2
β’ (πΌ β Fin β
(distβ((βfld βΎs β)
βs πΌ)) β (Metβπ)) |
5 | 3 | rrnmet 36028 |
. 2
β’ (πΌ β Fin β
(βnβπΌ) β (Metβπ)) |
6 | | hashcl 14112 |
. . . 4
β’ (πΌ β Fin β
(β―βπΌ) β
β0) |
7 | | nn0re 12284 |
. . . . 5
β’
((β―βπΌ)
β β0 β (β―βπΌ) β β) |
8 | | nn0ge0 12300 |
. . . . 5
β’
((β―βπΌ)
β β0 β 0 β€ (β―βπΌ)) |
9 | 7, 8 | resqrtcld 15170 |
. . . 4
β’
((β―βπΌ)
β β0 β (ββ(β―βπΌ)) β
β) |
10 | 6, 9 | syl 17 |
. . 3
β’ (πΌ β Fin β
(ββ(β―βπΌ)) β β) |
11 | 7, 8 | sqrtge0d 15173 |
. . . 4
β’
((β―βπΌ)
β β0 β 0 β€ (ββ(β―βπΌ))) |
12 | 6, 11 | syl 17 |
. . 3
β’ (πΌ β Fin β 0 β€
(ββ(β―βπΌ))) |
13 | 10, 12 | ge0p1rpd 12844 |
. 2
β’ (πΌ β Fin β
((ββ(β―βπΌ)) + 1) β
β+) |
14 | | 1rp 12776 |
. . 3
β’ 1 β
β+ |
15 | 14 | a1i 11 |
. 2
β’ (πΌ β Fin β 1 β
β+) |
16 | | metcl 23526 |
. . . . 5
β’
(((βnβπΌ) β (Metβπ) β§ π₯ β π β§ π¦ β π) β (π₯(βnβπΌ)π¦) β β) |
17 | 16 | 3expb 1120 |
. . . 4
β’
(((βnβπΌ) β (Metβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) β β) |
18 | 5, 17 | sylan 581 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) β β) |
19 | 10 | adantr 482 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
(ββ(β―βπΌ)) β β) |
20 | 4 | adantr 482 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
(distβ((βfld βΎs β)
βs πΌ)) β (Metβπ)) |
21 | | simprl 769 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
22 | | simprr 771 |
. . . . . 6
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
23 | | metcl 23526 |
. . . . . . 7
β’
(((distβ((βfld βΎs β)
βs πΌ)) β (Metβπ) β§ π₯ β π β§ π¦ β π) β (π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β β) |
24 | | metge0 23539 |
. . . . . . 7
β’
(((distβ((βfld βΎs β)
βs πΌ)) β (Metβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)) |
25 | 23, 24 | jca 513 |
. . . . . 6
β’
(((distβ((βfld βΎs β)
βs πΌ)) β (Metβπ) β§ π₯ β π β§ π¦ β π) β ((π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β β β§ 0 β€ (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
26 | 20, 21, 22, 25 | syl3anc 1371 |
. . . . 5
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β β β§ 0 β€ (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
27 | 26 | simpld 496 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β β) |
28 | 19, 27 | remulcld 11047 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
((ββ(β―βπΌ)) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)) β β) |
29 | | peano2re 11190 |
. . . . . 6
β’
((ββ(β―βπΌ)) β β β
((ββ(β―βπΌ)) + 1) β β) |
30 | 10, 29 | syl 17 |
. . . . 5
β’ (πΌ β Fin β
((ββ(β―βπΌ)) + 1) β β) |
31 | 30 | adantr 482 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
((ββ(β―βπΌ)) + 1) β β) |
32 | 31, 27 | remulcld 11047 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
(((ββ(β―βπΌ)) + 1) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)) β β) |
33 | | id 22 |
. . . . 5
β’ (πΌ β Fin β πΌ β Fin) |
34 | 1, 2, 3, 33 | rrnequiv 36034 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β ((π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β€ (π₯(βnβπΌ)π¦) β§ (π₯(βnβπΌ)π¦) β€ ((ββ(β―βπΌ)) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)))) |
35 | 34 | simprd 497 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) β€ ((ββ(β―βπΌ)) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
36 | 19 | lep1d 11948 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
(ββ(β―βπΌ)) β€ ((ββ(β―βπΌ)) + 1)) |
37 | | lemul1a 11871 |
. . . 4
β’
((((ββ(β―βπΌ)) β β β§
((ββ(β―βπΌ)) + 1) β β β§ ((π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β β β§ 0 β€ (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) β§ (ββ(β―βπΌ)) β€
((ββ(β―βπΌ)) + 1)) β
((ββ(β―βπΌ)) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)) β€ (((ββ(β―βπΌ)) + 1) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
38 | 19, 31, 26, 36, 37 | syl31anc 1373 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β
((ββ(β―βπΌ)) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦)) β€ (((ββ(β―βπΌ)) + 1) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
39 | 18, 28, 32, 35, 38 | letrd 11174 |
. 2
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) β€ (((ββ(β―βπΌ)) + 1) Β· (π₯(distβ((βfld
βΎs β) βs πΌ))π¦))) |
40 | 34 | simpld 496 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β€ (π₯(βnβπΌ)π¦)) |
41 | 18 | recnd 11045 |
. . . 4
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(βnβπΌ)π¦) β β) |
42 | 41 | mulid2d 11035 |
. . 3
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (1 Β· (π₯(βnβπΌ)π¦)) = (π₯(βnβπΌ)π¦)) |
43 | 40, 42 | breqtrrd 5109 |
. 2
β’ ((πΌ β Fin β§ (π₯ β π β§ π¦ β π)) β (π₯(distβ((βfld
βΎs β) βs πΌ))π¦) β€ (1 Β· (π₯(βnβπΌ)π¦))) |
44 | | eqid 2736 |
. 2
β’
((distβ((βfld βΎs β)
βs πΌ)) βΎ (π Γ π)) = ((distβ((βfld
βΎs β) βs πΌ)) βΎ (π Γ π)) |
45 | | rrntotbnd.2 |
. 2
β’ π =
((βnβπΌ) βΎ (π Γ π)) |
46 | | ax-resscn 10970 |
. . 3
β’ β
β β |
47 | 1, 44 | cnpwstotbnd 35996 |
. . 3
β’ ((β
β β β§ πΌ
β Fin) β (((distβ((βfld βΎs
β) βs πΌ)) βΎ (π Γ π)) β (TotBndβπ) β
((distβ((βfld βΎs β)
βs πΌ)) βΎ (π Γ π)) β (Bndβπ))) |
48 | 46, 47 | mpan 688 |
. 2
β’ (πΌ β Fin β
(((distβ((βfld βΎs β)
βs πΌ)) βΎ (π Γ π)) β (TotBndβπ) β
((distβ((βfld βΎs β)
βs πΌ)) βΎ (π Γ π)) β (Bndβπ))) |
49 | 4, 5, 13, 15, 39, 43, 44, 45, 48 | equivbnd2 35991 |
1
β’ (πΌ β Fin β (π β (TotBndβπ) β π β (Bndβπ))) |