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

Theorem lgsquadlem2 26732
Description: Lemma for lgsquad 26734. Count the members of ๐‘† with even coordinates, and combine with lgsquadlem1 26731 to get the total count of lattice points in ๐‘† (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
lgseisen.2 (๐œ‘ โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
lgseisen.3 (๐œ‘ โ†’ ๐‘ƒ โ‰  ๐‘„)
lgsquad.4 ๐‘€ = ((๐‘ƒ โˆ’ 1) / 2)
lgsquad.5 ๐‘ = ((๐‘„ โˆ’ 1) / 2)
lgsquad.6 ๐‘† = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„))}
Assertion
Ref Expression
lgsquadlem2 (๐œ‘ โ†’ (๐‘„ /L ๐‘ƒ) = (-1โ†‘(โ™ฏโ€˜๐‘†)))
Distinct variable groups:   ๐‘ฅ,๐‘ฆ,๐‘ƒ   ๐œ‘,๐‘ฅ,๐‘ฆ   ๐‘ฆ,๐‘€   ๐‘ฅ,๐‘,๐‘ฆ   ๐‘ฅ,๐‘„,๐‘ฆ   ๐‘ฅ,๐‘†   ๐‘ฅ,๐‘€   ๐‘ฆ,๐‘†

Proof of Theorem lgsquadlem2
Dummy variables ๐‘ข ๐‘ฃ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgseisen.1 . . 3 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
2 lgseisen.2 . . 3 (๐œ‘ โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
3 lgseisen.3 . . 3 (๐œ‘ โ†’ ๐‘ƒ โ‰  ๐‘„)
41, 2, 3lgseisen 26730 . 2 (๐œ‘ โ†’ (๐‘„ /L ๐‘ƒ) = (-1โ†‘ฮฃ๐‘ข โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
5 lgsquad.4 . . . . . 6 ๐‘€ = ((๐‘ƒ โˆ’ 1) / 2)
65oveq2i 7369 . . . . 5 (1...๐‘€) = (1...((๐‘ƒ โˆ’ 1) / 2))
76sumeq1i 15584 . . . 4 ฮฃ๐‘ข โˆˆ (1...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = ฮฃ๐‘ข โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))
81, 5gausslemma2dlem0b 26708 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
98nnred 12169 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
109rehalfcld 12401 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ / 2) โˆˆ โ„)
1110flcld 13704 . . . . . . . 8 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„ค)
1211zred 12608 . . . . . . 7 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„)
1312ltp1d 12086 . . . . . 6 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) < ((โŒŠโ€˜(๐‘€ / 2)) + 1))
14 fzdisj 13469 . . . . . 6 ((โŒŠโ€˜(๐‘€ / 2)) < ((โŒŠโ€˜(๐‘€ / 2)) + 1) โ†’ ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆฉ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)) = โˆ…)
1513, 14syl 17 . . . . 5 (๐œ‘ โ†’ ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆฉ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)) = โˆ…)
168nnrpd 12956 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„+)
1716rphalfcld 12970 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘€ / 2) โˆˆ โ„+)
1817rpge0d 12962 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (๐‘€ / 2))
19 flge0nn0 13726 . . . . . . . . 9 (((๐‘€ / 2) โˆˆ โ„ โˆง 0 โ‰ค (๐‘€ / 2)) โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„•0)
2010, 18, 19syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„•0)
218nnnn0d 12474 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
22 rphalflt 12945 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„+ โ†’ (๐‘€ / 2) < ๐‘€)
2316, 22syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘€ / 2) < ๐‘€)
248nnzd 12527 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
25 fllt 13712 . . . . . . . . . . 11 (((๐‘€ / 2) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘€ / 2) < ๐‘€ โ†” (โŒŠโ€˜(๐‘€ / 2)) < ๐‘€))
2610, 24, 25syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€ / 2) < ๐‘€ โ†” (โŒŠโ€˜(๐‘€ / 2)) < ๐‘€))
2723, 26mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) < ๐‘€)
2812, 9, 27ltled 11304 . . . . . . . 8 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) โ‰ค ๐‘€)
29 elfz2nn0 13533 . . . . . . . 8 ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ (0...๐‘€) โ†” ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„•0 โˆง ๐‘€ โˆˆ โ„•0 โˆง (โŒŠโ€˜(๐‘€ / 2)) โ‰ค ๐‘€))
3020, 21, 28, 29syl3anbrc 1344 . . . . . . 7 (๐œ‘ โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ (0...๐‘€))
31 nn0uz 12806 . . . . . . . . 9 โ„•0 = (โ„คโ‰ฅโ€˜0)
3221, 31eleqtrdi 2848 . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜0))
33 elfzp12 13521 . . . . . . . 8 (๐‘€ โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ (0...๐‘€) โ†” ((โŒŠโ€˜(๐‘€ / 2)) = 0 โˆจ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ ((0 + 1)...๐‘€))))
3432, 33syl 17 . . . . . . 7 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ (0...๐‘€) โ†” ((โŒŠโ€˜(๐‘€ / 2)) = 0 โˆจ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ ((0 + 1)...๐‘€))))
3530, 34mpbid 231 . . . . . 6 (๐œ‘ โ†’ ((โŒŠโ€˜(๐‘€ / 2)) = 0 โˆจ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ ((0 + 1)...๐‘€)))
36 un0 4351 . . . . . . . . 9 ((1...๐‘€) โˆช โˆ…) = (1...๐‘€)
37 uncom 4114 . . . . . . . . 9 ((1...๐‘€) โˆช โˆ…) = (โˆ… โˆช (1...๐‘€))
3836, 37eqtr3i 2767 . . . . . . . 8 (1...๐‘€) = (โˆ… โˆช (1...๐‘€))
39 oveq2 7366 . . . . . . . . . 10 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ (1...(โŒŠโ€˜(๐‘€ / 2))) = (1...0))
40 fz10 13463 . . . . . . . . . 10 (1...0) = โˆ…
4139, 40eqtrdi 2793 . . . . . . . . 9 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ (1...(โŒŠโ€˜(๐‘€ / 2))) = โˆ…)
42 oveq1 7365 . . . . . . . . . . 11 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ ((โŒŠโ€˜(๐‘€ / 2)) + 1) = (0 + 1))
43 0p1e1 12276 . . . . . . . . . . 11 (0 + 1) = 1
4442, 43eqtrdi 2793 . . . . . . . . . 10 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ ((โŒŠโ€˜(๐‘€ / 2)) + 1) = 1)
4544oveq1d 7373 . . . . . . . . 9 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€) = (1...๐‘€))
4641, 45uneq12d 4125 . . . . . . . 8 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)) = (โˆ… โˆช (1...๐‘€)))
4738, 46eqtr4id 2796 . . . . . . 7 ((โŒŠโ€˜(๐‘€ / 2)) = 0 โ†’ (1...๐‘€) = ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)))
48 fzsplit 13468 . . . . . . . 8 ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ (1...๐‘€) โ†’ (1...๐‘€) = ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)))
4943oveq1i 7368 . . . . . . . 8 ((0 + 1)...๐‘€) = (1...๐‘€)
5048, 49eleq2s 2856 . . . . . . 7 ((โŒŠโ€˜(๐‘€ / 2)) โˆˆ ((0 + 1)...๐‘€) โ†’ (1...๐‘€) = ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)))
5147, 50jaoi 856 . . . . . 6 (((โŒŠโ€˜(๐‘€ / 2)) = 0 โˆจ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ ((0 + 1)...๐‘€)) โ†’ (1...๐‘€) = ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)))
5235, 51syl 17 . . . . 5 (๐œ‘ โ†’ (1...๐‘€) = ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)))
53 fzfid 13879 . . . . 5 (๐œ‘ โ†’ (1...๐‘€) โˆˆ Fin)
542gausslemma2dlem0a 26707 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„•)
5554nnred 12169 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„)
561gausslemma2dlem0a 26707 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
5755, 56nndivred 12208 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘„ / ๐‘ƒ) โˆˆ โ„)
5857adantr 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (๐‘„ / ๐‘ƒ) โˆˆ โ„)
59 2nn 12227 . . . . . . . . . 10 2 โˆˆ โ„•
60 elfznn 13471 . . . . . . . . . . 11 (๐‘ข โˆˆ (1...๐‘€) โ†’ ๐‘ข โˆˆ โ„•)
6160adantl 483 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ ๐‘ข โˆˆ โ„•)
62 nnmulcl 12178 . . . . . . . . . 10 ((2 โˆˆ โ„• โˆง ๐‘ข โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โˆˆ โ„•)
6359, 61, 62sylancr 588 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (2 ยท ๐‘ข) โˆˆ โ„•)
6463nnred 12169 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (2 ยท ๐‘ข) โˆˆ โ„)
6558, 64remulcld 11186 . . . . . . 7 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โˆˆ โ„)
6654nnrpd 12956 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„+)
6756nnrpd 12956 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„+)
6866, 67rpdivcld 12975 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘„ / ๐‘ƒ) โˆˆ โ„+)
6968adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (๐‘„ / ๐‘ƒ) โˆˆ โ„+)
7063nnrpd 12956 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (2 ยท ๐‘ข) โˆˆ โ„+)
7169, 70rpmulcld 12974 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โˆˆ โ„+)
7271rpge0d 12962 . . . . . . 7 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ 0 โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))
73 flge0nn0 13726 . . . . . . 7 ((((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โˆˆ โ„ โˆง 0 โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
7465, 72, 73syl2anc 585 . . . . . 6 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
7574nn0cnd 12476 . . . . 5 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...๐‘€)) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„‚)
7615, 52, 53, 75fsumsplit 15627 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (1...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = (ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) + ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
777, 76eqtr3id 2791 . . 3 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = (ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) + ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
7877oveq2d 7374 . 2 (๐œ‘ โ†’ (-1โ†‘ฮฃ๐‘ข โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) = (-1โ†‘(ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) + ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
79 neg1cn 12268 . . . . 5 -1 โˆˆ โ„‚
8079a1i 11 . . . 4 (๐œ‘ โ†’ -1 โˆˆ โ„‚)
81 fzfid 13879 . . . . 5 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€) โˆˆ Fin)
82 ssun2 4134 . . . . . . . 8 (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€) โŠ† ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€))
8382, 52sseqtrrid 3998 . . . . . . 7 (๐œ‘ โ†’ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€) โŠ† (1...๐‘€))
8483sselda 3945 . . . . . 6 ((๐œ‘ โˆง ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)) โ†’ ๐‘ข โˆˆ (1...๐‘€))
8584, 74syldan 592 . . . . 5 ((๐œ‘ โˆง ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
8681, 85fsumnn0cl 15622 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
87 fzfid 13879 . . . . 5 (๐œ‘ โ†’ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆˆ Fin)
88 ssun1 4133 . . . . . . . 8 (1...(โŒŠโ€˜(๐‘€ / 2))) โŠ† ((1...(โŒŠโ€˜(๐‘€ / 2))) โˆช (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€))
8988, 52sseqtrrid 3998 . . . . . . 7 (๐œ‘ โ†’ (1...(โŒŠโ€˜(๐‘€ / 2))) โŠ† (1...๐‘€))
9089sselda 3945 . . . . . 6 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โˆˆ (1...๐‘€))
9190, 74syldan 592 . . . . 5 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
9287, 91fsumnn0cl 15622 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0)
9380, 86, 92expaddd 14054 . . 3 (๐œ‘ โ†’ (-1โ†‘(ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) + ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = ((-1โ†‘ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) ยท (-1โ†‘ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
94 fzfid 13879 . . . . . . . . 9 (๐œ‘ โ†’ (1...๐‘) โˆˆ Fin)
95 xpfi 9262 . . . . . . . . 9 (((1...๐‘€) โˆˆ Fin โˆง (1...๐‘) โˆˆ Fin) โ†’ ((1...๐‘€) ร— (1...๐‘)) โˆˆ Fin)
9653, 94, 95syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ ((1...๐‘€) ร— (1...๐‘)) โˆˆ Fin)
97 lgsquad.6 . . . . . . . . 9 ๐‘† = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„))}
98 opabssxp 5725 . . . . . . . . 9 {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„))} โŠ† ((1...๐‘€) ร— (1...๐‘))
9997, 98eqsstri 3979 . . . . . . . 8 ๐‘† โŠ† ((1...๐‘€) ร— (1...๐‘))
100 ssfi 9118 . . . . . . . 8 ((((1...๐‘€) ร— (1...๐‘)) โˆˆ Fin โˆง ๐‘† โŠ† ((1...๐‘€) ร— (1...๐‘))) โ†’ ๐‘† โˆˆ Fin)
10196, 99, 100sylancl 587 . . . . . . 7 (๐œ‘ โ†’ ๐‘† โˆˆ Fin)
102 ssrab2 4038 . . . . . . 7 {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โŠ† ๐‘†
103 ssfi 9118 . . . . . . 7 ((๐‘† โˆˆ Fin โˆง {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โŠ† ๐‘†) โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin)
104101, 102, 103sylancl 587 . . . . . 6 (๐œ‘ โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin)
105 hashcl 14257 . . . . . 6 ({๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) โˆˆ โ„•0)
106104, 105syl 17 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) โˆˆ โ„•0)
107 ssrab2 4038 . . . . . . 7 {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โŠ† ๐‘†
108 ssfi 9118 . . . . . . 7 ((๐‘† โˆˆ Fin โˆง {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โŠ† ๐‘†) โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin)
109101, 107, 108sylancl 587 . . . . . 6 (๐œ‘ โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin)
110 hashcl 14257 . . . . . 6 ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin โ†’ (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) โˆˆ โ„•0)
111109, 110syl 17 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) โˆˆ โ„•0)
11280, 106, 111expaddd 14054 . . . 4 (๐œ‘ โ†’ (-1โ†‘((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}))) = ((-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)})) ยท (-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}))))
11390, 63syldan 592 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (2 ยท ๐‘ข) โˆˆ โ„•)
114 fzfid 13879 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โˆˆ Fin)
115 xpsnen2g 9010 . . . . . . . . . . 11 (((2 ยท ๐‘ข) โˆˆ โ„• โˆง (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โˆˆ Fin) โ†’ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ‰ˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
116113, 114, 115syl2anc 585 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ‰ˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
117 hasheni 14249 . . . . . . . . . 10 (({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ‰ˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โ†’ (โ™ฏโ€˜({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))) = (โ™ฏโ€˜(1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
118116, 117syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โ™ฏโ€˜({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))) = (โ™ฏโ€˜(1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
119 ssrab2 4038 . . . . . . . . . . . . 13 {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โŠ† ๐‘†
12097relopabiv 5777 . . . . . . . . . . . . 13 Rel ๐‘†
121 relss 5738 . . . . . . . . . . . . 13 ({๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โŠ† ๐‘† โ†’ (Rel ๐‘† โ†’ Rel {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}))
122119, 120, 121mp2 9 . . . . . . . . . . . 12 Rel {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}
123 relxp 5652 . . . . . . . . . . . 12 Rel ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
12497eleq2i 2830 . . . . . . . . . . . . . . . 16 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘† โ†” โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„))})
125 opabidw 5482 . . . . . . . . . . . . . . . 16 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„))} โ†” ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„)))
126124, 125bitri 275 . . . . . . . . . . . . . . 15 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘† โ†” ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„)))
127 anass 470 . . . . . . . . . . . . . . . . . 18 (((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข))) โ†” (๐‘ฆ โˆˆ โ„• โˆง (๐‘ฆ โ‰ค ๐‘ โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)))))
128113adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โˆˆ โ„•)
129128nnred 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โˆˆ โ„)
13056ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„•)
131130nnred 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„)
132131rehalfcld 12401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ / 2) โˆˆ โ„)
1339adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘€ โˆˆ โ„)
134133adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
135 elfzle2 13446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โ†’ ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2)))
136135adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2)))
137133rehalfcld 12401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (๐‘€ / 2) โˆˆ โ„)
138 elfzelz 13442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โ†’ ๐‘ข โˆˆ โ„ค)
139138adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โˆˆ โ„ค)
140 flge 13711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((๐‘€ / 2) โˆˆ โ„ โˆง ๐‘ข โˆˆ โ„ค) โ†’ (๐‘ข โ‰ค (๐‘€ / 2) โ†” ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2))))
141137, 139, 140syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (๐‘ข โ‰ค (๐‘€ / 2) โ†” ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2))))
142136, 141mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โ‰ค (๐‘€ / 2))
143 elfznn 13471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โ†’ ๐‘ข โˆˆ โ„•)
144143adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โˆˆ โ„•)
145144nnred 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โˆˆ โ„)
146 2re 12228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 โˆˆ โ„
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ 2 โˆˆ โ„)
148 2pos 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 < 2
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ 0 < 2)
150 lemuldiv2 12037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐‘ข โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท ๐‘ข) โ‰ค ๐‘€ โ†” ๐‘ข โ‰ค (๐‘€ / 2)))
151145, 133, 147, 149, 150syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((2 ยท ๐‘ข) โ‰ค ๐‘€ โ†” ๐‘ข โ‰ค (๐‘€ / 2)))
152142, 151mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (2 ยท ๐‘ข) โ‰ค ๐‘€)
153152adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โ‰ค ๐‘€)
154131ltm1d 12088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ โˆ’ 1) < ๐‘ƒ)
155 peano2rem 11469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
156131, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
157146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 2 โˆˆ โ„)
158148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 0 < 2)
159 ltdiv1 12020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((๐‘ƒ โˆ’ 1) < ๐‘ƒ โ†” ((๐‘ƒ โˆ’ 1) / 2) < (๐‘ƒ / 2)))
160156, 131, 157, 158, 159syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ƒ โˆ’ 1) < ๐‘ƒ โ†” ((๐‘ƒ โˆ’ 1) / 2) < (๐‘ƒ / 2)))
161154, 160mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ƒ โˆ’ 1) / 2) < (๐‘ƒ / 2))
1625, 161eqbrtrid 5141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘€ < (๐‘ƒ / 2))
163129, 134, 132, 153, 162lelttrd 11314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) < (๐‘ƒ / 2))
164130nnrpd 12956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„+)
165 rphalflt 12945 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„+ โ†’ (๐‘ƒ / 2) < ๐‘ƒ)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ / 2) < ๐‘ƒ)
167129, 132, 131, 163, 166lttrd 11317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) < ๐‘ƒ)
168129, 131ltnled 11303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((2 ยท ๐‘ข) < ๐‘ƒ โ†” ยฌ ๐‘ƒ โ‰ค (2 ยท ๐‘ข)))
169167, 168mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ยฌ ๐‘ƒ โ‰ค (2 ยท ๐‘ข))
1701eldifad 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
171170ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„™)
172 prmz 16552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„ค)
174 dvdsle 16193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ƒ โˆˆ โ„ค โˆง (2 ยท ๐‘ข) โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (2 ยท ๐‘ข) โ†’ ๐‘ƒ โ‰ค (2 ยท ๐‘ข)))
175173, 128, 174syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (2 ยท ๐‘ข) โ†’ ๐‘ƒ โ‰ค (2 ยท ๐‘ข)))
176169, 175mtod 197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ยฌ ๐‘ƒ โˆฅ (2 ยท ๐‘ข))
1772eldifad 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„™)
178 prmrp 16589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘„ โˆˆ โ„™) โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
179170, 177, 178syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
1803, 179mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐‘ƒ gcd ๐‘„) = 1)
181180ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ gcd ๐‘„) = 1)
182177ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘„ โˆˆ โ„™)
183 prmz 16552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘„ โˆˆ โ„™ โ†’ ๐‘„ โˆˆ โ„ค)
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘„ โˆˆ โ„ค)
185128nnzd 12527 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โˆˆ โ„ค)
186 coprmdvds 16530 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ƒ โˆˆ โ„ค โˆง ๐‘„ โˆˆ โ„ค โˆง (2 ยท ๐‘ข) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (2 ยท ๐‘ข)))
187173, 184, 185, 186syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (2 ยท ๐‘ข)))
188181, 187mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ ๐‘ƒ โˆฅ (2 ยท ๐‘ข)))
189176, 188mtod 197 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)))
190 nnz 12521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„ค)
191190adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ฆ โˆˆ โ„ค)
192 dvdsmul2 16162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ ๐‘ƒ โˆฅ (๐‘ฆ ยท ๐‘ƒ))
193191, 173, 192syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆฅ (๐‘ฆ ยท ๐‘ƒ))
194 breq2 5110 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘„ ยท (2 ยท ๐‘ข)) = (๐‘ฆ ยท ๐‘ƒ) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)) โ†” ๐‘ƒ โˆฅ (๐‘ฆ ยท ๐‘ƒ)))
195193, 194syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ ยท (2 ยท ๐‘ข)) = (๐‘ฆ ยท ๐‘ƒ) โ†’ ๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข))))
196195necon3bd 2958 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (ยฌ ๐‘ƒ โˆฅ (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) โ‰  (๐‘ฆ ยท ๐‘ƒ)))
197189, 196mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) โ‰  (๐‘ฆ ยท ๐‘ƒ))
198 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ฆ โˆˆ โ„•)
199198, 130nnmulcld 12207 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ ยท ๐‘ƒ) โˆˆ โ„•)
200199nnred 12169 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ ยท ๐‘ƒ) โˆˆ โ„)
20154adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘„ โˆˆ โ„•)
202201, 113nnmulcld 12207 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) โˆˆ โ„•)
203202adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) โˆˆ โ„•)
204203nnred 12169 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) โˆˆ โ„)
205200, 204ltlend 11301 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†” ((๐‘ฆ ยท ๐‘ƒ) โ‰ค (๐‘„ ยท (2 ยท ๐‘ข)) โˆง (๐‘„ ยท (2 ยท ๐‘ข)) โ‰  (๐‘ฆ ยท ๐‘ƒ))))
206197, 205mpbiran2d 707 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†” (๐‘ฆ ยท ๐‘ƒ) โ‰ค (๐‘„ ยท (2 ยท ๐‘ข))))
207 nnre 12161 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„)
208207adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ฆ โˆˆ โ„)
209130nngt0d 12203 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 0 < ๐‘ƒ)
210 lemuldiv 12036 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฆ โˆˆ โ„ โˆง (๐‘„ ยท (2 ยท ๐‘ข)) โˆˆ โ„ โˆง (๐‘ƒ โˆˆ โ„ โˆง 0 < ๐‘ƒ)) โ†’ ((๐‘ฆ ยท ๐‘ƒ) โ‰ค (๐‘„ ยท (2 ยท ๐‘ข)) โ†” ๐‘ฆ โ‰ค ((๐‘„ ยท (2 ยท ๐‘ข)) / ๐‘ƒ)))
211208, 204, 131, 209, 210syl112anc 1375 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) โ‰ค (๐‘„ ยท (2 ยท ๐‘ข)) โ†” ๐‘ฆ โ‰ค ((๐‘„ ยท (2 ยท ๐‘ข)) / ๐‘ƒ)))
212201adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘„ โˆˆ โ„•)
213212nncnd 12170 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘„ โˆˆ โ„‚)
214128nncnd 12170 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ข) โˆˆ โ„‚)
215130nncnd 12170 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„‚)
216130nnne0d 12204 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ƒ โ‰  0)
217213, 214, 215, 216div23d 11969 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ ยท (2 ยท ๐‘ข)) / ๐‘ƒ) = ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))
218217breq2d 5118 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ((๐‘„ ยท (2 ยท ๐‘ข)) / ๐‘ƒ) โ†” ๐‘ฆ โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))
219206, 211, 2183bitrd 305 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†” ๐‘ฆ โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))
220212nnred 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘„ โˆˆ โ„)
221212nngt0d 12203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 0 < ๐‘„)
222 ltmul2 12007 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 ยท ๐‘ข) โˆˆ โ„ โˆง (๐‘ƒ / 2) โˆˆ โ„ โˆง (๐‘„ โˆˆ โ„ โˆง 0 < ๐‘„)) โ†’ ((2 ยท ๐‘ข) < (๐‘ƒ / 2) โ†” (๐‘„ ยท (2 ยท ๐‘ข)) < (๐‘„ ยท (๐‘ƒ / 2))))
223129, 132, 220, 221, 222syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((2 ยท ๐‘ข) < (๐‘ƒ / 2) โ†” (๐‘„ ยท (2 ยท ๐‘ข)) < (๐‘„ ยท (๐‘ƒ / 2))))
224163, 223mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) < (๐‘„ ยท (๐‘ƒ / 2)))
225 2cnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 2 โˆˆ โ„‚)
226 2ne0 12258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 โ‰  0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 2 โ‰  0)
228 divass 11832 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘„ โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ ((๐‘„ ยท ๐‘ƒ) / 2) = (๐‘„ ยท (๐‘ƒ / 2)))
229 div23 11833 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘„ โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ ((๐‘„ ยท ๐‘ƒ) / 2) = ((๐‘„ / 2) ยท ๐‘ƒ))
230228, 229eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘„ โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (๐‘„ ยท (๐‘ƒ / 2)) = ((๐‘„ / 2) ยท ๐‘ƒ))
231213, 215, 225, 227, 230syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (๐‘ƒ / 2)) = ((๐‘„ / 2) ยท ๐‘ƒ))
232224, 231breqtrd 5132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ ยท (2 ยท ๐‘ข)) < ((๐‘„ / 2) ยท ๐‘ƒ))
233220rehalfcld 12401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ / 2) โˆˆ โ„)
234233, 131remulcld 11186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ / 2) ยท ๐‘ƒ) โˆˆ โ„)
235 lttr 11232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐‘ฆ ยท ๐‘ƒ) โˆˆ โ„ โˆง (๐‘„ ยท (2 ยท ๐‘ข)) โˆˆ โ„ โˆง ((๐‘„ / 2) ยท ๐‘ƒ) โˆˆ โ„) โ†’ (((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โˆง (๐‘„ ยท (2 ยท ๐‘ข)) < ((๐‘„ / 2) ยท ๐‘ƒ)) โ†’ (๐‘ฆ ยท ๐‘ƒ) < ((๐‘„ / 2) ยท ๐‘ƒ)))
236200, 204, 234, 235syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โˆง (๐‘„ ยท (2 ยท ๐‘ข)) < ((๐‘„ / 2) ยท ๐‘ƒ)) โ†’ (๐‘ฆ ยท ๐‘ƒ) < ((๐‘„ / 2) ยท ๐‘ƒ)))
237232, 236mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ (๐‘ฆ ยท ๐‘ƒ) < ((๐‘„ / 2) ยท ๐‘ƒ)))
238 ltmul1 12006 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ โ„ โˆง (๐‘„ / 2) โˆˆ โ„ โˆง (๐‘ƒ โˆˆ โ„ โˆง 0 < ๐‘ƒ)) โ†’ (๐‘ฆ < (๐‘„ / 2) โ†” (๐‘ฆ ยท ๐‘ƒ) < ((๐‘„ / 2) ยท ๐‘ƒ)))
239208, 233, 131, 209, 238syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ < (๐‘„ / 2) โ†” (๐‘ฆ ยท ๐‘ƒ) < ((๐‘„ / 2) ยท ๐‘ƒ)))
240237, 239sylibrd 259 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ ๐‘ฆ < (๐‘„ / 2)))
241 peano2rem 11469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘„ โˆˆ โ„ โ†’ (๐‘„ โˆ’ 1) โˆˆ โ„)
242220, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ โˆ’ 1) โˆˆ โ„)
243242recnd 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ โˆ’ 1) โˆˆ โ„‚)
244213, 243, 225, 227divsubdird 11971 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ โˆ’ (๐‘„ โˆ’ 1)) / 2) = ((๐‘„ / 2) โˆ’ ((๐‘„ โˆ’ 1) / 2)))
245 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ๐‘ = ((๐‘„ โˆ’ 1) / 2)
246245oveq2i 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘„ / 2) โˆ’ ๐‘) = ((๐‘„ / 2) โˆ’ ((๐‘„ โˆ’ 1) / 2))
247244, 246eqtr4di 2795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ โˆ’ (๐‘„ โˆ’ 1)) / 2) = ((๐‘„ / 2) โˆ’ ๐‘))
248 ax-1cn 11110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 โˆˆ โ„‚
249 nncan 11431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐‘„ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (๐‘„ โˆ’ (๐‘„ โˆ’ 1)) = 1)
250213, 248, 249sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ โˆ’ (๐‘„ โˆ’ 1)) = 1)
251250oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ โˆ’ (๐‘„ โˆ’ 1)) / 2) = (1 / 2))
252 halflt1 12372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
253251, 252eqbrtrdi 5145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ โˆ’ (๐‘„ โˆ’ 1)) / 2) < 1)
254247, 253eqbrtrrd 5130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘„ / 2) โˆ’ ๐‘) < 1)
2552, 245gausslemma2dlem0b 26708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
256255ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„•)
257256nnred 12169 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„)
258 1red 11157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ 1 โˆˆ โ„)
259233, 257, 258ltsubadd2d 11754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (((๐‘„ / 2) โˆ’ ๐‘) < 1 โ†” (๐‘„ / 2) < (๐‘ + 1)))
260254, 259mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘„ / 2) < (๐‘ + 1))
261 peano2re 11329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ โˆˆ โ„ โ†’ (๐‘ + 1) โˆˆ โ„)
262257, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ + 1) โˆˆ โ„)
263 lttr 11232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ โ„ โˆง (๐‘„ / 2) โˆˆ โ„ โˆง (๐‘ + 1) โˆˆ โ„) โ†’ ((๐‘ฆ < (๐‘„ / 2) โˆง (๐‘„ / 2) < (๐‘ + 1)) โ†’ ๐‘ฆ < (๐‘ + 1)))
264208, 233, 262, 263syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ < (๐‘„ / 2) โˆง (๐‘„ / 2) < (๐‘ + 1)) โ†’ ๐‘ฆ < (๐‘ + 1)))
265260, 264mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ < (๐‘„ / 2) โ†’ ๐‘ฆ < (๐‘ + 1)))
266240, 265syld 47 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ ๐‘ฆ < (๐‘ + 1)))
267 nnleltp1 12559 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ๐‘ โ†” ๐‘ฆ < (๐‘ + 1)))
268198, 256, 267syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ๐‘ โ†” ๐‘ฆ < (๐‘ + 1)))
269266, 268sylibrd 259 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†’ ๐‘ฆ โ‰ค ๐‘))
270269pm4.71rd 564 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)) โ†” (๐‘ฆ โ‰ค ๐‘ โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)))))
27190, 65syldan 592 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โˆˆ โ„)
272 flge 13711 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘ฆ โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โ†” ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
273271, 190, 272syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)) โ†” ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
274219, 270, 2733bitr3d 309 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฆ โˆˆ โ„•) โ†’ ((๐‘ฆ โ‰ค ๐‘ โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข))) โ†” ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))
275274pm5.32da 580 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง (๐‘ฆ โ‰ค ๐‘ โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
276127, 275bitrid 283 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
277276adantr 482 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
278 simpr 486 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ ๐‘ฅ = (2 ยท ๐‘ข))
279 nnuz 12807 . . . . . . . . . . . . . . . . . . . . . . . 24 โ„• = (โ„คโ‰ฅโ€˜1)
280113, 279eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (2 ยท ๐‘ข) โˆˆ (โ„คโ‰ฅโ€˜1))
28124adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘€ โˆˆ โ„ค)
282 elfz5 13434 . . . . . . . . . . . . . . . . . . . . . . 23 (((2 ยท ๐‘ข) โˆˆ (โ„คโ‰ฅโ€˜1) โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ข) โˆˆ (1...๐‘€) โ†” (2 ยท ๐‘ข) โ‰ค ๐‘€))
283280, 281, 282syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((2 ยท ๐‘ข) โˆˆ (1...๐‘€) โ†” (2 ยท ๐‘ข) โ‰ค ๐‘€))
284152, 283mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (2 ยท ๐‘ข) โˆˆ (1...๐‘€))
285284adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (2 ยท ๐‘ข) โˆˆ (1...๐‘€))
286278, 285eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ ๐‘ฅ โˆˆ (1...๐‘€))
287286biantrurd 534 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (๐‘ฆ โˆˆ (1...๐‘) โ†” (๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘))))
288255nnzd 12527 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
289288ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ ๐‘ โˆˆ โ„ค)
290 fznn 13510 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ โ„ค โ†’ (๐‘ฆ โˆˆ (1...๐‘) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘)))
291289, 290syl 17 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (๐‘ฆ โˆˆ (1...๐‘) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘)))
292287, 291bitr3d 281 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ ((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘)))
293 oveq1 7365 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = (2 ยท ๐‘ข) โ†’ (๐‘ฅ ยท ๐‘„) = ((2 ยท ๐‘ข) ยท ๐‘„))
294113nncnd 12170 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (2 ยท ๐‘ข) โˆˆ โ„‚)
295201nncnd 12170 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘„ โˆˆ โ„‚)
296294, 295mulcomd 11177 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((2 ยท ๐‘ข) ยท ๐‘„) = (๐‘„ ยท (2 ยท ๐‘ข)))
297293, 296sylan9eqr 2799 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (๐‘ฅ ยท ๐‘„) = (๐‘„ ยท (2 ยท ๐‘ข)))
298297breq2d 5118 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ ((๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„) โ†” (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข))))
299292, 298anbi12d 632 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„)) โ†” ((๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐‘) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘„ ยท (2 ยท ๐‘ข)))))
300271flcld 13704 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„ค)
301 fznn 13510 . . . . . . . . . . . . . . . . . 18 ((โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„ค โ†’ (๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
302300, 301syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
303302adantr 482 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐‘ฆ โ‰ค (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
304277, 299, 3033bitr4d 311 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (((๐‘ฅ โˆˆ (1...๐‘€) โˆง ๐‘ฆ โˆˆ (1...๐‘)) โˆง (๐‘ฆ ยท ๐‘ƒ) < (๐‘ฅ ยท ๐‘„)) โ†” ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
305126, 304bitrid 283 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โˆง ๐‘ฅ = (2 ยท ๐‘ข)) โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘† โ†” ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
306305pm5.32da 580 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ((๐‘ฅ = (2 ยท ๐‘ข) โˆง โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘†) โ†” (๐‘ฅ = (2 ยท ๐‘ข) โˆง ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))))
307 vex 3450 . . . . . . . . . . . . . . . . . 18 ๐‘ฅ โˆˆ V
308 vex 3450 . . . . . . . . . . . . . . . . . 18 ๐‘ฆ โˆˆ V
309307, 308op1std 7932 . . . . . . . . . . . . . . . . 17 (๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†’ (1st โ€˜๐‘ง) = ๐‘ฅ)
310309eqeq2d 2748 . . . . . . . . . . . . . . . 16 (๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†’ ((2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” (2 ยท ๐‘ข) = ๐‘ฅ))
311 eqcom 2744 . . . . . . . . . . . . . . . 16 ((2 ยท ๐‘ข) = ๐‘ฅ โ†” ๐‘ฅ = (2 ยท ๐‘ข))
312310, 311bitrdi 287 . . . . . . . . . . . . . . 15 (๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†’ ((2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” ๐‘ฅ = (2 ยท ๐‘ข)))
313312elrab 3646 . . . . . . . . . . . . . 14 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โ†” (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘† โˆง ๐‘ฅ = (2 ยท ๐‘ข)))
314313biancomi 464 . . . . . . . . . . . . 13 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โ†” (๐‘ฅ = (2 ยท ๐‘ข) โˆง โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐‘†))
315 opelxp 5670 . . . . . . . . . . . . . 14 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ†” (๐‘ฅ โˆˆ {(2 ยท ๐‘ข)} โˆง ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
316 velsn 4603 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ {(2 ยท ๐‘ข)} โ†” ๐‘ฅ = (2 ยท ๐‘ข))
317316anbi1i 625 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆˆ {(2 ยท ๐‘ข)} โˆง ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ†” (๐‘ฅ = (2 ยท ๐‘ข) โˆง ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
318315, 317bitri 275 . . . . . . . . . . . . 13 (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) โ†” (๐‘ฅ = (2 ยท ๐‘ข) โˆง ๐‘ฆ โˆˆ (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
319306, 314, 3183bitr4g 314 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โ†” โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))))
320122, 123, 319eqrelrdv 5749 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} = ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
321320eqcomd 2743 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})
322321fveq2d 6847 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โ™ฏโ€˜({(2 ยท ๐‘ข)} ร— (1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))))) = (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}))
323 hashfz1 14247 . . . . . . . . . 10 ((โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))
32491, 323syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โ™ฏโ€˜(1...(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))
325118, 322, 3243eqtr3rd 2786 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ (โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}))
326325sumeq2dv 15589 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}))
327101adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘† โˆˆ Fin)
328 ssfi 9118 . . . . . . . . 9 ((๐‘† โˆˆ Fin โˆง {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โŠ† ๐‘†) โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โˆˆ Fin)
329327, 119, 328sylancl 587 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โˆˆ Fin)
330 fveq2 6843 . . . . . . . . . . . . . . . 16 (๐‘ง = ๐‘ฃ โ†’ (1st โ€˜๐‘ง) = (1st โ€˜๐‘ฃ))
331330eqeq2d 2748 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘ฃ โ†’ ((2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” (2 ยท ๐‘ข) = (1st โ€˜๐‘ฃ)))
332331elrab 3646 . . . . . . . . . . . . . 14 (๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โ†” (๐‘ฃ โˆˆ ๐‘† โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ฃ)))
333332simprbi 498 . . . . . . . . . . . . 13 (๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} โ†’ (2 ยท ๐‘ข) = (1st โ€˜๐‘ฃ))
334333ad2antll 728 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ (2 ยท ๐‘ข) = (1st โ€˜๐‘ฃ))
335334oveq1d 7373 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ ((2 ยท ๐‘ข) / 2) = ((1st โ€˜๐‘ฃ) / 2))
336144nncnd 12170 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))) โ†’ ๐‘ข โˆˆ โ„‚)
337336adantrr 716 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ ๐‘ข โˆˆ โ„‚)
338 2cnd 12232 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ 2 โˆˆ โ„‚)
339226a1i 11 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ 2 โ‰  0)
340337, 338, 339divcan3d 11937 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ ((2 ยท ๐‘ข) / 2) = ๐‘ข)
341335, 340eqtr3d 2779 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง ๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})) โ†’ ((1st โ€˜๐‘ฃ) / 2) = ๐‘ข)
342341ralrimivva 3198 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))โˆ€๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} ((1st โ€˜๐‘ฃ) / 2) = ๐‘ข)
343 invdisj 5090 . . . . . . . . 9 (โˆ€๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))โˆ€๐‘ฃ โˆˆ {๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} ((1st โ€˜๐‘ฃ) / 2) = ๐‘ข โ†’ Disj ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})
344342, 343syl 17 . . . . . . . 8 (๐œ‘ โ†’ Disj ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)})
34587, 329, 344hashiun 15708 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}) = ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}))
346 iunrab 5013 . . . . . . . . 9 โˆช ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} = {๐‘ง โˆˆ ๐‘† โˆฃ โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}
347 2cn 12229 . . . . . . . . . . . . . 14 2 โˆˆ โ„‚
348 zcn 12505 . . . . . . . . . . . . . . 15 (๐‘ข โˆˆ โ„ค โ†’ ๐‘ข โˆˆ โ„‚)
349348adantl 483 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง ๐‘ข โˆˆ โ„ค) โ†’ ๐‘ข โˆˆ โ„‚)
350 mulcom 11138 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„‚ โˆง ๐‘ข โˆˆ โ„‚) โ†’ (2 ยท ๐‘ข) = (๐‘ข ยท 2))
351347, 349, 350sylancr 588 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง ๐‘ข โˆˆ โ„ค) โ†’ (2 ยท ๐‘ข) = (๐‘ข ยท 2))
352351eqeq1d 2739 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง ๐‘ข โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” (๐‘ข ยท 2) = (1st โ€˜๐‘ง)))
353352rexbidva 3174 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (โˆƒ๐‘ข โˆˆ โ„ค (2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” โˆƒ๐‘ข โˆˆ โ„ค (๐‘ข ยท 2) = (1st โ€˜๐‘ง)))
354138anim1i 616 . . . . . . . . . . . . 13 ((๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)) โ†’ (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)))
355354reximi2 3083 . . . . . . . . . . . 12 (โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†’ โˆƒ๐‘ข โˆˆ โ„ค (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))
356 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))
357 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ ๐‘ง โˆˆ ๐‘†)
35899, 357sselid 3943 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ ๐‘ง โˆˆ ((1...๐‘€) ร— (1...๐‘)))
359 xp1st 7954 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง โˆˆ ((1...๐‘€) ร— (1...๐‘)) โ†’ (1st โ€˜๐‘ง) โˆˆ (1...๐‘€))
360358, 359syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (1st โ€˜๐‘ง) โˆˆ (1...๐‘€))
361360adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (1st โ€˜๐‘ง) โˆˆ (1...๐‘€))
362 elfzle2 13446 . . . . . . . . . . . . . . . . . . . 20 ((1st โ€˜๐‘ง) โˆˆ (1...๐‘€) โ†’ (1st โ€˜๐‘ง) โ‰ค ๐‘€)
363361, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (1st โ€˜๐‘ง) โ‰ค ๐‘€)
364356, 363eqbrtrd 5128 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (2 ยท ๐‘ข) โ‰ค ๐‘€)
365 zre 12504 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข โˆˆ โ„ค โ†’ ๐‘ข โˆˆ โ„)
366365ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โˆˆ โ„)
3679ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘€ โˆˆ โ„)
368146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ 2 โˆˆ โ„)
369148a1i 11 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ 0 < 2)
370366, 367, 368, 369, 150syl112anc 1375 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ((2 ยท ๐‘ข) โ‰ค ๐‘€ โ†” ๐‘ข โ‰ค (๐‘€ / 2)))
371364, 370mpbid 231 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โ‰ค (๐‘€ / 2))
37210ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (๐‘€ / 2) โˆˆ โ„)
373 simprl 770 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โˆˆ โ„ค)
374372, 373, 140syl2anc 585 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (๐‘ข โ‰ค (๐‘€ / 2) โ†” ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2))))
375371, 374mpbid 231 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2)))
376 2t0e0 12323 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท 0) = 0
377 elfznn 13471 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st โ€˜๐‘ง) โˆˆ (1...๐‘€) โ†’ (1st โ€˜๐‘ง) โˆˆ โ„•)
378361, 377syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (1st โ€˜๐‘ง) โˆˆ โ„•)
379356, 378eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (2 ยท ๐‘ข) โˆˆ โ„•)
380379nngt0d 12203 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ 0 < (2 ยท ๐‘ข))
381376, 380eqbrtrid 5141 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (2 ยท 0) < (2 ยท ๐‘ข))
382 0red 11159 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ 0 โˆˆ โ„)
383 ltmul2 12007 . . . . . . . . . . . . . . . . . . . . 21 ((0 โˆˆ โ„ โˆง ๐‘ข โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ (0 < ๐‘ข โ†” (2 ยท 0) < (2 ยท ๐‘ข)))
384382, 366, 368, 369, 383syl112anc 1375 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (0 < ๐‘ข โ†” (2 ยท 0) < (2 ยท ๐‘ข)))
385381, 384mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ 0 < ๐‘ข)
386 elnnz 12510 . . . . . . . . . . . . . . . . . . 19 (๐‘ข โˆˆ โ„• โ†” (๐‘ข โˆˆ โ„ค โˆง 0 < ๐‘ข))
387373, 385, 386sylanbrc 584 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โˆˆ โ„•)
388387, 279eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โˆˆ (โ„คโ‰ฅโ€˜1))
38911ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„ค)
390 elfz5 13434 . . . . . . . . . . . . . . . . 17 ((๐‘ข โˆˆ (โ„คโ‰ฅโ€˜1) โˆง (โŒŠโ€˜(๐‘€ / 2)) โˆˆ โ„ค) โ†’ (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โ†” ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2))))
391388, 389, 390syl2anc 585 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โ†” ๐‘ข โ‰ค (โŒŠโ€˜(๐‘€ / 2))))
392375, 391mpbird 257 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))))
393392, 356jca 513 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โˆง (๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))) โ†’ (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)))
394393ex 414 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ ((๐‘ข โˆˆ โ„ค โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)) โ†’ (๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))) โˆง (2 ยท ๐‘ข) = (1st โ€˜๐‘ง))))
395394reximdv2 3162 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (โˆƒ๐‘ข โˆˆ โ„ค (2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†’ โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง)))
396355, 395impbid2 225 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” โˆƒ๐‘ข โˆˆ โ„ค (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)))
397 2z 12536 . . . . . . . . . . . 12 2 โˆˆ โ„ค
398360elfzelzd 13443 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (1st โ€˜๐‘ง) โˆˆ โ„ค)
399 divides 16139 . . . . . . . . . . . 12 ((2 โˆˆ โ„ค โˆง (1st โ€˜๐‘ง) โˆˆ โ„ค) โ†’ (2 โˆฅ (1st โ€˜๐‘ง) โ†” โˆƒ๐‘ข โˆˆ โ„ค (๐‘ข ยท 2) = (1st โ€˜๐‘ง)))
400397, 398, 399sylancr 588 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (2 โˆฅ (1st โ€˜๐‘ง) โ†” โˆƒ๐‘ข โˆˆ โ„ค (๐‘ข ยท 2) = (1st โ€˜๐‘ง)))
401353, 396, 4003bitr4d 311 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ ๐‘†) โ†’ (โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง) โ†” 2 โˆฅ (1st โ€˜๐‘ง)))
402401rabbidva 3415 . . . . . . . . 9 (๐œ‘ โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ โˆƒ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} = {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)})
403346, 402eqtrid 2789 . . . . . . . 8 (๐œ‘ โ†’ โˆช ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)} = {๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)})
404403fveq2d 6847 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜โˆช ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2))){๐‘ง โˆˆ ๐‘† โˆฃ (2 ยท ๐‘ข) = (1st โ€˜๐‘ง)}) = (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}))
405326, 345, 4043eqtr2d 2783 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) = (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}))
406405oveq2d 7374 . . . . 5 (๐œ‘ โ†’ (-1โ†‘ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) = (-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)})))
4071, 2, 3, 5, 245, 97lgsquadlem1 26731 . . . . 5 (๐œ‘ โ†’ (-1โ†‘ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) = (-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})))
408406, 407oveq12d 7376 . . . 4 (๐œ‘ โ†’ ((-1โ†‘ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) ยท (-1โ†‘ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = ((-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)})) ยท (-1โ†‘(โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}))))
409112, 408eqtr4d 2780 . . 3 (๐œ‘ โ†’ (-1โ†‘((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}))) = ((-1โ†‘ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข)))) ยท (-1โ†‘ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))))
410 inrab 4267 . . . . . . 7 ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆฉ {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) = {๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง))}
411 pm3.24 404 . . . . . . . . . 10 ยฌ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง))
412411a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง)))
413412ralrimivw 3148 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ง โˆˆ ๐‘† ยฌ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง)))
414 rabeq0 4345 . . . . . . . 8 ({๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง))} = โˆ… โ†” โˆ€๐‘ง โˆˆ ๐‘† ยฌ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง)))
415413, 414sylibr 233 . . . . . . 7 (๐œ‘ โ†’ {๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆง ยฌ 2 โˆฅ (1st โ€˜๐‘ง))} = โˆ…)
416410, 415eqtrid 2789 . . . . . 6 (๐œ‘ โ†’ ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆฉ {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) = โˆ…)
417 hashun 14283 . . . . . 6 (({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin โˆง {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)} โˆˆ Fin โˆง ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆฉ {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) = โˆ…) โ†’ (โ™ฏโ€˜({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆช {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})) = ((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})))
418109, 104, 416, 417syl3anc 1372 . . . . 5 (๐œ‘ โ†’ (โ™ฏโ€˜({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆช {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})) = ((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})))
419 unrab 4266 . . . . . . 7 ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆช {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) = {๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง))}
420 exmid 894 . . . . . . . . 9 (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง))
421420rgenw 3069 . . . . . . . 8 โˆ€๐‘ง โˆˆ ๐‘† (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง))
422 rabid2 3437 . . . . . . . 8 (๐‘† = {๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง))} โ†” โˆ€๐‘ง โˆˆ ๐‘† (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)))
423421, 422mpbir 230 . . . . . . 7 ๐‘† = {๐‘ง โˆˆ ๐‘† โˆฃ (2 โˆฅ (1st โ€˜๐‘ง) โˆจ ยฌ 2 โˆฅ (1st โ€˜๐‘ง))}
424419, 423eqtr4i 2768 . . . . . 6 ({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆช {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}) = ๐‘†
425424fveq2i 6846 . . . . 5 (โ™ฏโ€˜({๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)} โˆช {๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})) = (โ™ฏโ€˜๐‘†)
426418, 425eqtr3di 2792 . . . 4 (๐œ‘ โ†’ ((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)})) = (โ™ฏโ€˜๐‘†))
427426oveq2d 7374 . . 3 (๐œ‘ โ†’ (-1โ†‘((โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ 2 โˆฅ (1st โ€˜๐‘ง)}) + (โ™ฏโ€˜{๐‘ง โˆˆ ๐‘† โˆฃ ยฌ 2 โˆฅ (1st โ€˜๐‘ง)}))) = (-1โ†‘(โ™ฏโ€˜๐‘†)))
42893, 409, 4273eqtr2d 2783 . 2 (๐œ‘ โ†’ (-1โ†‘(ฮฃ๐‘ข โˆˆ (1...(โŒŠโ€˜(๐‘€ / 2)))(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))) + ฮฃ๐‘ข โˆˆ (((โŒŠโ€˜(๐‘€ / 2)) + 1)...๐‘€)(โŒŠโ€˜((๐‘„ / ๐‘ƒ) ยท (2 ยท ๐‘ข))))) = (-1โ†‘(โ™ฏโ€˜๐‘†)))
4294, 78, 4283eqtrd 2781 1 (๐œ‘ โ†’ (๐‘„ /L ๐‘ƒ) = (-1โ†‘(โ™ฏโ€˜๐‘†)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  โˆƒwrex 3074  {crab 3408   โˆ– cdif 3908   โˆช cun 3909   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  {csn 4587  โŸจcop 4593  โˆช ciun 4955  Disj wdisj 5071   class class class wbr 5106  {copab 5168   ร— cxp 5632  Rel wrel 5639  โ€˜cfv 6497  (class class class)co 7358  1st c1st 7920   โ‰ˆ cen 8881  Fincfn 8884  โ„‚cc 11050  โ„cr 11051  0cc0 11052  1c1 11053   + caddc 11055   ยท cmul 11057   < clt 11190   โ‰ค cle 11191   โˆ’ cmin 11386  -cneg 11387   / cdiv 11813  โ„•cn 12154  2c2 12209  โ„•0cn0 12414  โ„คcz 12500  โ„คโ‰ฅcuz 12764  โ„+crp 12916  ...cfz 13425  โŒŠcfl 13696  โ†‘cexp 13968  โ™ฏchash 14231  ฮฃcsu 15571   โˆฅ cdvds 16137   gcd cgcd 16375  โ„™cprime 16548   /L clgs 26645
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130  ax-addf 11131  ax-mulf 11132
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 3354  df-reu 3355  df-rab 3409  df-v 3448  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-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-disj 5072  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-se 5590  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-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8649  df-ec 8651  df-qs 8655  df-map 8768  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fsupp 9307  df-sup 9379  df-inf 9380  df-oi 9447  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12765  df-q 12875  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-clim 15371  df-sum 15572  df-dvds 16138  df-gcd 16376  df-prm 16549  df-phi 16639  df-pc 16710  df-struct 17020  df-sets 17037  df-slot 17055  df-ndx 17067  df-base 17085  df-ress 17114  df-plusg 17147  df-mulr 17148  df-starv 17149  df-sca 17150  df-vsca 17151  df-ip 17152  df-tset 17153  df-ple 17154  df-ds 17156  df-unif 17157  df-0g 17324  df-gsum 17325  df-imas 17391  df-qus 17392  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-mhm 18602  df-submnd 18603  df-grp 18752  df-minusg 18753  df-sbg 18754  df-mulg 18874  df-subg 18926  df-nsg 18927  df-eqg 18928  df-ghm 19007  df-cntz 19098  df-cmn 19565  df-abl 19566  df-mgp 19898  df-ur 19915  df-ring 19967  df-cring 19968  df-oppr 20050  df-dvdsr 20071  df-unit 20072  df-invr 20102  df-dvr 20113  df-rnghom 20147  df-drng 20188  df-field 20189  df-subrg 20223  df-lmod 20327  df-lss 20396  df-lsp 20436  df-sra 20636  df-rgmod 20637  df-lidl 20638  df-rsp 20639  df-2idl 20705  df-nzr 20731  df-rlreg 20756  df-domn 20757  df-idom 20758  df-cnfld 20800  df-zring 20873  df-zrh 20907  df-zn 20910  df-lgs 26646
This theorem is referenced by:  lgsquadlem3  26733
  Copyright terms: Public domain W3C validator