Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcval Structured version   Visualization version   Unicode version

Theorem pcval 14806
 Description: The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
Hypotheses
Ref Expression
pcval.1
pcval.2
Assertion
Ref Expression
pcval
Distinct variable groups:   ,,,,   ,,,,   ,   ,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem pcval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 463 . . . . . 6
21eqeq1d 2455 . . . . 5
3 eqeq1 2457 . . . . . . . 8
4 oveq1 6302 . . . . . . . . . . . . . 14
54breq1d 4415 . . . . . . . . . . . . 13
65rabbidv 3038 . . . . . . . . . . . 12
76supeq1d 7965 . . . . . . . . . . 11
8 pcval.1 . . . . . . . . . . 11
97, 8syl6eqr 2505 . . . . . . . . . 10
104breq1d 4415 . . . . . . . . . . . . 13
1110rabbidv 3038 . . . . . . . . . . . 12
1211supeq1d 7965 . . . . . . . . . . 11
13 pcval.2 . . . . . . . . . . 11
1412, 13syl6eqr 2505 . . . . . . . . . 10
159, 14oveq12d 6313 . . . . . . . . 9
1615eqeq2d 2463 . . . . . . . 8
173, 16bi2anan9r 886 . . . . . . 7
18172rexbidv 2910 . . . . . 6
1918iotabidv 5570 . . . . 5
202, 19ifbieq2d 3908 . . . 4
21 df-pc 14799 . . . 4
22 pnfex 11420 . . . . 5
23 iotaex 5566 . . . . 5
2422, 23ifex 3951 . . . 4
2520, 21, 24ovmpt2a 6432 . . 3
26 ifnefalse 3895 . . 3
2725, 26sylan9eq 2507 . 2
2827anasss 653 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1446   wcel 1889   wne 2624  wrex 2740  crab 2743  cif 3883   class class class wbr 4405  cio 5547  (class class class)co 6295  csup 7959  cr 9543  cc0 9544   cpnf 9677   clt 9680   cmin 9865   cdiv 10276  cn 10616  cn0 10876  cz 10944  cq 11271  cexp 12279   cdvds 14317  cprime 14634   cpc 14798 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5549  df-fun 5587  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-sup 7961  df-pnf 9682  df-xr 9684  df-pc 14799 This theorem is referenced by:  pczpre  14809  pcdiv  14814
 Copyright terms: Public domain W3C validator