Step | Hyp | Ref
| Expression |
1 | | qex 12894 |
. . . 4
β’ β
β V |
2 | 1 | mptex 7177 |
. . 3
β’ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯)))) β V |
3 | | padic.j |
. . 3
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
4 | 2, 3 | fnmpti 6648 |
. 2
β’ π½ Fn β |
5 | 3 | padicfval 26987 |
. . . . 5
β’ (π β β β (π½βπ) = (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
6 | | prmnn 16558 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
7 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β
β) |
8 | 7 | nncnd 12177 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β
β) |
9 | 7 | nnne0d 12211 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β 0) |
10 | | df-ne 2941 |
. . . . . . . . . 10
β’ (π₯ β 0 β Β¬ π₯ = 0) |
11 | | pcqcl 16736 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β β β§ π₯ β 0)) β (π pCnt π₯) β β€) |
12 | 11 | anassrs 469 |
. . . . . . . . . 10
β’ (((π β β β§ π₯ β β) β§ π₯ β 0) β (π pCnt π₯) β β€) |
13 | 10, 12 | sylan2br 596 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (π pCnt π₯) β β€) |
14 | 8, 9, 13 | expnegd 14067 |
. . . . . . . 8
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (πβ-(π pCnt π₯)) = (1 / (πβ(π pCnt π₯)))) |
15 | 8, 9, 13 | exprecd 14068 |
. . . . . . . 8
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β ((1 / π)β(π pCnt π₯)) = (1 / (πβ(π pCnt π₯)))) |
16 | 14, 15 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (πβ-(π pCnt π₯)) = ((1 / π)β(π pCnt π₯))) |
17 | 16 | ifeq2da 4522 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β if(π₯ = 0, 0, (πβ-(π pCnt π₯))) = if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) |
18 | 17 | mpteq2dva 5209 |
. . . . 5
β’ (π β β β (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯)))) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯))))) |
19 | 5, 18 | eqtrd 2773 |
. . . 4
β’ (π β β β (π½βπ) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯))))) |
20 | 6 | nnrecred 12212 |
. . . . . 6
β’ (π β β β (1 /
π) β
β) |
21 | 6 | nnred 12176 |
. . . . . . . 8
β’ (π β β β π β
β) |
22 | | prmgt1 16581 |
. . . . . . . 8
β’ (π β β β 1 <
π) |
23 | | recgt1i 12060 |
. . . . . . . 8
β’ ((π β β β§ 1 <
π) β (0 < (1 /
π) β§ (1 / π) < 1)) |
24 | 21, 22, 23 | syl2anc 585 |
. . . . . . 7
β’ (π β β β (0 <
(1 / π) β§ (1 / π) < 1)) |
25 | 24 | simpld 496 |
. . . . . 6
β’ (π β β β 0 < (1
/ π)) |
26 | 24 | simprd 497 |
. . . . . 6
β’ (π β β β (1 /
π) < 1) |
27 | | 0xr 11210 |
. . . . . . 7
β’ 0 β
β* |
28 | | 1xr 11222 |
. . . . . . 7
β’ 1 β
β* |
29 | | elioo2 13314 |
. . . . . . 7
β’ ((0
β β* β§ 1 β β*) β ((1 /
π) β (0(,)1) β
((1 / π) β β
β§ 0 < (1 / π) β§
(1 / π) <
1))) |
30 | 27, 28, 29 | mp2an 691 |
. . . . . 6
β’ ((1 /
π) β (0(,)1) β
((1 / π) β β
β§ 0 < (1 / π) β§
(1 / π) <
1)) |
31 | 20, 25, 26, 30 | syl3anbrc 1344 |
. . . . 5
β’ (π β β β (1 /
π) β
(0(,)1)) |
32 | | qrng.q |
. . . . . 6
β’ π = (βfld
βΎs β) |
33 | | qabsabv.a |
. . . . . 6
β’ π΄ = (AbsValβπ) |
34 | | eqid 2733 |
. . . . . 6
β’ (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) |
35 | 32, 33, 34 | padicabv 27001 |
. . . . 5
β’ ((π β β β§ (1 / π) β (0(,)1)) β (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) β π΄) |
36 | 31, 35 | mpdan 686 |
. . . 4
β’ (π β β β (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) β π΄) |
37 | 19, 36 | eqeltrd 2834 |
. . 3
β’ (π β β β (π½βπ) β π΄) |
38 | 37 | rgen 3063 |
. 2
β’
βπ β
β (π½βπ) β π΄ |
39 | | ffnfv 7070 |
. 2
β’ (π½:ββΆπ΄ β (π½ Fn β β§ βπ β β (π½βπ) β π΄)) |
40 | 4, 38, 39 | mpbir2an 710 |
1
β’ π½:ββΆπ΄ |