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

Theorem lgsquad2lem1 26603
Description: Lemma for lgsquad2 26605. (Contributed by Mario Carneiro, 19-Jun-2015.)
Hypotheses
Ref Expression
lgsquad2.1 (𝜑𝑀 ∈ ℕ)
lgsquad2.2 (𝜑 → ¬ 2 ∥ 𝑀)
lgsquad2.3 (𝜑𝑁 ∈ ℕ)
lgsquad2.4 (𝜑 → ¬ 2 ∥ 𝑁)
lgsquad2.5 (𝜑 → (𝑀 gcd 𝑁) = 1)
lgsquad2lem1.a (𝜑𝐴 ∈ ℕ)
lgsquad2lem1.b (𝜑𝐵 ∈ ℕ)
lgsquad2lem1.m (𝜑 → (𝐴 · 𝐵) = 𝑀)
lgsquad2lem1.1 (𝜑 → ((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) = (-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))))
lgsquad2lem1.2 (𝜑 → ((𝐵 /L 𝑁) · (𝑁 /L 𝐵)) = (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
Assertion
Ref Expression
lgsquad2lem1 (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))

Proof of Theorem lgsquad2lem1
StepHypRef Expression
1 lgsquad2lem1.m . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) = 𝑀)
2 lgsquad2lem1.a . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℕ)
32nnzd 12495 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℤ)
43zcnd 12497 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℂ)
5 ax-1cn 10999 . . . . . . . . . . . . . 14 1 ∈ ℂ
6 npcan 11300 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 − 1) + 1) = 𝐴)
74, 5, 6sylancl 586 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 − 1) + 1) = 𝐴)
8 lgsquad2lem1.b . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℕ)
98nnzd 12495 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℤ)
109zcnd 12497 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℂ)
11 npcan 11300 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐵 − 1) + 1) = 𝐵)
1210, 5, 11sylancl 586 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 − 1) + 1) = 𝐵)
137, 12oveq12d 7331 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = (𝐴 · 𝐵))
14 peano2zm 12433 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
153, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 − 1) ∈ ℤ)
1615zcnd 12497 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 − 1) ∈ ℂ)
175a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
18 peano2zm 12433 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
199, 18syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℤ)
2019zcnd 12497 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℂ)
2116, 17, 20, 17muladdd 11503 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))))
22 1t1e1 12205 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
2322a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 1) = 1)
2423oveq2d 7329 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) = (((𝐴 − 1) · (𝐵 − 1)) + 1))
2516mulid1d 11062 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 − 1) · 1) = (𝐴 − 1))
2620mulid1d 11062 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 − 1) · 1) = (𝐵 − 1))
2725, 26oveq12d 7331 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1)) = ((𝐴 − 1) + (𝐵 − 1)))
2824, 27oveq12d 7331 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
2921, 28eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3013, 29eqtr3d 2779 . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
311, 30eqtr3d 2779 . . . . . . . . . 10 (𝜑𝑀 = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3231oveq1d 7328 . . . . . . . . 9 (𝜑 → (𝑀 − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1))
3316, 20mulcld 11065 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ)
34 addcl 11023 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3533, 5, 34sylancl 586 . . . . . . . . . 10 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3616, 20addcld 11064 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) + (𝐵 − 1)) ∈ ℂ)
3735, 36, 17addsubd 11423 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))))
38 pncan 11297 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
3933, 5, 38sylancl 586 . . . . . . . . . 10 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
4039oveq1d 7328 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4132, 37, 403eqtrd 2781 . . . . . . . 8 (𝜑 → (𝑀 − 1) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4241oveq1d 7328 . . . . . . 7 (𝜑 → ((𝑀 − 1) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2))
43 2cnd 12121 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
44 2ne0 12147 . . . . . . . . 9 2 ≠ 0
4544a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
4633, 36, 43, 45divdird 11859 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)))
4716, 20, 43, 45divassd 11856 . . . . . . . . 9 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
4816, 43, 45divcan2d 11823 . . . . . . . . . 10 (𝜑 → (2 · ((𝐴 − 1) / 2)) = (𝐴 − 1))
4948oveq1d 7328 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
50 lgsquad2.2 . . . . . . . . . . . . . 14 (𝜑 → ¬ 2 ∥ 𝑀)
51 dvdsmul1 16056 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
523, 9, 51syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∥ (𝐴 · 𝐵))
5352, 1breqtrd 5111 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑀)
54 2z 12422 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
55 lgsquad2.1 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5655nnzd 12495 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
57 dvdstr 16072 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5854, 3, 56, 57mp3an2i 1465 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5953, 58mpan2d 691 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐴 → 2 ∥ 𝑀))
6050, 59mtod 197 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐴)
61 1zzd 12421 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
62 2prm 16464 . . . . . . . . . . . . . 14 2 ∈ ℙ
63 nprmdvds1 16478 . . . . . . . . . . . . . 14 (2 ∈ ℙ → ¬ 2 ∥ 1)
6462, 63mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 1)
65 omoe 16142 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐴 − 1))
663, 60, 61, 64, 65syl22anc 836 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐴 − 1))
67 dvdsval2 16035 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐴 − 1) ∈ ℤ) → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6854, 45, 15, 67mp3an2i 1465 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6966, 68mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) / 2) ∈ ℤ)
7069zcnd 12497 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) / 2) ∈ ℂ)
71 dvdsmul2 16057 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∥ (𝐴 · 𝐵))
723, 9, 71syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∥ (𝐴 · 𝐵))
7372, 1breqtrd 5111 . . . . . . . . . . . . . . 15 (𝜑𝐵𝑀)
74 dvdstr 16072 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7554, 9, 56, 74mp3an2i 1465 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7673, 75mpan2d 691 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐵 → 2 ∥ 𝑀))
7750, 76mtod 197 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐵)
78 omoe 16142 . . . . . . . . . . . . 13 (((𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐵 − 1))
799, 77, 61, 64, 78syl22anc 836 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐵 − 1))
80 dvdsval2 16035 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐵 − 1) ∈ ℤ) → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8154, 45, 19, 80mp3an2i 1465 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8279, 81mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝐵 − 1) / 2) ∈ ℤ)
8382zcnd 12497 . . . . . . . . . 10 (𝜑 → ((𝐵 − 1) / 2) ∈ ℂ)
8443, 70, 83mulassd 11068 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8547, 49, 843eqtr2d 2783 . . . . . . . 8 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8616, 20, 43, 45divdird 11859 . . . . . . . 8 (𝜑 → (((𝐴 − 1) + (𝐵 − 1)) / 2) = (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)))
8785, 86oveq12d 7331 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8842, 46, 873eqtrd 2781 . . . . . 6 (𝜑 → ((𝑀 − 1) / 2) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8988oveq1d 7328 . . . . 5 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)))
9054a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
9169, 82zmulcld 12502 . . . . . . . 8 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℤ)
9290, 91zmulcld 12502 . . . . . . 7 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℤ)
9392zcnd 12497 . . . . . 6 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℂ)
9469, 82zaddcld 12500 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℤ)
9594zcnd 12497 . . . . . 6 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℂ)
96 lgsquad2.3 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
9796nnzd 12495 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
98 lgsquad2.4 . . . . . . . . 9 (𝜑 → ¬ 2 ∥ 𝑁)
99 omoe 16142 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1))
10097, 98, 61, 64, 99syl22anc 836 . . . . . . . 8 (𝜑 → 2 ∥ (𝑁 − 1))
101 peano2zm 12433 . . . . . . . . . 10 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10297, 101syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ ℤ)
103 dvdsval2 16035 . . . . . . . . 9 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
10454, 45, 102, 103mp3an2i 1465 . . . . . . . 8 (𝜑 → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
105100, 104mpbid 231 . . . . . . 7 (𝜑 → ((𝑁 − 1) / 2) ∈ ℤ)
106105zcnd 12497 . . . . . 6 (𝜑 → ((𝑁 − 1) / 2) ∈ ℂ)
10793, 95, 106adddird 11070 . . . . 5 (𝜑 → (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) = (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
10891zcnd 12497 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℂ)
10943, 108, 106mulassd 11068 . . . . . 6 (𝜑 → ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) = (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
110109oveq1d 7328 . . . . 5 (𝜑 → (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
11189, 107, 1103eqtrd 2781 . . . 4 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
112111oveq2d 7329 . . 3 (𝜑 → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
113 neg1cn 12157 . . . . . 6 -1 ∈ ℂ
114113a1i 11 . . . . 5 (𝜑 → -1 ∈ ℂ)
115 neg1ne0 12159 . . . . . 6 -1 ≠ 0
116115a1i 11 . . . . 5 (𝜑 → -1 ≠ 0)
11791, 105zmulcld 12502 . . . . . 6 (𝜑 → ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
11890, 117zmulcld 12502 . . . . 5 (𝜑 → (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℤ)
11994, 105zmulcld 12502 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
120 expaddz 13897 . . . . 5 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℤ ∧ ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)) → (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
121114, 116, 118, 119, 120syl22anc 836 . . . 4 (𝜑 → (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
122 expmulz 13899 . . . . . . 7 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)) → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
123114, 116, 90, 117, 122syl22anc 836 . . . . . 6 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
124 neg1sqe1 13983 . . . . . . . 8 (-1↑2) = 1
125124oveq1i 7323 . . . . . . 7 ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))
126 1exp 13882 . . . . . . . 8 (((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ → (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
127117, 126syl 17 . . . . . . 7 (𝜑 → (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
128125, 127eqtrid 2789 . . . . . 6 (𝜑 → ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
129123, 128eqtrd 2777 . . . . 5 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = 1)
130129oveq1d 7328 . . . 4 (𝜑 → ((-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
131121, 130eqtrd 2777 . . 3 (𝜑 → (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
132114, 116, 119expclzd 13939 . . . . 5 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℂ)
133132mulid2d 11063 . . . 4 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
13470, 83, 106adddird 11070 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) = ((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
135134oveq2d 7329 . . . 4 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
136133, 135eqtrd 2777 . . 3 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
137112, 131, 1363eqtrd 2781 . 2 (𝜑 → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
138 lgsquad2lem1.1 . . . 4 (𝜑 → ((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) = (-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))))
139 lgsquad2lem1.2 . . . 4 (𝜑 → ((𝐵 /L 𝑁) · (𝑁 /L 𝐵)) = (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
140138, 139oveq12d 7331 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
14169, 105zmulcld 12502 . . . 4 (𝜑 → (((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
14282, 105zmulcld 12502 . . . 4 (𝜑 → (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
143 expaddz 13897 . . . 4 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ ∧ (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)) → (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
144114, 116, 141, 142, 143syl22anc 836 . . 3 (𝜑 → (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
145140, 144eqtr4d 2780 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
146 lgscl 26530 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
1473, 97, 146syl2anc 584 . . . . 5 (𝜑 → (𝐴 /L 𝑁) ∈ ℤ)
148147zcnd 12497 . . . 4 (𝜑 → (𝐴 /L 𝑁) ∈ ℂ)
149 lgscl 26530 . . . . . 6 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈ ℤ)
1509, 97, 149syl2anc 584 . . . . 5 (𝜑 → (𝐵 /L 𝑁) ∈ ℤ)
151150zcnd 12497 . . . 4 (𝜑 → (𝐵 /L 𝑁) ∈ ℂ)
152 lgscl 26530 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 /L 𝐴) ∈ ℤ)
15397, 3, 152syl2anc 584 . . . . 5 (𝜑 → (𝑁 /L 𝐴) ∈ ℤ)
154153zcnd 12497 . . . 4 (𝜑 → (𝑁 /L 𝐴) ∈ ℂ)
155 lgscl 26530 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 /L 𝐵) ∈ ℤ)
15697, 9, 155syl2anc 584 . . . . 5 (𝜑 → (𝑁 /L 𝐵) ∈ ℤ)
157156zcnd 12497 . . . 4 (𝜑 → (𝑁 /L 𝐵) ∈ ℂ)
158148, 151, 154, 157mul4d 11257 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))))
1592nnne0d 12093 . . . . . 6 (𝜑𝐴 ≠ 0)
1608nnne0d 12093 . . . . . 6 (𝜑𝐵 ≠ 0)
161 lgsdir 26551 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1623, 9, 97, 159, 160, 161syl32anc 1377 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1631oveq1d 7328 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = (𝑀 /L 𝑁))
164162, 163eqtr3d 2779 . . . 4 (𝜑 → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (𝑀 /L 𝑁))
165 lgsdi 26553 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
16697, 3, 9, 159, 160, 165syl32anc 1377 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
1671oveq2d 7329 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = (𝑁 /L 𝑀))
168166, 167eqtr3d 2779 . . . 4 (𝜑 → ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)) = (𝑁 /L 𝑀))
169164, 168oveq12d 7331 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
170158, 169eqtr3d 2779 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
171137, 145, 1703eqtr2rd 2784 1 (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2941   class class class wbr 5085  (class class class)co 7313  cc 10939  0cc0 10941  1c1 10942   + caddc 10944   · cmul 10946  cmin 11275  -cneg 11276   / cdiv 11702  cn 12043  2c2 12098  cz 12389  cexp 13852  cdvds 16032   gcd cgcd 16270  cprime 16443   /L clgs 26513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5222  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017  ax-pre-mulgt0 11018  ax-pre-sup 11019
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-int 4891  df-iun 4937  df-br 5086  df-opab 5148  df-mpt 5169  df-tr 5203  df-id 5505  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5560  df-we 5562  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-pred 6222  df-ord 6289  df-on 6290  df-lim 6291  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-om 7756  df-1st 7874  df-2nd 7875  df-frecs 8142  df-wrecs 8173  df-recs 8247  df-rdg 8286  df-1o 8342  df-2o 8343  df-oadd 8346  df-er 8544  df-en 8780  df-dom 8781  df-sdom 8782  df-fin 8783  df-sup 9269  df-inf 9270  df-dju 9727  df-card 9765  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-sub 11277  df-neg 11278  df-div 11703  df-nn 12044  df-2 12106  df-3 12107  df-4 12108  df-5 12109  df-6 12110  df-7 12111  df-8 12112  df-9 12113  df-n0 12304  df-xnn0 12376  df-z 12390  df-uz 12653  df-q 12759  df-rp 12801  df-fz 13310  df-fzo 13453  df-fl 13582  df-mod 13660  df-seq 13792  df-exp 13853  df-hash 14115  df-cj 14879  df-re 14880  df-im 14881  df-sqrt 15015  df-abs 15016  df-dvds 16033  df-gcd 16271  df-prm 16444  df-phi 16534  df-pc 16605  df-lgs 26514
This theorem is referenced by:  lgsquad2lem2  26604
  Copyright terms: Public domain W3C validator