Proof of Theorem padicabvcxp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | padic.j | . . . . . . 7
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) | 
| 2 | 1 | padicval 27661 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℚ) → ((𝐽‘𝑃)‘𝑦) = if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))) | 
| 3 | 2 | adantlr 715 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ ((𝐽‘𝑃)‘𝑦) = if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))) | 
| 4 | 3 | oveq1d 7446 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅)) | 
| 5 |  | ovif 7531 | . . . . 5
⊢ (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅) = if(𝑦 = 0, (0↑𝑐𝑅), ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) | 
| 6 |  | rpre 13043 | . . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) | 
| 7 | 6 | adantl 481 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℝ) | 
| 8 | 7 | recnd 11289 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ∈
ℂ) | 
| 9 |  | rpne0 13051 | . . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) | 
| 10 | 9 | adantl 481 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑅 ≠
0) | 
| 11 | 8, 10 | 0cxpd 26752 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (0↑𝑐𝑅) = 0) | 
| 12 | 11 | adantr 480 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (0↑𝑐𝑅) = 0) | 
| 13 | 12 | ifeq1d 4545 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ if(𝑦 = 0,
(0↑𝑐𝑅), ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) = if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅))) | 
| 14 | 5, 13 | eqtrid 2789 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (if(𝑦 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑦)))↑𝑐𝑅) = if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅))) | 
| 15 |  | df-ne 2941 | . . . . . 6
⊢ (𝑦 ≠ 0 ↔ ¬ 𝑦 = 0) | 
| 16 |  | pcqcl 16894 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℚ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ) | 
| 17 | 16 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃 pCnt 𝑦) ∈ ℤ) | 
| 18 | 17 | zcnd 12723 | . . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃 pCnt 𝑦) ∈ ℂ) | 
| 19 | 8 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑅 ∈
ℂ) | 
| 20 |  | mulneg12 11701 | . . . . . . . . . . . 12
⊢ (((𝑃 pCnt 𝑦) ∈ ℂ ∧ 𝑅 ∈ ℂ) → (-(𝑃 pCnt 𝑦) · 𝑅) = ((𝑃 pCnt 𝑦) · -𝑅)) | 
| 21 | 18, 19, 20 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(-(𝑃 pCnt 𝑦) · 𝑅) = ((𝑃 pCnt 𝑦) · -𝑅)) | 
| 22 | 19 | negcld 11607 | . . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-𝑅 ∈
ℂ) | 
| 23 | 18, 22 | mulcomd 11282 | . . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃 pCnt 𝑦) · -𝑅) = (-𝑅 · (𝑃 pCnt 𝑦))) | 
| 24 | 21, 23 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(-(𝑃 pCnt 𝑦) · 𝑅) = (-𝑅 · (𝑃 pCnt 𝑦))) | 
| 25 | 24 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-(𝑃 pCnt 𝑦) · 𝑅)) = (𝑃↑𝑐(-𝑅 · (𝑃 pCnt 𝑦)))) | 
| 26 |  | prmuz2 16733 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 27 | 26 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
(ℤ≥‘2)) | 
| 28 |  | eluz2b2 12963 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) | 
| 29 | 27, 28 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃 ∈ ℕ
∧ 1 < 𝑃)) | 
| 30 | 29 | simpld 494 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℕ) | 
| 31 | 30 | nnrpd 13075 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℝ+) | 
| 32 | 31 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ∈
ℝ+) | 
| 33 | 17 | znegcld 12724 | . . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-(𝑃 pCnt 𝑦) ∈ ℤ) | 
| 34 | 33 | zred 12722 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-(𝑃 pCnt 𝑦) ∈ ℝ) | 
| 35 | 32, 34, 19 | cxpmuld 26779 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-(𝑃 pCnt 𝑦) · 𝑅)) = ((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅)) | 
| 36 | 7 | renegcld 11690 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ -𝑅 ∈
ℝ) | 
| 37 | 36 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
-𝑅 ∈
ℝ) | 
| 38 | 32, 37, 18 | cxpmuld 26779 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐(-𝑅 · (𝑃 pCnt 𝑦))) = ((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦))) | 
| 39 | 25, 35, 38 | 3eqtr3d 2785 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦))) | 
| 40 | 30 | nnred 12281 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℝ) | 
| 41 | 40 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ∈
ℂ) | 
| 42 | 41 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ∈
ℂ) | 
| 43 | 30 | nnne0d 12316 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 𝑃 ≠
0) | 
| 44 | 43 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
𝑃 ≠ 0) | 
| 45 | 42, 44, 33 | cxpexpzd 26753 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-(𝑃 pCnt 𝑦)) = (𝑃↑-(𝑃 pCnt 𝑦))) | 
| 46 | 45 | oveq1d 7446 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) | 
| 47 | 31, 36 | rpcxpcld 26775 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) ∈
ℝ+) | 
| 48 | 47 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ∈
ℝ+) | 
| 49 | 48 | rpcnd 13079 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ∈ ℂ) | 
| 50 | 48 | rpne0d 13082 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
(𝑃↑𝑐-𝑅) ≠ 0) | 
| 51 | 49, 50, 17 | cxpexpzd 26753 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑𝑐-𝑅)↑𝑐(𝑃 pCnt 𝑦)) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) | 
| 52 | 39, 46, 51 | 3eqtr3d 2785 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ (𝑦 ∈ ℚ
∧ 𝑦 ≠ 0)) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) | 
| 53 | 52 | anassrs 467 | . . . . . 6
⊢ ((((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
∧ 𝑦 ≠ 0) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) | 
| 54 | 15, 53 | sylan2br 595 | . . . . 5
⊢ ((((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
∧ ¬ 𝑦 = 0) →
((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅) = ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))) | 
| 55 | 54 | ifeq2da 4558 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ if(𝑦 = 0, 0, ((𝑃↑-(𝑃 pCnt 𝑦))↑𝑐𝑅)) = if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) | 
| 56 | 4, 14, 55 | 3eqtrd 2781 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
∧ 𝑦 ∈ ℚ)
→ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) | 
| 57 | 56 | mpteq2dva 5242 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦))))) | 
| 58 |  | rpre 13043 | . . . . 5
⊢ ((𝑃↑𝑐-𝑅) ∈ ℝ+
→ (𝑃↑𝑐-𝑅) ∈ ℝ) | 
| 59 | 47, 58 | syl 17 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) ∈ ℝ) | 
| 60 |  | rpgt0 13047 | . . . . 5
⊢ ((𝑃↑𝑐-𝑅) ∈ ℝ+
→ 0 < (𝑃↑𝑐-𝑅)) | 
| 61 | 47, 60 | syl 17 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 < (𝑃↑𝑐-𝑅)) | 
| 62 |  | rpgt0 13047 | . . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) | 
| 63 | 62 | adantl 481 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 < 𝑅) | 
| 64 | 7 | lt0neg2d 11833 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (0 < 𝑅 ↔
-𝑅 <
0)) | 
| 65 | 63, 64 | mpbid 232 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ -𝑅 <
0) | 
| 66 | 29 | simprd 495 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 1 < 𝑃) | 
| 67 |  | 0red 11264 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ 0 ∈ ℝ) | 
| 68 | 40, 66, 36, 67 | cxpltd 26761 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (-𝑅 < 0 ↔
(𝑃↑𝑐-𝑅) < (𝑃↑𝑐0))) | 
| 69 | 65, 68 | mpbid 232 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) < (𝑃↑𝑐0)) | 
| 70 | 41 | cxp0d 26747 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐0) =
1) | 
| 71 | 69, 70 | breqtrd 5169 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑃↑𝑐-𝑅) < 1) | 
| 72 |  | 0xr 11308 | . . . . 5
⊢ 0 ∈
ℝ* | 
| 73 |  | 1xr 11320 | . . . . 5
⊢ 1 ∈
ℝ* | 
| 74 |  | elioo2 13428 | . . . . 5
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑃↑𝑐-𝑅) ∈ (0(,)1) ↔ ((𝑃↑𝑐-𝑅) ∈ ℝ ∧ 0 <
(𝑃↑𝑐-𝑅) ∧ (𝑃↑𝑐-𝑅) < 1))) | 
| 75 | 72, 73, 74 | mp2an 692 | . . . 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 2737 | . . . 4
⊢ (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) = (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) | 
| 80 | 77, 78, 79 | padicabv 27674 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑃↑𝑐-𝑅) ∈ (0(,)1)) → (𝑦 ∈ ℚ ↦ if(𝑦 = 0, 0, ((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) ∈ 𝐴) | 
| 81 | 76, 80 | syldan 591 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ if(𝑦 = 0, 0,
((𝑃↑𝑐-𝑅)↑(𝑃 pCnt 𝑦)))) ∈ 𝐴) | 
| 82 | 57, 81 | eqeltrd 2841 | 1
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |