ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1arithlem4 GIF version

Theorem 1arithlem4 12322
Description: Lemma for 1arith 12323. (Contributed by Mario Carneiro, 30-May-2014.)
Hypotheses
Ref Expression
1arith.1 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
1arithlem4.2 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹𝑦)), 1))
1arithlem4.3 (𝜑𝐹:ℙ⟶ℕ0)
1arithlem4.4 (𝜑𝑁 ∈ ℕ)
1arithlem4.5 ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁𝑞)) → (𝐹𝑞) = 0)
Assertion
Ref Expression
1arithlem4 (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀𝑥))
Distinct variable groups:   𝑛,𝑝,𝑞,𝑥,𝑦   𝐹,𝑞,𝑥,𝑦   𝑀,𝑞,𝑥,𝑦   𝜑,𝑞,𝑦   𝑛,𝐺,𝑝,𝑞,𝑥   𝑛,𝑁,𝑝,𝑞,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑝)   𝐹(𝑛,𝑝)   𝐺(𝑦)   𝑀(𝑛,𝑝)   𝑁(𝑦)

Proof of Theorem 1arithlem4
StepHypRef Expression
1 1arithlem4.2 . . . . 5 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹𝑦)), 1))
2 1arithlem4.3 . . . . . . 7 (𝜑𝐹:ℙ⟶ℕ0)
32ffvelcdmda 5635 . . . . . 6 ((𝜑𝑦 ∈ ℙ) → (𝐹𝑦) ∈ ℕ0)
43ralrimiva 2544 . . . . 5 (𝜑 → ∀𝑦 ∈ ℙ (𝐹𝑦) ∈ ℕ0)
51, 4pcmptcl 12298 . . . 4 (𝜑 → (𝐺:ℕ⟶ℕ ∧ seq1( · , 𝐺):ℕ⟶ℕ))
65simprd 113 . . 3 (𝜑 → seq1( · , 𝐺):ℕ⟶ℕ)
7 1arithlem4.4 . . 3 (𝜑𝑁 ∈ ℕ)
86, 7ffvelrnd 5636 . 2 (𝜑 → (seq1( · , 𝐺)‘𝑁) ∈ ℕ)
9 1arith.1 . . . . . . 7 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
1091arithlem2 12320 . . . . . 6 (((seq1( · , 𝐺)‘𝑁) ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞) = (𝑞 pCnt (seq1( · , 𝐺)‘𝑁)))
118, 10sylan 281 . . . . 5 ((𝜑𝑞 ∈ ℙ) → ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞) = (𝑞 pCnt (seq1( · , 𝐺)‘𝑁)))
124adantr 274 . . . . . 6 ((𝜑𝑞 ∈ ℙ) → ∀𝑦 ∈ ℙ (𝐹𝑦) ∈ ℕ0)
137adantr 274 . . . . . 6 ((𝜑𝑞 ∈ ℙ) → 𝑁 ∈ ℕ)
14 simpr 109 . . . . . 6 ((𝜑𝑞 ∈ ℙ) → 𝑞 ∈ ℙ)
15 fveq2 5499 . . . . . 6 (𝑦 = 𝑞 → (𝐹𝑦) = (𝐹𝑞))
161, 12, 13, 14, 15pcmpt 12299 . . . . 5 ((𝜑𝑞 ∈ ℙ) → (𝑞 pCnt (seq1( · , 𝐺)‘𝑁)) = if(𝑞𝑁, (𝐹𝑞), 0))
17 1arithlem4.5 . . . . . . . . 9 ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁𝑞)) → (𝐹𝑞) = 0)
1817anassrs 398 . . . . . . . 8 (((𝜑𝑞 ∈ ℙ) ∧ 𝑁𝑞) → (𝐹𝑞) = 0)
1918ifeq2d 3545 . . . . . . 7 (((𝜑𝑞 ∈ ℙ) ∧ 𝑁𝑞) → if(𝑞𝑁, (𝐹𝑞), (𝐹𝑞)) = if(𝑞𝑁, (𝐹𝑞), 0))
20 prmz 12069 . . . . . . . . . . 11 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
2120adantl 275 . . . . . . . . . 10 ((𝜑𝑞 ∈ ℙ) → 𝑞 ∈ ℤ)
2213nnzd 9337 . . . . . . . . . 10 ((𝜑𝑞 ∈ ℙ) → 𝑁 ∈ ℤ)
23 zdcle 9292 . . . . . . . . . 10 ((𝑞 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑞𝑁)
2421, 22, 23syl2anc 409 . . . . . . . . 9 ((𝜑𝑞 ∈ ℙ) → DECID 𝑞𝑁)
25 ifiddc 3560 . . . . . . . . 9 (DECID 𝑞𝑁 → if(𝑞𝑁, (𝐹𝑞), (𝐹𝑞)) = (𝐹𝑞))
2624, 25syl 14 . . . . . . . 8 ((𝜑𝑞 ∈ ℙ) → if(𝑞𝑁, (𝐹𝑞), (𝐹𝑞)) = (𝐹𝑞))
2726adantr 274 . . . . . . 7 (((𝜑𝑞 ∈ ℙ) ∧ 𝑁𝑞) → if(𝑞𝑁, (𝐹𝑞), (𝐹𝑞)) = (𝐹𝑞))
2819, 27eqtr3d 2206 . . . . . 6 (((𝜑𝑞 ∈ ℙ) ∧ 𝑁𝑞) → if(𝑞𝑁, (𝐹𝑞), 0) = (𝐹𝑞))
29 iftrue 3532 . . . . . . 7 (𝑞𝑁 → if(𝑞𝑁, (𝐹𝑞), 0) = (𝐹𝑞))
3029adantl 275 . . . . . 6 (((𝜑𝑞 ∈ ℙ) ∧ 𝑞𝑁) → if(𝑞𝑁, (𝐹𝑞), 0) = (𝐹𝑞))
31 zletric 9260 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑁𝑞𝑞𝑁))
3222, 21, 31syl2anc 409 . . . . . 6 ((𝜑𝑞 ∈ ℙ) → (𝑁𝑞𝑞𝑁))
3328, 30, 32mpjaodan 794 . . . . 5 ((𝜑𝑞 ∈ ℙ) → if(𝑞𝑁, (𝐹𝑞), 0) = (𝐹𝑞))
3411, 16, 333eqtrrd 2209 . . . 4 ((𝜑𝑞 ∈ ℙ) → (𝐹𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞))
3534ralrimiva 2544 . . 3 (𝜑 → ∀𝑞 ∈ ℙ (𝐹𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞))
3691arithlem3 12321 . . . . 5 ((seq1( · , 𝐺)‘𝑁) ∈ ℕ → (𝑀‘(seq1( · , 𝐺)‘𝑁)):ℙ⟶ℕ0)
378, 36syl 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( · , 𝐺)‘𝑁))‘𝑞)))
4138, 39, 40syl2an 287 . . . 4 ((𝐹:ℙ⟶ℕ0 ∧ (𝑀‘(seq1( · , 𝐺)‘𝑁)):ℙ⟶ℕ0) → (𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)) ↔ ∀𝑞 ∈ ℙ (𝐹𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞)))
422, 37, 41syl2anc 409 . . 3 (𝜑 → (𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)) ↔ ∀𝑞 ∈ ℙ (𝐹𝑞) = ((𝑀‘(seq1( · , 𝐺)‘𝑁))‘𝑞)))
4335, 42mpbird 166 . 2 (𝜑𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁)))
44 fveq2 5499 . . 3 (𝑥 = (seq1( · , 𝐺)‘𝑁) → (𝑀𝑥) = (𝑀‘(seq1( · , 𝐺)‘𝑁)))
4544rspceeqv 2853 . 2 (((seq1( · , 𝐺)‘𝑁) ∈ ℕ ∧ 𝐹 = (𝑀‘(seq1( · , 𝐺)‘𝑁))) → ∃𝑥 ∈ ℕ 𝐹 = (𝑀𝑥))
468, 43, 45syl2anc 409 1 (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀𝑥))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 704  DECID wdc 830   = wceq 1349  wcel 2142  wral 2449  wrex 2450  ifcif 3527   class class class wbr 3990  cmpt 4051   Fn wfn 5195  wf 5196  cfv 5200  (class class class)co 5857  0cc0 7778  1c1 7779   · cmul 7783  cle 7959  cn 8882  0cn0 9139  cz 9216  seqcseq 10405  cexp 10479  cprime 12065   pCnt cpc 12242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-iinf 4573  ax-cnex 7869  ax-resscn 7870  ax-1cn 7871  ax-1re 7872  ax-icn 7873  ax-addcl 7874  ax-addrcl 7875  ax-mulcl 7876  ax-mulrcl 7877  ax-addcom 7878  ax-mulcom 7879  ax-addass 7880  ax-mulass 7881  ax-distr 7882  ax-i2m1 7883  ax-0lt1 7884  ax-1rid 7885  ax-0id 7886  ax-rnegex 7887  ax-precex 7888  ax-cnre 7889  ax-pre-ltirr 7890  ax-pre-ltwlin 7891  ax-pre-lttrn 7892  ax-pre-apti 7893  ax-pre-ltadd 7894  ax-pre-mulgt0 7895  ax-pre-mulext 7896  ax-arch 7897  ax-caucvg 7898
This theorem depends on definitions:  df-bi 116  df-stab 827  df-dc 831  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-reu 2456  df-rmo 2457  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-if 3528  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-tr 4089  df-id 4279  df-po 4282  df-iso 4283  df-iord 4352  df-on 4354  df-ilim 4355  df-suc 4357  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-isom 5209  df-riota 5813  df-ov 5860  df-oprab 5861  df-mpo 5862  df-1st 6123  df-2nd 6124  df-recs 6288  df-frec 6374  df-1o 6399  df-2o 6400  df-er 6517  df-en 6723  df-fin 6725  df-sup 6965  df-inf 6966  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964  df-sub 8096  df-neg 8097  df-reap 8498  df-ap 8505  df-div 8594  df-inn 8883  df-2 8941  df-3 8942  df-4 8943  df-n0 9140  df-z 9217  df-uz 9492  df-q 9583  df-rp 9615  df-fz 9970  df-fzo 10103  df-fl 10230  df-mod 10283  df-seqfrec 10406  df-exp 10480  df-cj 10810  df-re 10811  df-im 10812  df-rsqrt 10966  df-abs 10967  df-dvds 11754  df-gcd 11902  df-prm 12066  df-pc 12243
This theorem is referenced by:  1arith  12323
  Copyright terms: Public domain W3C validator