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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
padic.j ⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
Assertion padicabvcxp ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
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 syl5eq ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℚ ) → ( 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 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )