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
|
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 |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 ) |