Step | Hyp | Ref
| Expression |
1 | | qex 12949 |
. . . 4
β’ β
β V |
2 | 1 | mptex 7220 |
. . 3
β’ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯)))) β V |
3 | | padic.j |
. . 3
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
4 | 2, 3 | fnmpti 6687 |
. 2
β’ π½ Fn β |
5 | 3 | padicfval 27504 |
. . . . 5
β’ (π β β β (π½βπ) = (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
6 | | prmnn 16618 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
7 | 6 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β
β) |
8 | 7 | nncnd 12232 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β
β) |
9 | 7 | nnne0d 12266 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β π β 0) |
10 | | df-ne 2935 |
. . . . . . . . . 10
β’ (π₯ β 0 β Β¬ π₯ = 0) |
11 | | pcqcl 16798 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β β β§ π₯ β 0)) β (π pCnt π₯) β β€) |
12 | 11 | anassrs 467 |
. . . . . . . . . 10
β’ (((π β β β§ π₯ β β) β§ π₯ β 0) β (π pCnt π₯) β β€) |
13 | 10, 12 | sylan2br 594 |
. . . . . . . . 9
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (π pCnt π₯) β β€) |
14 | 8, 9, 13 | expnegd 14123 |
. . . . . . . 8
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (πβ-(π pCnt π₯)) = (1 / (πβ(π pCnt π₯)))) |
15 | 8, 9, 13 | exprecd 14124 |
. . . . . . . 8
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β ((1 / π)β(π pCnt π₯)) = (1 / (πβ(π pCnt π₯)))) |
16 | 14, 15 | eqtr4d 2769 |
. . . . . . 7
β’ (((π β β β§ π₯ β β) β§ Β¬
π₯ = 0) β (πβ-(π pCnt π₯)) = ((1 / π)β(π pCnt π₯))) |
17 | 16 | ifeq2da 4555 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β if(π₯ = 0, 0, (πβ-(π pCnt π₯))) = if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) |
18 | 17 | mpteq2dva 5241 |
. . . . 5
β’ (π β β β (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯)))) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯))))) |
19 | 5, 18 | eqtrd 2766 |
. . . 4
β’ (π β β β (π½βπ) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯))))) |
20 | 6 | nnrecred 12267 |
. . . . . 6
β’ (π β β β (1 /
π) β
β) |
21 | 6 | nnred 12231 |
. . . . . . . 8
β’ (π β β β π β
β) |
22 | | prmgt1 16641 |
. . . . . . . 8
β’ (π β β β 1 <
π) |
23 | | recgt1i 12115 |
. . . . . . . 8
β’ ((π β β β§ 1 <
π) β (0 < (1 /
π) β§ (1 / π) < 1)) |
24 | 21, 22, 23 | syl2anc 583 |
. . . . . . 7
β’ (π β β β (0 <
(1 / π) β§ (1 / π) < 1)) |
25 | 24 | simpld 494 |
. . . . . 6
β’ (π β β β 0 < (1
/ π)) |
26 | 24 | simprd 495 |
. . . . . 6
β’ (π β β β (1 /
π) < 1) |
27 | | 0xr 11265 |
. . . . . . 7
β’ 0 β
β* |
28 | | 1xr 11277 |
. . . . . . 7
β’ 1 β
β* |
29 | | elioo2 13371 |
. . . . . . 7
β’ ((0
β β* β§ 1 β β*) β ((1 /
π) β (0(,)1) β
((1 / π) β β
β§ 0 < (1 / π) β§
(1 / π) <
1))) |
30 | 27, 28, 29 | mp2an 689 |
. . . . . 6
β’ ((1 /
π) β (0(,)1) β
((1 / π) β β
β§ 0 < (1 / π) β§
(1 / π) <
1)) |
31 | 20, 25, 26, 30 | syl3anbrc 1340 |
. . . . 5
β’ (π β β β (1 /
π) β
(0(,)1)) |
32 | | qrng.q |
. . . . . 6
β’ π = (βfld
βΎs β) |
33 | | qabsabv.a |
. . . . . 6
β’ π΄ = (AbsValβπ) |
34 | | eqid 2726 |
. . . . . 6
β’ (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) = (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) |
35 | 32, 33, 34 | padicabv 27518 |
. . . . 5
β’ ((π β β β§ (1 / π) β (0(,)1)) β (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) β π΄) |
36 | 31, 35 | mpdan 684 |
. . . 4
β’ (π β β β (π₯ β β β¦ if(π₯ = 0, 0, ((1 / π)β(π pCnt π₯)))) β π΄) |
37 | 19, 36 | eqeltrd 2827 |
. . 3
β’ (π β β β (π½βπ) β π΄) |
38 | 37 | rgen 3057 |
. 2
β’
βπ β
β (π½βπ) β π΄ |
39 | | ffnfv 7114 |
. 2
β’ (π½:ββΆπ΄ β (π½ Fn β β§ βπ β β (π½βπ) β π΄)) |
40 | 4, 38, 39 | mpbir2an 708 |
1
β’ π½:ββΆπ΄ |