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

Theorem lgsquad2lem1 25004
Description: Lemma for lgsquad2 25006. (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 11425 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℤ)
43zcnd 11427 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℂ)
5 ax-1cn 9939 . . . . . . . . . . . . . 14 1 ∈ ℂ
6 npcan 10235 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 − 1) + 1) = 𝐴)
74, 5, 6sylancl 693 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 − 1) + 1) = 𝐴)
8 lgsquad2lem1.b . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℕ)
98nnzd 11425 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℤ)
109zcnd 11427 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℂ)
11 npcan 10235 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐵 − 1) + 1) = 𝐵)
1210, 5, 11sylancl 693 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 − 1) + 1) = 𝐵)
137, 12oveq12d 6623 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = (𝐴 · 𝐵))
14 peano2zm 11365 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
153, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 − 1) ∈ ℤ)
1615zcnd 11427 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 − 1) ∈ ℂ)
175a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
18 peano2zm 11365 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
199, 18syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℤ)
2019zcnd 11427 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℂ)
2116, 17, 20, 17muladdd 10434 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))))
22 1t1e1 11120 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
2322a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 1) = 1)
2423oveq2d 6621 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) = (((𝐴 − 1) · (𝐵 − 1)) + 1))
2516mulid1d 10002 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 − 1) · 1) = (𝐴 − 1))
2620mulid1d 10002 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 − 1) · 1) = (𝐵 − 1))
2725, 26oveq12d 6623 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1)) = ((𝐴 − 1) + (𝐵 − 1)))
2824, 27oveq12d 6623 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
2921, 28eqtrd 2660 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3013, 29eqtr3d 2662 . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
311, 30eqtr3d 2662 . . . . . . . . . 10 (𝜑𝑀 = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3231oveq1d 6620 . . . . . . . . 9 (𝜑 → (𝑀 − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1))
3316, 20mulcld 10005 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ)
34 addcl 9963 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3533, 5, 34sylancl 693 . . . . . . . . . 10 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3616, 20addcld 10004 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) + (𝐵 − 1)) ∈ ℂ)
3735, 36, 17addsubd 10358 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))))
38 pncan 10232 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
3933, 5, 38sylancl 693 . . . . . . . . . 10 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
4039oveq1d 6620 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4132, 37, 403eqtrd 2664 . . . . . . . 8 (𝜑 → (𝑀 − 1) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4241oveq1d 6620 . . . . . . 7 (𝜑 → ((𝑀 − 1) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2))
43 2cnd 11038 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
44 2ne0 11058 . . . . . . . . 9 2 ≠ 0
4544a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
4633, 36, 43, 45divdird 10784 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)))
4716, 20, 43, 45divassd 10781 . . . . . . . . 9 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
4816, 43, 45divcan2d 10748 . . . . . . . . . 10 (𝜑 → (2 · ((𝐴 − 1) / 2)) = (𝐴 − 1))
4948oveq1d 6620 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
50 lgsquad2.2 . . . . . . . . . . . . . 14 (𝜑 → ¬ 2 ∥ 𝑀)
51 dvdsmul1 14922 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
523, 9, 51syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∥ (𝐴 · 𝐵))
5352, 1breqtrd 4644 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑀)
54 2z 11354 . . . . . . . . . . . . . . . . 17 2 ∈ ℤ
5554a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℤ)
56 lgsquad2.1 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5756nnzd 11425 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
58 dvdstr 14937 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5955, 3, 57, 58syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
6053, 59mpan2d 709 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐴 → 2 ∥ 𝑀))
6150, 60mtod 189 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐴)
62 1zzd 11353 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
63 2prm 15324 . . . . . . . . . . . . . 14 2 ∈ ℙ
64 nprmdvds1 15337 . . . . . . . . . . . . . 14 (2 ∈ ℙ → ¬ 2 ∥ 1)
6563, 64mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 1)
66 omoe 15007 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐴 − 1))
673, 61, 62, 65, 66syl22anc 1324 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐴 − 1))
68 dvdsval2 14905 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐴 − 1) ∈ ℤ) → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6955, 45, 15, 68syl3anc 1323 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
7067, 69mpbid 222 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) / 2) ∈ ℤ)
7170zcnd 11427 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) / 2) ∈ ℂ)
72 dvdsmul2 14923 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∥ (𝐴 · 𝐵))
733, 9, 72syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∥ (𝐴 · 𝐵))
7473, 1breqtrd 4644 . . . . . . . . . . . . . . 15 (𝜑𝐵𝑀)
75 dvdstr 14937 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7655, 9, 57, 75syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7774, 76mpan2d 709 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐵 → 2 ∥ 𝑀))
7850, 77mtod 189 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐵)
79 omoe 15007 . . . . . . . . . . . . 13 (((𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐵 − 1))
809, 78, 62, 65, 79syl22anc 1324 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐵 − 1))
81 dvdsval2 14905 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐵 − 1) ∈ ℤ) → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8255, 45, 19, 81syl3anc 1323 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8380, 82mpbid 222 . . . . . . . . . . 11 (𝜑 → ((𝐵 − 1) / 2) ∈ ℤ)
8483zcnd 11427 . . . . . . . . . 10 (𝜑 → ((𝐵 − 1) / 2) ∈ ℂ)
8543, 71, 84mulassd 10008 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8647, 49, 853eqtr2d 2666 . . . . . . . 8 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8716, 20, 43, 45divdird 10784 . . . . . . . 8 (𝜑 → (((𝐴 − 1) + (𝐵 − 1)) / 2) = (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)))
8886, 87oveq12d 6623 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8942, 46, 883eqtrd 2664 . . . . . 6 (𝜑 → ((𝑀 − 1) / 2) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
9089oveq1d 6620 . . . . 5 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)))
9170, 83zmulcld 11432 . . . . . . . 8 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℤ)
9255, 91zmulcld 11432 . . . . . . 7 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℤ)
9392zcnd 11427 . . . . . 6 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℂ)
9470, 83zaddcld 11430 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℤ)
9594zcnd 11427 . . . . . 6 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℂ)
96 lgsquad2.3 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
9796nnzd 11425 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
98 lgsquad2.4 . . . . . . . . 9 (𝜑 → ¬ 2 ∥ 𝑁)
99 omoe 15007 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1))
10097, 98, 62, 65, 99syl22anc 1324 . . . . . . . 8 (𝜑 → 2 ∥ (𝑁 − 1))
101 peano2zm 11365 . . . . . . . . . 10 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10297, 101syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ ℤ)
103 dvdsval2 14905 . . . . . . . . 9 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
10455, 45, 102, 103syl3anc 1323 . . . . . . . 8 (𝜑 → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
105100, 104mpbid 222 . . . . . . 7 (𝜑 → ((𝑁 − 1) / 2) ∈ ℤ)
106105zcnd 11427 . . . . . 6 (𝜑 → ((𝑁 − 1) / 2) ∈ ℂ)
10793, 95, 106adddird 10010 . . . . 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 11427 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℂ)
10943, 108, 106mulassd 10008 . . . . . 6 (𝜑 → ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) = (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
110109oveq1d 6620 . . . . 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))))
11190, 107, 1103eqtrd 2664 . . . 4 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
112111oveq2d 6621 . . 3 (𝜑 → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
113 neg1cn 11069 . . . . . 6 -1 ∈ ℂ
114113a1i 11 . . . . 5 (𝜑 → -1 ∈ ℂ)
115 neg1ne0 11071 . . . . . 6 -1 ≠ 0
116115a1i 11 . . . . 5 (𝜑 → -1 ≠ 0)
11791, 105zmulcld 11432 . . . . . 6 (𝜑 → ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
11855, 117zmulcld 11432 . . . . 5 (𝜑 → (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℤ)
11994, 105zmulcld 11432 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
120 expaddz 12841 . . . . 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 1324 . . . 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 12843 . . . . . . 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, 55, 117, 122syl22anc 1324 . . . . . 6 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
124 neg1sqe1 12896 . . . . . . . 8 (-1↑2) = 1
125124oveq1i 6615 . . . . . . 7 ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))
126 1exp 12826 . . . . . . . 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, 127syl5eq 2672 . . . . . 6 (𝜑 → ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
129123, 128eqtrd 2660 . . . . 5 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = 1)
130129oveq1d 6620 . . . 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 2660 . . 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 12950 . . . . 5 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℂ)
133132mulid2d 10003 . . . 4 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
13471, 84, 106adddird 10010 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) = ((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
135134oveq2d 6621 . . . 4 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
136133, 135eqtrd 2660 . . 3 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
137112, 131, 1363eqtrd 2664 . 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 6623 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
14170, 105zmulcld 11432 . . . 4 (𝜑 → (((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
14283, 105zmulcld 11432 . . . 4 (𝜑 → (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
143 expaddz 12841 . . . 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 1324 . . 3 (𝜑 → (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
145140, 144eqtr4d 2663 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
146 lgscl 24931 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
1473, 97, 146syl2anc 692 . . . . 5 (𝜑 → (𝐴 /L 𝑁) ∈ ℤ)
148147zcnd 11427 . . . 4 (𝜑 → (𝐴 /L 𝑁) ∈ ℂ)
149 lgscl 24931 . . . . . 6 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈ ℤ)
1509, 97, 149syl2anc 692 . . . . 5 (𝜑 → (𝐵 /L 𝑁) ∈ ℤ)
151150zcnd 11427 . . . 4 (𝜑 → (𝐵 /L 𝑁) ∈ ℂ)
152 lgscl 24931 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 /L 𝐴) ∈ ℤ)
15397, 3, 152syl2anc 692 . . . . 5 (𝜑 → (𝑁 /L 𝐴) ∈ ℤ)
154153zcnd 11427 . . . 4 (𝜑 → (𝑁 /L 𝐴) ∈ ℂ)
155 lgscl 24931 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 /L 𝐵) ∈ ℤ)
15697, 9, 155syl2anc 692 . . . . 5 (𝜑 → (𝑁 /L 𝐵) ∈ ℤ)
157156zcnd 11427 . . . 4 (𝜑 → (𝑁 /L 𝐵) ∈ ℂ)
158148, 151, 154, 157mul4d 10193 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))))
1592nnne0d 11010 . . . . . 6 (𝜑𝐴 ≠ 0)
1608nnne0d 11010 . . . . . 6 (𝜑𝐵 ≠ 0)
161 lgsdir 24952 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1623, 9, 97, 159, 160, 161syl32anc 1331 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1631oveq1d 6620 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = (𝑀 /L 𝑁))
164162, 163eqtr3d 2662 . . . 4 (𝜑 → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (𝑀 /L 𝑁))
165 lgsdi 24954 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
16697, 3, 9, 159, 160, 165syl32anc 1331 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
1671oveq2d 6621 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = (𝑁 /L 𝑀))
168166, 167eqtr3d 2662 . . . 4 (𝜑 → ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)) = (𝑁 /L 𝑀))
169164, 168oveq12d 6623 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
170158, 169eqtr3d 2662 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
171137, 145, 1703eqtr2rd 2667 1 (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wne 2796   class class class wbr 4618  (class class class)co 6605  cc 9879  0cc0 9881  1c1 9882   + caddc 9884   · cmul 9886  cmin 10211  -cneg 10212   / cdiv 10629  cn 10965  2c2 11015  cz 11322  cexp 12797  cdvds 14902   gcd cgcd 15135  cprime 15304   /L clgs 24914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-card 8710  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-4 11026  df-5 11027  df-6 11028  df-7 11029  df-8 11030  df-9 11031  df-n0 11238  df-xnn0 11309  df-z 11323  df-uz 11632  df-q 11733  df-rp 11777  df-fz 12266  df-fzo 12404  df-fl 12530  df-mod 12606  df-seq 12739  df-exp 12798  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-dvds 14903  df-gcd 15136  df-prm 15305  df-phi 15390  df-pc 15461  df-lgs 24915
This theorem is referenced by:  lgsquad2lem2  25005
  Copyright terms: Public domain W3C validator