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

Theorem prmreclem5 16799
Description: Lemma for prmrec 16801. Here we show the inequality ๐‘ / 2 < โ™ฏ๐‘€ by decomposing the set (1...๐‘) into the disjoint union of the set ๐‘€ of those numbers that are not divisible by any "large" primes (above ๐พ) and the indexed union over ๐พ < ๐‘˜ of the numbers ๐‘Šโ€˜๐‘˜ that divide the prime ๐‘˜. By prmreclem4 16798 the second of these has size less than ๐‘ times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part ๐‘€ must be at least ๐‘ / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (1 / ๐‘›), 0))
prmrec.2 (๐œ‘ โ†’ ๐พ โˆˆ โ„•)
prmrec.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
prmrec.4 ๐‘€ = {๐‘› โˆˆ (1...๐‘) โˆฃ โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘›}
prmrec.5 (๐œ‘ โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
prmrec.6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) < (1 / 2))
prmrec.7 ๐‘Š = (๐‘ โˆˆ โ„• โ†ฆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›)})
Assertion
Ref Expression
prmreclem5 (๐œ‘ โ†’ (๐‘ / 2) < ((2โ†‘๐พ) ยท (โˆšโ€˜๐‘)))
Distinct variable groups:   ๐‘˜,๐‘›,๐‘,๐น   ๐‘˜,๐พ,๐‘›,๐‘   ๐‘˜,๐‘€,๐‘›,๐‘   ๐œ‘,๐‘˜,๐‘›,๐‘   ๐‘˜,๐‘Š   ๐‘˜,๐‘,๐‘›,๐‘
Allowed substitution hints:   ๐‘Š(๐‘›,๐‘)

Proof of Theorem prmreclem5
Dummy variables ๐‘Ÿ ๐‘ฅ ๐‘ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmrec.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
21nnred 12175 . . 3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
32rehalfcld 12407 . 2 (๐œ‘ โ†’ (๐‘ / 2) โˆˆ โ„)
4 fzfi 13884 . . . . . 6 (1...๐‘) โˆˆ Fin
5 prmrec.4 . . . . . . 7 ๐‘€ = {๐‘› โˆˆ (1...๐‘) โˆฃ โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘›}
65ssrab3 4045 . . . . . 6 ๐‘€ โŠ† (1...๐‘)
7 ssfi 9124 . . . . . 6 (((1...๐‘) โˆˆ Fin โˆง ๐‘€ โŠ† (1...๐‘)) โ†’ ๐‘€ โˆˆ Fin)
84, 6, 7mp2an 691 . . . . 5 ๐‘€ โˆˆ Fin
9 hashcl 14263 . . . . 5 (๐‘€ โˆˆ Fin โ†’ (โ™ฏโ€˜๐‘€) โˆˆ โ„•0)
108, 9ax-mp 5 . . . 4 (โ™ฏโ€˜๐‘€) โˆˆ โ„•0
1110nn0rei 12431 . . 3 (โ™ฏโ€˜๐‘€) โˆˆ โ„
1211a1i 11 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘€) โˆˆ โ„)
13 2nn 12233 . . . . 5 2 โˆˆ โ„•
14 prmrec.2 . . . . . 6 (๐œ‘ โ†’ ๐พ โˆˆ โ„•)
1514nnnn0d 12480 . . . . 5 (๐œ‘ โ†’ ๐พ โˆˆ โ„•0)
16 nnexpcl 13987 . . . . 5 ((2 โˆˆ โ„• โˆง ๐พ โˆˆ โ„•0) โ†’ (2โ†‘๐พ) โˆˆ โ„•)
1713, 15, 16sylancr 588 . . . 4 (๐œ‘ โ†’ (2โ†‘๐พ) โˆˆ โ„•)
1817nnred 12175 . . 3 (๐œ‘ โ†’ (2โ†‘๐พ) โˆˆ โ„)
191nnrpd 12962 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
2019rpsqrtcld 15303 . . . 4 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
2120rpred 12964 . . 3 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„)
2218, 21remulcld 11192 . 2 (๐œ‘ โ†’ ((2โ†‘๐พ) ยท (โˆšโ€˜๐‘)) โˆˆ โ„)
232recnd 11190 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
24232halvesd 12406 . . . . 5 (๐œ‘ โ†’ ((๐‘ / 2) + (๐‘ / 2)) = ๐‘)
256a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โŠ† (1...๐‘))
2614peano2nnd 12177 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐พ + 1) โˆˆ โ„•)
27 elfzuz 13444 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1)))
28 eluznn 12850 . . . . . . . . . . . . 13 (((๐พ + 1) โˆˆ โ„• โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))) โ†’ ๐‘˜ โˆˆ โ„•)
2926, 27, 28syl2an 597 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ ๐‘˜ โˆˆ โ„•)
30 eleq1w 2821 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘˜ โ†’ (๐‘ โˆˆ โ„™ โ†” ๐‘˜ โˆˆ โ„™))
31 breq1 5113 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘˜ โ†’ (๐‘ โˆฅ ๐‘› โ†” ๐‘˜ โˆฅ ๐‘›))
3230, 31anbi12d 632 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘˜ โ†’ ((๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›) โ†” (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)))
3332rabbidv 3418 . . . . . . . . . . . . . . 15 (๐‘ = ๐‘˜ โ†’ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›)} = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)})
34 prmrec.7 . . . . . . . . . . . . . . 15 ๐‘Š = (๐‘ โˆˆ โ„• โ†ฆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›)})
35 ovex 7395 . . . . . . . . . . . . . . . 16 (1...๐‘) โˆˆ V
3635rabex 5294 . . . . . . . . . . . . . . 15 {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)} โˆˆ V
3733, 34, 36fvmpt 6953 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ โ„• โ†’ (๐‘Šโ€˜๐‘˜) = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)})
3837adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘Šโ€˜๐‘˜) = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)})
39 ssrab2 4042 . . . . . . . . . . . . 13 {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)} โŠ† (1...๐‘)
4038, 39eqsstrdi 4003 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘))
4129, 40syldan 592 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ (๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘))
4241ralrimiva 3144 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘))
43 iunss 5010 . . . . . . . . . 10 (โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘) โ†” โˆ€๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘))
4442, 43sylibr 233 . . . . . . . . 9 (๐œ‘ โ†’ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘))
4525, 44unssd 4151 . . . . . . . 8 (๐œ‘ โ†’ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โŠ† (1...๐‘))
46 breq1 5113 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘ž โ†’ (๐‘ โˆฅ ๐‘› โ†” ๐‘ž โˆฅ ๐‘›))
4746notbid 318 . . . . . . . . . . . . . . 15 (๐‘ = ๐‘ž โ†’ (ยฌ ๐‘ โˆฅ ๐‘› โ†” ยฌ ๐‘ž โˆฅ ๐‘›))
4847cbvralvw 3228 . . . . . . . . . . . . . 14 (โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘› โ†” โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘›)
49 breq2 5114 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘ฅ โ†’ (๐‘ž โˆฅ ๐‘› โ†” ๐‘ž โˆฅ ๐‘ฅ))
5049notbid 318 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘ฅ โ†’ (ยฌ ๐‘ž โˆฅ ๐‘› โ†” ยฌ ๐‘ž โˆฅ ๐‘ฅ))
5150ralbidv 3175 . . . . . . . . . . . . . 14 (๐‘› = ๐‘ฅ โ†’ (โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘› โ†” โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ))
5248, 51bitrid 283 . . . . . . . . . . . . 13 (๐‘› = ๐‘ฅ โ†’ (โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘› โ†” โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ))
5352, 5elrab2 3653 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐‘€ โ†” (๐‘ฅ โˆˆ (1...๐‘) โˆง โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ))
54 elun1 4141 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ ๐‘€ โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
5553, 54sylbir 234 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ (1...๐‘) โˆง โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ) โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
5655ex 414 . . . . . . . . . 10 (๐‘ฅ โˆˆ (1...๐‘) โ†’ (โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
5756adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โ†’ (โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
58 dfrex2 3077 . . . . . . . . . 10 (โˆƒ๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ))๐‘ž โˆฅ ๐‘ฅ โ†” ยฌ โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ)
5914nnzd 12533 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐พ โˆˆ โ„ค)
6059peano2zd 12617 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐พ + 1) โˆˆ โ„ค)
6160ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐พ + 1) โˆˆ โ„ค)
621nnzd 12533 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
6362ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ โˆˆ โ„ค)
64 eldifi 4091 . . . . . . . . . . . . . . . 16 (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โ†’ ๐‘ž โˆˆ โ„™)
6564ad2antrl 727 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ โ„™)
66 prmz 16558 . . . . . . . . . . . . . . 15 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„ค)
6765, 66syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ โ„ค)
68 eldifn 4092 . . . . . . . . . . . . . . . . . 18 (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โ†’ ยฌ ๐‘ž โˆˆ (1...๐พ))
6968ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ยฌ ๐‘ž โˆˆ (1...๐พ))
70 prmnn 16557 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„•)
7165, 70syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ โ„•)
72 nnuz 12813 . . . . . . . . . . . . . . . . . . 19 โ„• = (โ„คโ‰ฅโ€˜1)
7371, 72eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ (โ„คโ‰ฅโ€˜1))
7459ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐พ โˆˆ โ„ค)
75 elfz5 13440 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ (โ„คโ‰ฅโ€˜1) โˆง ๐พ โˆˆ โ„ค) โ†’ (๐‘ž โˆˆ (1...๐พ) โ†” ๐‘ž โ‰ค ๐พ))
7673, 74, 75syl2anc 585 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐‘ž โˆˆ (1...๐พ) โ†” ๐‘ž โ‰ค ๐พ))
7769, 76mtbid 324 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ยฌ ๐‘ž โ‰ค ๐พ)
7814nnred 12175 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐พ โˆˆ โ„)
7978ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐พ โˆˆ โ„)
8071nnred 12175 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ โ„)
8179, 80ltnled 11309 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐พ < ๐‘ž โ†” ยฌ ๐‘ž โ‰ค ๐พ))
8277, 81mpbird 257 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐พ < ๐‘ž)
83 zltp1le 12560 . . . . . . . . . . . . . . . 16 ((๐พ โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค) โ†’ (๐พ < ๐‘ž โ†” (๐พ + 1) โ‰ค ๐‘ž))
8474, 67, 83syl2anc 585 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐พ < ๐‘ž โ†” (๐พ + 1) โ‰ค ๐‘ž))
8582, 84mpbid 231 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐พ + 1) โ‰ค ๐‘ž)
86 elfznn 13477 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ (1...๐‘) โ†’ ๐‘ฅ โˆˆ โ„•)
8786ad2antlr 726 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ โ„•)
8887nnred 12175 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ โ„)
892ad2antrr 725 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ โˆˆ โ„)
90 simprr 772 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆฅ ๐‘ฅ)
91 dvdsle 16199 . . . . . . . . . . . . . . . . 17 ((๐‘ž โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ž โ‰ค ๐‘ฅ))
9267, 87, 91syl2anc 585 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ž โ‰ค ๐‘ฅ))
9390, 92mpd 15 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โ‰ค ๐‘ฅ)
94 elfzle2 13452 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ (1...๐‘) โ†’ ๐‘ฅ โ‰ค ๐‘)
9594ad2antlr 726 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โ‰ค ๐‘)
9680, 88, 89, 93, 95letrd 11319 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โ‰ค ๐‘)
9761, 63, 67, 85, 96elfzd 13439 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ž โˆˆ ((๐พ + 1)...๐‘))
9849anbi2d 630 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘ฅ โ†’ ((๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›) โ†” (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ)))
99 simplr 768 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ (1...๐‘))
10065, 90jca 513 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ))
10198, 99, 100elrabd 3652 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)})
102 eleq1w 2821 . . . . . . . . . . . . . . . . . 18 (๐‘ = ๐‘ž โ†’ (๐‘ โˆˆ โ„™ โ†” ๐‘ž โˆˆ โ„™))
103102, 46anbi12d 632 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘ž โ†’ ((๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›) โ†” (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)))
104103rabbidv 3418 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘ž โ†’ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ โˆˆ โ„™ โˆง ๐‘ โˆฅ ๐‘›)} = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)})
10535rabex 5294 . . . . . . . . . . . . . . . 16 {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)} โˆˆ V
106104, 34, 105fvmpt 6953 . . . . . . . . . . . . . . 15 (๐‘ž โˆˆ โ„• โ†’ (๐‘Šโ€˜๐‘ž) = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)})
10771, 106syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ (๐‘Šโ€˜๐‘ž) = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘›)})
108101, 107eleqtrrd 2841 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘ž))
109 fveq2 6847 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘ž โ†’ (๐‘Šโ€˜๐‘˜) = (๐‘Šโ€˜๐‘ž))
110109eliuni 4965 . . . . . . . . . . . . 13 ((๐‘ž โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘ž)) โ†’ ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))
11197, 108, 110syl2anc 585 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))
112 elun2 4142 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
113111, 112syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โˆง (๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) โˆง ๐‘ž โˆฅ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
114113rexlimdvaa 3154 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โ†’ (โˆƒ๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ))๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
11558, 114biimtrrid 242 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โ†’ (ยฌ โˆ€๐‘ž โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ž โˆฅ ๐‘ฅ โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
11657, 115pm2.61d 179 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐‘)) โ†’ ๐‘ฅ โˆˆ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
11745, 116eqelssd 3970 . . . . . . 7 (๐œ‘ โ†’ (๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) = (1...๐‘))
118117fveq2d 6851 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜(๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))) = (โ™ฏโ€˜(1...๐‘)))
1191nnnn0d 12480 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
120 hashfz1 14253 . . . . . . 7 (๐‘ โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
121119, 120syl 17 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
122118, 121eqtr2d 2778 . . . . 5 (๐œ‘ โ†’ ๐‘ = (โ™ฏโ€˜(๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
1238a1i 11 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ Fin)
124 ssfi 9124 . . . . . . 7 (((1...๐‘) โˆˆ Fin โˆง โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โŠ† (1...๐‘)) โ†’ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โˆˆ Fin)
1254, 44, 124sylancr 588 . . . . . 6 (๐œ‘ โ†’ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โˆˆ Fin)
126 breq1 5113 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘˜ โ†’ (๐‘ โˆฅ ๐‘ฅ โ†” ๐‘˜ โˆฅ ๐‘ฅ))
127126notbid 318 . . . . . . . . . . . . . . . 16 (๐‘ = ๐‘˜ โ†’ (ยฌ ๐‘ โˆฅ ๐‘ฅ โ†” ยฌ ๐‘˜ โˆฅ ๐‘ฅ))
128 breq2 5114 . . . . . . . . . . . . . . . . . . . . 21 (๐‘› = ๐‘ฅ โ†’ (๐‘ โˆฅ ๐‘› โ†” ๐‘ โˆฅ ๐‘ฅ))
129128notbid 318 . . . . . . . . . . . . . . . . . . . 20 (๐‘› = ๐‘ฅ โ†’ (ยฌ ๐‘ โˆฅ ๐‘› โ†” ยฌ ๐‘ โˆฅ ๐‘ฅ))
130129ralbidv 3175 . . . . . . . . . . . . . . . . . . 19 (๐‘› = ๐‘ฅ โ†’ (โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘› โ†” โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘ฅ))
131130, 5elrab2 3653 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ ๐‘€ โ†” (๐‘ฅ โˆˆ (1...๐‘) โˆง โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘ฅ))
132131simprbi 498 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ ๐‘€ โ†’ โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘ฅ)
133132ad2antlr 726 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ โˆ€๐‘ โˆˆ (โ„™ โˆ– (1...๐พ)) ยฌ ๐‘ โˆฅ ๐‘ฅ)
134 simprr 772 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ๐‘˜ โˆˆ โ„™)
135 noel 4295 . . . . . . . . . . . . . . . . . 18 ยฌ ๐‘˜ โˆˆ โˆ…
136 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ๐‘˜ โˆˆ ((๐พ + 1)...๐‘))
137136biantrud 533 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ (๐‘˜ โˆˆ (1...๐พ) โ†” (๐‘˜ โˆˆ (1...๐พ) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘))))
138 elin 3931 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ โˆˆ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘)) โ†” (๐‘˜ โˆˆ (1...๐พ) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)))
139137, 138bitr4di 289 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ (๐‘˜ โˆˆ (1...๐พ) โ†” ๐‘˜ โˆˆ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘))))
14078ltp1d 12092 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐พ < (๐พ + 1))
141 fzdisj 13475 . . . . . . . . . . . . . . . . . . . . . 22 (๐พ < (๐พ + 1) โ†’ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘)) = โˆ…)
142140, 141syl 17 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘)) = โˆ…)
143142ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘)) = โˆ…)
144143eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ (๐‘˜ โˆˆ ((1...๐พ) โˆฉ ((๐พ + 1)...๐‘)) โ†” ๐‘˜ โˆˆ โˆ…))
145139, 144bitrd 279 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ (๐‘˜ โˆˆ (1...๐พ) โ†” ๐‘˜ โˆˆ โˆ…))
146135, 145mtbiri 327 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ยฌ ๐‘˜ โˆˆ (1...๐พ))
147134, 146eldifd 3926 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ๐‘˜ โˆˆ (โ„™ โˆ– (1...๐พ)))
148127, 133, 147rspcdva 3585 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง (๐‘˜ โˆˆ ((๐พ + 1)...๐‘) โˆง ๐‘˜ โˆˆ โ„™)) โ†’ ยฌ ๐‘˜ โˆฅ ๐‘ฅ)
149148expr 458 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ (๐‘˜ โˆˆ โ„™ โ†’ ยฌ ๐‘˜ โˆฅ ๐‘ฅ))
150 imnan 401 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„™ โ†’ ยฌ ๐‘˜ โˆฅ ๐‘ฅ) โ†” ยฌ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ))
151149, 150sylib 217 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ ยฌ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ))
15229adantlr 714 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ ๐‘˜ โˆˆ โ„•)
153152, 37syl 17 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ (๐‘Šโ€˜๐‘˜) = {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)})
154153eleq2d 2824 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ (๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘˜) โ†” ๐‘ฅ โˆˆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)}))
155 breq2 5114 . . . . . . . . . . . . . . . . 17 (๐‘› = ๐‘ฅ โ†’ (๐‘˜ โˆฅ ๐‘› โ†” ๐‘˜ โˆฅ ๐‘ฅ))
156155anbi2d 630 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘ฅ โ†’ ((๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›) โ†” (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ)))
157156elrab 3650 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)} โ†” (๐‘ฅ โˆˆ (1...๐‘) โˆง (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ)))
158157simprbi 498 . . . . . . . . . . . . . 14 (๐‘ฅ โˆˆ {๐‘› โˆˆ (1...๐‘) โˆฃ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘›)} โ†’ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ))
159154, 158syl6bi 253 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ (๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘˜) โ†’ (๐‘˜ โˆˆ โ„™ โˆง ๐‘˜ โˆฅ ๐‘ฅ)))
160151, 159mtod 197 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ ยฌ ๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘˜))
161160nrexdv 3147 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โ†’ ยฌ โˆƒ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘˜))
162 eliun 4963 . . . . . . . . . . 11 (๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โ†” โˆƒ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)๐‘ฅ โˆˆ (๐‘Šโ€˜๐‘˜))
163161, 162sylnibr 329 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘€) โ†’ ยฌ ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))
164163ex 414 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐‘€ โ†’ ยฌ ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
165 imnan 401 . . . . . . . . 9 ((๐‘ฅ โˆˆ ๐‘€ โ†’ ยฌ ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ†” ยฌ (๐‘ฅ โˆˆ ๐‘€ โˆง ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
166164, 165sylib 217 . . . . . . . 8 (๐œ‘ โ†’ ยฌ (๐‘ฅ โˆˆ ๐‘€ โˆง ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
167 elin 3931 . . . . . . . 8 (๐‘ฅ โˆˆ (๐‘€ โˆฉ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ†” (๐‘ฅ โˆˆ ๐‘€ โˆง ๐‘ฅ โˆˆ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
168166, 167sylnibr 329 . . . . . . 7 (๐œ‘ โ†’ ยฌ ๐‘ฅ โˆˆ (๐‘€ โˆฉ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)))
169168eq0rdv 4369 . . . . . 6 (๐œ‘ โ†’ (๐‘€ โˆฉ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) = โˆ…)
170 hashun 14289 . . . . . 6 ((๐‘€ โˆˆ Fin โˆง โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โˆˆ Fin โˆง (๐‘€ โˆฉ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) = โˆ…) โ†’ (โ™ฏโ€˜(๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))) = ((โ™ฏโ€˜๐‘€) + (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
171123, 125, 169, 170syl3anc 1372 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜(๐‘€ โˆช โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))) = ((โ™ฏโ€˜๐‘€) + (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
17224, 122, 1713eqtrd 2781 . . . 4 (๐œ‘ โ†’ ((๐‘ / 2) + (๐‘ / 2)) = ((โ™ฏโ€˜๐‘€) + (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))))
173 hashcl 14263 . . . . . . 7 (โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) โˆˆ Fin โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โˆˆ โ„•0)
174125, 173syl 17 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โˆˆ โ„•0)
175174nn0red 12481 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โˆˆ โ„)
176 fzfid 13885 . . . . . . . 8 (๐œ‘ โ†’ ((๐พ + 1)...๐‘) โˆˆ Fin)
17726, 28sylan 581 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))) โ†’ ๐‘˜ โˆˆ โ„•)
178 nnrecre 12202 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ (1 / ๐‘˜) โˆˆ โ„)
179 0re 11164 . . . . . . . . . . 11 0 โˆˆ โ„
180 ifcl 4536 . . . . . . . . . . 11 (((1 / ๐‘˜) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
181178, 179, 180sylancl 587 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
182177, 181syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))) โ†’ if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
18327, 182sylan2 594 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)) โ†’ if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
184176, 183fsumrecl 15626 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
1852, 184remulcld 11192 . . . . . 6 (๐œ‘ โ†’ (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) โˆˆ โ„)
186 prmrec.1 . . . . . . . 8 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (1 / ๐‘›), 0))
187 prmrec.5 . . . . . . . 8 (๐œ‘ โ†’ seq1( + , ๐น) โˆˆ dom โ‡ )
188 prmrec.6 . . . . . . . 8 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) < (1 / 2))
189186, 14, 1, 5, 187, 188, 34prmreclem4 16798 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐พ) โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ‰ค (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))))
190 eluz 12784 . . . . . . . . . 10 ((๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค) โ†’ (๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†” ๐‘ โ‰ค ๐พ))
19162, 59, 190syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ (๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†” ๐‘ โ‰ค ๐พ))
192 nnleltp1 12565 . . . . . . . . . 10 ((๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ โ„•) โ†’ (๐‘ โ‰ค ๐พ โ†” ๐‘ < (๐พ + 1)))
1931, 14, 192syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ โ‰ค ๐พ โ†” ๐‘ < (๐พ + 1)))
194 fzn 13464 . . . . . . . . . 10 (((๐พ + 1) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘ < (๐พ + 1) โ†” ((๐พ + 1)...๐‘) = โˆ…))
19560, 62, 194syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ < (๐พ + 1) โ†” ((๐พ + 1)...๐‘) = โˆ…))
196191, 193, 1953bitrd 305 . . . . . . . 8 (๐œ‘ โ†’ (๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†” ((๐พ + 1)...๐‘) = โˆ…))
197 0le0 12261 . . . . . . . . . 10 0 โ‰ค 0
19823mul01d 11361 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ ยท 0) = 0)
199197, 198breqtrrid 5148 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (๐‘ ยท 0))
200 iuneq1 4975 . . . . . . . . . . . . 13 (((๐พ + 1)...๐‘) = โˆ… โ†’ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) = โˆช ๐‘˜ โˆˆ โˆ… (๐‘Šโ€˜๐‘˜))
201 0iun 5028 . . . . . . . . . . . . 13 โˆช ๐‘˜ โˆˆ โˆ… (๐‘Šโ€˜๐‘˜) = โˆ…
202200, 201eqtrdi 2793 . . . . . . . . . . . 12 (((๐พ + 1)...๐‘) = โˆ… โ†’ โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜) = โˆ…)
203202fveq2d 6851 . . . . . . . . . . 11 (((๐พ + 1)...๐‘) = โˆ… โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) = (โ™ฏโ€˜โˆ…))
204 hash0 14274 . . . . . . . . . . 11 (โ™ฏโ€˜โˆ…) = 0
205203, 204eqtrdi 2793 . . . . . . . . . 10 (((๐พ + 1)...๐‘) = โˆ… โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) = 0)
206 sumeq1 15580 . . . . . . . . . . . 12 (((๐พ + 1)...๐‘) = โˆ… โ†’ ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) = ฮฃ๐‘˜ โˆˆ โˆ… if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
207 sum0 15613 . . . . . . . . . . . 12 ฮฃ๐‘˜ โˆˆ โˆ… if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) = 0
208206, 207eqtrdi 2793 . . . . . . . . . . 11 (((๐พ + 1)...๐‘) = โˆ… โ†’ ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) = 0)
209208oveq2d 7378 . . . . . . . . . 10 (((๐พ + 1)...๐‘) = โˆ… โ†’ (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) = (๐‘ ยท 0))
210205, 209breq12d 5123 . . . . . . . . 9 (((๐พ + 1)...๐‘) = โˆ… โ†’ ((โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ‰ค (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) โ†” 0 โ‰ค (๐‘ ยท 0)))
211199, 210syl5ibrcom 247 . . . . . . . 8 (๐œ‘ โ†’ (((๐พ + 1)...๐‘) = โˆ… โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ‰ค (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))))
212196, 211sylbid 239 . . . . . . 7 (๐œ‘ โ†’ (๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ‰ค (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))))
213 uztric 12794 . . . . . . . 8 ((๐พ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐พ) โˆจ ๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘)))
21459, 62, 213syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐พ) โˆจ ๐พ โˆˆ (โ„คโ‰ฅโ€˜๐‘)))
215189, 212, 214mpjaod 859 . . . . . 6 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) โ‰ค (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)))
216 eqid 2737 . . . . . . . . . 10 (โ„คโ‰ฅโ€˜(๐พ + 1)) = (โ„คโ‰ฅโ€˜(๐พ + 1))
217 eleq1w 2821 . . . . . . . . . . . . 13 (๐‘› = ๐‘˜ โ†’ (๐‘› โˆˆ โ„™ โ†” ๐‘˜ โˆˆ โ„™))
218 oveq2 7370 . . . . . . . . . . . . 13 (๐‘› = ๐‘˜ โ†’ (1 / ๐‘›) = (1 / ๐‘˜))
219217, 218ifbieq1d 4515 . . . . . . . . . . . 12 (๐‘› = ๐‘˜ โ†’ if(๐‘› โˆˆ โ„™, (1 / ๐‘›), 0) = if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
220 ovex 7395 . . . . . . . . . . . . 13 (1 / ๐‘˜) โˆˆ V
221 c0ex 11156 . . . . . . . . . . . . 13 0 โˆˆ V
222220, 221ifex 4541 . . . . . . . . . . . 12 if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ V
223219, 186, 222fvmpt 6953 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
224177, 223syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
225181recnd 11190 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ โ„• โ†’ if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„‚)
226223, 225eqeltrd 2838 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
227226adantl 483 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
22872, 26, 227iserex 15548 . . . . . . . . . . 11 (๐œ‘ โ†’ (seq1( + , ๐น) โˆˆ dom โ‡ โ†” seq(๐พ + 1)( + , ๐น) โˆˆ dom โ‡ ))
229187, 228mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ seq(๐พ + 1)( + , ๐น) โˆˆ dom โ‡ )
230216, 60, 224, 182, 229isumrecl 15657 . . . . . . . . 9 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„)
231 halfre 12374 . . . . . . . . . 10 (1 / 2) โˆˆ โ„
232231a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ (1 / 2) โˆˆ โ„)
233 fzssuz 13489 . . . . . . . . . . 11 ((๐พ + 1)...๐‘) โŠ† (โ„คโ‰ฅโ€˜(๐พ + 1))
234233a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐พ + 1)...๐‘) โŠ† (โ„คโ‰ฅโ€˜(๐พ + 1)))
235 nnrp 12933 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„+)
236235rpreccld 12974 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (1 / ๐‘˜) โˆˆ โ„+)
237236rpge0d 12968 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ 0 โ‰ค (1 / ๐‘˜))
238 breq2 5114 . . . . . . . . . . . . 13 ((1 / ๐‘˜) = if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โ†’ (0 โ‰ค (1 / ๐‘˜) โ†” 0 โ‰ค if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)))
239 breq2 5114 . . . . . . . . . . . . 13 (0 = if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โ†’ (0 โ‰ค 0 โ†” 0 โ‰ค if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)))
240238, 239ifboth 4530 . . . . . . . . . . . 12 ((0 โ‰ค (1 / ๐‘˜) โˆง 0 โ‰ค 0) โ†’ 0 โ‰ค if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
241237, 197, 240sylancl 587 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ 0 โ‰ค if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
242177, 241syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))) โ†’ 0 โ‰ค if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
243216, 60, 176, 234, 224, 182, 242, 229isumless 15737 . . . . . . . . 9 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โ‰ค ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐พ + 1))if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0))
244184, 230, 232, 243, 188lelttrd 11320 . . . . . . . 8 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) < (1 / 2))
2451nngt0d 12209 . . . . . . . . 9 (๐œ‘ โ†’ 0 < ๐‘)
246 ltmul2 12013 . . . . . . . . 9 ((ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) โˆˆ โ„ โˆง (1 / 2) โˆˆ โ„ โˆง (๐‘ โˆˆ โ„ โˆง 0 < ๐‘)) โ†’ (ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) < (1 / 2) โ†” (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) < (๐‘ ยท (1 / 2))))
247184, 232, 2, 245, 246syl112anc 1375 . . . . . . . 8 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0) < (1 / 2) โ†” (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) < (๐‘ ยท (1 / 2))))
248244, 247mpbid 231 . . . . . . 7 (๐œ‘ โ†’ (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) < (๐‘ ยท (1 / 2)))
249 2cn 12235 . . . . . . . . 9 2 โˆˆ โ„‚
250 2ne0 12264 . . . . . . . . 9 2 โ‰  0
251 divrec 11836 . . . . . . . . 9 ((๐‘ โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ (๐‘ / 2) = (๐‘ ยท (1 / 2)))
252249, 250, 251mp3an23 1454 . . . . . . . 8 (๐‘ โˆˆ โ„‚ โ†’ (๐‘ / 2) = (๐‘ ยท (1 / 2)))
25323, 252syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐‘ / 2) = (๐‘ ยท (1 / 2)))
254248, 253breqtrrd 5138 . . . . . 6 (๐œ‘ โ†’ (๐‘ ยท ฮฃ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)if(๐‘˜ โˆˆ โ„™, (1 / ๐‘˜), 0)) < (๐‘ / 2))
255175, 185, 3, 215, 254lelttrd 11320 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜)) < (๐‘ / 2))
256175, 3, 12, 255ltadd2dd 11321 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜๐‘€) + (โ™ฏโ€˜โˆช ๐‘˜ โˆˆ ((๐พ + 1)...๐‘)(๐‘Šโ€˜๐‘˜))) < ((โ™ฏโ€˜๐‘€) + (๐‘ / 2)))
257172, 256eqbrtrd 5132 . . 3 (๐œ‘ โ†’ ((๐‘ / 2) + (๐‘ / 2)) < ((โ™ฏโ€˜๐‘€) + (๐‘ / 2)))
2583, 12, 3ltadd1d 11755 . . 3 (๐œ‘ โ†’ ((๐‘ / 2) < (โ™ฏโ€˜๐‘€) โ†” ((๐‘ / 2) + (๐‘ / 2)) < ((โ™ฏโ€˜๐‘€) + (๐‘ / 2))))
259257, 258mpbird 257 . 2 (๐œ‘ โ†’ (๐‘ / 2) < (โ™ฏโ€˜๐‘€))
260 oveq1 7369 . . . . . . . 8 (๐‘˜ = ๐‘Ÿ โ†’ (๐‘˜โ†‘2) = (๐‘Ÿโ†‘2))
261260breq1d 5120 . . . . . . 7 (๐‘˜ = ๐‘Ÿ โ†’ ((๐‘˜โ†‘2) โˆฅ ๐‘ฅ โ†” (๐‘Ÿโ†‘2) โˆฅ ๐‘ฅ))
262261cbvrabv 3420 . . . . . 6 {๐‘˜ โˆˆ โ„• โˆฃ (๐‘˜โ†‘2) โˆฅ ๐‘ฅ} = {๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘ฅ}
263 breq2 5114 . . . . . . 7 (๐‘ฅ = ๐‘› โ†’ ((๐‘Ÿโ†‘2) โˆฅ ๐‘ฅ โ†” (๐‘Ÿโ†‘2) โˆฅ ๐‘›))
264263rabbidv 3418 . . . . . 6 (๐‘ฅ = ๐‘› โ†’ {๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘ฅ} = {๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘›})
265262, 264eqtrid 2789 . . . . 5 (๐‘ฅ = ๐‘› โ†’ {๐‘˜ โˆˆ โ„• โˆฃ (๐‘˜โ†‘2) โˆฅ ๐‘ฅ} = {๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘›})
266265supeq1d 9389 . . . 4 (๐‘ฅ = ๐‘› โ†’ sup({๐‘˜ โˆˆ โ„• โˆฃ (๐‘˜โ†‘2) โˆฅ ๐‘ฅ}, โ„, < ) = sup({๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘›}, โ„, < ))
267266cbvmptv 5223 . . 3 (๐‘ฅ โˆˆ โ„• โ†ฆ sup({๐‘˜ โˆˆ โ„• โˆฃ (๐‘˜โ†‘2) โˆฅ ๐‘ฅ}, โ„, < )) = (๐‘› โˆˆ โ„• โ†ฆ sup({๐‘Ÿ โˆˆ โ„• โˆฃ (๐‘Ÿโ†‘2) โˆฅ ๐‘›}, โ„, < ))
268186, 14, 1, 5, 267prmreclem3 16797 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘€) โ‰ค ((2โ†‘๐พ) ยท (โˆšโ€˜๐‘)))
2693, 12, 22, 259, 268ltletrd 11322 1 (๐œ‘ โ†’ (๐‘ / 2) < ((2โ†‘๐พ) ยท (โˆšโ€˜๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  โˆƒwrex 3074  {crab 3410   โˆ– cdif 3912   โˆช cun 3913   โˆฉ cin 3914   โŠ† wss 3915  โˆ…c0 4287  ifcif 4491  โˆช ciun 4959   class class class wbr 5110   โ†ฆ cmpt 5193  dom cdm 5638  โ€˜cfv 6501  (class class class)co 7362  Fincfn 8890  supcsup 9383  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   / cdiv 11819  โ„•cn 12160  2c2 12215  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  ...cfz 13431  seqcseq 13913  โ†‘cexp 13974  โ™ฏchash 14237  โˆšcsqrt 15125   โ‡ cli 15373  ฮฃcsu 15577   โˆฅ cdvds 16143  โ„™cprime 16554
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-q 12881  df-rp 12923  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378  df-sum 15578  df-dvds 16144  df-gcd 16382  df-prm 16555  df-pc 16716
This theorem is referenced by:  prmreclem6  16800
  Copyright terms: Public domain W3C validator