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 ⊢ φ → M gcd N = 1
lgsquad2lem2.f ⊢ φ ∧ m ∈ ℙ ∖ 2 ∧ m gcd N = 1 → m / L N ⁢ N / L m = − 1 m − 1 2 ⁢ N − 1 2
lgsquad2lem2.s ⊢ ψ ↔ ∀ x ∈ 1 … k x gcd 2 ⋅ N = 1 → x / L N ⁢ N / L x = − 1 x − 1 2 ⁢ N − 1 2
Assertion lgsquad2lem2 ⊢ φ → M / L N ⁢ N / L M = − 1 M − 1 2 ⁢ N − 1 2

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