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

Theorem pcfac 12362
Description: Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
Assertion
Ref Expression
pcfac ((๐‘ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
Distinct variable groups:   ๐‘ƒ,๐‘˜   ๐‘˜,๐‘   ๐‘˜,๐‘€

Proof of Theorem pcfac
Dummy variables ๐‘š ๐‘› ๐‘ฅ ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5527 . . . . . . . 8 (๐‘ฅ = 0 โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜0))
2 fveq2 5527 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (!โ€˜๐‘ฅ) = (!โ€˜0))
32oveq2d 5904 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜0)))
4 fvoveq1 5911 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
54sumeq2sdv 11392 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
63, 5eqeq12d 2202 . . . . . . . 8 (๐‘ฅ = 0 โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜)))))
71, 6raleqbidv 2695 . . . . . . 7 (๐‘ฅ = 0 โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜)))))
87imbi2d 230 . . . . . 6 (๐‘ฅ = 0 โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))))
9 fveq2 5527 . . . . . . . 8 (๐‘ฅ = ๐‘› โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜๐‘›))
10 fveq2 5527 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (!โ€˜๐‘ฅ) = (!โ€˜๐‘›))
1110oveq2d 5904 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜๐‘›)))
12 fvoveq1 5911 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))
1312sumeq2sdv 11392 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))
1411, 13eqeq12d 2202 . . . . . . . 8 (๐‘ฅ = ๐‘› โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
159, 14raleqbidv 2695 . . . . . . 7 (๐‘ฅ = ๐‘› โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
1615imbi2d 230 . . . . . 6 (๐‘ฅ = ๐‘› โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))))))
17 fveq2 5527 . . . . . . . 8 (๐‘ฅ = (๐‘› + 1) โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜(๐‘› + 1)))
18 fveq2 5527 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (!โ€˜๐‘ฅ) = (!โ€˜(๐‘› + 1)))
1918oveq2d 5904 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))))
20 fvoveq1 5911 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
2120sumeq2sdv 11392 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
2219, 21eqeq12d 2202 . . . . . . . 8 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
2317, 22raleqbidv 2695 . . . . . . 7 (๐‘ฅ = (๐‘› + 1) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
2423imbi2d 230 . . . . . 6 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
25 fveq2 5527 . . . . . . . 8 (๐‘ฅ = ๐‘ โ†’ (โ„คโ‰ฅโ€˜๐‘ฅ) = (โ„คโ‰ฅโ€˜๐‘))
26 fveq2 5527 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (!โ€˜๐‘ฅ) = (!โ€˜๐‘))
2726oveq2d 5904 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ (๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = (๐‘ƒ pCnt (!โ€˜๐‘)))
28 fvoveq1 5911 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = (โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
2928sumeq2sdv 11392 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
3027, 29eqeq12d 2202 . . . . . . . 8 (๐‘ฅ = ๐‘ โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
3125, 30raleqbidv 2695 . . . . . . 7 (๐‘ฅ = ๐‘ โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜))) โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
3231imbi2d 230 . . . . . 6 (๐‘ฅ = ๐‘ โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฅ)(๐‘ƒ pCnt (!โ€˜๐‘ฅ)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ฅ / (๐‘ƒโ†‘๐‘˜)))) โ†” (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))))
33 1zzd 9294 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ 1 โˆˆ โ„ค)
34 eluzelz 9551 . . . . . . . . . . 11 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ ๐‘š โˆˆ โ„ค)
3534adantl 277 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘š โˆˆ โ„ค)
3633, 35fzfigd 10445 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (1...๐‘š) โˆˆ Fin)
37 isumz 11411 . . . . . . . . . 10 (((1 โˆˆ โ„ค โˆง (1...๐‘š) โІ (โ„คโ‰ฅโ€˜1) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜1)DECID ๐‘— โˆˆ (1...๐‘š)) โˆจ (1...๐‘š) โˆˆ Fin) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
3837olcs 737 . . . . . . . . 9 ((1...๐‘š) โˆˆ Fin โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
3936, 38syl 14 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)0 = 0)
40 0nn0 9205 . . . . . . . . . 10 0 โˆˆ โ„•0
41 elfznn 10068 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ โ„•)
4241nnnn0d 9243 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ โ„•0)
43 nn0uz 9576 . . . . . . . . . . . 12 โ„•0 = (โ„คโ‰ฅโ€˜0)
4442, 43eleqtrdi 2280 . . . . . . . . . . 11 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0))
4544adantl 277 . . . . . . . . . 10 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0))
46 simpll 527 . . . . . . . . . 10 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘ƒ โˆˆ โ„™)
47 pcfaclem 12361 . . . . . . . . . 10 ((0 โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = 0)
4840, 45, 46, 47mp3an2i 1352 . . . . . . . . 9 (((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = 0)
4948sumeq2dv 11390 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)0)
50 fac0 10722 . . . . . . . . . . 11 (!โ€˜0) = 1
5150oveq2i 5899 . . . . . . . . . 10 (๐‘ƒ pCnt (!โ€˜0)) = (๐‘ƒ pCnt 1)
52 pc1 12319 . . . . . . . . . 10 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ pCnt 1) = 0)
5351, 52eqtrid 2232 . . . . . . . . 9 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ pCnt (!โ€˜0)) = 0)
5453adantr 276 . . . . . . . 8 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ƒ pCnt (!โ€˜0)) = 0)
5539, 49, 543eqtr4rd 2231 . . . . . . 7 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
5655ralrimiva 2560 . . . . . 6 (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜0)(๐‘ƒ pCnt (!โ€˜0)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(0 / (๐‘ƒโ†‘๐‘˜))))
57 nn0z 9287 . . . . . . . . . . . 12 (๐‘› โˆˆ โ„•0 โ†’ ๐‘› โˆˆ โ„ค)
5857adantr 276 . . . . . . . . . . 11 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„ค)
59 uzid 9556 . . . . . . . . . . 11 (๐‘› โˆˆ โ„ค โ†’ ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
60 peano2uz 9597 . . . . . . . . . . 11 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘›) โ†’ (๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
6158, 59, 603syl 17 . . . . . . . . . 10 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›))
62 uzss 9562 . . . . . . . . . 10 ((๐‘› + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘›) โ†’ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โІ (โ„คโ‰ฅโ€˜๐‘›))
63 ssralv 3231 . . . . . . . . . 10 ((โ„คโ‰ฅโ€˜(๐‘› + 1)) โІ (โ„คโ‰ฅโ€˜๐‘›) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
6461, 62, 633syl 17 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
65 oveq1 5895 . . . . . . . . . . 11 ((๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))))
66 simpll 527 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘› โˆˆ โ„•0)
67 facp1 10724 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜(๐‘› + 1)) = ((!โ€˜๐‘›) ยท (๐‘› + 1)))
6866, 67syl 14 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (!โ€˜(๐‘› + 1)) = ((!โ€˜๐‘›) ยท (๐‘› + 1)))
6968oveq2d 5904 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))))
70 simplr 528 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ โ„™)
71 faccl 10729 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (!โ€˜๐‘›) โˆˆ โ„•)
72 nnz 9286 . . . . . . . . . . . . . . . 16 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โˆˆ โ„ค)
73 nnne0 8961 . . . . . . . . . . . . . . . 16 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ (!โ€˜๐‘›) โ‰  0)
7472, 73jca 306 . . . . . . . . . . . . . . 15 ((!โ€˜๐‘›) โˆˆ โ„• โ†’ ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0))
7566, 71, 743syl 17 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0))
76 nn0p1nn 9229 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„•0 โ†’ (๐‘› + 1) โˆˆ โ„•)
77 nnz 9286 . . . . . . . . . . . . . . . 16 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„ค)
78 nnne0 8961 . . . . . . . . . . . . . . . 16 ((๐‘› + 1) โˆˆ โ„• โ†’ (๐‘› + 1) โ‰  0)
7977, 78jca 306 . . . . . . . . . . . . . . 15 ((๐‘› + 1) โˆˆ โ„• โ†’ ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0))
8066, 76, 793syl 17 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0))
81 pcmul 12315 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง ((!โ€˜๐‘›) โˆˆ โ„ค โˆง (!โ€˜๐‘›) โ‰  0) โˆง ((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โ‰  0)) โ†’ (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))) = ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))))
8270, 75, 80, 81syl3anc 1248 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt ((!โ€˜๐‘›) ยท (๐‘› + 1))) = ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))))
8369, 82eqtr2d 2221 . . . . . . . . . . . 12 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))))
8466adantr 276 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘› โˆˆ โ„•0)
8584nn0zd 9387 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘› โˆˆ โ„ค)
86 prmnn 12124 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
8786ad2antlr 489 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ โ„•)
88 nnexpcl 10547 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•)
8987, 42, 88syl2an 289 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•)
90 fldivp1 12360 . . . . . . . . . . . . . . . . 17 ((๐‘› โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0))
9185, 89, 90syl2anc 411 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0))
92 elfzuz 10035 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (1...๐‘š) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1))
9366, 76syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„•)
9470, 93pccld 12314 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„•0)
9594nn0zd 9387 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค)
96 elfz5 10031 . . . . . . . . . . . . . . . . . . 19 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1) โˆง (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค) โ†’ (๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))) โ†” ๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
9792, 95, 96syl2anr 290 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))) โ†” ๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
98 simpllr 534 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘ƒ โˆˆ โ„™)
9984, 76syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› + 1) โˆˆ โ„•)
10099nnzd 9388 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› + 1) โˆˆ โ„ค)
10142adantl 277 . . . . . . . . . . . . . . . . . . 19 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ๐‘˜ โˆˆ โ„•0)
102 pcdvdsb 12333 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„™ โˆง (๐‘› + 1) โˆˆ โ„ค โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1)))
10398, 100, 101, 102syl3anc 1248 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘˜ โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1)))
10497, 103bitr2d 189 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1) โ†” ๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1)))))
105104ifbid 3567 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ if((๐‘ƒโ†‘๐‘˜) โˆฅ (๐‘› + 1), 1, 0) = if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
10691, 105eqtrd 2220 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
107106sumeq2dv 11390 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0))
108 1zzd 9294 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ 1 โˆˆ โ„ค)
109 eluzelz 9551 . . . . . . . . . . . . . . . . 17 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โ†’ ๐‘š โˆˆ โ„ค)
110109adantl 277 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ โ„ค)
111108, 110fzfigd 10445 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1...๐‘š) โˆˆ Fin)
112 znq 9638 . . . . . . . . . . . . . . . . . 18 (((๐‘› + 1) โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ ((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
113100, 89, 112syl2anc 411 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ ((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
114113flqcld 10291 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„ค)
115114zcnd 9390 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
116 znq 9638 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ โ„ค โˆง (๐‘ƒโ†‘๐‘˜) โˆˆ โ„•) โ†’ (๐‘› / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
11785, 89, 116syl2anc 411 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (๐‘› / (๐‘ƒโ†‘๐‘˜)) โˆˆ โ„š)
118117flqcld 10291 . . . . . . . . . . . . . . . 16 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„ค)
119118zcnd 9390 . . . . . . . . . . . . . . 15 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘˜ โˆˆ (1...๐‘š)) โ†’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
120111, 115, 119fsumsub 11474 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)((โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ (โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))))
12194nn0red 9244 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„)
12266nn0red 9244 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘› โˆˆ โ„)
123 peano2re 8107 . . . . . . . . . . . . . . . . . . . 20 (๐‘› โˆˆ โ„ โ†’ (๐‘› + 1) โˆˆ โ„)
124122, 123syl 14 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„)
125110zred 9389 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ โ„)
12693nnzd 9388 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„ค)
127 zdcle 9343 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„ค) โ†’ DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
12895, 126, 127syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
129 zletric 9311 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„ค) โ†’ ((๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โˆจ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
13095, 126, 129syl2anc 411 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โˆจ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
131130ord 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ (๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1))))
13293nnnn0d 9243 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โˆˆ โ„•0)
133 pcdvdsb 12333 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„™ โˆง (๐‘› + 1) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1)))
13470, 126, 132, 133syl3anc 1248 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†” (๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1)))
13587, 132nnexpcld 10690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„•)
136135nnzd 9388 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„ค)
137 dvdsle 11864 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„ค โˆง (๐‘› + 1) โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1)))
138136, 93, 137syl2anc 411 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1)))
139135nnred 8946 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒโ†‘(๐‘› + 1)) โˆˆ โ„)
140139, 124lenltd 8089 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โ‰ค (๐‘› + 1) โ†” ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
141138, 140sylibd 149 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒโ†‘(๐‘› + 1)) โˆฅ (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
142134, 141sylbid 150 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘› + 1) โ‰ค (๐‘ƒ pCnt (๐‘› + 1)) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
143131, 142syld 45 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))))
144 prmuz2 12145 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
145144ad2antlr 489 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
146 bernneq3 10657 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)))
147145, 132, 146syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)))
148 condc 854 . . . . . . . . . . . . . . . . . . . 20 (DECID (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ((ยฌ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1) โ†’ ยฌ (๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1))) โ†’ ((๐‘› + 1) < (๐‘ƒโ†‘(๐‘› + 1)) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))))
149128, 143, 147, 148syl3c 63 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค (๐‘› + 1))
150 eluzle 9554 . . . . . . . . . . . . . . . . . . . 20 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1)) โ†’ (๐‘› + 1) โ‰ค ๐‘š)
151150adantl 277 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘› + 1) โ‰ค ๐‘š)
152121, 124, 125, 149, 151letrd 8095 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š)
153 eluz 9555 . . . . . . . . . . . . . . . . . . 19 (((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค โˆง ๐‘š โˆˆ โ„ค) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š))
15495, 110, 153syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (๐‘› + 1)) โ‰ค ๐‘š))
155152, 154mpbird 167 . . . . . . . . . . . . . . . . 17 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))))
156 fzss2 10078 . . . . . . . . . . . . . . . . 17 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘ƒ pCnt (๐‘› + 1))) โ†’ (1...(๐‘ƒ pCnt (๐‘› + 1))) โІ (1...๐‘š))
157155, 156syl 14 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1...(๐‘ƒ pCnt (๐‘› + 1))) โІ (1...๐‘š))
158 elfzelz 10039 . . . . . . . . . . . . . . . . . . 19 (๐‘— โˆˆ (1...๐‘š) โ†’ ๐‘— โˆˆ โ„ค)
159158adantl 277 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ ๐‘— โˆˆ โ„ค)
160 1zzd 9294 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ 1 โˆˆ โ„ค)
16195adantr 276 . . . . . . . . . . . . . . . . . 18 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค)
162 fzdcel 10054 . . . . . . . . . . . . . . . . . 18 ((๐‘— โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„ค) โ†’ DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
163159, 160, 161, 162syl3anc 1248 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง ๐‘— โˆˆ (1...๐‘š)) โ†’ DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
164163ralrimiva 2560 . . . . . . . . . . . . . . . 16 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ โˆ€๐‘— โˆˆ (1...๐‘š)DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))))
165 sumhashdc 12359 . . . . . . . . . . . . . . . 16 (((1...๐‘š) โˆˆ Fin โˆง (1...(๐‘ƒ pCnt (๐‘› + 1))) โІ (1...๐‘š) โˆง โˆ€๐‘— โˆˆ (1...๐‘š)DECID ๐‘— โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1)))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))))
166111, 157, 164, 165syl3anc 1248 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))))
167 hashfz1 10777 . . . . . . . . . . . . . . . 16 ((๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))) = (๐‘ƒ pCnt (๐‘› + 1)))
16894, 167syl 14 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (โ™ฏโ€˜(1...(๐‘ƒ pCnt (๐‘› + 1)))) = (๐‘ƒ pCnt (๐‘› + 1)))
169166, 168eqtrd 2220 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)if(๐‘˜ โˆˆ (1...(๐‘ƒ pCnt (๐‘› + 1))), 1, 0) = (๐‘ƒ pCnt (๐‘› + 1)))
170107, 120, 1693eqtr3d 2228 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (๐‘ƒ pCnt (๐‘› + 1)))
171111, 115fsumcl 11422 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
172111, 119fsumcl 11422 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โˆˆ โ„‚)
17394nn0cnd 9245 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐‘ƒ pCnt (๐‘› + 1)) โˆˆ โ„‚)
174171, 172, 173subaddd 8300 . . . . . . . . . . . . 13 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))) โˆ’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) = (๐‘ƒ pCnt (๐‘› + 1)) โ†” (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
175170, 174mpbid 147 . . . . . . . . . . . 12 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))
17683, 175eqeq12d 2202 . . . . . . . . . . 11 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (((๐‘ƒ pCnt (!โ€˜๐‘›)) + (๐‘ƒ pCnt (๐‘› + 1))) = (ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) + (๐‘ƒ pCnt (๐‘› + 1))) โ†” (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
17765, 176imbitrid 154 . . . . . . . . . 10 (((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ (๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
178177ralimdva 2554 . . . . . . . . 9 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
17964, 178syld 45 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜)))))
180179ex 115 . . . . . . 7 (๐‘› โˆˆ โ„•0 โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜))) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
181180a2d 26 . . . . . 6 (๐‘› โˆˆ โ„•0 โ†’ ((๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘›)(๐‘ƒ pCnt (!โ€˜๐‘›)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘› / (๐‘ƒโ†‘๐‘˜)))) โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐‘ƒ pCnt (!โ€˜(๐‘› + 1))) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜((๐‘› + 1) / (๐‘ƒโ†‘๐‘˜))))))
1828, 16, 24, 32, 56, 181nn0ind 9381 . . . . 5 (๐‘ โˆˆ โ„•0 โ†’ (๐‘ƒ โˆˆ โ„™ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
183182imp 124 . . . 4 ((๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
184 oveq2 5896 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (1...๐‘š) = (1...๐‘€))
185184sumeq1d 11388 . . . . . 6 (๐‘š = ๐‘€ โ†’ ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
186185eqeq2d 2199 . . . . 5 (๐‘š = ๐‘€ โ†’ ((๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) โ†” (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
187186rspcv 2849 . . . 4 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘)(๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘š)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
188183, 187syl5 32 . . 3 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ ((๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜)))))
1891883impib 1202 . 2 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
1901893com12 1208 1 ((๐‘ โˆˆ โ„•0 โˆง ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘ƒ pCnt (!โ€˜๐‘)) = ฮฃ๐‘˜ โˆˆ (1...๐‘€)(โŒŠโ€˜(๐‘ / (๐‘ƒโ†‘๐‘˜))))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 709  DECID wdc 835   โˆง w3a 979   = wceq 1363   โˆˆ wcel 2158   โ‰  wne 2357  โˆ€wral 2465   โІ wss 3141  ifcif 3546   class class class wbr 4015  โ€˜cfv 5228  (class class class)co 5888  Fincfn 6754  โ„cr 7824  0cc0 7825  1c1 7826   + caddc 7828   ยท cmul 7830   < clt 8006   โ‰ค cle 8007   โˆ’ cmin 8142   / cdiv 8643  โ„•cn 8933  2c2 8984  โ„•0cn0 9190  โ„คcz 9267  โ„คโ‰ฅcuz 9542  โ„šcq 9633  ...cfz 10022  โŒŠcfl 10282  โ†‘cexp 10533  !cfa 10719  โ™ฏchash 10769  ฮฃcsu 11375   โˆฅ cdvds 11808  โ„™cprime 12121   pCnt cpc 12298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944  ax-caucvg 7945
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-irdg 6385  df-frec 6406  df-1o 6431  df-2o 6432  df-oadd 6435  df-er 6549  df-en 6755  df-dom 6756  df-fin 6757  df-sup 6997  df-inf 6998  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-3 8993  df-4 8994  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-fl 10284  df-mod 10337  df-seqfrec 10460  df-exp 10534  df-fac 10720  df-ihash 10770  df-cj 10865  df-re 10866  df-im 10867  df-rsqrt 11021  df-abs 11022  df-clim 11301  df-sumdc 11376  df-dvds 11809  df-gcd 11958  df-prm 12122  df-pc 12299
This theorem is referenced by:  pcbc  12363
  Copyright terms: Public domain W3C validator