Metamath Proof Explorer

Theorem lgsquad2lem2

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

Ref Expression
Hypotheses lgsquad2.1 ⊢φ→M∈ℕ
lgsquad2.2 ⊢φ→¬2∥M
lgsquad2.3 ⊢φ→N∈ℕ
lgsquad2.4 ⊢φ→¬2∥N
lgsquad2.5 ⊢φ→MgcdN=1
lgsquad2lem2.f ⊢φ∧m∈ℙ∖2∧mgcdN=1→m/LN⁢N/Lm=−1m−12⁢N−12
lgsquad2lem2.s ⊢ψ↔∀x∈1…kxgcd2⋅ N=1→x/LN⁢N/Lx=−1x−12⁢N−12
Assertion lgsquad2lem2 ⊢φ→M/LN⁢N/LM=−1M−12⁢N−12

Proof

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