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

Theorem lgseisenlem2 27322
Description: Lemma for lgseisen 27325. The function ๐‘€ is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
lgseisen.2 (๐œ‘ โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
lgseisen.3 (๐œ‘ โ†’ ๐‘ƒ โ‰  ๐‘„)
lgseisen.4 ๐‘… = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ)
lgseisen.5 ๐‘€ = (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†ฆ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
lgseisen.6 ๐‘† = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ)
Assertion
Ref Expression
lgseisenlem2 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1-ontoโ†’(1...((๐‘ƒ โˆ’ 1) / 2)))
Distinct variable groups:   ๐‘ฅ,๐‘ฆ,๐‘ƒ   ๐œ‘,๐‘ฅ,๐‘ฆ   ๐‘ฆ,๐‘€   ๐‘ฅ,๐‘„,๐‘ฆ   ๐‘ฅ,๐‘†
Allowed substitution hints:   ๐‘…(๐‘ฅ,๐‘ฆ)   ๐‘†(๐‘ฆ)   ๐‘€(๐‘ฅ)

Proof of Theorem lgseisenlem2
Dummy variable ๐‘ง is distinct from all other variables.
StepHypRef Expression
1 lgseisen.1 . . . 4 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
2 lgseisen.2 . . . 4 (๐œ‘ โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
3 lgseisen.3 . . . 4 (๐œ‘ โ†’ ๐‘ƒ โ‰  ๐‘„)
4 lgseisen.4 . . . 4 ๐‘… = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ)
5 lgseisen.5 . . . 4 ๐‘€ = (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†ฆ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
61, 2, 3, 4, 5lgseisenlem1 27321 . . 3 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โŸถ(1...((๐‘ƒ โˆ’ 1) / 2)))
7 oveq2 7421 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ฆ โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘ฆ))
87oveq2d 7429 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) = (๐‘„ ยท (2 ยท ๐‘ฆ)))
98oveq1d 7428 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
10 lgseisen.6 . . . . . . . . . . . . . 14 ๐‘† = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ)
119, 4, 103eqtr4g 2790 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ฆ โ†’ ๐‘… = ๐‘†)
1211oveq2d 7429 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ฆ โ†’ (-1โ†‘๐‘…) = (-1โ†‘๐‘†))
1312, 11oveq12d 7431 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ ((-1โ†‘๐‘…) ยท ๐‘…) = ((-1โ†‘๐‘†) ยท ๐‘†))
1413oveq1d 7428 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) = (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ))
1514oveq1d 7428 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
16 ovex 7446 . . . . . . . . 9 ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) โˆˆ V
1715, 5, 16fvmpt 6998 . . . . . . . 8 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ (๐‘€โ€˜๐‘ฆ) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
1817ad2antrl 726 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘€โ€˜๐‘ฆ) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
19 ovex 7446 . . . . . . . . 9 ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โˆˆ V
205fvmpt2 7009 . . . . . . . . 9 ((๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โˆˆ V) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2119, 20mpan2 689 . . . . . . . 8 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2221ad2antll 727 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2318, 22eqeq12d 2741 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†” ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2)))
242adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
2524eldifad 3953 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„™)
26 prmz 16640 . . . . . . . . . . . . . . . . 17 (๐‘„ โˆˆ โ„™ โ†’ ๐‘„ โˆˆ โ„ค)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„ค)
28 2z 12619 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„ค
29 elfzelz 13528 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โˆˆ โ„ค)
3029ad2antrl 726 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„ค)
31 zmulcl 12636 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„ค)
3228, 30, 31sylancr 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„ค)
3327, 32zmulcld 12697 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
341adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
3534eldifad 3953 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„™)
36 prmnn 16639 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„•)
3833, 37zmodcld 13884 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) โˆˆ โ„•0)
3910, 38eqeltrid 2829 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘† โˆˆ โ„•0)
4039nn0zd 12609 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘† โˆˆ โ„ค)
41 m1expcl 14078 . . . . . . . . . . . 12 (๐‘† โˆˆ โ„ค โ†’ (-1โ†‘๐‘†) โˆˆ โ„ค)
4240, 41syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘†) โˆˆ โ„ค)
4342, 40zmulcld 12697 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท ๐‘†) โˆˆ โ„ค)
4443, 37zmodcld 13884 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„•0)
4544nn0cnd 12559 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„‚)
46 elfzelz 13528 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โˆˆ โ„ค)
4746ad2antll 727 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„ค)
48 zmulcl 12636 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„ค)
4928, 47, 48sylancr 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„ค)
5027, 49zmulcld 12697 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ค)
5150, 37zmodcld 13884 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) โˆˆ โ„•0)
524, 51eqeltrid 2829 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘… โˆˆ โ„•0)
5352nn0zd 12609 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘… โˆˆ โ„ค)
54 m1expcl 14078 . . . . . . . . . . . 12 (๐‘… โˆˆ โ„ค โ†’ (-1โ†‘๐‘…) โˆˆ โ„ค)
5553, 54syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โˆˆ โ„ค)
5655, 53zmulcld 12697 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ๐‘…) โˆˆ โ„ค)
5756, 37zmodcld 13884 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„•0)
5857nn0cnd 12559 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„‚)
59 2cnd 12315 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„‚)
60 2ne0 12341 . . . . . . . . 9 2 โ‰  0
6160a1i 11 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โ‰  0)
62 div11 11925 . . . . . . . 8 (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„‚ โˆง (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โ†” (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ)))
6345, 58, 59, 61, 62syl112anc 1371 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โ†” (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ)))
6437nnrpd 13041 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„+)
65 eqidd 2726 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) mod ๐‘ƒ) = ((-1โ†‘๐‘†) mod ๐‘ƒ))
6610oveq1i 7423 . . . . . . . . . . 11 (๐‘† mod ๐‘ƒ) = (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ)
6733zred 12691 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„)
68 modabs2 13897 . . . . . . . . . . . 12 (((๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
6967, 64, 68syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
7066, 69eqtrid 2777 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘† mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
7142, 42, 40, 33, 64, 65, 70modmul12d 13917 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ))
72 eqidd 2726 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) mod ๐‘ƒ) = ((-1โ†‘๐‘…) mod ๐‘ƒ))
734oveq1i 7423 . . . . . . . . . . 11 (๐‘… mod ๐‘ƒ) = (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ)
7450zred 12691 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„)
75 modabs2 13897 . . . . . . . . . . . 12 (((๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7674, 64, 75syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7773, 76eqtrid 2777 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7855, 55, 53, 50, 64, 72, 77modmul12d 13917 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ))
7971, 78eqeq12d 2741 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โ†” (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ)))
8042, 33zmulcld 12697 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆˆ โ„ค)
8155, 50zmulcld 12697 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค)
82 moddvds 16236 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„• โˆง ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆˆ โ„ค โˆง ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ ((((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
8337, 80, 81, 82syl3anc 1368 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
8427zcnd 12692 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„‚)
8542, 32zmulcld 12697 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
8685zcnd 12692 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„‚)
8755, 49zmulcld 12697 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ค)
8887zcnd 12692 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)) โˆˆ โ„‚)
8984, 86, 88subdid 11695 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = ((๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
9042zcnd 12692 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘†) โˆˆ โ„‚)
9132zcnd 12692 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
9284, 90, 91mul12d 11448 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) = ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))))
9355zcnd 12692 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โˆˆ โ„‚)
9449zcnd 12692 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„‚)
9584, 93, 94mul12d 11448 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) = ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))
9692, 95oveq12d 7431 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ)))))
9789, 96eqtrd 2765 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ)))))
9897breq2d 5156 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
993adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โ‰  ๐‘„)
100 prmrp 16677 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘„ โˆˆ โ„™) โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
10135, 25, 100syl2anc 582 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
10299, 101mpbird 256 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ gcd ๐‘„) = 1)
103 prmz 16640 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
10435, 103syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„ค)
10585, 87zsubcld 12696 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค)
106 coprmdvds 16618 . . . . . . . . . . . . 13 ((๐‘ƒ โˆˆ โ„ค โˆง ๐‘„ โˆˆ โ„ค โˆง (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
107104, 27, 105, 106syl3anc 1368 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
108102, 107mpan2d 692 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
109 dvdsmultr2 16269 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„ค โˆง (-1โ†‘๐‘…) โˆˆ โ„ค โˆง (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โ†’ ๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))))
110104, 55, 105, 109syl3anc 1368 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โ†’ ๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))))
11193, 86, 88subdid 11695 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
112 neg1cn 12351 . . . . . . . . . . . . . . . . . . 19 -1 โˆˆ โ„‚
113112a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -1 โˆˆ โ„‚)
114113, 39, 52expaddd 14139 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘(๐‘… + ๐‘†)) = ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)))
115114oveq1d 7428 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)) ยท (2 ยท ๐‘ฆ)))
11693, 90, 91mulassd 11262 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)) ยท (2 ยท ๐‘ฆ)) = ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))))
117115, 116eqtr2d 2766 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) = ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)))
118 ax-1cn 11191 . . . . . . . . . . . . . . . . . . . . . . 23 1 โˆˆ โ„‚
119 ax-1ne0 11202 . . . . . . . . . . . . . . . . . . . . . . 23 1 โ‰  0
120 divneg2 11963 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง 1 โ‰  0) โ†’ -(1 / 1) = (1 / -1))
121118, 118, 119, 120mp3an 1457 . . . . . . . . . . . . . . . . . . . . . 22 -(1 / 1) = (1 / -1)
122 1div1e1 11929 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / 1) = 1
123122negeqi 11478 . . . . . . . . . . . . . . . . . . . . . 22 -(1 / 1) = -1
124121, 123eqtr3i 2755 . . . . . . . . . . . . . . . . . . . . 21 (1 / -1) = -1
125124oveq1i 7423 . . . . . . . . . . . . . . . . . . . 20 ((1 / -1)โ†‘๐‘…) = (-1โ†‘๐‘…)
126 neg1ne0 12353 . . . . . . . . . . . . . . . . . . . . . 22 -1 โ‰  0
127126a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -1 โ‰  0)
128113, 127, 53exprecd 14145 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 / -1)โ†‘๐‘…) = (1 / (-1โ†‘๐‘…)))
129125, 128eqtr3id 2779 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) = (1 / (-1โ†‘๐‘…)))
130129oveq2d 7429 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) = ((-1โ†‘๐‘…) ยท (1 / (-1โ†‘๐‘…))))
131113, 127, 53expne0d 14143 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โ‰  0)
13293, 131recidd 12010 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (1 / (-1โ†‘๐‘…))) = 1)
133130, 132eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) = 1)
134133oveq1d 7428 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) ยท (2 ยท ๐‘ฅ)) = (1 ยท (2 ยท ๐‘ฅ)))
13593, 93, 94mulassd 11262 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) ยท (2 ยท ๐‘ฅ)) = ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))
13694mullidd 11257 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (1 ยท (2 ยท ๐‘ฅ)) = (2 ยท ๐‘ฅ))
137134, 135, 1363eqtr3d 2773 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) = (2 ยท ๐‘ฅ))
138117, 137oveq12d 7431 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ)))
139111, 138eqtrd 2765 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ)))
140139breq2d 5156 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
141 eqcom 2732 . . . . . . . . . . . . . . . . 17 (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
14291mulm1d 11691 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1 ยท (2 ยท ๐‘ฆ)) = -(2 ยท ๐‘ฆ))
143142oveq1d 7428 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ))
144143eqeq2d 2736 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ)))
145141, 144bitrid 282 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ)))
14632znegcld 12693 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -(2 ยท ๐‘ฆ) โˆˆ โ„ค)
147 moddvds 16236 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„• โˆง (2 ยท ๐‘ฅ) โˆˆ โ„ค โˆง -(2 ยท ๐‘ฆ) โˆˆ โ„ค) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ))))
14837, 49, 146, 147syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ))))
149 elfznn 13557 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โˆˆ โ„•)
150149ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„•)
151 elfznn 13557 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โˆˆ โ„•)
152151ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„•)
153150, 152nnaddcld 12289 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„•)
154150nnred 12252 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„)
15530zred 12691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„)
156 oddprm 16773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
15734, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
158157nnred 12252 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„)
159 elfzle2 13532 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
160159ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
161 elfzle2 13532 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
162161ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
163154, 155, 158, 158, 160, 162le2addd 11858 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โ‰ค (((๐‘ƒ โˆ’ 1) / 2) + ((๐‘ƒ โˆ’ 1) / 2)))
16437nnred 12252 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„)
165 peano2rem 11552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
167166recnd 11267 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„‚)
1681672halvesd 12483 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘ƒ โˆ’ 1) / 2) + ((๐‘ƒ โˆ’ 1) / 2)) = (๐‘ƒ โˆ’ 1))
169163, 168breqtrd 5170 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))
170 peano2zm 12630 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„ค โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„ค)
171 fznn 13596 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆ’ 1) โˆˆ โ„ค โ†’ ((๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” ((๐‘ฅ + ๐‘ฆ) โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))))
172104, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” ((๐‘ฅ + ๐‘ฆ) โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))))
173153, 169, 172mpbir2and 711 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)))
174 fzm1ndvds 16293 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ƒ โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1))) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ))
17537, 173, 174syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ))
176 eldifsni 4790 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โ‰  2)
17734, 176syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โ‰  2)
178 2prm 16657 . . . . . . . . . . . . . . . . . . . . . . 23 2 โˆˆ โ„™
179 prmrp 16677 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„™ โˆง 2 โˆˆ โ„™) โ†’ ((๐‘ƒ gcd 2) = 1 โ†” ๐‘ƒ โ‰  2))
18035, 178, 179sylancl 584 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ gcd 2) = 1 โ†” ๐‘ƒ โ‰  2))
181177, 180mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ gcd 2) = 1)
18228a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„ค)
183153nnzd 12610 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„ค)
184 coprmdvds 16618 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ƒ โˆˆ โ„ค โˆง 2 โˆˆ โ„ค โˆง (๐‘ฅ + ๐‘ฆ) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โˆง (๐‘ƒ gcd 2) = 1) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
185104, 182, 183, 184syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โˆง (๐‘ƒ gcd 2) = 1) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
186181, 185mpan2d 692 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
187175, 186mtod 197 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ยฌ ๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)))
18894, 91subnegd 11603 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) = ((2 ยท ๐‘ฅ) + (2 ยท ๐‘ฆ)))
18947zcnd 12692 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„‚)
19030zcnd 12692 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„‚)
19159, 189, 190adddid 11263 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท (๐‘ฅ + ๐‘ฆ)) = ((2 ยท ๐‘ฅ) + (2 ยท ๐‘ฆ)))
192188, 191eqtr4d 2768 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) = (2 ยท (๐‘ฅ + ๐‘ฆ)))
193192breq2d 5156 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) โ†” ๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ))))
194187, 193mtbird 324 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ยฌ ๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)))
195194pm2.21d 121 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
196148, 195sylbid 239 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
197145, 196sylbid 239 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
198 oveq1 7420 . . . . . . . . . . . . . . . . . 18 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (-1 ยท (2 ยท ๐‘ฆ)))
199198oveq1d 7428 . . . . . . . . . . . . . . . . 17 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
200199eqeq1d 2727 . . . . . . . . . . . . . . . 16 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ)))
201200imbi1d 340 . . . . . . . . . . . . . . 15 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ (((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)) โ†” (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ))))
202197, 201syl5ibrcom 246 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ))))
20391mullidd 11257 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (1 ยท (2 ยท ๐‘ฆ)) = (2 ยท ๐‘ฆ))
204203oveq1d 7428 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฆ) mod ๐‘ƒ))
20532zred 12691 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„)
206 2nn 12310 . . . . . . . . . . . . . . . . . . . . . 22 2 โˆˆ โ„•
207 nnmulcl 12261 . . . . . . . . . . . . . . . . . . . . . 22 ((2 โˆˆ โ„• โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•)
208206, 152, 207sylancr 585 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•)
209208nnnn0d 12557 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•0)
210209nn0ge0d 12560 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 โ‰ค (2 ยท ๐‘ฆ))
211 2re 12311 . . . . . . . . . . . . . . . . . . . . . . 23 2 โˆˆ โ„
212211a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„)
213 2pos 12340 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 < 2)
215 lemuldiv2 12120 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฆ โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
216155, 166, 212, 214, 215syl112anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
217162, 216mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))
218 zltlem1 12640 . . . . . . . . . . . . . . . . . . . . 21 (((2 ยท ๐‘ฆ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ฆ) < ๐‘ƒ โ†” (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1)))
21932, 104, 218syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) < ๐‘ƒ โ†” (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1)))
220217, 219mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) < ๐‘ƒ)
221 modid 13888 . . . . . . . . . . . . . . . . . . 19 ((((2 ยท ๐‘ฆ) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โˆง (0 โ‰ค (2 ยท ๐‘ฆ) โˆง (2 ยท ๐‘ฆ) < ๐‘ƒ)) โ†’ ((2 ยท ๐‘ฆ) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
222205, 64, 210, 220, 221syl22anc 837 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
223204, 222eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
22449zred 12691 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„)
225 nnmulcl 12261 . . . . . . . . . . . . . . . . . . . . 21 ((2 โˆˆ โ„• โˆง ๐‘ฅ โˆˆ โ„•) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•)
226206, 150, 225sylancr 585 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•)
227226nnnn0d 12557 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•0)
228227nn0ge0d 12560 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 โ‰ค (2 ยท ๐‘ฅ))
229 lemuldiv2 12120 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
230154, 166, 212, 214, 229syl112anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
231160, 230mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1))
232 zltlem1 12640 . . . . . . . . . . . . . . . . . . . 20 (((2 ยท ๐‘ฅ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ฅ) < ๐‘ƒ โ†” (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1)))
23349, 104, 232syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) < ๐‘ƒ โ†” (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1)))
234231, 233mpbird 256 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) < ๐‘ƒ)
235 modid 13888 . . . . . . . . . . . . . . . . . 18 ((((2 ยท ๐‘ฅ) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โˆง (0 โ‰ค (2 ยท ๐‘ฅ) โˆง (2 ยท ๐‘ฅ) < ๐‘ƒ)) โ†’ ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (2 ยท ๐‘ฅ))
236224, 64, 228, 234, 235syl22anc 837 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (2 ยท ๐‘ฅ))
237223, 236eqeq12d 2741 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
238237biimpd 228 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
239 oveq1 7420 . . . . . . . . . . . . . . . . . 18 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (1 ยท (2 ยท ๐‘ฆ)))
240239oveq1d 7428 . . . . . . . . . . . . . . . . 17 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
241240eqeq1d 2727 . . . . . . . . . . . . . . . 16 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ)))
242241imbi1d 340 . . . . . . . . . . . . . . 15 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ (((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)) โ†” (((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ))))
243238, 242syl5ibrcom 246 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ))))
24452, 39nn0addcld 12561 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… + ๐‘†) โˆˆ โ„•0)
245244nn0zd 12609 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… + ๐‘†) โˆˆ โ„ค)
246 m1expcl2 14077 . . . . . . . . . . . . . . 15 ((๐‘… + ๐‘†) โˆˆ โ„ค โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ {-1, 1})
247 elpri 4648 . . . . . . . . . . . . . . 15 ((-1โ†‘(๐‘… + ๐‘†)) โˆˆ {-1, 1} โ†’ ((-1โ†‘(๐‘… + ๐‘†)) = -1 โˆจ (-1โ†‘(๐‘… + ๐‘†)) = 1))
248245, 246, 2473syl 18 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) = -1 โˆจ (-1โ†‘(๐‘… + ๐‘†)) = 1))
249202, 243, 248mpjaod 858 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
250 neg1z 12623 . . . . . . . . . . . . . . . 16 -1 โˆˆ โ„ค
251 zexpcl 14068 . . . . . . . . . . . . . . . 16 ((-1 โˆˆ โ„ค โˆง (๐‘… + ๐‘†) โˆˆ โ„•0) โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ โ„ค)
252250, 244, 251sylancr 585 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ โ„ค)
253252, 32zmulcld 12697 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
254 moddvds 16236 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„• โˆง ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค โˆง (2 ยท ๐‘ฅ) โˆˆ โ„ค) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
25537, 253, 49, 254syl3anc 1368 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
256190, 189, 59, 61mulcand 11872 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ) โ†” ๐‘ฆ = ๐‘ฅ))
257249, 255, 2563imtr3d 292 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ)) โ†’ ๐‘ฆ = ๐‘ฅ))
258140, 257sylbid 239 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฆ = ๐‘ฅ))
259108, 110, 2583syld 60 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฆ = ๐‘ฅ))
26098, 259sylbird 259 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฆ = ๐‘ฅ))
26183, 260sylbid 239 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ) โ†’ ๐‘ฆ = ๐‘ฅ))
26279, 261sylbid 239 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โ†’ ๐‘ฆ = ๐‘ฅ))
26363, 262sylbid 239 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โ†’ ๐‘ฆ = ๐‘ฅ))
26423, 263sylbid 239 . . . . 5 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
265264ralrimivva 3191 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
266 nfmpt1 5252 . . . . . . . . . 10 โ„ฒ๐‘ฅ(๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†ฆ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2675, 266nfcxfr 2890 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘€
268 nfcv 2892 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘ฆ
269267, 268nffv 6900 . . . . . . . 8 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ฆ)
270 nfcv 2892 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘ง
271267, 270nffv 6900 . . . . . . . 8 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ง)
272269, 271nfeq 2906 . . . . . . 7 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง)
273 nfv 1909 . . . . . . 7 โ„ฒ๐‘ฅ ๐‘ฆ = ๐‘ง
274272, 273nfim 1891 . . . . . 6 โ„ฒ๐‘ฅ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง)
275 nfv 1909 . . . . . 6 โ„ฒ๐‘ง((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ)
276 fveq2 6890 . . . . . . . 8 (๐‘ง = ๐‘ฅ โ†’ (๐‘€โ€˜๐‘ง) = (๐‘€โ€˜๐‘ฅ))
277276eqeq2d 2736 . . . . . . 7 (๐‘ง = ๐‘ฅ โ†’ ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†” (๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ)))
278 equequ2 2021 . . . . . . 7 (๐‘ง = ๐‘ฅ โ†’ (๐‘ฆ = ๐‘ง โ†” ๐‘ฆ = ๐‘ฅ))
279277, 278imbi12d 343 . . . . . 6 (๐‘ง = ๐‘ฅ โ†’ (((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง) โ†” ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ)))
280274, 275, 279cbvralw 3294 . . . . 5 (โˆ€๐‘ง โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง) โ†” โˆ€๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
281280ralbii 3083 . . . 4 (โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ง โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง) โ†” โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
282265, 281sylibr 233 . . 3 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ง โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง))
283 dff13 7259 . . 3 (๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1โ†’(1...((๐‘ƒ โˆ’ 1) / 2)) โ†” (๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โŸถ(1...((๐‘ƒ โˆ’ 1) / 2)) โˆง โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ง โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง)))
2846, 282, 283sylanbrc 581 . 2 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1โ†’(1...((๐‘ƒ โˆ’ 1) / 2)))
285 ovex 7446 . . . 4 (1...((๐‘ƒ โˆ’ 1) / 2)) โˆˆ V
286285enref 8999 . . 3 (1...((๐‘ƒ โˆ’ 1) / 2)) โ‰ˆ (1...((๐‘ƒ โˆ’ 1) / 2))
287 fzfi 13964 . . 3 (1...((๐‘ƒ โˆ’ 1) / 2)) โˆˆ Fin
288 f1finf1o 9289 . . 3 (((1...((๐‘ƒ โˆ’ 1) / 2)) โ‰ˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง (1...((๐‘ƒ โˆ’ 1) / 2)) โˆˆ Fin) โ†’ (๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1โ†’(1...((๐‘ƒ โˆ’ 1) / 2)) โ†” ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1-ontoโ†’(1...((๐‘ƒ โˆ’ 1) / 2))))
289286, 287, 288mp2an 690 . 2 (๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1โ†’(1...((๐‘ƒ โˆ’ 1) / 2)) โ†” ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1-ontoโ†’(1...((๐‘ƒ โˆ’ 1) / 2)))
290284, 289sylib 217 1 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1-ontoโ†’(1...((๐‘ƒ โˆ’ 1) / 2)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  โˆ€wral 3051  Vcvv 3463   โˆ– cdif 3938  {csn 4625  {cpr 4627   class class class wbr 5144   โ†ฆ cmpt 5227  โŸถwf 6539  โ€“1-1โ†’wf1 6540  โ€“1-1-ontoโ†’wf1o 6542  โ€˜cfv 6543  (class class class)co 7413   โ‰ˆ cen 8954  Fincfn 8957  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   ยท cmul 11138   < clt 11273   โ‰ค cle 11274   โˆ’ cmin 11469  -cneg 11470   / cdiv 11896  โ„•cn 12237  2c2 12292  โ„•0cn0 12497  โ„คcz 12583  โ„+crp 13001  ...cfz 13511   mod cmo 13861  โ†‘cexp 14053   โˆฅ cdvds 16225   gcd cgcd 16463  โ„™cprime 16636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9460  df-inf 9461  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-z 12584  df-uz 12848  df-rp 13002  df-fz 13512  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-dvds 16226  df-gcd 16464  df-prm 16637
This theorem is referenced by:  lgseisenlem3  27323
  Copyright terms: Public domain W3C validator