Metamath Proof Explorer

Theorem 1arithlem4

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
1arithlem4.2 ⊢ G = y ∈ ℕ ⟼ if y ∈ ℙ y F ⁡ y 1
1arithlem4.3 ⊢ φ → F : ℙ ⟶ ℕ 0
1arithlem4.4 ⊢ φ → N ∈ ℕ
1arithlem4.5 ⊢ φ ∧ q ∈ ℙ ∧ N ≤ q → F ⁡ q = 0
Assertion 1arithlem4 ⊢ φ → ∃ x ∈ ℕ F = M ⁡ x

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
2 1arithlem4.2 ⊢ G = y ∈ ℕ ⟼ if y ∈ ℙ y F ⁡ y 1
3 1arithlem4.3 ⊢ φ → F : ℙ ⟶ ℕ 0
4 1arithlem4.4 ⊢ φ → N ∈ ℕ
5 1arithlem4.5 ⊢ φ ∧ q ∈ ℙ ∧ N ≤ q → F ⁡ q = 0
6 3 ffvelrnda ⊢ φ ∧ y ∈ ℙ → F ⁡ y ∈ ℕ 0
7 6 ralrimiva ⊢ φ → ∀ y ∈ ℙ F ⁡ y ∈ ℕ 0
8 2 7 pcmptcl ⊢ φ → G : ℕ ⟶ ℕ ∧ seq 1 × G : ℕ ⟶ ℕ
9 8 simprd ⊢ φ → seq 1 × G : ℕ ⟶ ℕ
10 9 4 ffvelrnd ⊢ φ → seq 1 × G ⁡ N ∈ ℕ
11 1 1arithlem2 ⊢ seq 1 × G ⁡ N ∈ ℕ ∧ q ∈ ℙ → M ⁡ seq 1 × G ⁡ N ⁡ q = q pCnt seq 1 × G ⁡ N
12 10 11 sylan ⊢ φ ∧ q ∈ ℙ → M ⁡ seq 1 × G ⁡ N ⁡ q = q pCnt seq 1 × G ⁡ N
13 7 adantr ⊢ φ ∧ q ∈ ℙ → ∀ y ∈ ℙ F ⁡ y ∈ ℕ 0
14 4 adantr ⊢ φ ∧ q ∈ ℙ → N ∈ ℕ
15 simpr ⊢ φ ∧ q ∈ ℙ → q ∈ ℙ
16 fveq2 ⊢ y = q → F ⁡ y = F ⁡ q
17 2 13 14 15 16 pcmpt ⊢ φ ∧ q ∈ ℙ → q pCnt seq 1 × G ⁡ N = if q ≤ N F ⁡ q 0
18 14 nnred ⊢ φ ∧ q ∈ ℙ → N ∈ ℝ
19 prmz ⊢ q ∈ ℙ → q ∈ ℤ
20 19 zred ⊢ q ∈ ℙ → q ∈ ℝ
21 20 adantl ⊢ φ ∧ q ∈ ℙ → q ∈ ℝ
22 5 anassrs ⊢ φ ∧ q ∈ ℙ ∧ N ≤ q → F ⁡ q = 0
23 22 ifeq2d ⊢ φ ∧ q ∈ ℙ ∧ N ≤ q → if q ≤ N F ⁡ q F ⁡ q = if q ≤ N F ⁡ q 0
24 ifid ⊢ if q ≤ N F ⁡ q F ⁡ q = F ⁡ q
25 23 24 eqtr3di ⊢ φ ∧ q ∈ ℙ ∧ N ≤ q → if q ≤ N F ⁡ q 0 = F ⁡ q
26 iftrue ⊢ q ≤ N → if q ≤ N F ⁡ q 0 = F ⁡ q
27 26 adantl ⊢ φ ∧ q ∈ ℙ ∧ q ≤ N → if q ≤ N F ⁡ q 0 = F ⁡ q
28 18 21 25 27 lecasei ⊢ φ ∧ q ∈ ℙ → if q ≤ N F ⁡ q 0 = F ⁡ q
29 12 17 28 3eqtrrd ⊢ φ ∧ q ∈ ℙ → F ⁡ q = M ⁡ seq 1 × G ⁡ N ⁡ q
30 29 ralrimiva ⊢ φ → ∀ q ∈ ℙ F ⁡ q = M ⁡ seq 1 × G ⁡ N ⁡ q
31 1 1arithlem3 ⊢ seq 1 × G ⁡ N ∈ ℕ → M ⁡ seq 1 × G ⁡ N : ℙ ⟶ ℕ 0
32 10 31 syl ⊢ φ → M ⁡ seq 1 × G ⁡ N : ℙ ⟶ ℕ 0
33 ffn ⊢ F : ℙ ⟶ ℕ 0 → F Fn ℙ
34 ffn ⊢ M ⁡ seq 1 × G ⁡ N : ℙ ⟶ ℕ 0 → M ⁡ seq 1 × G ⁡ N Fn ℙ
35 eqfnfv ⊢ F Fn ℙ ∧ M ⁡ seq 1 × G ⁡ N Fn ℙ → F = M ⁡ seq 1 × G ⁡ N ↔ ∀ q ∈ ℙ F ⁡ q = M ⁡ seq 1 × G ⁡ N ⁡ q
36 33 34 35 syl2an ⊢ F : ℙ ⟶ ℕ 0 ∧ M ⁡ seq 1 × G ⁡ N : ℙ ⟶ ℕ 0 → F = M ⁡ seq 1 × G ⁡ N ↔ ∀ q ∈ ℙ F ⁡ q = M ⁡ seq 1 × G ⁡ N ⁡ q
37 3 32 36 syl2anc ⊢ φ → F = M ⁡ seq 1 × G ⁡ N ↔ ∀ q ∈ ℙ F ⁡ q = M ⁡ seq 1 × G ⁡ N ⁡ q
38 30 37 mpbird ⊢ φ → F = M ⁡ seq 1 × G ⁡ N
39 fveq2 ⊢ x = seq 1 × G ⁡ N → M ⁡ x = M ⁡ seq 1 × G ⁡ N
40 39 rspceeqv ⊢ seq 1 × G ⁡ N ∈ ℕ ∧ F = M ⁡ seq 1 × G ⁡ N → ∃ x ∈ ℕ F = M ⁡ x
41 10 38 40 syl2anc ⊢ φ → ∃ x ∈ ℕ F = M ⁡ x