Proof of Theorem pcmpt2
Step | Hyp | Ref
| Expression |
1 | | pcmpt.4 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
2 | | pcmpt.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) |
3 | | pcmpt.2 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) |
4 | 2, 3 | pcmptcl 12281 |
. . . . . 6
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) |
5 | 4 | simprd 113 |
. . . . 5
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) |
6 | | pcmpt.3 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
7 | | pcmpt2.6 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁)) |
8 | | eluznn 9546 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) |
9 | 6, 7, 8 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
10 | 5, 9 | ffvelrnd 5629 |
. . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ) |
11 | 10 | nnzd 9320 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ) |
12 | 10 | nnne0d 8910 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0) |
13 | 5, 6 | ffvelrnd 5629 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑁) ∈ ℕ) |
14 | | pcdiv 12243 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ((seq1(
· , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑀) ≠ 0) ∧ (seq1( ·
, 𝐹)‘𝑁) ∈ ℕ) → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑀)) − (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)))) |
15 | 1, 11, 12, 13, 14 | syl121anc 1238 |
. 2
⊢ (𝜑 → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = ((𝑃 pCnt (seq1( · , 𝐹)‘𝑀)) − (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)))) |
16 | | pcmpt.5 |
. . . 4
⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) |
17 | 2, 3, 9, 1, 16 | pcmpt 12282 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑀)) = if(𝑃 ≤ 𝑀, 𝐵, 0)) |
18 | 2, 3, 6, 1, 16 | pcmpt 12282 |
. . 3
⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |
19 | 17, 18 | oveq12d 5868 |
. 2
⊢ (𝜑 → ((𝑃 pCnt (seq1( · , 𝐹)‘𝑀)) − (𝑃 pCnt (seq1( · , 𝐹)‘𝑁))) = (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0))) |
20 | 16 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑛 = 𝑃 → (𝐴 ∈ ℕ0 ↔ 𝐵 ∈
ℕ0)) |
21 | 20, 3, 1 | rspcdva 2839 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
22 | 21 | nn0cnd 9177 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
23 | 22 | subidd 8205 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
24 | 23 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → (𝐵 − 𝐵) = 0) |
25 | | prmnn 12051 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
26 | 1, 25 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
27 | 26 | nnred 8878 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℝ) |
28 | 27 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑃 ∈ ℝ) |
29 | 6 | nnred 8878 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
30 | 29 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑁 ∈ ℝ) |
31 | 9 | nnred 8878 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
32 | 31 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑀 ∈ ℝ) |
33 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑃 ≤ 𝑁) |
34 | | eluzle 9486 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑀) |
35 | 7, 34 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≤ 𝑀) |
36 | 35 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑁 ≤ 𝑀) |
37 | 28, 30, 32, 33, 36 | letrd 8030 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → 𝑃 ≤ 𝑀) |
38 | 37 | iftrued 3532 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → if(𝑃 ≤ 𝑀, 𝐵, 0) = 𝐵) |
39 | | iftrue 3530 |
. . . . . 6
⊢ (𝑃 ≤ 𝑁 → if(𝑃 ≤ 𝑁, 𝐵, 0) = 𝐵) |
40 | 39 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → if(𝑃 ≤ 𝑁, 𝐵, 0) = 𝐵) |
41 | 38, 40 | oveq12d 5868 |
. . . 4
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = (𝐵 − 𝐵)) |
42 | | simpr 109 |
. . . . . 6
⊢ ((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁) → ¬ 𝑃 ≤ 𝑁) |
43 | 42, 33 | nsyl3 621 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → ¬ (𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁)) |
44 | 43 | iffalsed 3535 |
. . . 4
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0) = 0) |
45 | 24, 41, 44 | 3eqtr4d 2213 |
. . 3
⊢ ((𝜑 ∧ 𝑃 ≤ 𝑁) → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |
46 | | iffalse 3533 |
. . . . . 6
⊢ (¬
𝑃 ≤ 𝑁 → if(𝑃 ≤ 𝑁, 𝐵, 0) = 0) |
47 | 46 | oveq2d 5866 |
. . . . 5
⊢ (¬
𝑃 ≤ 𝑁 → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = (if(𝑃 ≤ 𝑀, 𝐵, 0) − 0)) |
48 | | 0cnd 7900 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℂ) |
49 | 26 | nnzd 9320 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) |
50 | 9 | nnzd 9320 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
51 | | zdcle 9275 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑃 ≤
𝑀) |
52 | 49, 50, 51 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → DECID 𝑃 ≤ 𝑀) |
53 | 22, 48, 52 | ifcldcd 3560 |
. . . . . 6
⊢ (𝜑 → if(𝑃 ≤ 𝑀, 𝐵, 0) ∈ ℂ) |
54 | 53 | subid1d 8206 |
. . . . 5
⊢ (𝜑 → (if(𝑃 ≤ 𝑀, 𝐵, 0) − 0) = if(𝑃 ≤ 𝑀, 𝐵, 0)) |
55 | 47, 54 | sylan9eqr 2225 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑃 ≤ 𝑁) → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = if(𝑃 ≤ 𝑀, 𝐵, 0)) |
56 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑃 ≤ 𝑁) → ¬ 𝑃 ≤ 𝑁) |
57 | 56 | biantrud 302 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑃 ≤ 𝑁) → (𝑃 ≤ 𝑀 ↔ (𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁))) |
58 | 57 | ifbid 3546 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑃 ≤ 𝑁) → if(𝑃 ≤ 𝑀, 𝐵, 0) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |
59 | 55, 58 | eqtrd 2203 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑃 ≤ 𝑁) → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |
60 | 6 | nnzd 9320 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
61 | | zdcle 9275 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑃 ≤
𝑁) |
62 | 49, 60, 61 | syl2anc 409 |
. . . 4
⊢ (𝜑 → DECID 𝑃 ≤ 𝑁) |
63 | | exmiddc 831 |
. . . 4
⊢
(DECID 𝑃 ≤ 𝑁 → (𝑃 ≤ 𝑁 ∨ ¬ 𝑃 ≤ 𝑁)) |
64 | 62, 63 | syl 14 |
. . 3
⊢ (𝜑 → (𝑃 ≤ 𝑁 ∨ ¬ 𝑃 ≤ 𝑁)) |
65 | 45, 59, 64 | mpjaodan 793 |
. 2
⊢ (𝜑 → (if(𝑃 ≤ 𝑀, 𝐵, 0) − if(𝑃 ≤ 𝑁, 𝐵, 0)) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |
66 | 15, 19, 65 | 3eqtrd 2207 |
1
⊢ (𝜑 → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |