Metamath Proof Explorer


Theorem padicabvcxp

Description: All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses qrng.q 𝑄 = ( ℂflds ℚ )
qabsabv.a 𝐴 = ( AbsVal ‘ 𝑄 )
padic.j 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
Assertion padicabvcxp ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
2 qabsabv.a 𝐴 = ( AbsVal ‘ 𝑄 )
3 padic.j 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4 3 padicval ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℚ ) → ( ( 𝐽𝑃 ) ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ) )
5 4 adantlr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( ( 𝐽𝑃 ) ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ) )
6 5 oveq1d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( ( ( 𝐽𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) = ( if ( 𝑦 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ) ↑𝑐 𝑅 ) )
7 ovif ( if ( 𝑦 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ) ↑𝑐 𝑅 ) = if ( 𝑦 = 0 , ( 0 ↑𝑐 𝑅 ) , ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) )
8 rpre ( 𝑅 ∈ ℝ+𝑅 ∈ ℝ )
9 8 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℝ )
10 9 recnd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℂ )
11 rpne0 ( 𝑅 ∈ ℝ+𝑅 ≠ 0 )
12 11 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ≠ 0 )
13 10 12 0cxpd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 0 ↑𝑐 𝑅 ) = 0 )
14 13 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( 0 ↑𝑐 𝑅 ) = 0 )
15 14 ifeq1d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → if ( 𝑦 = 0 , ( 0 ↑𝑐 𝑅 ) , ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) ) = if ( 𝑦 = 0 , 0 , ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) ) )
16 7 15 eqtrid ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( if ( 𝑦 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ) ↑𝑐 𝑅 ) = if ( 𝑦 = 0 , 0 , ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) ) )
17 df-ne ( 𝑦 ≠ 0 ↔ ¬ 𝑦 = 0 )
18 pcqcl ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
19 18 adantlr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
20 19 zcnd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℂ )
21 10 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → 𝑅 ∈ ℂ )
22 mulneg12 ( ( ( 𝑃 pCnt 𝑦 ) ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( - ( 𝑃 pCnt 𝑦 ) · 𝑅 ) = ( ( 𝑃 pCnt 𝑦 ) · - 𝑅 ) )
23 20 21 22 syl2anc ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( - ( 𝑃 pCnt 𝑦 ) · 𝑅 ) = ( ( 𝑃 pCnt 𝑦 ) · - 𝑅 ) )
24 21 negcld ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → - 𝑅 ∈ ℂ )
25 20 24 mulcomd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝑦 ) · - 𝑅 ) = ( - 𝑅 · ( 𝑃 pCnt 𝑦 ) ) )
26 23 25 eqtrd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( - ( 𝑃 pCnt 𝑦 ) · 𝑅 ) = ( - 𝑅 · ( 𝑃 pCnt 𝑦 ) ) )
27 26 oveq2d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 ( - ( 𝑃 pCnt 𝑦 ) · 𝑅 ) ) = ( 𝑃𝑐 ( - 𝑅 · ( 𝑃 pCnt 𝑦 ) ) ) )
28 prmuz2 ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ ‘ 2 ) )
29 28 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ( ℤ ‘ 2 ) )
30 eluz2b2 ( 𝑃 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
31 29 30 sylib ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
32 31 simpld ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ℕ )
33 32 nnrpd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ℝ+ )
34 33 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → 𝑃 ∈ ℝ+ )
35 19 znegcld ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → - ( 𝑃 pCnt 𝑦 ) ∈ ℤ )
36 35 zred ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → - ( 𝑃 pCnt 𝑦 ) ∈ ℝ )
37 34 36 21 cxpmuld ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 ( - ( 𝑃 pCnt 𝑦 ) · 𝑅 ) ) = ( ( 𝑃𝑐 - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) )
38 9 renegcld ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → - 𝑅 ∈ ℝ )
39 38 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → - 𝑅 ∈ ℝ )
40 34 39 20 cxpmuld ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 ( - 𝑅 · ( 𝑃 pCnt 𝑦 ) ) ) = ( ( 𝑃𝑐 - 𝑅 ) ↑𝑐 ( 𝑃 pCnt 𝑦 ) ) )
41 27 37 40 3eqtr3d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑃𝑐 - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) = ( ( 𝑃𝑐 - 𝑅 ) ↑𝑐 ( 𝑃 pCnt 𝑦 ) ) )
42 32 nnred ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ℝ )
43 42 recnd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ℂ )
44 43 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → 𝑃 ∈ ℂ )
45 32 nnne0d ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ≠ 0 )
46 45 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → 𝑃 ≠ 0 )
47 44 46 35 cxpexpzd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 - ( 𝑃 pCnt 𝑦 ) ) = ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) )
48 47 oveq1d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑃𝑐 - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) = ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) )
49 33 38 rpcxpcld ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 - 𝑅 ) ∈ ℝ+ )
50 49 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 - 𝑅 ) ∈ ℝ+ )
51 50 rpcnd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 - 𝑅 ) ∈ ℂ )
52 50 rpne0d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃𝑐 - 𝑅 ) ≠ 0 )
53 51 52 19 cxpexpzd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑃𝑐 - 𝑅 ) ↑𝑐 ( 𝑃 pCnt 𝑦 ) ) = ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) )
54 41 48 53 3eqtr3d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) = ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) )
55 54 anassrs ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) ∧ 𝑦 ≠ 0 ) → ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) = ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) )
56 17 55 sylan2br ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) ∧ ¬ 𝑦 = 0 ) → ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) = ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) )
57 56 ifeq2da ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → if ( 𝑦 = 0 , 0 , ( ( 𝑃 ↑ - ( 𝑃 pCnt 𝑦 ) ) ↑𝑐 𝑅 ) ) = if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
58 6 16 57 3eqtrd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( ( ( 𝐽𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) = if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
59 58 mpteq2dva ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) = ( 𝑦 ∈ ℚ ↦ if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) )
60 rpre ( ( 𝑃𝑐 - 𝑅 ) ∈ ℝ+ → ( 𝑃𝑐 - 𝑅 ) ∈ ℝ )
61 49 60 syl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 - 𝑅 ) ∈ ℝ )
62 rpgt0 ( ( 𝑃𝑐 - 𝑅 ) ∈ ℝ+ → 0 < ( 𝑃𝑐 - 𝑅 ) )
63 49 62 syl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 0 < ( 𝑃𝑐 - 𝑅 ) )
64 rpgt0 ( 𝑅 ∈ ℝ+ → 0 < 𝑅 )
65 64 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 0 < 𝑅 )
66 9 lt0neg2d ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 0 < 𝑅 ↔ - 𝑅 < 0 ) )
67 65 66 mpbid ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → - 𝑅 < 0 )
68 31 simprd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 1 < 𝑃 )
69 0red ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → 0 ∈ ℝ )
70 42 68 38 69 cxpltd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( - 𝑅 < 0 ↔ ( 𝑃𝑐 - 𝑅 ) < ( 𝑃𝑐 0 ) ) )
71 67 70 mpbid ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 - 𝑅 ) < ( 𝑃𝑐 0 ) )
72 43 cxp0d ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 0 ) = 1 )
73 71 72 breqtrd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 - 𝑅 ) < 1 )
74 0xr 0 ∈ ℝ*
75 1xr 1 ∈ ℝ*
76 elioo2 ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑃𝑐 - 𝑅 ) ∈ ( 0 (,) 1 ) ↔ ( ( 𝑃𝑐 - 𝑅 ) ∈ ℝ ∧ 0 < ( 𝑃𝑐 - 𝑅 ) ∧ ( 𝑃𝑐 - 𝑅 ) < 1 ) ) )
77 74 75 76 mp2an ( ( 𝑃𝑐 - 𝑅 ) ∈ ( 0 (,) 1 ) ↔ ( ( 𝑃𝑐 - 𝑅 ) ∈ ℝ ∧ 0 < ( 𝑃𝑐 - 𝑅 ) ∧ ( 𝑃𝑐 - 𝑅 ) < 1 ) )
78 61 63 73 77 syl3anbrc ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃𝑐 - 𝑅 ) ∈ ( 0 (,) 1 ) )
79 eqid ( 𝑦 ∈ ℚ ↦ if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) = ( 𝑦 ∈ ℚ ↦ if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) )
80 1 2 79 padicabv ( ( 𝑃 ∈ ℙ ∧ ( 𝑃𝑐 - 𝑅 ) ∈ ( 0 (,) 1 ) ) → ( 𝑦 ∈ ℚ ↦ if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) ∈ 𝐴 )
81 78 80 syldan ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ if ( 𝑦 = 0 , 0 , ( ( 𝑃𝑐 - 𝑅 ) ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) ∈ 𝐴 )
82 59 81 eqeltrd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )