Proof of Theorem 1arithlem4
Step | Hyp | Ref
| Expression |
1 | | 1arithlem4.2 |
. . . . 5
⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1)) |
2 | | 1arithlem4.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℙ⟶ℕ0) |
3 | 2 | ffvelcdmda 5635 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℙ) → (𝐹‘𝑦) ∈
ℕ0) |
4 | 3 | ralrimiva 2544 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ℙ (𝐹‘𝑦) ∈
ℕ0) |
5 | 1, 4 | pcmptcl 12298 |
. . . 4
⊢ (𝜑 → (𝐺:ℕ⟶ℕ ∧ seq1( ·
, 𝐺):ℕ⟶ℕ)) |
6 | 5 | simprd 113 |
. . 3
⊢ (𝜑 → seq1( · , 𝐺):ℕ⟶ℕ) |
7 | | 1arithlem4.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
8 | 6, 7 | ffvelrnd 5636 |
. 2
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) ∈ ℕ) |
9 | | 1arith.1 |
. . . . . . 7
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
10 | 9 | 1arithlem2 12320 |
. . . . . 6
⊢ (((seq1(
· , 𝐺)‘𝑁) ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞) = (𝑞 pCnt (seq1( · , 𝐺)‘𝑁))) |
11 | 8, 10 | sylan 281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞) = (𝑞 pCnt (seq1( · , 𝐺)‘𝑁))) |
12 | 4 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → ∀𝑦 ∈ ℙ (𝐹‘𝑦) ∈
ℕ0) |
13 | 7 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℕ) |
14 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ) |
15 | | fveq2 5499 |
. . . . . 6
⊢ (𝑦 = 𝑞 → (𝐹‘𝑦) = (𝐹‘𝑞)) |
16 | 1, 12, 13, 14, 15 | pcmpt 12299 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (seq1( · , 𝐺)‘𝑁)) = if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0)) |
17 | | 1arithlem4.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0) |
18 | 17 | anassrs 398 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑁 ≤ 𝑞) → (𝐹‘𝑞) = 0) |
19 | 18 | ifeq2d 3545 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑁 ≤ 𝑞) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), (𝐹‘𝑞)) = if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0)) |
20 | | prmz 12069 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
21 | 20 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℤ) |
22 | 13 | nnzd 9337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 𝑁 ∈ ℤ) |
23 | | zdcle 9292 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑞 ≤
𝑁) |
24 | 21, 22, 23 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → DECID
𝑞 ≤ 𝑁) |
25 | | ifiddc 3560 |
. . . . . . . . 9
⊢
(DECID 𝑞 ≤ 𝑁 → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), (𝐹‘𝑞)) = (𝐹‘𝑞)) |
26 | 24, 25 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), (𝐹‘𝑞)) = (𝐹‘𝑞)) |
27 | 26 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑁 ≤ 𝑞) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), (𝐹‘𝑞)) = (𝐹‘𝑞)) |
28 | 19, 27 | eqtr3d 2206 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑁 ≤ 𝑞) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0) = (𝐹‘𝑞)) |
29 | | iftrue 3532 |
. . . . . . 7
⊢ (𝑞 ≤ 𝑁 → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0) = (𝐹‘𝑞)) |
30 | 29 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ≤ 𝑁) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0) = (𝐹‘𝑞)) |
31 | | zletric 9260 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑁 ≤ 𝑞 ∨ 𝑞 ≤ 𝑁)) |
32 | 22, 21, 31 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑁 ≤ 𝑞 ∨ 𝑞 ≤ 𝑁)) |
33 | 28, 30, 32 | mpjaodan 794 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → if(𝑞 ≤ 𝑁, (𝐹‘𝑞), 0) = (𝐹‘𝑞)) |
34 | 11, 16, 33 | 3eqtrrd 2209 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞)) |
35 | 34 | ralrimiva 2544 |
. . 3
⊢ (𝜑 → ∀𝑞 ∈ ℙ (𝐹‘𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞)) |
36 | 9 | 1arithlem3 12321 |
. . . . 5
⊢ ((seq1(
· , 𝐺)‘𝑁) ∈ ℕ → (𝑀‘(seq1( · , 𝐺)‘𝑁)):ℙ⟶ℕ0) |
37 | 8, 36 | syl 14 |
. . . 4
⊢ (𝜑 → (𝑀‘(seq1( · , 𝐺)‘𝑁)):ℙ⟶ℕ0) |
38 | | ffn 5349 |
. . . . 5
⊢ (𝐹:ℙ⟶ℕ0 →
𝐹 Fn
ℙ) |
39 | | ffn 5349 |
. . . . 5
⊢ ((𝑀‘(seq1( · , 𝐺)‘𝑁)):ℙ⟶ℕ0 →
(𝑀‘(seq1( · ,
𝐺)‘𝑁)) Fn ℙ) |
40 | | eqfnfv 5597 |
. . . . 5
⊢ ((𝐹 Fn ℙ ∧ (𝑀‘(seq1( · , 𝐺)‘𝑁)) Fn ℙ) → (𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)) ↔ ∀𝑞 ∈ ℙ (𝐹‘𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞))) |
41 | 38, 39, 40 | syl2an 287 |
. . . 4
⊢ ((𝐹:ℙ⟶ℕ0 ∧
(𝑀‘(seq1( · ,
𝐺)‘𝑁)):ℙ⟶ℕ0)
→ (𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)) ↔ ∀𝑞 ∈ ℙ (𝐹‘𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞))) |
42 | 2, 37, 41 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)) ↔ ∀𝑞 ∈ ℙ (𝐹‘𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞))) |
43 | 35, 42 | mpbird 166 |
. 2
⊢ (𝜑 → 𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁))) |
44 | | fveq2 5499 |
. . 3
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑁) → (𝑀‘𝑥) = (𝑀‘(seq1( · , 𝐺)‘𝑁))) |
45 | 44 | rspceeqv 2853 |
. 2
⊢ (((seq1(
· , 𝐺)‘𝑁) ∈ ℕ ∧ 𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁))) → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) |
46 | 8, 43, 45 | syl2anc 409 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) |