MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1arithlem4 Structured version   Visualization version   GIF version

Theorem 1arithlem4 16892
Description: Lemma for 1arith 16893. (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 7088 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ β„™) β†’ (πΉβ€˜π‘¦) ∈ β„•0)
43ralrimiva 3136 . . . . 5 (πœ‘ β†’ βˆ€π‘¦ ∈ β„™ (πΉβ€˜π‘¦) ∈ β„•0)
51, 4pcmptcl 16857 . . . 4 (πœ‘ β†’ (𝐺:β„•βŸΆβ„• ∧ seq1( Β· , 𝐺):β„•βŸΆβ„•))
65simprd 494 . . 3 (πœ‘ β†’ seq1( Β· , 𝐺):β„•βŸΆβ„•)
7 1arithlem4.4 . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
86, 7ffvelcdmd 7089 . 2 (πœ‘ β†’ (seq1( Β· , 𝐺)β€˜π‘) ∈ β„•)
9 1arith.1 . . . . . . 7 𝑀 = (𝑛 ∈ β„• ↦ (𝑝 ∈ β„™ ↦ (𝑝 pCnt 𝑛)))
1091arithlem2 16890 . . . . . 6 (((seq1( Β· , 𝐺)β€˜π‘) ∈ β„• ∧ π‘ž ∈ β„™) β†’ ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž) = (π‘ž pCnt (seq1( Β· , 𝐺)β€˜π‘)))
118, 10sylan 578 . . . . 5 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž) = (π‘ž pCnt (seq1( Β· , 𝐺)β€˜π‘)))
124adantr 479 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ βˆ€π‘¦ ∈ β„™ (πΉβ€˜π‘¦) ∈ β„•0)
137adantr 479 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ 𝑁 ∈ β„•)
14 simpr 483 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ π‘ž ∈ β„™)
15 fveq2 6891 . . . . . 6 (𝑦 = π‘ž β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘ž))
161, 12, 13, 14, 15pcmpt 16858 . . . . 5 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ (π‘ž pCnt (seq1( Β· , 𝐺)β€˜π‘)) = if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0))
1713nnred 12255 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ 𝑁 ∈ ℝ)
18 prmz 16643 . . . . . . . 8 (π‘ž ∈ β„™ β†’ π‘ž ∈ β„€)
1918zred 12694 . . . . . . 7 (π‘ž ∈ β„™ β†’ π‘ž ∈ ℝ)
2019adantl 480 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ π‘ž ∈ ℝ)
21 1arithlem4.5 . . . . . . . . 9 ((πœ‘ ∧ (π‘ž ∈ β„™ ∧ 𝑁 ≀ π‘ž)) β†’ (πΉβ€˜π‘ž) = 0)
2221anassrs 466 . . . . . . . 8 (((πœ‘ ∧ π‘ž ∈ β„™) ∧ 𝑁 ≀ π‘ž) β†’ (πΉβ€˜π‘ž) = 0)
2322ifeq2d 4544 . . . . . . 7 (((πœ‘ ∧ π‘ž ∈ β„™) ∧ 𝑁 ≀ π‘ž) β†’ if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), (πΉβ€˜π‘ž)) = if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0))
24 ifid 4564 . . . . . . 7 if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), (πΉβ€˜π‘ž)) = (πΉβ€˜π‘ž)
2523, 24eqtr3di 2780 . . . . . 6 (((πœ‘ ∧ π‘ž ∈ β„™) ∧ 𝑁 ≀ π‘ž) β†’ if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0) = (πΉβ€˜π‘ž))
26 iftrue 4530 . . . . . . 7 (π‘ž ≀ 𝑁 β†’ if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0) = (πΉβ€˜π‘ž))
2726adantl 480 . . . . . 6 (((πœ‘ ∧ π‘ž ∈ β„™) ∧ π‘ž ≀ 𝑁) β†’ if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0) = (πΉβ€˜π‘ž))
2817, 20, 25, 27lecasei 11348 . . . . 5 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ if(π‘ž ≀ 𝑁, (πΉβ€˜π‘ž), 0) = (πΉβ€˜π‘ž))
2911, 16, 283eqtrrd 2770 . . . 4 ((πœ‘ ∧ π‘ž ∈ β„™) β†’ (πΉβ€˜π‘ž) = ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž))
3029ralrimiva 3136 . . 3 (πœ‘ β†’ βˆ€π‘ž ∈ β„™ (πΉβ€˜π‘ž) = ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž))
3191arithlem3 16891 . . . . 5 ((seq1( Β· , 𝐺)β€˜π‘) ∈ β„• β†’ (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)):β„™βŸΆβ„•0)
328, 31syl 17 . . . 4 (πœ‘ β†’ (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)):β„™βŸΆβ„•0)
33 ffn 6716 . . . . 5 (𝐹:β„™βŸΆβ„•0 β†’ 𝐹 Fn β„™)
34 ffn 6716 . . . . 5 ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)):β„™βŸΆβ„•0 β†’ (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)) Fn β„™)
35 eqfnfv 7034 . . . . 5 ((𝐹 Fn β„™ ∧ (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)) Fn β„™) β†’ (𝐹 = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)) ↔ βˆ€π‘ž ∈ β„™ (πΉβ€˜π‘ž) = ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž)))
3633, 34, 35syl2an 594 . . . 4 ((𝐹:β„™βŸΆβ„•0 ∧ (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)):β„™βŸΆβ„•0) β†’ (𝐹 = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)) ↔ βˆ€π‘ž ∈ β„™ (πΉβ€˜π‘ž) = ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž)))
372, 32, 36syl2anc 582 . . 3 (πœ‘ β†’ (𝐹 = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)) ↔ βˆ€π‘ž ∈ β„™ (πΉβ€˜π‘ž) = ((π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))β€˜π‘ž)))
3830, 37mpbird 256 . 2 (πœ‘ β†’ 𝐹 = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)))
39 fveq2 6891 . . 3 (π‘₯ = (seq1( Β· , 𝐺)β€˜π‘) β†’ (π‘€β€˜π‘₯) = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘)))
4039rspceeqv 3624 . 2 (((seq1( Β· , 𝐺)β€˜π‘) ∈ β„• ∧ 𝐹 = (π‘€β€˜(seq1( Β· , 𝐺)β€˜π‘))) β†’ βˆƒπ‘₯ ∈ β„• 𝐹 = (π‘€β€˜π‘₯))
418, 38, 40syl2anc 582 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ β„• 𝐹 = (π‘€β€˜π‘₯))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  βˆƒwrex 3060  ifcif 4524   class class class wbr 5143   ↦ cmpt 5226   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7415  β„cr 11135  0cc0 11136  1c1 11137   Β· cmul 11141   ≀ cle 11277  β„•cn 12240  β„•0cn0 12500  seqcseq 13996  β†‘cexp 14056  β„™cprime 16639   pCnt cpc 16802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-2o 8484  df-er 8721  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-sup 9463  df-inf 9464  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-n0 12501  df-z 12587  df-uz 12851  df-q 12961  df-rp 13005  df-fz 13515  df-fl 13787  df-mod 13865  df-seq 13997  df-exp 14057  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-dvds 16229  df-gcd 16467  df-prm 16640  df-pc 16803
This theorem is referenced by:  1arith  16893
  Copyright terms: Public domain W3C validator