Step | Hyp | Ref
| Expression |
1 | | padic.j |
. . . . . . 7
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
2 | 1 | padicval 27117 |
. . . . . 6
β’ ((π β β β§ π¦ β β) β ((π½βπ)βπ¦) = if(π¦ = 0, 0, (πβ-(π pCnt π¦)))) |
3 | 2 | adantlr 713 |
. . . . 5
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β ((π½βπ)βπ¦) = if(π¦ = 0, 0, (πβ-(π pCnt π¦)))) |
4 | 3 | oveq1d 7423 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (((π½βπ)βπ¦)βππ
) = (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
)) |
5 | | ovif 7505 |
. . . . 5
β’ (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
) = if(π¦ = 0, (0βππ
), ((πβ-(π pCnt π¦))βππ
)) |
6 | | rpre 12981 |
. . . . . . . . . 10
β’ (π
β β+
β π
β
β) |
7 | 6 | adantl 482 |
. . . . . . . . 9
β’ ((π β β β§ π
β β+)
β π
β
β) |
8 | 7 | recnd 11241 |
. . . . . . . 8
β’ ((π β β β§ π
β β+)
β π
β
β) |
9 | | rpne0 12989 |
. . . . . . . . 9
β’ (π
β β+
β π
β
0) |
10 | 9 | adantl 482 |
. . . . . . . 8
β’ ((π β β β§ π
β β+)
β π
β
0) |
11 | 8, 10 | 0cxpd 26217 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β (0βππ
) = 0) |
12 | 11 | adantr 481 |
. . . . . 6
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (0βππ
) = 0) |
13 | 12 | ifeq1d 4547 |
. . . . 5
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β if(π¦ = 0,
(0βππ
), ((πβ-(π pCnt π¦))βππ
)) = if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
))) |
14 | 5, 13 | eqtrid 2784 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
) = if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
))) |
15 | | df-ne 2941 |
. . . . . 6
β’ (π¦ β 0 β Β¬ π¦ = 0) |
16 | | pcqcl 16788 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π¦ β β β§ π¦ β 0)) β (π pCnt π¦) β β€) |
17 | 16 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(π pCnt π¦) β β€) |
18 | 17 | zcnd 12666 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(π pCnt π¦) β β) |
19 | 8 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π
β
β) |
20 | | mulneg12 11651 |
. . . . . . . . . . . 12
β’ (((π pCnt π¦) β β β§ π
β β) β (-(π pCnt π¦) Β· π
) = ((π pCnt π¦) Β· -π
)) |
21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(-(π pCnt π¦) Β· π
) = ((π pCnt π¦) Β· -π
)) |
22 | 19 | negcld 11557 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-π
β
β) |
23 | 18, 22 | mulcomd 11234 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((π pCnt π¦) Β· -π
) = (-π
Β· (π pCnt π¦))) |
24 | 21, 23 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(-(π pCnt π¦) Β· π
) = (-π
Β· (π pCnt π¦))) |
25 | 24 | oveq2d 7424 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-(π pCnt π¦) Β· π
)) = (πβπ(-π
Β· (π pCnt π¦)))) |
26 | | prmuz2 16632 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
(β€β₯β2)) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π
β β+)
β π β
(β€β₯β2)) |
28 | | eluz2b2 12904 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π
β β+)
β (π β β
β§ 1 < π)) |
30 | 29 | simpld 495 |
. . . . . . . . . . . 12
β’ ((π β β β§ π
β β+)
β π β
β) |
31 | 30 | nnrpd 13013 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
β+) |
32 | 31 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β
β+) |
33 | 17 | znegcld 12667 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-(π pCnt π¦) β β€) |
34 | 33 | zred 12665 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-(π pCnt π¦) β β) |
35 | 32, 34, 19 | cxpmuld 26243 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-(π pCnt π¦) Β· π
)) = ((πβπ-(π pCnt π¦))βππ
)) |
36 | 7 | renegcld 11640 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β -π
β
β) |
37 | 36 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-π
β
β) |
38 | 32, 37, 18 | cxpmuld 26243 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-π
Β· (π pCnt π¦))) = ((πβπ-π
)βπ(π pCnt π¦))) |
39 | 25, 35, 38 | 3eqtr3d 2780 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-(π pCnt π¦))βππ
) = ((πβπ-π
)βπ(π pCnt π¦))) |
40 | 30 | nnred 12226 |
. . . . . . . . . . . 12
β’ ((π β β β§ π
β β+)
β π β
β) |
41 | 40 | recnd 11241 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
β) |
42 | 41 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β
β) |
43 | 30 | nnne0d 12261 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
0) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β 0) |
45 | 42, 44, 33 | cxpexpzd 26218 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-(π pCnt π¦)) = (πβ-(π pCnt π¦))) |
46 | 45 | oveq1d 7423 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-(π pCnt π¦))βππ
) = ((πβ-(π pCnt π¦))βππ
)) |
47 | 31, 36 | rpcxpcld 26239 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β
β+) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β
β+) |
49 | 48 | rpcnd 13017 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β β) |
50 | 48 | rpne0d 13020 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β 0) |
51 | 49, 50, 17 | cxpexpzd 26218 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-π
)βπ(π pCnt π¦)) = ((πβπ-π
)β(π pCnt π¦))) |
52 | 39, 46, 51 | 3eqtr3d 2780 |
. . . . . . 7
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
53 | 52 | anassrs 468 |
. . . . . 6
β’ ((((π β β β§ π
β β+)
β§ π¦ β β)
β§ π¦ β 0) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
54 | 15, 53 | sylan2br 595 |
. . . . 5
β’ ((((π β β β§ π
β β+)
β§ π¦ β β)
β§ Β¬ π¦ = 0) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
55 | 54 | ifeq2da 4560 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
)) = if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
56 | 4, 14, 55 | 3eqtrd 2776 |
. . 3
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (((π½βπ)βπ¦)βππ
) = if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
57 | 56 | mpteq2dva 5248 |
. 2
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ
)) = (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦))))) |
58 | | rpre 12981 |
. . . . 5
β’ ((πβπ-π
) β β+
β (πβπ-π
) β β) |
59 | 47, 58 | syl 17 |
. . . 4
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β β) |
60 | | rpgt0 12985 |
. . . . 5
β’ ((πβπ-π
) β β+
β 0 < (πβπ-π
)) |
61 | 47, 60 | syl 17 |
. . . 4
β’ ((π β β β§ π
β β+)
β 0 < (πβπ-π
)) |
62 | | rpgt0 12985 |
. . . . . . . 8
β’ (π
β β+
β 0 < π
) |
63 | 62 | adantl 482 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 0 < π
) |
64 | 7 | lt0neg2d 11783 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β (0 < π
β
-π
<
0)) |
65 | 63, 64 | mpbid 231 |
. . . . . 6
β’ ((π β β β§ π
β β+)
β -π
<
0) |
66 | 29 | simprd 496 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 1 < π) |
67 | | 0red 11216 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 0 β β) |
68 | 40, 66, 36, 67 | cxpltd 26226 |
. . . . . 6
β’ ((π β β β§ π
β β+)
β (-π
< 0 β
(πβπ-π
) < (πβπ0))) |
69 | 65, 68 | mpbid 231 |
. . . . 5
β’ ((π β β β§ π
β β+)
β (πβπ-π
) < (πβπ0)) |
70 | 41 | cxp0d 26212 |
. . . . 5
β’ ((π β β β§ π
β β+)
β (πβπ0) =
1) |
71 | 69, 70 | breqtrd 5174 |
. . . 4
β’ ((π β β β§ π
β β+)
β (πβπ-π
) < 1) |
72 | | 0xr 11260 |
. . . . 5
β’ 0 β
β* |
73 | | 1xr 11272 |
. . . . 5
β’ 1 β
β* |
74 | | elioo2 13364 |
. . . . 5
β’ ((0
β β* β§ 1 β β*) β ((πβπ-π
) β (0(,)1) β ((πβπ-π
) β β β§ 0 <
(πβπ-π
) β§ (πβπ-π
) < 1))) |
75 | 72, 73, 74 | mp2an 690 |
. . . 4
β’ ((πβπ-π
) β (0(,)1) β ((πβπ-π
) β β β§ 0 <
(πβπ-π
) β§ (πβπ-π
) < 1)) |
76 | 59, 61, 71, 75 | syl3anbrc 1343 |
. . 3
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β (0(,)1)) |
77 | | qrng.q |
. . . 4
β’ π = (βfld
βΎs β) |
78 | | qabsabv.a |
. . . 4
β’ π΄ = (AbsValβπ) |
79 | | eqid 2732 |
. . . 4
β’ (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) = (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
80 | 77, 78, 79 | padicabv 27130 |
. . 3
β’ ((π β β β§ (πβπ-π
) β (0(,)1)) β (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) β π΄) |
81 | 76, 80 | syldan 591 |
. 2
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ if(π¦ = 0, 0,
((πβπ-π
)β(π pCnt π¦)))) β π΄) |
82 | 57, 81 | eqeltrd 2833 |
1
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ
)) β π΄) |