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

Theorem lgseisenlem2 27296
Description: Lemma for lgseisen 27299. 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 27295 . . 3 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โŸถ(1...((๐‘ƒ โˆ’ 1) / 2)))
7 oveq2 7422 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ฆ โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘ฆ))
87oveq2d 7430 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) = (๐‘„ ยท (2 ยท ๐‘ฆ)))
98oveq1d 7429 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
10 lgseisen.6 . . . . . . . . . . . . . 14 ๐‘† = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ)
119, 4, 103eqtr4g 2792 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ฆ โ†’ ๐‘… = ๐‘†)
1211oveq2d 7430 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ฆ โ†’ (-1โ†‘๐‘…) = (-1โ†‘๐‘†))
1312, 11oveq12d 7432 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ ((-1โ†‘๐‘…) ยท ๐‘…) = ((-1โ†‘๐‘†) ยท ๐‘†))
1413oveq1d 7429 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) = (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ))
1514oveq1d 7429 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
16 ovex 7447 . . . . . . . . 9 ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) โˆˆ V
1715, 5, 16fvmpt 6999 . . . . . . . 8 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ (๐‘€โ€˜๐‘ฆ) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
1817ad2antrl 727 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘€โ€˜๐‘ฆ) = ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2))
19 ovex 7447 . . . . . . . . 9 ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โˆˆ V
205fvmpt2 7010 . . . . . . . . 9 ((๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โˆˆ V) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2119, 20mpan2 690 . . . . . . . 8 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2221ad2antll 728 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘€โ€˜๐‘ฅ) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2318, 22eqeq12d 2743 . . . . . 6 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†” ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2)))
242adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ (โ„™ โˆ– {2}))
2524eldifad 3956 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„™)
26 prmz 16637 . . . . . . . . . . . . . . . . 17 (๐‘„ โˆˆ โ„™ โ†’ ๐‘„ โˆˆ โ„ค)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„ค)
28 2z 12616 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„ค
29 elfzelz 13525 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โˆˆ โ„ค)
3029ad2antrl 727 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„ค)
31 zmulcl 12633 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„ค)
3228, 30, 31sylancr 586 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„ค)
3327, 32zmulcld 12694 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
341adantr 480 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
3534eldifad 3956 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„™)
36 prmnn 16636 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„•)
3833, 37zmodcld 13881 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) โˆˆ โ„•0)
3910, 38eqeltrid 2832 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘† โˆˆ โ„•0)
4039nn0zd 12606 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘† โˆˆ โ„ค)
41 m1expcl 14075 . . . . . . . . . . . 12 (๐‘† โˆˆ โ„ค โ†’ (-1โ†‘๐‘†) โˆˆ โ„ค)
4240, 41syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘†) โˆˆ โ„ค)
4342, 40zmulcld 12694 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท ๐‘†) โˆˆ โ„ค)
4443, 37zmodcld 13881 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„•0)
4544nn0cnd 12556 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„‚)
46 elfzelz 13525 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โˆˆ โ„ค)
4746ad2antll 728 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„ค)
48 zmulcl 12633 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„ค)
4928, 47, 48sylancr 586 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„ค)
5027, 49zmulcld 12694 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ค)
5150, 37zmodcld 13881 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) โˆˆ โ„•0)
524, 51eqeltrid 2832 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘… โˆˆ โ„•0)
5352nn0zd 12606 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘… โˆˆ โ„ค)
54 m1expcl 14075 . . . . . . . . . . . 12 (๐‘… โˆˆ โ„ค โ†’ (-1โ†‘๐‘…) โˆˆ โ„ค)
5553, 54syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โˆˆ โ„ค)
5655, 53zmulcld 12694 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ๐‘…) โˆˆ โ„ค)
5756, 37zmodcld 13881 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„•0)
5857nn0cnd 12556 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„‚)
59 2cnd 12312 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„‚)
60 2ne0 12338 . . . . . . . . 9 2 โ‰  0
6160a1i 11 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โ‰  0)
62 div11 11922 . . . . . . . 8 (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) โˆˆ โ„‚ โˆง (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โ†” (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ)))
6345, 58, 59, 61, 62syl112anc 1372 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) / 2) = ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2) โ†” (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ)))
6437nnrpd 13038 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„+)
65 eqidd 2728 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) mod ๐‘ƒ) = ((-1โ†‘๐‘†) mod ๐‘ƒ))
6610oveq1i 7424 . . . . . . . . . . 11 (๐‘† mod ๐‘ƒ) = (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ)
6733zred 12688 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„)
68 modabs2 13894 . . . . . . . . . . . 12 (((๐‘„ ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
6967, 64, 68syl2anc 583 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
7066, 69eqtrid 2779 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘† mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
7142, 42, 40, 33, 64, 65, 70modmul12d 13914 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ))
72 eqidd 2728 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) mod ๐‘ƒ) = ((-1โ†‘๐‘…) mod ๐‘ƒ))
734oveq1i 7424 . . . . . . . . . . 11 (๐‘… mod ๐‘ƒ) = (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ)
7450zred 12688 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„)
75 modabs2 13894 . . . . . . . . . . . 12 (((๐‘„ ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7674, 64, 75syl2anc 583 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ) mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7773, 76eqtrid 2779 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… mod ๐‘ƒ) = ((๐‘„ ยท (2 ยท ๐‘ฅ)) mod ๐‘ƒ))
7855, 55, 53, 50, 64, 72, 77modmul12d 13914 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ))
7971, 78eqeq12d 2743 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท ๐‘†) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) โ†” (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ)))
8042, 33zmulcld 12694 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆˆ โ„ค)
8155, 50zmulcld 12694 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค)
82 moddvds 16233 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„• โˆง ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆˆ โ„ค โˆง ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ ((((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
8337, 80, 81, 82syl3anc 1369 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) mod ๐‘ƒ) = (((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
8427zcnd 12689 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘„ โˆˆ โ„‚)
8542, 32zmulcld 12694 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
8685zcnd 12689 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„‚)
8755, 49zmulcld 12694 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)) โˆˆ โ„ค)
8887zcnd 12689 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)) โˆˆ โ„‚)
8984, 86, 88subdid 11692 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = ((๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
9042zcnd 12689 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘†) โˆˆ โ„‚)
9132zcnd 12689 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
9284, 90, 91mul12d 11445 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) = ((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))))
9355zcnd 12689 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โˆˆ โ„‚)
9449zcnd 12689 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„‚)
9584, 93, 94mul12d 11445 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) = ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))
9692, 95oveq12d 7432 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘„ ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ (๐‘„ ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ)))))
9789, 96eqtrd 2767 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ)))))
9897breq2d 5154 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†” ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (๐‘„ ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท (๐‘„ ยท (2 ยท ๐‘ฅ))))))
993adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โ‰  ๐‘„)
100 prmrp 16674 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘„ โˆˆ โ„™) โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
10135, 25, 100syl2anc 583 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ gcd ๐‘„) = 1 โ†” ๐‘ƒ โ‰  ๐‘„))
10299, 101mpbird 257 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ gcd ๐‘„) = 1)
103 prmz 16637 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
10435, 103syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„ค)
10585, 87zsubcld 12693 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค)
106 coprmdvds 16615 . . . . . . . . . . . . 13 ((๐‘ƒ โˆˆ โ„ค โˆง ๐‘„ โˆˆ โ„ค โˆง (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
107104, 27, 105, 106syl3anc 1369 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โˆง (๐‘ƒ gcd ๐‘„) = 1) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
108102, 107mpan2d 693 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (๐‘„ ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
109 dvdsmultr2 16266 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„ค โˆง (-1โ†‘๐‘…) โˆˆ โ„ค โˆง (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โ†’ ๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))))
110104, 55, 105, 109syl3anc 1369 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) โ†’ ๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))))
11193, 86, 88subdid 11692 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))))
112 neg1cn 12348 . . . . . . . . . . . . . . . . . . 19 -1 โˆˆ โ„‚
113112a1i 11 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -1 โˆˆ โ„‚)
114113, 39, 52expaddd 14136 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘(๐‘… + ๐‘†)) = ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)))
115114oveq1d 7429 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)) ยท (2 ยท ๐‘ฆ)))
11693, 90, 91mulassd 11259 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘†)) ยท (2 ยท ๐‘ฆ)) = ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))))
117115, 116eqtr2d 2768 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) = ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)))
118 ax-1cn 11188 . . . . . . . . . . . . . . . . . . . . . . 23 1 โˆˆ โ„‚
119 ax-1ne0 11199 . . . . . . . . . . . . . . . . . . . . . . 23 1 โ‰  0
120 divneg2 11960 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง 1 โ‰  0) โ†’ -(1 / 1) = (1 / -1))
121118, 118, 119, 120mp3an 1458 . . . . . . . . . . . . . . . . . . . . . 22 -(1 / 1) = (1 / -1)
122 1div1e1 11926 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / 1) = 1
123122negeqi 11475 . . . . . . . . . . . . . . . . . . . . . 22 -(1 / 1) = -1
124121, 123eqtr3i 2757 . . . . . . . . . . . . . . . . . . . . 21 (1 / -1) = -1
125124oveq1i 7424 . . . . . . . . . . . . . . . . . . . 20 ((1 / -1)โ†‘๐‘…) = (-1โ†‘๐‘…)
126 neg1ne0 12350 . . . . . . . . . . . . . . . . . . . . . 22 -1 โ‰  0
127126a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -1 โ‰  0)
128113, 127, 53exprecd 14142 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 / -1)โ†‘๐‘…) = (1 / (-1โ†‘๐‘…)))
129125, 128eqtr3id 2781 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) = (1 / (-1โ†‘๐‘…)))
130129oveq2d 7430 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) = ((-1โ†‘๐‘…) ยท (1 / (-1โ†‘๐‘…))))
131113, 127, 53expne0d 14140 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘๐‘…) โ‰  0)
13293, 131recidd 12007 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (1 / (-1โ†‘๐‘…))) = 1)
133130, 132eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) = 1)
134133oveq1d 7429 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) ยท (2 ยท ๐‘ฅ)) = (1 ยท (2 ยท ๐‘ฅ)))
13593, 93, 94mulassd 11259 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท (-1โ†‘๐‘…)) ยท (2 ยท ๐‘ฅ)) = ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))))
13694mullidd 11254 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (1 ยท (2 ยท ๐‘ฅ)) = (2 ยท ๐‘ฅ))
137134, 135, 1363eqtr3d 2775 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ))) = (2 ยท ๐‘ฅ))
138117, 137oveq12d 7432 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ))) โˆ’ ((-1โ†‘๐‘…) ยท ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ)))
139111, 138eqtrd 2767 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) = (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ)))
140139breq2d 5154 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((-1โ†‘๐‘…) ยท (((-1โ†‘๐‘†) ยท (2 ยท ๐‘ฆ)) โˆ’ ((-1โ†‘๐‘…) ยท (2 ยท ๐‘ฅ)))) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
141 eqcom 2734 . . . . . . . . . . . . . . . . 17 (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
14291mulm1d 11688 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1 ยท (2 ยท ๐‘ฆ)) = -(2 ยท ๐‘ฆ))
143142oveq1d 7429 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ))
144143eqeq2d 2738 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ)))
145141, 144bitrid 283 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ)))
14632znegcld 12690 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ -(2 ยท ๐‘ฆ) โˆˆ โ„ค)
147 moddvds 16233 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„• โˆง (2 ยท ๐‘ฅ) โˆˆ โ„ค โˆง -(2 ยท ๐‘ฆ) โˆˆ โ„ค) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ))))
14837, 49, 146, 147syl3anc 1369 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (-(2 ยท ๐‘ฆ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ))))
149 elfznn 13554 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โˆˆ โ„•)
150149ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„•)
151 elfznn 13554 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โˆˆ โ„•)
152151ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„•)
153150, 152nnaddcld 12286 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„•)
154150nnred 12249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„)
15530zred 12688 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„)
156 oddprm 16770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
15734, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
158157nnred 12249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„)
159 elfzle2 13529 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
160159ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
161 elfzle2 13529 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†’ ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
162161ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
163154, 155, 158, 158, 160, 162le2addd 11855 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โ‰ค (((๐‘ƒ โˆ’ 1) / 2) + ((๐‘ƒ โˆ’ 1) / 2)))
16437nnred 12249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โˆˆ โ„)
165 peano2rem 11549 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
167166recnd 11264 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„‚)
1681672halvesd 12480 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (((๐‘ƒ โˆ’ 1) / 2) + ((๐‘ƒ โˆ’ 1) / 2)) = (๐‘ƒ โˆ’ 1))
169163, 168breqtrd 5168 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))
170 peano2zm 12627 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„ค โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„ค)
171 fznn 13593 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆ’ 1) โˆˆ โ„ค โ†’ ((๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” ((๐‘ฅ + ๐‘ฆ) โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))))
172104, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” ((๐‘ฅ + ๐‘ฆ) โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))))
173153, 169, 172mpbir2and 712 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1)))
174 fzm1ndvds 16290 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ƒ โˆˆ โ„• โˆง (๐‘ฅ + ๐‘ฆ) โˆˆ (1...(๐‘ƒ โˆ’ 1))) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ))
17537, 173, 174syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ))
176 eldifsni 4789 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โ‰  2)
17734, 176syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ƒ โ‰  2)
178 2prm 16654 . . . . . . . . . . . . . . . . . . . . . . 23 2 โˆˆ โ„™
179 prmrp 16674 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„™ โˆง 2 โˆˆ โ„™) โ†’ ((๐‘ƒ gcd 2) = 1 โ†” ๐‘ƒ โ‰  2))
18035, 178, 179sylancl 585 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ gcd 2) = 1 โ†” ๐‘ƒ โ‰  2))
181177, 180mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ gcd 2) = 1)
18228a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„ค)
183153nnzd 12607 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ โ„ค)
184 coprmdvds 16615 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ƒ โˆˆ โ„ค โˆง 2 โˆˆ โ„ค โˆง (๐‘ฅ + ๐‘ฆ) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โˆง (๐‘ƒ gcd 2) = 1) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
185104, 182, 183, 184syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โˆง (๐‘ƒ gcd 2) = 1) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
186181, 185mpan2d 693 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)) โ†’ ๐‘ƒ โˆฅ (๐‘ฅ + ๐‘ฆ)))
187175, 186mtod 197 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ยฌ ๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ)))
18894, 91subnegd 11600 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) = ((2 ยท ๐‘ฅ) + (2 ยท ๐‘ฆ)))
18947zcnd 12689 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฅ โˆˆ โ„‚)
19030zcnd 12689 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ๐‘ฆ โˆˆ โ„‚)
19159, 189, 190adddid 11260 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท (๐‘ฅ + ๐‘ฆ)) = ((2 ยท ๐‘ฅ) + (2 ยท ๐‘ฆ)))
192188, 191eqtr4d 2770 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) = (2 ยท (๐‘ฅ + ๐‘ฆ)))
193192breq2d 5154 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘ƒ โˆฅ ((2 ยท ๐‘ฅ) โˆ’ -(2 ยท ๐‘ฆ)) โ†” ๐‘ƒ โˆฅ (2 ยท (๐‘ฅ + ๐‘ฆ))))
194187, 193mtbird 325 . . . . . . . . . . . . . . . . . 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 7421 . . . . . . . . . . . . . . . . . 18 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (-1 ยท (2 ยท ๐‘ฆ)))
199198oveq1d 7429 . . . . . . . . . . . . . . . . 17 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
200199eqeq1d 2729 . . . . . . . . . . . . . . . 16 ((-1โ†‘(๐‘… + ๐‘†)) = -1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((-1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ)))
201200imbi1d 341 . . . . . . . . . . . . . . 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 11254 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (1 ยท (2 ยท ๐‘ฆ)) = (2 ยท ๐‘ฆ))
204203oveq1d 7429 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฆ) mod ๐‘ƒ))
20532zred 12688 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„)
206 2nn 12307 . . . . . . . . . . . . . . . . . . . . . 22 2 โˆˆ โ„•
207 nnmulcl 12258 . . . . . . . . . . . . . . . . . . . . . 22 ((2 โˆˆ โ„• โˆง ๐‘ฆ โˆˆ โ„•) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•)
208206, 152, 207sylancr 586 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•)
209208nnnn0d 12554 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„•0)
210209nn0ge0d 12557 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 โ‰ค (2 ยท ๐‘ฆ))
211 2re 12308 . . . . . . . . . . . . . . . . . . . . . . 23 2 โˆˆ โ„
212211a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 2 โˆˆ โ„)
213 2pos 12337 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 < 2)
215 lemuldiv2 12117 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฆ โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
216155, 166, 212, 214, 215syl112anc 1372 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
217162, 216mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))
218 zltlem1 12637 . . . . . . . . . . . . . . . . . . . . 21 (((2 ยท ๐‘ฆ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ฆ) < ๐‘ƒ โ†” (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1)))
21932, 104, 218syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) < ๐‘ƒ โ†” (2 ยท ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1)))
220217, 219mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฆ) < ๐‘ƒ)
221 modid 13885 . . . . . . . . . . . . . . . . . . 19 ((((2 ยท ๐‘ฆ) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โˆง (0 โ‰ค (2 ยท ๐‘ฆ) โˆง (2 ยท ๐‘ฆ) < ๐‘ƒ)) โ†’ ((2 ยท ๐‘ฆ) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
222205, 64, 210, 220, 221syl22anc 838 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
223204, 222eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = (2 ยท ๐‘ฆ))
22449zred 12688 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„)
225 nnmulcl 12258 . . . . . . . . . . . . . . . . . . . . 21 ((2 โˆˆ โ„• โˆง ๐‘ฅ โˆˆ โ„•) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•)
226206, 150, 225sylancr 586 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•)
227226nnnn0d 12554 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โˆˆ โ„•0)
228227nn0ge0d 12557 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ 0 โ‰ค (2 ยท ๐‘ฅ))
229 lemuldiv2 12117 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
230154, 166, 212, 214, 229syl112anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
231160, 230mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1))
232 zltlem1 12637 . . . . . . . . . . . . . . . . . . . 20 (((2 ยท ๐‘ฅ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ ((2 ยท ๐‘ฅ) < ๐‘ƒ โ†” (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1)))
23349, 104, 232syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) < ๐‘ƒ โ†” (2 ยท ๐‘ฅ) โ‰ค (๐‘ƒ โˆ’ 1)))
234231, 233mpbird 257 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (2 ยท ๐‘ฅ) < ๐‘ƒ)
235 modid 13885 . . . . . . . . . . . . . . . . . 18 ((((2 ยท ๐‘ฅ) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โˆง (0 โ‰ค (2 ยท ๐‘ฅ) โˆง (2 ยท ๐‘ฅ) < ๐‘ƒ)) โ†’ ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (2 ยท ๐‘ฅ))
236224, 64, 228, 234, 235syl22anc 838 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฅ) mod ๐‘ƒ) = (2 ยท ๐‘ฅ))
237223, 236eqeq12d 2743 . . . . . . . . . . . . . . . 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 7421 . . . . . . . . . . . . . . . . . 18 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) = (1 ยท (2 ยท ๐‘ฆ)))
240239oveq1d 7429 . . . . . . . . . . . . . . . . 17 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ))
241240eqeq1d 2729 . . . . . . . . . . . . . . . 16 ((-1โ†‘(๐‘… + ๐‘†)) = 1 โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ((1 ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ)))
242241imbi1d 341 . . . . . . . . . . . . . . 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 12558 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… + ๐‘†) โˆˆ โ„•0)
245244nn0zd 12606 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (๐‘… + ๐‘†) โˆˆ โ„ค)
246 m1expcl2 14074 . . . . . . . . . . . . . . 15 ((๐‘… + ๐‘†) โˆˆ โ„ค โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ {-1, 1})
247 elpri 4646 . . . . . . . . . . . . . . 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 859 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†’ (2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ)))
250 neg1z 12620 . . . . . . . . . . . . . . . 16 -1 โˆˆ โ„ค
251 zexpcl 14065 . . . . . . . . . . . . . . . 16 ((-1 โˆˆ โ„ค โˆง (๐‘… + ๐‘†) โˆˆ โ„•0) โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ โ„ค)
252250, 244, 251sylancr 586 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ (-1โ†‘(๐‘… + ๐‘†)) โˆˆ โ„ค)
253252, 32zmulcld 12694 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค)
254 moddvds 16233 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„• โˆง ((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆˆ โ„ค โˆง (2 ยท ๐‘ฅ) โˆˆ โ„ค) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
25537, 253, 49, 254syl3anc 1369 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) mod ๐‘ƒ) = ((2 ยท ๐‘ฅ) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ (((-1โ†‘(๐‘… + ๐‘†)) ยท (2 ยท ๐‘ฆ)) โˆ’ (2 ยท ๐‘ฅ))))
256190, 189, 59, 61mulcand 11869 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โˆง ๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))) โ†’ ((2 ยท ๐‘ฆ) = (2 ยท ๐‘ฅ) โ†” ๐‘ฆ = ๐‘ฅ))
257249, 255, 2563imtr3d 293 . . . . . . . . . . . 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 260 . . . . . . . . 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 3195 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))โˆ€๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
266 nfmpt1 5250 . . . . . . . . . 10 โ„ฒ๐‘ฅ(๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†ฆ ((((-1โ†‘๐‘…) ยท ๐‘…) mod ๐‘ƒ) / 2))
2675, 266nfcxfr 2896 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘€
268 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘ฆ
269267, 268nffv 6901 . . . . . . . 8 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ฆ)
270 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘ฅ๐‘ง
271267, 270nffv 6901 . . . . . . . 8 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ง)
272269, 271nfeq 2911 . . . . . . 7 โ„ฒ๐‘ฅ(๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง)
273 nfv 1910 . . . . . . 7 โ„ฒ๐‘ฅ ๐‘ฆ = ๐‘ง
274272, 273nfim 1892 . . . . . 6 โ„ฒ๐‘ฅ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง)
275 nfv 1910 . . . . . 6 โ„ฒ๐‘ง((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ)
276 fveq2 6891 . . . . . . . 8 (๐‘ง = ๐‘ฅ โ†’ (๐‘€โ€˜๐‘ง) = (๐‘€โ€˜๐‘ฅ))
277276eqeq2d 2738 . . . . . . 7 (๐‘ง = ๐‘ฅ โ†’ ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†” (๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ)))
278 equequ2 2022 . . . . . . 7 (๐‘ง = ๐‘ฅ โ†’ (๐‘ฆ = ๐‘ง โ†” ๐‘ฆ = ๐‘ฅ))
279277, 278imbi12d 344 . . . . . 6 (๐‘ง = ๐‘ฅ โ†’ (((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง) โ†” ((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ)))
280274, 275, 279cbvralw 3298 . . . . 5 (โˆ€๐‘ง โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ง) โ†’ ๐‘ฆ = ๐‘ง) โ†” โˆ€๐‘ฅ โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2))((๐‘€โ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฅ) โ†’ ๐‘ฆ = ๐‘ฅ))
281280ralbii 3088 . . . 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 582 . 2 (๐œ‘ โ†’ ๐‘€:(1...((๐‘ƒ โˆ’ 1) / 2))โ€“1-1โ†’(1...((๐‘ƒ โˆ’ 1) / 2)))
285 ovex 7447 . . . 4 (1...((๐‘ƒ โˆ’ 1) / 2)) โˆˆ V
286285enref 8997 . . 3 (1...((๐‘ƒ โˆ’ 1) / 2)) โ‰ˆ (1...((๐‘ƒ โˆ’ 1) / 2))
287 fzfi 13961 . . 3 (1...((๐‘ƒ โˆ’ 1) / 2)) โˆˆ Fin
288 f1finf1o 9287 . . 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 691 . 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 395   โˆจ wo 846   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆ€wral 3056  Vcvv 3469   โˆ– cdif 3941  {csn 4624  {cpr 4626   class class class wbr 5142   โ†ฆ cmpt 5225  โŸถwf 6538  โ€“1-1โ†’wf1 6539  โ€“1-1-ontoโ†’wf1o 6541  โ€˜cfv 6542  (class class class)co 7414   โ‰ˆ cen 8952  Fincfn 8955  โ„‚cc 11128  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135   < clt 11270   โ‰ค cle 11271   โˆ’ cmin 11466  -cneg 11467   / cdiv 11893  โ„•cn 12234  2c2 12289  โ„•0cn0 12494  โ„คcz 12580  โ„+crp 12998  ...cfz 13508   mod cmo 13858  โ†‘cexp 14050   โˆฅ cdvds 16222   gcd cgcd 16460  โ„™cprime 16633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  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 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-fz 13509  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-dvds 16223  df-gcd 16461  df-prm 16634
This theorem is referenced by:  lgseisenlem3  27297
  Copyright terms: Public domain W3C validator