# Metamath Proof Explorer

Description: Lemma for lgsquad2 . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgsquad2.1 ${⊢}{\phi }\to {M}\in ℕ$
lgsquad2.2 ${⊢}{\phi }\to ¬2\parallel {M}$
lgsquad2.3 ${⊢}{\phi }\to {N}\in ℕ$
lgsquad2.4 ${⊢}{\phi }\to ¬2\parallel {N}$
lgsquad2.5 ${⊢}{\phi }\to {M}\mathrm{gcd}{N}=1$
lgsquad2lem2.f ${⊢}\left({\phi }\wedge \left({m}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {m}\mathrm{gcd}{N}=1\right)\right)\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
lgsquad2lem2.s ${⊢}{\psi }↔\forall {x}\in \left(1\dots {k}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
Assertion lgsquad2lem2 ${⊢}{\phi }\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$

### Proof

Step Hyp Ref Expression
1 lgsquad2.1 ${⊢}{\phi }\to {M}\in ℕ$
2 lgsquad2.2 ${⊢}{\phi }\to ¬2\parallel {M}$
3 lgsquad2.3 ${⊢}{\phi }\to {N}\in ℕ$
4 lgsquad2.4 ${⊢}{\phi }\to ¬2\parallel {N}$
5 lgsquad2.5 ${⊢}{\phi }\to {M}\mathrm{gcd}{N}=1$
6 lgsquad2lem2.f ${⊢}\left({\phi }\wedge \left({m}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {m}\mathrm{gcd}{N}=1\right)\right)\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
7 lgsquad2lem2.s ${⊢}{\psi }↔\forall {x}\in \left(1\dots {k}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
8 2nn ${⊢}2\in ℕ$
9 8 a1i ${⊢}{\phi }\to 2\in ℕ$
10 1 nnzd ${⊢}{\phi }\to {M}\in ℤ$
11 2z ${⊢}2\in ℤ$
12 gcdcom ${⊢}\left({M}\in ℤ\wedge 2\in ℤ\right)\to {M}\mathrm{gcd}2=2\mathrm{gcd}{M}$
13 10 11 12 sylancl ${⊢}{\phi }\to {M}\mathrm{gcd}2=2\mathrm{gcd}{M}$
14 2prm ${⊢}2\in ℙ$
15 coprm ${⊢}\left(2\in ℙ\wedge {M}\in ℤ\right)\to \left(¬2\parallel {M}↔2\mathrm{gcd}{M}=1\right)$
16 14 10 15 sylancr ${⊢}{\phi }\to \left(¬2\parallel {M}↔2\mathrm{gcd}{M}=1\right)$
17 2 16 mpbid ${⊢}{\phi }\to 2\mathrm{gcd}{M}=1$
18 13 17 eqtrd ${⊢}{\phi }\to {M}\mathrm{gcd}2=1$
19 rpmulgcd ${⊢}\left(\left({M}\in ℕ\wedge 2\in ℕ\wedge {N}\in ℕ\right)\wedge {M}\mathrm{gcd}2=1\right)\to {M}\mathrm{gcd}2\cdot {N}={M}\mathrm{gcd}{N}$
20 1 9 3 18 19 syl31anc ${⊢}{\phi }\to {M}\mathrm{gcd}2\cdot {N}={M}\mathrm{gcd}{N}$
21 20 5 eqtrd ${⊢}{\phi }\to {M}\mathrm{gcd}2\cdot {N}=1$
22 oveq1 ${⊢}{m}=1\to {m}{/}_{L}{N}=1{/}_{L}{N}$
23 oveq2 ${⊢}{m}=1\to {N}{/}_{L}{m}={N}{/}_{L}1$
24 22 23 oveq12d ${⊢}{m}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)=\left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)$
25 oveq1 ${⊢}{m}=1\to {m}-1=1-1$
26 1m1e0 ${⊢}1-1=0$
27 25 26 eqtrdi ${⊢}{m}=1\to {m}-1=0$
28 27 oveq1d ${⊢}{m}=1\to \frac{{m}-1}{2}=\frac{0}{2}$
29 2cn ${⊢}2\in ℂ$
30 2ne0 ${⊢}2\ne 0$
31 29 30 div0i ${⊢}\frac{0}{2}=0$
32 28 31 eqtrdi ${⊢}{m}=1\to \frac{{m}-1}{2}=0$
33 32 oveq1d ${⊢}{m}=1\to \left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=0\cdot \left(\frac{{N}-1}{2}\right)$
34 33 oveq2d ${⊢}{m}=1\to {\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}$
35 24 34 eqeq12d ${⊢}{m}=1\to \left(\left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}↔\left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}\right)$
36 35 imbi2d ${⊢}{m}=1\to \left(\left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)↔\left({m}\mathrm{gcd}2\cdot {N}=1\to \left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}\right)\right)$
37 36 imbi2d ${⊢}{m}=1\to \left(\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)↔\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
38 oveq1 ${⊢}{m}={x}\to {m}\mathrm{gcd}2\cdot {N}={x}\mathrm{gcd}2\cdot {N}$
39 38 eqeq1d ${⊢}{m}={x}\to \left({m}\mathrm{gcd}2\cdot {N}=1↔{x}\mathrm{gcd}2\cdot {N}=1\right)$
40 oveq1 ${⊢}{m}={x}\to {m}{/}_{L}{N}={x}{/}_{L}{N}$
41 oveq2 ${⊢}{m}={x}\to {N}{/}_{L}{m}={N}{/}_{L}{x}$
42 40 41 oveq12d ${⊢}{m}={x}\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)=\left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)$
43 oveq1 ${⊢}{m}={x}\to {m}-1={x}-1$
44 43 oveq1d ${⊢}{m}={x}\to \frac{{m}-1}{2}=\frac{{x}-1}{2}$
45 44 oveq1d ${⊢}{m}={x}\to \left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
46 45 oveq2d ${⊢}{m}={x}\to {\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
47 42 46 eqeq12d ${⊢}{m}={x}\to \left(\left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}↔\left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
48 39 47 imbi12d ${⊢}{m}={x}\to \left(\left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)↔\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
49 48 imbi2d ${⊢}{m}={x}\to \left(\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)↔\left({\phi }\to \left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
50 oveq1 ${⊢}{m}={y}\to {m}\mathrm{gcd}2\cdot {N}={y}\mathrm{gcd}2\cdot {N}$
51 50 eqeq1d ${⊢}{m}={y}\to \left({m}\mathrm{gcd}2\cdot {N}=1↔{y}\mathrm{gcd}2\cdot {N}=1\right)$
52 oveq1 ${⊢}{m}={y}\to {m}{/}_{L}{N}={y}{/}_{L}{N}$
53 oveq2 ${⊢}{m}={y}\to {N}{/}_{L}{m}={N}{/}_{L}{y}$
54 52 53 oveq12d ${⊢}{m}={y}\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)=\left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)$
55 oveq1 ${⊢}{m}={y}\to {m}-1={y}-1$
56 55 oveq1d ${⊢}{m}={y}\to \frac{{m}-1}{2}=\frac{{y}-1}{2}$
57 56 oveq1d ${⊢}{m}={y}\to \left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
58 57 oveq2d ${⊢}{m}={y}\to {\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
59 54 58 eqeq12d ${⊢}{m}={y}\to \left(\left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}↔\left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
60 51 59 imbi12d ${⊢}{m}={y}\to \left(\left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)↔\left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
61 60 imbi2d ${⊢}{m}={y}\to \left(\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)↔\left({\phi }\to \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
62 oveq1 ${⊢}{m}={x}{y}\to {m}\mathrm{gcd}2\cdot {N}={x}{y}\mathrm{gcd}2\cdot {N}$
63 62 eqeq1d ${⊢}{m}={x}{y}\to \left({m}\mathrm{gcd}2\cdot {N}=1↔{x}{y}\mathrm{gcd}2\cdot {N}=1\right)$
64 oveq1 ${⊢}{m}={x}{y}\to {m}{/}_{L}{N}={x}{y}{/}_{L}{N}$
65 oveq2 ${⊢}{m}={x}{y}\to {N}{/}_{L}{m}={N}{/}_{L}{x}{y}$
66 64 65 oveq12d ${⊢}{m}={x}{y}\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)=\left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)$
67 oveq1 ${⊢}{m}={x}{y}\to {m}-1={x}{y}-1$
68 67 oveq1d ${⊢}{m}={x}{y}\to \frac{{m}-1}{2}=\frac{{x}{y}-1}{2}$
69 68 oveq1d ${⊢}{m}={x}{y}\to \left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
70 69 oveq2d ${⊢}{m}={x}{y}\to {\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
71 66 70 eqeq12d ${⊢}{m}={x}{y}\to \left(\left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}↔\left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
72 63 71 imbi12d ${⊢}{m}={x}{y}\to \left(\left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)↔\left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
73 72 imbi2d ${⊢}{m}={x}{y}\to \left(\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)↔\left({\phi }\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
74 oveq1 ${⊢}{m}={M}\to {m}\mathrm{gcd}2\cdot {N}={M}\mathrm{gcd}2\cdot {N}$
75 74 eqeq1d ${⊢}{m}={M}\to \left({m}\mathrm{gcd}2\cdot {N}=1↔{M}\mathrm{gcd}2\cdot {N}=1\right)$
76 oveq1 ${⊢}{m}={M}\to {m}{/}_{L}{N}={M}{/}_{L}{N}$
77 oveq2 ${⊢}{m}={M}\to {N}{/}_{L}{m}={N}{/}_{L}{M}$
78 76 77 oveq12d ${⊢}{m}={M}\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)$
79 oveq1 ${⊢}{m}={M}\to {m}-1={M}-1$
80 79 oveq1d ${⊢}{m}={M}\to \frac{{m}-1}{2}=\frac{{M}-1}{2}$
81 80 oveq1d ${⊢}{m}={M}\to \left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
82 81 oveq2d ${⊢}{m}={M}\to {\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
83 78 82 eqeq12d ${⊢}{m}={M}\to \left(\left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}↔\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
84 75 83 imbi12d ${⊢}{m}={M}\to \left(\left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)↔\left({M}\mathrm{gcd}2\cdot {N}=1\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
85 84 imbi2d ${⊢}{m}={M}\to \left(\left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)↔\left({\phi }\to \left({M}\mathrm{gcd}2\cdot {N}=1\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
86 1t1e1 ${⊢}1\cdot 1=1$
87 neg1cn ${⊢}-1\in ℂ$
88 exp0 ${⊢}-1\in ℂ\to {\left(-1\right)}^{0}=1$
89 87 88 ax-mp ${⊢}{\left(-1\right)}^{0}=1$
90 86 89 eqtr4i ${⊢}1\cdot 1={\left(-1\right)}^{0}$
91 sq1 ${⊢}{1}^{2}=1$
92 91 oveq1i ${⊢}{1}^{2}{/}_{L}{N}=1{/}_{L}{N}$
93 1z ${⊢}1\in ℤ$
94 ax-1ne0 ${⊢}1\ne 0$
95 93 94 pm3.2i ${⊢}\left(1\in ℤ\wedge 1\ne 0\right)$
96 3 nnzd ${⊢}{\phi }\to {N}\in ℤ$
97 1gcd ${⊢}{N}\in ℤ\to 1\mathrm{gcd}{N}=1$
98 96 97 syl ${⊢}{\phi }\to 1\mathrm{gcd}{N}=1$
99 lgssq ${⊢}\left(\left(1\in ℤ\wedge 1\ne 0\right)\wedge {N}\in ℤ\wedge 1\mathrm{gcd}{N}=1\right)\to {1}^{2}{/}_{L}{N}=1$
100 95 96 98 99 mp3an2i ${⊢}{\phi }\to {1}^{2}{/}_{L}{N}=1$
101 92 100 syl5eqr ${⊢}{\phi }\to 1{/}_{L}{N}=1$
102 91 oveq2i ${⊢}{N}{/}_{L}{1}^{2}={N}{/}_{L}1$
103 1nn ${⊢}1\in ℕ$
104 103 a1i ${⊢}{\phi }\to 1\in ℕ$
105 gcd1 ${⊢}{N}\in ℤ\to {N}\mathrm{gcd}1=1$
106 96 105 syl ${⊢}{\phi }\to {N}\mathrm{gcd}1=1$
107 lgssq2 ${⊢}\left({N}\in ℤ\wedge 1\in ℕ\wedge {N}\mathrm{gcd}1=1\right)\to {N}{/}_{L}{1}^{2}=1$
108 96 104 106 107 syl3anc ${⊢}{\phi }\to {N}{/}_{L}{1}^{2}=1$
109 102 108 syl5eqr ${⊢}{\phi }\to {N}{/}_{L}1=1$
110 101 109 oveq12d ${⊢}{\phi }\to \left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)=1\cdot 1$
111 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
112 3 111 syl ${⊢}{\phi }\to {N}-1\in {ℕ}_{0}$
113 112 nn0cnd ${⊢}{\phi }\to {N}-1\in ℂ$
114 113 halfcld ${⊢}{\phi }\to \frac{{N}-1}{2}\in ℂ$
115 114 mul02d ${⊢}{\phi }\to 0\cdot \left(\frac{{N}-1}{2}\right)=0$
116 115 oveq2d ${⊢}{\phi }\to {\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{0}$
117 90 110 116 3eqtr4a ${⊢}{\phi }\to \left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}$
118 117 a1d ${⊢}{\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left(1{/}_{L}{N}\right)\left({N}{/}_{L}1\right)={\left(-1\right)}^{0\cdot \left(\frac{{N}-1}{2}\right)}\right)$
119 simprl ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\in ℙ$
120 prmz ${⊢}{m}\in ℙ\to {m}\in ℤ$
121 120 ad2antrl ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\in ℤ$
122 11 a1i ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to 2\in ℤ$
123 3 adantr ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {N}\in ℕ$
124 123 nnzd ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {N}\in ℤ$
125 zmulcl ${⊢}\left(2\in ℤ\wedge {N}\in ℤ\right)\to 2\cdot {N}\in ℤ$
126 11 124 125 sylancr ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to 2\cdot {N}\in ℤ$
127 simprr ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\mathrm{gcd}2\cdot {N}=1$
128 dvdsmul1 ${⊢}\left(2\in ℤ\wedge {N}\in ℤ\right)\to 2\parallel 2\cdot {N}$
129 11 124 128 sylancr ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to 2\parallel 2\cdot {N}$
130 rpdvds ${⊢}\left(\left({m}\in ℤ\wedge 2\in ℤ\wedge 2\cdot {N}\in ℤ\right)\wedge \left({m}\mathrm{gcd}2\cdot {N}=1\wedge 2\parallel 2\cdot {N}\right)\right)\to {m}\mathrm{gcd}2=1$
131 121 122 126 127 129 130 syl32anc ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\mathrm{gcd}2=1$
132 prmrp ${⊢}\left({m}\in ℙ\wedge 2\in ℙ\right)\to \left({m}\mathrm{gcd}2=1↔{m}\ne 2\right)$
133 119 14 132 sylancl ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to \left({m}\mathrm{gcd}2=1↔{m}\ne 2\right)$
134 131 133 mpbid ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\ne 2$
135 eldifsn ${⊢}{m}\in \left(ℙ\setminus \left\{2\right\}\right)↔\left({m}\in ℙ\wedge {m}\ne 2\right)$
136 119 134 135 sylanbrc ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\in \left(ℙ\setminus \left\{2\right\}\right)$
137 prmnn ${⊢}{m}\in ℙ\to {m}\in ℕ$
138 137 ad2antrl ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\in ℕ$
139 8 a1i ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to 2\in ℕ$
140 rpmulgcd ${⊢}\left(\left({m}\in ℕ\wedge 2\in ℕ\wedge {N}\in ℕ\right)\wedge {m}\mathrm{gcd}2=1\right)\to {m}\mathrm{gcd}2\cdot {N}={m}\mathrm{gcd}{N}$
141 138 139 123 131 140 syl31anc ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\mathrm{gcd}2\cdot {N}={m}\mathrm{gcd}{N}$
142 141 127 eqtr3d ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to {m}\mathrm{gcd}{N}=1$
143 136 142 jca ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to \left({m}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {m}\mathrm{gcd}{N}=1\right)$
144 143 6 syldan ${⊢}\left({\phi }\wedge \left({m}\in ℙ\wedge {m}\mathrm{gcd}2\cdot {N}=1\right)\right)\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
145 144 exp32 ${⊢}{\phi }\to \left({m}\in ℙ\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
146 145 com12 ${⊢}{m}\in ℙ\to \left({\phi }\to \left({m}\mathrm{gcd}2\cdot {N}=1\to \left({m}{/}_{L}{N}\right)\left({N}{/}_{L}{m}\right)={\left(-1\right)}^{\left(\frac{{m}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
147 jcab ${⊢}\left({\phi }\to \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)↔\left(\left({\phi }\to \left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\wedge \left({\phi }\to \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
148 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}\in {ℤ}_{\ge 2}$
149 eluz2nn ${⊢}{x}\in {ℤ}_{\ge 2}\to {x}\in ℕ$
150 148 149 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}\in ℕ$
151 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {y}\in {ℤ}_{\ge 2}$
152 eluz2nn ${⊢}{y}\in {ℤ}_{\ge 2}\to {y}\in ℕ$
153 151 152 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {y}\in ℕ$
154 150 153 nnmulcld ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}{y}\in ℕ$
155 n2dvds1 ${⊢}¬2\parallel 1$
156 96 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {N}\in ℤ$
157 11 156 128 sylancr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\parallel 2\cdot {N}$
158 eluzelz ${⊢}{x}\in {ℤ}_{\ge 2}\to {x}\in ℤ$
159 eluzelz ${⊢}{y}\in {ℤ}_{\ge 2}\to {y}\in ℤ$
160 158 159 anim12i ${⊢}\left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\to \left({x}\in ℤ\wedge {y}\in ℤ\right)$
161 160 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to \left({x}\in ℤ\wedge {y}\in ℤ\right)$
162 zmulcl ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {x}{y}\in ℤ$
163 161 162 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}{y}\in ℤ$
164 11 156 125 sylancr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\cdot {N}\in ℤ$
165 dvdsgcd ${⊢}\left(2\in ℤ\wedge {x}{y}\in ℤ\wedge 2\cdot {N}\in ℤ\right)\to \left(\left(2\parallel {x}{y}\wedge 2\parallel 2\cdot {N}\right)\to 2\parallel \left({x}{y}\mathrm{gcd}2\cdot {N}\right)\right)$
166 11 163 164 165 mp3an2i ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to \left(\left(2\parallel {x}{y}\wedge 2\parallel 2\cdot {N}\right)\to 2\parallel \left({x}{y}\mathrm{gcd}2\cdot {N}\right)\right)$
167 157 166 mpan2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to \left(2\parallel {x}{y}\to 2\parallel \left({x}{y}\mathrm{gcd}2\cdot {N}\right)\right)$
168 simpr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}{y}\mathrm{gcd}2\cdot {N}=1$
169 168 breq2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to \left(2\parallel \left({x}{y}\mathrm{gcd}2\cdot {N}\right)↔2\parallel 1\right)$
170 167 169 sylibd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to \left(2\parallel {x}{y}\to 2\parallel 1\right)$
171 155 170 mtoi ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to ¬2\parallel {x}{y}$
172 171 adantrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to ¬2\parallel {x}{y}$
173 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {N}\in ℕ$
174 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to ¬2\parallel {N}$
175 dvdsmul2 ${⊢}\left(2\in ℤ\wedge {N}\in ℤ\right)\to {N}\parallel 2\cdot {N}$
176 11 156 175 sylancr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {N}\parallel 2\cdot {N}$
177 rpdvds ${⊢}\left(\left({x}{y}\in ℤ\wedge {N}\in ℤ\wedge 2\cdot {N}\in ℤ\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge {N}\parallel 2\cdot {N}\right)\right)\to {x}{y}\mathrm{gcd}{N}=1$
178 163 156 164 168 176 177 syl32anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}{y}\mathrm{gcd}{N}=1$
179 178 adantrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}{y}\mathrm{gcd}{N}=1$
180 eqidd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}{y}={x}{y}$
181 161 simpld ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}\in ℤ$
182 gcdcom ${⊢}\left({x}\in ℤ\wedge 2\cdot {N}\in ℤ\right)\to {x}\mathrm{gcd}2\cdot {N}=2\cdot {N}\mathrm{gcd}{x}$
183 181 164 182 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}\mathrm{gcd}2\cdot {N}=2\cdot {N}\mathrm{gcd}{x}$
184 gcdcom ${⊢}\left(2\cdot {N}\in ℤ\wedge {x}{y}\in ℤ\right)\to 2\cdot {N}\mathrm{gcd}{x}{y}={x}{y}\mathrm{gcd}2\cdot {N}$
185 164 163 184 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\cdot {N}\mathrm{gcd}{x}{y}={x}{y}\mathrm{gcd}2\cdot {N}$
186 185 168 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\cdot {N}\mathrm{gcd}{x}{y}=1$
187 dvdsmul1 ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {x}\parallel {x}{y}$
188 161 187 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}\parallel {x}{y}$
189 rpdvds ${⊢}\left(\left(2\cdot {N}\in ℤ\wedge {x}\in ℤ\wedge {x}{y}\in ℤ\right)\wedge \left(2\cdot {N}\mathrm{gcd}{x}{y}=1\wedge {x}\parallel {x}{y}\right)\right)\to 2\cdot {N}\mathrm{gcd}{x}=1$
190 164 181 163 186 188 189 syl32anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\cdot {N}\mathrm{gcd}{x}=1$
191 183 190 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {x}\mathrm{gcd}2\cdot {N}=1$
192 191 adantrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {x}\mathrm{gcd}2\cdot {N}=1$
193 simprrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to \left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
194 192 193 mpd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
195 161 simprd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {y}\in ℤ$
196 gcdcom ${⊢}\left({y}\in ℤ\wedge 2\cdot {N}\in ℤ\right)\to {y}\mathrm{gcd}2\cdot {N}=2\cdot {N}\mathrm{gcd}{y}$
197 195 164 196 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {y}\mathrm{gcd}2\cdot {N}=2\cdot {N}\mathrm{gcd}{y}$
198 dvdsmul2 ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {y}\parallel {x}{y}$
199 161 198 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {y}\parallel {x}{y}$
200 rpdvds ${⊢}\left(\left(2\cdot {N}\in ℤ\wedge {y}\in ℤ\wedge {x}{y}\in ℤ\right)\wedge \left(2\cdot {N}\mathrm{gcd}{x}{y}=1\wedge {y}\parallel {x}{y}\right)\right)\to 2\cdot {N}\mathrm{gcd}{y}=1$
201 164 195 163 186 199 200 syl32anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to 2\cdot {N}\mathrm{gcd}{y}=1$
202 197 201 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge {x}{y}\mathrm{gcd}2\cdot {N}=1\right)\to {y}\mathrm{gcd}2\cdot {N}=1$
203 202 adantrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to {y}\mathrm{gcd}2\cdot {N}=1$
204 simprrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
205 203 204 mpd ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
206 154 172 173 174 179 150 153 180 194 205 lgsquad2lem1 ${⊢}\left(\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\wedge \left({x}{y}\mathrm{gcd}2\cdot {N}=1\wedge \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\right)\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
207 206 exp32 ${⊢}\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left(\left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
208 207 com23 ${⊢}\left({\phi }\wedge \left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\right)\to \left(\left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
209 208 expcom ${⊢}\left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\to \left({\phi }\to \left(\left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
210 209 a2d ${⊢}\left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\to \left(\left({\phi }\to \left(\left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\wedge \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\to \left({\phi }\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
211 147 210 syl5bir ${⊢}\left({x}\in {ℤ}_{\ge 2}\wedge {y}\in {ℤ}_{\ge 2}\right)\to \left(\left(\left({\phi }\to \left({x}\mathrm{gcd}2\cdot {N}=1\to \left({x}{/}_{L}{N}\right)\left({N}{/}_{L}{x}\right)={\left(-1\right)}^{\left(\frac{{x}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\wedge \left({\phi }\to \left({y}\mathrm{gcd}2\cdot {N}=1\to \left({y}{/}_{L}{N}\right)\left({N}{/}_{L}{y}\right)={\left(-1\right)}^{\left(\frac{{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)\to \left({\phi }\to \left({x}{y}\mathrm{gcd}2\cdot {N}=1\to \left({x}{y}{/}_{L}{N}\right)\left({N}{/}_{L}{x}{y}\right)={\left(-1\right)}^{\left(\frac{{x}{y}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)\right)$
212 37 49 61 73 85 118 146 211 prmind ${⊢}{M}\in ℕ\to \left({\phi }\to \left({M}\mathrm{gcd}2\cdot {N}=1\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)\right)$
213 1 212 mpcom ${⊢}{\phi }\to \left({M}\mathrm{gcd}2\cdot {N}=1\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\right)$
214 21 213 mpd ${⊢}{\phi }\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$