Metamath Proof Explorer

Theorem lgseisenlem1

Description: Lemma for lgseisen . If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ) , then for any even 1 <_ u <_ P - 1 , M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1 . To simplify these statements, we divide all the even numbers by 2 , so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2 . (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.2 ${⊢}{\phi }\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.3 ${⊢}{\phi }\to {P}\ne {Q}$
lgseisen.4 ${⊢}{R}={Q}2{x}\mathrm{mod}{P}$
lgseisen.5 ${⊢}{M}=\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)⟼\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\right)$
Assertion lgseisenlem1 ${⊢}{\phi }\to {M}:\left(1\dots \frac{{P}-1}{2}\right)⟶\left(1\dots \frac{{P}-1}{2}\right)$

Proof

Step Hyp Ref Expression
1 lgseisen.1 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
2 lgseisen.2 ${⊢}{\phi }\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
3 lgseisen.3 ${⊢}{\phi }\to {P}\ne {Q}$
4 lgseisen.4 ${⊢}{R}={Q}2{x}\mathrm{mod}{P}$
5 lgseisen.5 ${⊢}{M}=\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)⟼\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\right)$
6 neg1cn ${⊢}-1\in ℂ$
7 6 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to -1\in ℂ$
8 neg1ne0 ${⊢}-1\ne 0$
9 8 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to -1\ne 0$
10 2z ${⊢}2\in ℤ$
11 10 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to 2\in ℤ$
12 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to \frac{{R}}{2}\in ℤ$
13 expmulz ${⊢}\left(\left(-1\in ℂ\wedge -1\ne 0\right)\wedge \left(2\in ℤ\wedge \frac{{R}}{2}\in ℤ\right)\right)\to {\left(-1\right)}^{2\left(\frac{{R}}{2}\right)}={\left({-1}^{2}\right)}^{\frac{{R}}{2}}$
14 7 9 11 12 13 syl22anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{2\left(\frac{{R}}{2}\right)}={\left({-1}^{2}\right)}^{\frac{{R}}{2}}$
15 2 adantr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
16 15 eldifad ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}\in ℙ$
17 prmz ${⊢}{Q}\in ℙ\to {Q}\in ℤ$
18 16 17 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}\in ℤ$
19 elfzelz ${⊢}{x}\in \left(1\dots \frac{{P}-1}{2}\right)\to {x}\in ℤ$
20 19 adantl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {x}\in ℤ$
21 zmulcl ${⊢}\left(2\in ℤ\wedge {x}\in ℤ\right)\to 2{x}\in ℤ$
22 10 20 21 sylancr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 2{x}\in ℤ$
23 18 22 zmulcld ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}2{x}\in ℤ$
24 1 adantr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
25 24 eldifad ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in ℙ$
26 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
27 25 26 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in ℕ$
28 zmodfz ${⊢}\left({Q}2{x}\in ℤ\wedge {P}\in ℕ\right)\to {Q}2{x}\mathrm{mod}{P}\in \left(0\dots {P}-1\right)$
29 23 27 28 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}2{x}\mathrm{mod}{P}\in \left(0\dots {P}-1\right)$
30 4 29 eqeltrid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in \left(0\dots {P}-1\right)$
31 elfznn0 ${⊢}{R}\in \left(0\dots {P}-1\right)\to {R}\in {ℕ}_{0}$
32 30 31 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in {ℕ}_{0}$
33 32 nn0zd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in ℤ$
34 33 zcnd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in ℂ$
35 34 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {R}\in ℂ$
36 2cnd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to 2\in ℂ$
37 2ne0 ${⊢}2\ne 0$
38 37 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to 2\ne 0$
39 35 36 38 divcan2d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to 2\left(\frac{{R}}{2}\right)={R}$
40 39 oveq2d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{2\left(\frac{{R}}{2}\right)}={\left(-1\right)}^{{R}}$
41 neg1sqe1 ${⊢}{\left(-1\right)}^{2}=1$
42 41 oveq1i ${⊢}{\left({-1}^{2}\right)}^{\frac{{R}}{2}}={1}^{\frac{{R}}{2}}$
43 1exp ${⊢}\frac{{R}}{2}\in ℤ\to {1}^{\frac{{R}}{2}}=1$
44 43 adantl ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {1}^{\frac{{R}}{2}}=1$
45 42 44 syl5eq ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left({-1}^{2}\right)}^{\frac{{R}}{2}}=1$
46 14 40 45 3eqtr3d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}=1$
47 46 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}=1{R}$
48 35 mulid2d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to 1{R}={R}$
49 47 48 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}={R}$
50 49 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}={R}\mathrm{mod}{P}$
51 32 nn0red ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in ℝ$
52 27 nnrpd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in {ℝ}^{+}$
53 32 nn0ge0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0\le {R}$
54 23 zred ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}2{x}\in ℝ$
55 modlt ${⊢}\left({Q}2{x}\in ℝ\wedge {P}\in {ℝ}^{+}\right)\to {Q}2{x}\mathrm{mod}{P}<{P}$
56 54 52 55 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {Q}2{x}\mathrm{mod}{P}<{P}$
57 4 56 eqbrtrid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}<{P}$
58 modid ${⊢}\left(\left({R}\in ℝ\wedge {P}\in {ℝ}^{+}\right)\wedge \left(0\le {R}\wedge {R}<{P}\right)\right)\to {R}\mathrm{mod}{P}={R}$
59 51 52 53 57 58 syl22anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\mathrm{mod}{P}={R}$
60 59 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {R}\mathrm{mod}{P}={R}$
61 50 60 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}={R}$
62 61 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}=\frac{{R}}{2}$
63 62 12 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}}{2}\in ℤ\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℤ$
64 27 nncnd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in ℂ$
65 64 mulid2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 1{P}={P}$
66 65 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -{R}+1{P}=-{R}+{P}$
67 51 renegcld ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -{R}\in ℝ$
68 67 recnd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -{R}\in ℂ$
69 64 68 addcomd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}+\left(-{R}\right)=-{R}+{P}$
70 64 34 negsubd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}+\left(-{R}\right)={P}-{R}$
71 66 69 70 3eqtr2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -{R}+1{P}={P}-{R}$
72 71 oveq1d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(-{R}+1{P}\right)\mathrm{mod}{P}=\left({P}-{R}\right)\mathrm{mod}{P}$
73 1zzd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 1\in ℤ$
74 modcyc ${⊢}\left(-{R}\in ℝ\wedge {P}\in {ℝ}^{+}\wedge 1\in ℤ\right)\to \left(-{R}+1{P}\right)\mathrm{mod}{P}=\left(-{R}\right)\mathrm{mod}{P}$
75 67 52 73 74 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(-{R}+1{P}\right)\mathrm{mod}{P}=\left(-{R}\right)\mathrm{mod}{P}$
76 27 nnred ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in ℝ$
77 76 51 resubcld ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-{R}\in ℝ$
78 51 76 57 ltled ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\le {P}$
79 76 51 subge0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(0\le {P}-{R}↔{R}\le {P}\right)$
80 78 79 mpbird ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0\le {P}-{R}$
81 2nn ${⊢}2\in ℕ$
82 elfznn ${⊢}{x}\in \left(1\dots \frac{{P}-1}{2}\right)\to {x}\in ℕ$
83 82 adantl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {x}\in ℕ$
84 nnmulcl ${⊢}\left(2\in ℕ\wedge {x}\in ℕ\right)\to 2{x}\in ℕ$
85 81 83 84 sylancr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 2{x}\in ℕ$
86 elfzle2 ${⊢}{x}\in \left(1\dots \frac{{P}-1}{2}\right)\to {x}\le \frac{{P}-1}{2}$
87 86 adantl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {x}\le \frac{{P}-1}{2}$
88 83 nnred ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {x}\in ℝ$
89 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
90 uz2m1nn ${⊢}{P}\in {ℤ}_{\ge 2}\to {P}-1\in ℕ$
91 25 89 90 3syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-1\in ℕ$
92 91 nnred ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-1\in ℝ$
93 2re ${⊢}2\in ℝ$
94 93 a1i ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 2\in ℝ$
95 2pos ${⊢}0<2$
96 95 a1i ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0<2$
97 lemuldiv2 ${⊢}\left({x}\in ℝ\wedge {P}-1\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(2{x}\le {P}-1↔{x}\le \frac{{P}-1}{2}\right)$
98 88 92 94 96 97 syl112anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(2{x}\le {P}-1↔{x}\le \frac{{P}-1}{2}\right)$
99 87 98 mpbird ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 2{x}\le {P}-1$
100 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
101 25 100 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\in ℤ$
102 peano2zm ${⊢}{P}\in ℤ\to {P}-1\in ℤ$
103 fznn ${⊢}{P}-1\in ℤ\to \left(2{x}\in \left(1\dots {P}-1\right)↔\left(2{x}\in ℕ\wedge 2{x}\le {P}-1\right)\right)$
104 101 102 103 3syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(2{x}\in \left(1\dots {P}-1\right)↔\left(2{x}\in ℕ\wedge 2{x}\le {P}-1\right)\right)$
105 85 99 104 mpbir2and ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 2{x}\in \left(1\dots {P}-1\right)$
106 fzm1ndvds ${⊢}\left({P}\in ℕ\wedge 2{x}\in \left(1\dots {P}-1\right)\right)\to ¬{P}\parallel 2{x}$
107 27 105 106 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{P}\parallel 2{x}$
108 3 adantr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\ne {Q}$
109 prmrp ${⊢}\left({P}\in ℙ\wedge {Q}\in ℙ\right)\to \left({P}\mathrm{gcd}{Q}=1↔{P}\ne {Q}\right)$
110 25 16 109 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\mathrm{gcd}{Q}=1↔{P}\ne {Q}\right)$
111 108 110 mpbird ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}\mathrm{gcd}{Q}=1$
112 coprmdvds ${⊢}\left({P}\in ℤ\wedge {Q}\in ℤ\wedge 2{x}\in ℤ\right)\to \left(\left({P}\parallel {Q}2{x}\wedge {P}\mathrm{gcd}{Q}=1\right)\to {P}\parallel 2{x}\right)$
113 101 18 22 112 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\left({P}\parallel {Q}2{x}\wedge {P}\mathrm{gcd}{Q}=1\right)\to {P}\parallel 2{x}\right)$
114 111 113 mpan2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\parallel {Q}2{x}\to {P}\parallel 2{x}\right)$
115 107 114 mtod ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{P}\parallel {Q}2{x}$
116 dvdsval3 ${⊢}\left({P}\in ℕ\wedge {Q}2{x}\in ℤ\right)\to \left({P}\parallel {Q}2{x}↔{Q}2{x}\mathrm{mod}{P}=0\right)$
117 27 23 116 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\parallel {Q}2{x}↔{Q}2{x}\mathrm{mod}{P}=0\right)$
118 115 117 mtbid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{Q}2{x}\mathrm{mod}{P}=0$
119 4 eqeq1i ${⊢}{R}=0↔{Q}2{x}\mathrm{mod}{P}=0$
120 118 119 sylnibr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{R}=0$
121 91 nnnn0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-1\in {ℕ}_{0}$
122 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
123 121 122 eleqtrdi ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-1\in {ℤ}_{\ge 0}$
124 elfzp12 ${⊢}{P}-1\in {ℤ}_{\ge 0}\to \left({R}\in \left(0\dots {P}-1\right)↔\left({R}=0\vee {R}\in \left(0+1\dots {P}-1\right)\right)\right)$
125 123 124 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({R}\in \left(0\dots {P}-1\right)↔\left({R}=0\vee {R}\in \left(0+1\dots {P}-1\right)\right)\right)$
126 30 125 mpbid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({R}=0\vee {R}\in \left(0+1\dots {P}-1\right)\right)$
127 126 ord ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(¬{R}=0\to {R}\in \left(0+1\dots {P}-1\right)\right)$
128 120 127 mpd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in \left(0+1\dots {P}-1\right)$
129 1e0p1 ${⊢}1=0+1$
130 129 oveq1i ${⊢}\left(1\dots {P}-1\right)=\left(0+1\dots {P}-1\right)$
131 128 130 eleqtrrdi ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in \left(1\dots {P}-1\right)$
132 elfznn ${⊢}{R}\in \left(1\dots {P}-1\right)\to {R}\in ℕ$
133 131 132 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in ℕ$
134 133 nnrpd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}\in {ℝ}^{+}$
135 76 134 ltsubrpd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-{R}<{P}$
136 modid ${⊢}\left(\left({P}-{R}\in ℝ\wedge {P}\in {ℝ}^{+}\right)\wedge \left(0\le {P}-{R}\wedge {P}-{R}<{P}\right)\right)\to \left({P}-{R}\right)\mathrm{mod}{P}={P}-{R}$
137 77 52 80 135 136 syl22anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}-{R}\right)\mathrm{mod}{P}={P}-{R}$
138 72 75 137 3eqtr3d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(-{R}\right)\mathrm{mod}{P}={P}-{R}$
139 138 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \left(-{R}\right)\mathrm{mod}{P}={P}-{R}$
140 ax-1cn ${⊢}1\in ℂ$
141 140 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 1\in ℂ$
142 133 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {R}\in ℕ$
143 33 peano2zd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {R}+1\in ℤ$
144 dvdsval2 ${⊢}\left(2\in ℤ\wedge 2\ne 0\wedge {R}+1\in ℤ\right)\to \left(2\parallel \left({R}+1\right)↔\frac{{R}+1}{2}\in ℤ\right)$
145 10 37 143 144 mp3an12i ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(2\parallel \left({R}+1\right)↔\frac{{R}+1}{2}\in ℤ\right)$
146 145 biimpar ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 2\parallel \left({R}+1\right)$
147 33 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {R}\in ℤ$
148 81 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 2\in ℕ$
149 1lt2 ${⊢}1<2$
150 149 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 1<2$
151 ndvdsp1 ${⊢}\left({R}\in ℤ\wedge 2\in ℕ\wedge 1<2\right)\to \left(2\parallel {R}\to ¬2\parallel \left({R}+1\right)\right)$
152 147 148 150 151 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \left(2\parallel {R}\to ¬2\parallel \left({R}+1\right)\right)$
153 146 152 mt2d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to ¬2\parallel {R}$
154 oexpneg ${⊢}\left(1\in ℂ\wedge {R}\in ℕ\wedge ¬2\parallel {R}\right)\to {\left(-1\right)}^{{R}}=-{1}^{{R}}$
155 141 142 153 154 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}=-{1}^{{R}}$
156 1exp ${⊢}{R}\in ℤ\to {1}^{{R}}=1$
157 147 156 syl ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {1}^{{R}}=1$
158 157 negeqd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to -{1}^{{R}}=-1$
159 155 158 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}=-1$
160 159 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}=-1{R}$
161 34 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {R}\in ℂ$
162 161 mulm1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to -1{R}=-{R}$
163 160 162 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}=-{R}$
164 163 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=\left(-{R}\right)\mathrm{mod}{P}$
165 64 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}\in ℂ$
166 165 161 141 pnpcan2d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}+1-\left({R}+1\right)={P}-{R}$
167 139 164 166 3eqtr4d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}={P}+1-\left({R}+1\right)$
168 167 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}=\frac{{P}+1-\left({R}+1\right)}{2}$
169 peano2cn ${⊢}{P}\in ℂ\to {P}+1\in ℂ$
170 165 169 syl ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}+1\in ℂ$
171 peano2cn ${⊢}{R}\in ℂ\to {R}+1\in ℂ$
172 161 171 syl ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {R}+1\in ℂ$
173 2cnd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 2\in ℂ$
174 37 a1i ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to 2\ne 0$
175 170 172 173 174 divsubdird ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}+1-\left({R}+1\right)}{2}=\left(\frac{{P}+1}{2}\right)-\left(\frac{{R}+1}{2}\right)$
176 168 175 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}=\left(\frac{{P}+1}{2}\right)-\left(\frac{{R}+1}{2}\right)$
177 165 141 173 subadd23d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}-1+2={P}+2-1$
178 2m1e1 ${⊢}2-1=1$
179 178 oveq2i ${⊢}{P}+2-1={P}+1$
180 177 179 eqtr2di ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}+1={P}-1+2$
181 180 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}+1}{2}=\frac{{P}-1+2}{2}$
182 91 nncnd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {P}-1\in ℂ$
183 182 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to {P}-1\in ℂ$
184 183 173 173 174 divdird ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}-1+2}{2}=\left(\frac{{P}-1}{2}\right)+\left(\frac{2}{2}\right)$
185 2div2e1 ${⊢}\frac{2}{2}=1$
186 185 oveq2i ${⊢}\left(\frac{{P}-1}{2}\right)+\left(\frac{2}{2}\right)=\left(\frac{{P}-1}{2}\right)+1$
187 184 186 eqtrdi ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}-1+2}{2}=\left(\frac{{P}-1}{2}\right)+1$
188 181 187 eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}+1}{2}=\left(\frac{{P}-1}{2}\right)+1$
189 oddprm ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{P}-1}{2}\in ℕ$
190 24 189 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{P}-1}{2}\in ℕ$
191 190 nnzd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{P}-1}{2}\in ℤ$
192 191 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}-1}{2}\in ℤ$
193 192 peano2zd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \left(\frac{{P}-1}{2}\right)+1\in ℤ$
194 188 193 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{P}+1}{2}\in ℤ$
195 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{R}+1}{2}\in ℤ$
196 194 195 zsubcld ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \left(\frac{{P}+1}{2}\right)-\left(\frac{{R}+1}{2}\right)\in ℤ$
197 176 196 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge \frac{{R}+1}{2}\in ℤ\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℤ$
198 zeo ${⊢}{R}\in ℤ\to \left(\frac{{R}}{2}\in ℤ\vee \frac{{R}+1}{2}\in ℤ\right)$
199 33 198 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\frac{{R}}{2}\in ℤ\vee \frac{{R}+1}{2}\in ℤ\right)$
200 63 197 199 mpjaodan ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℤ$
201 m1expcl ${⊢}{R}\in ℤ\to {\left(-1\right)}^{{R}}\in ℤ$
202 33 201 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}\in ℤ$
203 202 33 zmulcld ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\in ℤ$
204 203 27 zmodcld ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in {ℕ}_{0}$
205 204 nn0red ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℝ$
206 fzm1ndvds ${⊢}\left({P}\in ℕ\wedge {R}\in \left(1\dots {P}-1\right)\right)\to ¬{P}\parallel {R}$
207 27 131 206 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{P}\parallel {R}$
208 ax-1ne0 ${⊢}1\ne 0$
209 divneg2 ${⊢}\left(1\in ℂ\wedge 1\in ℂ\wedge 1\ne 0\right)\to -\frac{1}{1}=\frac{1}{-1}$
210 140 140 208 209 mp3an ${⊢}-\frac{1}{1}=\frac{1}{-1}$
211 1div1e1 ${⊢}\frac{1}{1}=1$
212 211 negeqi ${⊢}-\frac{1}{1}=-1$
213 210 212 eqtr3i ${⊢}\frac{1}{-1}=-1$
214 213 oveq1i ${⊢}{\left(\frac{1}{-1}\right)}^{{R}}={\left(-1\right)}^{{R}}$
215 6 a1i ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -1\in ℂ$
216 8 a1i ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to -1\ne 0$
217 215 216 33 exprecd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(\frac{1}{-1}\right)}^{{R}}=\frac{1}{{\left(-1\right)}^{{R}}}$
218 214 217 syl5eqr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}=\frac{1}{{\left(-1\right)}^{{R}}}$
219 218 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}={\left(-1\right)}^{{R}}\left(\frac{1}{{\left(-1\right)}^{{R}}}\right)$
220 202 zcnd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}\in ℂ$
221 215 216 33 expne0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}\ne 0$
222 220 221 recidd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}\left(\frac{1}{{\left(-1\right)}^{{R}}}\right)=1$
223 219 222 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}=1$
224 223 oveq1d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}=1{R}$
225 220 220 34 mulassd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}={\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}$
226 34 mulid2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 1{R}={R}$
227 224 225 226 3eqtr3d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}={R}$
228 227 breq2d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\parallel {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}↔{P}\parallel {R}\right)$
229 207 228 mtbird ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{P}\parallel {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}$
230 dvdsmultr2 ${⊢}\left({P}\in ℤ\wedge {\left(-1\right)}^{{R}}\in ℤ\wedge {\left(-1\right)}^{{R}}{R}\in ℤ\right)\to \left({P}\parallel {\left(-1\right)}^{{R}}{R}\to {P}\parallel {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}\right)$
231 101 202 203 230 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\parallel {\left(-1\right)}^{{R}}{R}\to {P}\parallel {\left(-1\right)}^{{R}}{\left(-1\right)}^{{R}}{R}\right)$
232 229 231 mtod ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{P}\parallel {\left(-1\right)}^{{R}}{R}$
233 dvdsval3 ${⊢}\left({P}\in ℕ\wedge {\left(-1\right)}^{{R}}{R}\in ℤ\right)\to \left({P}\parallel {\left(-1\right)}^{{R}}{R}↔{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0\right)$
234 27 203 233 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({P}\parallel {\left(-1\right)}^{{R}}{R}↔{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0\right)$
235 232 234 mtbid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ¬{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0$
236 elnn0 ${⊢}{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in {ℕ}_{0}↔\left({\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℕ\vee {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0\right)$
237 204 236 sylib ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℕ\vee {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0\right)$
238 237 ord ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(¬{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℕ\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}=0\right)$
239 235 238 mt3d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℕ$
240 239 nngt0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0<{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}$
241 205 94 240 96 divgt0d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0<\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}$
242 elnnz ${⊢}\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℕ↔\left(\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℤ\wedge 0<\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\right)$
243 200 241 242 sylanbrc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℕ$
244 243 nnge1d ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 1\le \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}$
245 zmodfz ${⊢}\left({\left(-1\right)}^{{R}}{R}\in ℤ\wedge {P}\in ℕ\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in \left(0\dots {P}-1\right)$
246 203 27 245 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in \left(0\dots {P}-1\right)$
247 elfzle2 ${⊢}{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in \left(0\dots {P}-1\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\le {P}-1$
248 246 247 syl ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\le {P}-1$
249 lediv1 ${⊢}\left({\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\in ℝ\wedge {P}-1\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\le {P}-1↔\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\le \frac{{P}-1}{2}\right)$
250 205 92 94 96 249 syl112anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}\le {P}-1↔\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\le \frac{{P}-1}{2}\right)$
251 248 250 mpbid ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\le \frac{{P}-1}{2}$
252 elfz ${⊢}\left(\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in ℤ\wedge 1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\right)\to \left(\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in \left(1\dots \frac{{P}-1}{2}\right)↔\left(1\le \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\wedge \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\le \frac{{P}-1}{2}\right)\right)$
253 200 73 191 252 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in \left(1\dots \frac{{P}-1}{2}\right)↔\left(1\le \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\wedge \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\le \frac{{P}-1}{2}\right)\right)$
254 244 251 253 mpbir2and ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\in \left(1\dots \frac{{P}-1}{2}\right)$
255 254 5 fmptd ${⊢}{\phi }\to {M}:\left(1\dots \frac{{P}-1}{2}\right)⟶\left(1\dots \frac{{P}-1}{2}\right)$