Step | Hyp | Ref
| Expression |
1 | | padic.j |
. . . . . . 7
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
2 | 1 | padicval 26988 |
. . . . . 6
β’ ((π β β β§ π¦ β β) β ((π½βπ)βπ¦) = if(π¦ = 0, 0, (πβ-(π pCnt π¦)))) |
3 | 2 | adantlr 714 |
. . . . 5
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β ((π½βπ)βπ¦) = if(π¦ = 0, 0, (πβ-(π pCnt π¦)))) |
4 | 3 | oveq1d 7376 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (((π½βπ)βπ¦)βππ
) = (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
)) |
5 | | ovif 7458 |
. . . . 5
β’ (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
) = if(π¦ = 0, (0βππ
), ((πβ-(π pCnt π¦))βππ
)) |
6 | | rpre 12931 |
. . . . . . . . . 10
β’ (π
β β+
β π
β
β) |
7 | 6 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π
β β+)
β π
β
β) |
8 | 7 | recnd 11191 |
. . . . . . . 8
β’ ((π β β β§ π
β β+)
β π
β
β) |
9 | | rpne0 12939 |
. . . . . . . . 9
β’ (π
β β+
β π
β
0) |
10 | 9 | adantl 483 |
. . . . . . . 8
β’ ((π β β β§ π
β β+)
β π
β
0) |
11 | 8, 10 | 0cxpd 26088 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β (0βππ
) = 0) |
12 | 11 | adantr 482 |
. . . . . 6
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (0βππ
) = 0) |
13 | 12 | ifeq1d 4509 |
. . . . 5
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β if(π¦ = 0,
(0βππ
), ((πβ-(π pCnt π¦))βππ
)) = if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
))) |
14 | 5, 13 | eqtrid 2785 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (if(π¦ = 0, 0, (πβ-(π pCnt π¦)))βππ
) = if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
))) |
15 | | df-ne 2941 |
. . . . . 6
β’ (π¦ β 0 β Β¬ π¦ = 0) |
16 | | pcqcl 16736 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π¦ β β β§ π¦ β 0)) β (π pCnt π¦) β β€) |
17 | 16 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(π pCnt π¦) β β€) |
18 | 17 | zcnd 12616 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(π pCnt π¦) β β) |
19 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π
β
β) |
20 | | mulneg12 11601 |
. . . . . . . . . . . 12
β’ (((π pCnt π¦) β β β§ π
β β) β (-(π pCnt π¦) Β· π
) = ((π pCnt π¦) Β· -π
)) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(-(π pCnt π¦) Β· π
) = ((π pCnt π¦) Β· -π
)) |
22 | 19 | negcld 11507 |
. . . . . . . . . . . 12
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-π
β
β) |
23 | 18, 22 | mulcomd 11184 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((π pCnt π¦) Β· -π
) = (-π
Β· (π pCnt π¦))) |
24 | 21, 23 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(-(π pCnt π¦) Β· π
) = (-π
Β· (π pCnt π¦))) |
25 | 24 | oveq2d 7377 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-(π pCnt π¦) Β· π
)) = (πβπ(-π
Β· (π pCnt π¦)))) |
26 | | prmuz2 16580 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
(β€β₯β2)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π
β β+)
β π β
(β€β₯β2)) |
28 | | eluz2b2 12854 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π
β β+)
β (π β β
β§ 1 < π)) |
30 | 29 | simpld 496 |
. . . . . . . . . . . 12
β’ ((π β β β§ π
β β+)
β π β
β) |
31 | 30 | nnrpd 12963 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
β+) |
32 | 31 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β
β+) |
33 | 17 | znegcld 12617 |
. . . . . . . . . . 11
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-(π pCnt π¦) β β€) |
34 | 33 | zred 12615 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-(π pCnt π¦) β β) |
35 | 32, 34, 19 | cxpmuld 26114 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-(π pCnt π¦) Β· π
)) = ((πβπ-(π pCnt π¦))βππ
)) |
36 | 7 | renegcld 11590 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β -π
β
β) |
37 | 36 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
-π
β
β) |
38 | 32, 37, 18 | cxpmuld 26114 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ(-π
Β· (π pCnt π¦))) = ((πβπ-π
)βπ(π pCnt π¦))) |
39 | 25, 35, 38 | 3eqtr3d 2781 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-(π pCnt π¦))βππ
) = ((πβπ-π
)βπ(π pCnt π¦))) |
40 | 30 | nnred 12176 |
. . . . . . . . . . . 12
β’ ((π β β β§ π
β β+)
β π β
β) |
41 | 40 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
β) |
42 | 41 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β
β) |
43 | 30 | nnne0d 12211 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β π β
0) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
π β 0) |
45 | 42, 44, 33 | cxpexpzd 26089 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-(π pCnt π¦)) = (πβ-(π pCnt π¦))) |
46 | 45 | oveq1d 7376 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-(π pCnt π¦))βππ
) = ((πβ-(π pCnt π¦))βππ
)) |
47 | 31, 36 | rpcxpcld 26110 |
. . . . . . . . . . 11
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β
β+) |
48 | 47 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β
β+) |
49 | 48 | rpcnd 12967 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β β) |
50 | 48 | rpne0d 12970 |
. . . . . . . . 9
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
(πβπ-π
) β 0) |
51 | 49, 50, 17 | cxpexpzd 26089 |
. . . . . . . 8
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβπ-π
)βπ(π pCnt π¦)) = ((πβπ-π
)β(π pCnt π¦))) |
52 | 39, 46, 51 | 3eqtr3d 2781 |
. . . . . . 7
β’ (((π β β β§ π
β β+)
β§ (π¦ β β
β§ π¦ β 0)) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
53 | 52 | anassrs 469 |
. . . . . 6
β’ ((((π β β β§ π
β β+)
β§ π¦ β β)
β§ π¦ β 0) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
54 | 15, 53 | sylan2br 596 |
. . . . 5
β’ ((((π β β β§ π
β β+)
β§ π¦ β β)
β§ Β¬ π¦ = 0) β
((πβ-(π pCnt π¦))βππ
) = ((πβπ-π
)β(π pCnt π¦))) |
55 | 54 | ifeq2da 4522 |
. . . 4
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β if(π¦ = 0, 0, ((πβ-(π pCnt π¦))βππ
)) = if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
56 | 4, 14, 55 | 3eqtrd 2777 |
. . 3
β’ (((π β β β§ π
β β+)
β§ π¦ β β)
β (((π½βπ)βπ¦)βππ
) = if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
57 | 56 | mpteq2dva 5209 |
. 2
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ
)) = (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦))))) |
58 | | rpre 12931 |
. . . . 5
β’ ((πβπ-π
) β β+
β (πβπ-π
) β β) |
59 | 47, 58 | syl 17 |
. . . 4
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β β) |
60 | | rpgt0 12935 |
. . . . 5
β’ ((πβπ-π
) β β+
β 0 < (πβπ-π
)) |
61 | 47, 60 | syl 17 |
. . . 4
β’ ((π β β β§ π
β β+)
β 0 < (πβπ-π
)) |
62 | | rpgt0 12935 |
. . . . . . . 8
β’ (π
β β+
β 0 < π
) |
63 | 62 | adantl 483 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 0 < π
) |
64 | 7 | lt0neg2d 11733 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β (0 < π
β
-π
<
0)) |
65 | 63, 64 | mpbid 231 |
. . . . . 6
β’ ((π β β β§ π
β β+)
β -π
<
0) |
66 | 29 | simprd 497 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 1 < π) |
67 | | 0red 11166 |
. . . . . . 7
β’ ((π β β β§ π
β β+)
β 0 β β) |
68 | 40, 66, 36, 67 | cxpltd 26097 |
. . . . . 6
β’ ((π β β β§ π
β β+)
β (-π
< 0 β
(πβπ-π
) < (πβπ0))) |
69 | 65, 68 | mpbid 231 |
. . . . 5
β’ ((π β β β§ π
β β+)
β (πβπ-π
) < (πβπ0)) |
70 | 41 | cxp0d 26083 |
. . . . 5
β’ ((π β β β§ π
β β+)
β (πβπ0) =
1) |
71 | 69, 70 | breqtrd 5135 |
. . . 4
β’ ((π β β β§ π
β β+)
β (πβπ-π
) < 1) |
72 | | 0xr 11210 |
. . . . 5
β’ 0 β
β* |
73 | | 1xr 11222 |
. . . . 5
β’ 1 β
β* |
74 | | elioo2 13314 |
. . . . 5
β’ ((0
β β* β§ 1 β β*) β ((πβπ-π
) β (0(,)1) β ((πβπ-π
) β β β§ 0 <
(πβπ-π
) β§ (πβπ-π
) < 1))) |
75 | 72, 73, 74 | mp2an 691 |
. . . 4
β’ ((πβπ-π
) β (0(,)1) β ((πβπ-π
) β β β§ 0 <
(πβπ-π
) β§ (πβπ-π
) < 1)) |
76 | 59, 61, 71, 75 | syl3anbrc 1344 |
. . 3
β’ ((π β β β§ π
β β+)
β (πβπ-π
) β (0(,)1)) |
77 | | qrng.q |
. . . 4
β’ π = (βfld
βΎs β) |
78 | | qabsabv.a |
. . . 4
β’ π΄ = (AbsValβπ) |
79 | | eqid 2733 |
. . . 4
β’ (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) = (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) |
80 | 77, 78, 79 | padicabv 27001 |
. . 3
β’ ((π β β β§ (πβπ-π
) β (0(,)1)) β (π¦ β β β¦ if(π¦ = 0, 0, ((πβπ-π
)β(π pCnt π¦)))) β π΄) |
81 | 76, 80 | syldan 592 |
. 2
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ if(π¦ = 0, 0,
((πβπ-π
)β(π pCnt π¦)))) β π΄) |
82 | 57, 81 | eqeltrd 2834 |
1
β’ ((π β β β§ π
β β+)
β (π¦ β β
β¦ (((π½βπ)βπ¦)βππ
)) β π΄) |