Proof of Theorem padicabvcxp
Step | Hyp | Ref
| Expression |
1 | | padic.j |
. . . . . . 7
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) |
2 | 1 | padicval 26498 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℚ) → ((𝐽‘𝑃)‘𝑦) = if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))) |
3 | 2 | adantlr 715 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ ((𝐽‘𝑃)‘𝑦) = if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))) |
4 | 3 | oveq1d 7228 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅)) |
5 | | ovif 7308 |
. . . . 5
⊢ (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅) = if(𝑦 = 0, (0↑𝑐𝑅), ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) |
6 | | rpre 12594 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
7 | 6 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℝ) |
8 | 7 | recnd 10861 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℂ) |
9 | | rpne0 12602 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
10 | 9 | adantl 485 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ≠
0) |
11 | 8, 10 | 0cxpd 25598 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (0↑𝑐𝑅) = 0) |
12 | 11 | adantr 484 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (0↑𝑐𝑅) = 0) |
13 | 12 | ifeq1d 4458 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ if(𝑦 = 0,
(0↑𝑐𝑅), ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) = if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅))) |
14 | 5, 13 | syl5eq 2790 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅) = if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅))) |
15 | | df-ne 2941 |
. . . . . 6
⊢ (𝑦 ≠ 0 ↔ ¬ 𝑦 = 0) |
16 | | pcqcl 16409 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ) |
17 | 16 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃 pCnt 𝑦) ∈ ℤ) |
18 | 17 | zcnd 12283 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃 pCnt 𝑦) ∈ ℂ) |
19 | 8 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑅 ∈
ℂ) |
20 | | mulneg12 11270 |
. . . . . . . . . . . 12
⊢ (((𝑃 pCnt 𝑦) ∈ ℂ ∧ 𝑅 ∈ ℂ) → (-(𝑃 pCnt 𝑦) · 𝑅) = ((𝑃 pCnt 𝑦) · -𝑅)) |
21 | 18, 19, 20 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(-(𝑃 pCnt 𝑦) · 𝑅) = ((𝑃 pCnt 𝑦) · -𝑅)) |
22 | 19 | negcld 11176 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-𝑅 ∈
ℂ) |
23 | 18, 22 | mulcomd 10854 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃 pCnt 𝑦) · -𝑅) = (-𝑅 · (𝑃 pCnt 𝑦))) |
24 | 21, 23 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(-(𝑃 pCnt 𝑦) · 𝑅) = (-𝑅 · (𝑃 pCnt 𝑦))) |
25 | 24 | oveq2d 7229 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-(𝑃 pCnt 𝑦) · 𝑅)) = (𝑃↑𝑐(-𝑅 · (𝑃 pCnt 𝑦)))) |
26 | | prmuz2 16253 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
(ℤ≥‘2)) |
28 | | eluz2b2 12517 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
29 | 27, 28 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃 ∈ ℕ
∧ 1 < 𝑃)) |
30 | 29 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℕ) |
31 | 30 | nnrpd 12626 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℝ+) |
32 | 31 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ∈
ℝ+) |
33 | 17 | znegcld 12284 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-(𝑃 pCnt 𝑦) ∈ ℤ) |
34 | 33 | zred 12282 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-(𝑃 pCnt 𝑦) ∈ ℝ) |
35 | 32, 34, 19 | cxpmuld 25624 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-(𝑃 pCnt 𝑦) · 𝑅)) = ((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅)) |
36 | 7 | renegcld 11259 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ -𝑅 ∈
ℝ) |
37 | 36 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-𝑅 ∈
ℝ) |
38 | 32, 37, 18 | cxpmuld 25624 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-𝑅 · (𝑃 pCnt 𝑦))) = ((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦))) |
39 | 25, 35, 38 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦))) |
40 | 30 | nnred 11845 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℝ) |
41 | 40 | recnd 10861 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℂ) |
42 | 41 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ∈
ℂ) |
43 | 30 | nnne0d 11880 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ≠
0) |
44 | 43 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ≠ 0) |
45 | 42, 44, 33 | cxpexpzd 25599 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-(𝑃 pCnt 𝑦)) = (𝑃↑-(𝑃 pCnt 𝑦))) |
46 | 45 | oveq1d 7228 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) |
47 | 31, 36 | rpcxpcld 25620 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) ∈
ℝ+) |
48 | 47 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ∈
ℝ+) |
49 | 48 | rpcnd 12630 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ∈ ℂ) |
50 | 48 | rpne0d 12633 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ≠ 0) |
51 | 49, 50, 17 | cxpexpzd 25599 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦)) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) |
52 | 39, 46, 51 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) |
53 | 52 | anassrs 471 |
. . . . . 6
⊢ ((((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
∧ 𝑦 ≠ 0) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) |
54 | 15, 53 | sylan2br 598 |
. . . . 5
⊢ ((((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
∧ ¬ 𝑦 = 0) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) |
55 | 54 | ifeq2da 4471 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) = if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) |
56 | 4, 14, 55 | 3eqtrd 2781 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) |
57 | 56 | mpteq2dva 5150 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))))) |
58 | | rpre 12594 |
. . . . 5
⊢ ((𝑃↑𝑐-𝑅) ∈ ℝ+
→ (𝑃↑𝑐-𝑅) ∈ ℝ) |
59 | 47, 58 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) ∈ ℝ) |
60 | | rpgt0 12598 |
. . . . 5
⊢ ((𝑃↑𝑐-𝑅) ∈ ℝ+
→ 0 < (𝑃↑𝑐-𝑅)) |
61 | 47, 60 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 < (𝑃↑𝑐-𝑅)) |
62 | | rpgt0 12598 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) |
63 | 62 | adantl 485 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 < 𝑅) |
64 | 7 | lt0neg2d 11402 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (0 < 𝑅 ↔
-𝑅 <
0)) |
65 | 63, 64 | mpbid 235 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ -𝑅 <
0) |
66 | 29 | simprd 499 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 1 < 𝑃) |
67 | | 0red 10836 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 ∈ ℝ) |
68 | 40, 66, 36, 67 | cxpltd 25607 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (-𝑅 < 0 ↔
(𝑃↑𝑐-𝑅) < (𝑃↑𝑐0))) |
69 | 65, 68 | mpbid 235 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) < (𝑃↑𝑐0)) |
70 | 41 | cxp0d 25593 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐0) =
1) |
71 | 69, 70 | breqtrd 5079 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) < 1) |
72 | | 0xr 10880 |
. . . . 5
⊢ 0 ∈
ℝ* |
73 | | 1xr 10892 |
. . . . 5
⊢ 1 ∈
ℝ* |
74 | | elioo2 12976 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑃↑𝑐-𝑅) ∈ (0(,)1) ↔ ((𝑃↑𝑐-𝑅) ∈ ℝ ∧ 0 <
(𝑃↑𝑐-𝑅) ∧ (𝑃↑𝑐-𝑅) < 1))) |
75 | 72, 73, 74 | mp2an 692 |
. . . 4
⊢ ((𝑃↑𝑐-𝑅) ∈ (0(,)1) ↔ ((𝑃↑𝑐-𝑅) ∈ ℝ ∧ 0 <
(𝑃↑𝑐-𝑅) ∧ (𝑃↑𝑐-𝑅) < 1)) |
76 | 59, 61, 71, 75 | syl3anbrc 1345 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) ∈ (0(,)1)) |
77 | | qrng.q |
. . . 4
⊢ 𝑄 = (ℂfld
↾s ℚ) |
78 | | qabsabv.a |
. . . 4
⊢ 𝐴 = (AbsVal‘𝑄) |
79 | | eqid 2737 |
. . . 4
⊢ (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) = (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) |
80 | 77, 78, 79 | padicabv 26511 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑃↑𝑐-𝑅) ∈ (0(,)1)) → (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) ∈ 𝐴) |
81 | 76, 80 | syldan 594 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ if(𝑦 = 0, 0,
((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) ∈ 𝐴) |
82 | 57, 81 | eqeltrd 2838 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |