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

Theorem pcmpt 16769
Description: Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
Hypotheses
Ref Expression
pcmpt.1 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
pcmpt.2 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
pcmpt.3 (πœ‘ β†’ 𝑁 ∈ β„•)
pcmpt.4 (πœ‘ β†’ 𝑃 ∈ β„™)
pcmpt.5 (𝑛 = 𝑃 β†’ 𝐴 = 𝐡)
Assertion
Ref Expression
pcmpt (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))
Distinct variable groups:   𝐡,𝑛   𝑃,𝑛
Allowed substitution hints:   πœ‘(𝑛)   𝐴(𝑛)   𝐹(𝑛)   𝑁(𝑛)

Proof of Theorem pcmpt
Dummy variables π‘˜ 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcmpt.3 . 2 (πœ‘ β†’ 𝑁 ∈ β„•)
2 fveq2 6843 . . . . . 6 (𝑝 = 1 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜1))
32oveq2d 7374 . . . . 5 (𝑝 = 1 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)))
4 breq2 5110 . . . . . 6 (𝑝 = 1 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 1))
54ifbid 4510 . . . . 5 (𝑝 = 1 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 1, 𝐡, 0))
63, 5eqeq12d 2749 . . . 4 (𝑝 = 1 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0)))
76imbi2d 341 . . 3 (𝑝 = 1 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))))
8 fveq2 6843 . . . . . 6 (𝑝 = π‘˜ β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘˜))
98oveq2d 7374 . . . . 5 (𝑝 = π‘˜ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
10 breq2 5110 . . . . . 6 (𝑝 = π‘˜ β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ π‘˜))
1110ifbid 4510 . . . . 5 (𝑝 = π‘˜ β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
129, 11eqeq12d 2749 . . . 4 (𝑝 = π‘˜ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
1312imbi2d 341 . . 3 (𝑝 = π‘˜ β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0))))
14 fveq2 6843 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)))
1514oveq2d 7374 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))))
16 breq2 5110 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ (π‘˜ + 1)))
1716ifbid 4510 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))
1815, 17eqeq12d 2749 . . . 4 (𝑝 = (π‘˜ + 1) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
1918imbi2d 341 . . 3 (𝑝 = (π‘˜ + 1) β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
20 fveq2 6843 . . . . . 6 (𝑝 = 𝑁 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘))
2120oveq2d 7374 . . . . 5 (𝑝 = 𝑁 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)))
22 breq2 5110 . . . . . 6 (𝑝 = 𝑁 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 𝑁))
2322ifbid 4510 . . . . 5 (𝑝 = 𝑁 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 𝑁, 𝐡, 0))
2421, 23eqeq12d 2749 . . . 4 (𝑝 = 𝑁 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2524imbi2d 341 . . 3 (𝑝 = 𝑁 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))))
26 pcmpt.4 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„™)
27 1z 12538 . . . . . . . . 9 1 ∈ β„€
28 seq1 13925 . . . . . . . . 9 (1 ∈ β„€ β†’ (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1))
2927, 28ax-mp 5 . . . . . . . 8 (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1)
30 1nn 12169 . . . . . . . . 9 1 ∈ β„•
31 1nprm 16560 . . . . . . . . . . . 12 Β¬ 1 ∈ β„™
32 eleq1 2822 . . . . . . . . . . . 12 (𝑛 = 1 β†’ (𝑛 ∈ β„™ ↔ 1 ∈ β„™))
3331, 32mtbiri 327 . . . . . . . . . . 11 (𝑛 = 1 β†’ Β¬ 𝑛 ∈ β„™)
3433iffalsed 4498 . . . . . . . . . 10 (𝑛 = 1 β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = 1)
35 pcmpt.1 . . . . . . . . . 10 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
36 1ex 11156 . . . . . . . . . 10 1 ∈ V
3734, 35, 36fvmpt 6949 . . . . . . . . 9 (1 ∈ β„• β†’ (πΉβ€˜1) = 1)
3830, 37ax-mp 5 . . . . . . . 8 (πΉβ€˜1) = 1
3929, 38eqtri 2761 . . . . . . 7 (seq1( Β· , 𝐹)β€˜1) = 1
4039oveq2i 7369 . . . . . 6 (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = (𝑃 pCnt 1)
41 pc1 16732 . . . . . 6 (𝑃 ∈ β„™ β†’ (𝑃 pCnt 1) = 0)
4240, 41eqtrid 2785 . . . . 5 (𝑃 ∈ β„™ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = 0)
43 prmgt1 16578 . . . . . . 7 (𝑃 ∈ β„™ β†’ 1 < 𝑃)
44 1re 11160 . . . . . . . 8 1 ∈ ℝ
45 prmuz2 16577 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
46 eluzelre 12779 . . . . . . . . 9 (𝑃 ∈ (β„€β‰₯β€˜2) β†’ 𝑃 ∈ ℝ)
4745, 46syl 17 . . . . . . . 8 (𝑃 ∈ β„™ β†’ 𝑃 ∈ ℝ)
48 ltnle 11239 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ) β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
4944, 47, 48sylancr 588 . . . . . . 7 (𝑃 ∈ β„™ β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
5043, 49mpbid 231 . . . . . 6 (𝑃 ∈ β„™ β†’ Β¬ 𝑃 ≀ 1)
5150iffalsed 4498 . . . . 5 (𝑃 ∈ β„™ β†’ if(𝑃 ≀ 1, 𝐡, 0) = 0)
5242, 51eqtr4d 2776 . . . 4 (𝑃 ∈ β„™ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))
5326, 52syl 17 . . 3 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))
5426adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ β„™)
55 pcmpt.2 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
5635, 55pcmptcl 16768 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹:β„•βŸΆβ„• ∧ seq1( Β· , 𝐹):β„•βŸΆβ„•))
5756simpld 496 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„•βŸΆβ„•)
58 peano2nn 12170 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
59 ffvelcdm 7033 . . . . . . . . . . . . . . 15 ((𝐹:β„•βŸΆβ„• ∧ (π‘˜ + 1) ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6057, 58, 59syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6160adantrr 716 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6254, 61pccld 16727 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„•0)
6362nn0cnd 12480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„‚)
6463addid2d 11361 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))))
6558ad2antrl 727 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
66 ovex 7391 . . . . . . . . . . . . . . 15 (𝑛↑𝐴) ∈ V
6766, 36ifex 4537 . . . . . . . . . . . . . 14 if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V
6867csbex 5269 . . . . . . . . . . . . 13 ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V
6935fvmpts 6952 . . . . . . . . . . . . . 14 (((π‘˜ + 1) ∈ β„• ∧ ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V) β†’ (πΉβ€˜(π‘˜ + 1)) = ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
70 ovex 7391 . . . . . . . . . . . . . . 15 (π‘˜ + 1) ∈ V
71 nfv 1918 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(π‘˜ + 1) ∈ β„™
72 nfcv 2904 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛(π‘˜ + 1)
73 nfcv 2904 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛↑
74 nfcsb1v 3881 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄
7572, 73, 74nfov 7388 . . . . . . . . . . . . . . . 16 Ⅎ𝑛((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
76 nfcv 2904 . . . . . . . . . . . . . . . 16 Ⅎ𝑛1
7771, 75, 76nfif 4517 . . . . . . . . . . . . . . 15 Ⅎ𝑛if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1)
78 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑛 = (π‘˜ + 1) β†’ (𝑛 ∈ β„™ ↔ (π‘˜ + 1) ∈ β„™))
79 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = (π‘˜ + 1) β†’ 𝑛 = (π‘˜ + 1))
80 csbeq1a 3870 . . . . . . . . . . . . . . . . 17 (𝑛 = (π‘˜ + 1) β†’ 𝐴 = ⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
8179, 80oveq12d 7376 . . . . . . . . . . . . . . . 16 (𝑛 = (π‘˜ + 1) β†’ (𝑛↑𝐴) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
8278, 81ifbieq1d 4511 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
8370, 77, 82csbief 3891 . . . . . . . . . . . . . 14 ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1)
8469, 83eqtrdi 2789 . . . . . . . . . . . . 13 (((π‘˜ + 1) ∈ β„• ∧ ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
8565, 68, 84sylancl 587 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
86 simprr 772 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) = 𝑃)
8786, 54eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„™)
8887iftrued 4495 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
8986csbeq1d 3860 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = ⦋𝑃 / π‘›β¦Œπ΄)
90 nfcvd 2905 . . . . . . . . . . . . . . . 16 (𝑃 ∈ β„™ β†’ Ⅎ𝑛𝐡)
91 pcmpt.5 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑃 β†’ 𝐴 = 𝐡)
9290, 91csbiegf 3890 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
9354, 92syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
9489, 93eqtrd 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = 𝐡)
9586, 94oveq12d 7376 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) = (𝑃↑𝐡))
9685, 88, 953eqtrd 2777 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = (𝑃↑𝐡))
9796oveq2d 7374 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt (𝑃↑𝐡)))
9891eleq1d 2819 . . . . . . . . . . . . . 14 (𝑛 = 𝑃 β†’ (𝐴 ∈ β„•0 ↔ 𝐡 ∈ β„•0))
9998rspcv 3576 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ 𝐡 ∈ β„•0))
10026, 55, 99sylc 65 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ β„•0)
101100adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝐡 ∈ β„•0)
102 pcidlem 16749 . . . . . . . . . . 11 ((𝑃 ∈ β„™ ∧ 𝐡 ∈ β„•0) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
10354, 101, 102syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
10464, 97, 1033eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡)
105 oveq1 7365 . . . . . . . . . 10 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
106105eqeq1d 2735 . . . . . . . . 9 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ (((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡 ↔ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
107104, 106syl5ibrcom 247 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
108 nnre 12165 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
109108ad2antrl 727 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ π‘˜ ∈ ℝ)
110 ltp1 12000 . . . . . . . . . . . . 13 (π‘˜ ∈ ℝ β†’ π‘˜ < (π‘˜ + 1))
111 peano2re 11333 . . . . . . . . . . . . . 14 (π‘˜ ∈ ℝ β†’ (π‘˜ + 1) ∈ ℝ)
112 ltnle 11239 . . . . . . . . . . . . . 14 ((π‘˜ ∈ ℝ ∧ (π‘˜ + 1) ∈ ℝ) β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
113111, 112mpdan 686 . . . . . . . . . . . . 13 (π‘˜ ∈ ℝ β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
114110, 113mpbid 231 . . . . . . . . . . . 12 (π‘˜ ∈ ℝ β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
115109, 114syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
11686breq1d 5116 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1) ≀ π‘˜ ↔ 𝑃 ≀ π‘˜))
117115, 116mtbid 324 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ 𝑃 ≀ π‘˜)
118117iffalsed 4498 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ π‘˜, 𝐡, 0) = 0)
119118eqeq2d 2744 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0))
120 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
121 nnuz 12811 . . . . . . . . . . . . . 14 β„• = (β„€β‰₯β€˜1)
122120, 121eleqtrdi 2844 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
123 seqp1 13927 . . . . . . . . . . . . 13 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)) = ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1))))
124122, 123syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)) = ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1))))
125124oveq2d 7374 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))))
12626adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ β„™)
12756simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ seq1( Β· , 𝐹):β„•βŸΆβ„•)
128127ffvelcdmda 7036 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
129 nnz 12525 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€)
130 nnne0 12192 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0)
131129, 130jca 513 . . . . . . . . . . . . 13 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
132128, 131syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
133 nnz 12525 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„€)
134 nnne0 12192 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) β‰  0)
135133, 134jca 513 . . . . . . . . . . . . 13 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
13660, 135syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
137 pcmul 16728 . . . . . . . . . . . 12 ((𝑃 ∈ β„™ ∧ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0) ∧ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0)) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
138126, 132, 136, 137syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
139125, 138eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
140139adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
141 prmnn 16555 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
14226, 141syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ β„•)
143142nnred 12173 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑃 ∈ ℝ)
144143adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ ℝ)
145144leidd 11726 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ 𝑃)
146145, 86breqtrrd 5134 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ (π‘˜ + 1))
147146iftrued 4495 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = 𝐡)
148140, 147eqeq12d 2749 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
149107, 119, 1483imtr4d 294 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
150149expr 458 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) = 𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
151139adantrr 716 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
152 simplrr 777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) β‰  𝑃)
153152necomd 2996 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 β‰  (π‘˜ + 1))
15426ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 ∈ β„™)
155 simpr 486 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) ∈ β„™)
15655ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
15774nfel1 2920 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0
15880eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (π‘˜ + 1) β†’ (𝐴 ∈ β„•0 ↔ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
159157, 158rspc 3568 . . . . . . . . . . . . . . . . . 18 ((π‘˜ + 1) ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
160155, 156, 159sylc 65 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0)
161 prmdvdsexpr 16598 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ β„™ ∧ (π‘˜ + 1) ∈ β„™ ∧ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
162154, 155, 160, 161syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
163162necon3ad 2953 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 β‰  (π‘˜ + 1) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
164153, 163mpd 15 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
16558ad2antrl 727 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
166165, 68, 84sylancl 587 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
167 iftrue 4493 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
168166, 167sylan9eq 2793 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
169168breq2d 5118 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)) ↔ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
170164, 169mtbird 325 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)))
17157adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝐹:β„•βŸΆβ„•)
172171, 165, 59syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
173172adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
174 pceq0 16748 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ (πΉβ€˜(π‘˜ + 1)) ∈ β„•) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
175154, 173, 174syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
176170, 175mpbird 257 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
177 iffalse 4496 . . . . . . . . . . . . . . 15 (Β¬ (π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = 1)
178166, 177sylan9eq 2793 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = 1)
179178oveq2d 7374 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt 1))
18026, 41syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑃 pCnt 1) = 0)
181180ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt 1) = 0)
182179, 181eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
183176, 182pm2.61dan 812 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
184183oveq2d 7374 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0))
18526adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„™)
186128adantrr 716 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
187185, 186pccld 16727 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„•0)
188187nn0cnd 12480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„‚)
189188addid1d 11360 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
190151, 184, 1893eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
191142adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„•)
192191nnred 12173 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ ℝ)
193165nnred 12173 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ ℝ)
194192, 193ltlend 11305 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 < (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
195 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ π‘˜ ∈ β„•)
196 nnleltp1 12563 . . . . . . . . . . . 12 ((𝑃 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
197191, 195, 196syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
198 simprr 772 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) β‰  𝑃)
199198biantrud 533 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
200194, 197, 1993bitr4rd 312 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ 𝑃 ≀ π‘˜))
201200ifbid 4510 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
202190, 201eqeq12d 2749 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
203202biimprd 248 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
204203expr 458 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) β‰  𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
205150, 204pm2.61dne 3028 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
206205expcom 415 . . . 4 (π‘˜ ∈ β„• β†’ (πœ‘ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
207206a2d 29 . . 3 (π‘˜ ∈ β„• β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)) β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
2087, 13, 19, 25, 53, 207nnind 12176 . 2 (𝑁 ∈ β„• β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2091, 208mpcom 38 1 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  Vcvv 3444  β¦‹csb 3856  ifcif 4487   class class class wbr 5106   ↦ cmpt 5189  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   < clt 11194   ≀ cle 11195  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  seqcseq 13912  β†‘cexp 13973   βˆ₯ cdvds 16141  β„™cprime 16552   pCnt cpc 16713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9383  df-inf 9384  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-q 12879  df-rp 12921  df-fz 13431  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-dvds 16142  df-gcd 16380  df-prm 16553  df-pc 16714
This theorem is referenced by:  pcmpt2  16770  pcprod  16772  1arithlem4  16803  chtublem  26575  bposlem3  26650
  Copyright terms: Public domain W3C validator