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

Theorem lgsquad2lem1 25197
Description: Lemma for lgsquad2 25199. (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 11562 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℤ)
43zcnd 11564 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℂ)
5 ax-1cn 10075 . . . . . . . . . . . . . 14 1 ∈ ℂ
6 npcan 10371 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 − 1) + 1) = 𝐴)
74, 5, 6sylancl 697 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 − 1) + 1) = 𝐴)
8 lgsquad2lem1.b . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℕ)
98nnzd 11562 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℤ)
109zcnd 11564 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℂ)
11 npcan 10371 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐵 − 1) + 1) = 𝐵)
1210, 5, 11sylancl 697 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 − 1) + 1) = 𝐵)
137, 12oveq12d 6751 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = (𝐴 · 𝐵))
14 peano2zm 11501 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
153, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 − 1) ∈ ℤ)
1615zcnd 11564 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 − 1) ∈ ℂ)
175a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
18 peano2zm 11501 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
199, 18syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℤ)
2019zcnd 11564 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℂ)
2116, 17, 20, 17muladdd 10570 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))))
22 1t1e1 11256 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
2322a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 1) = 1)
2423oveq2d 6749 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) = (((𝐴 − 1) · (𝐵 − 1)) + 1))
2516mulid1d 10138 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 − 1) · 1) = (𝐴 − 1))
2620mulid1d 10138 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 − 1) · 1) = (𝐵 − 1))
2725, 26oveq12d 6751 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1)) = ((𝐴 − 1) + (𝐵 − 1)))
2824, 27oveq12d 6751 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
2921, 28eqtrd 2726 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3013, 29eqtr3d 2728 . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
311, 30eqtr3d 2728 . . . . . . . . . 10 (𝜑𝑀 = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3231oveq1d 6748 . . . . . . . . 9 (𝜑 → (𝑀 − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1))
3316, 20mulcld 10141 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ)
34 addcl 10099 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3533, 5, 34sylancl 697 . . . . . . . . . 10 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3616, 20addcld 10140 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) + (𝐵 − 1)) ∈ ℂ)
3735, 36, 17addsubd 10494 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))))
38 pncan 10368 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
3933, 5, 38sylancl 697 . . . . . . . . . 10 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
4039oveq1d 6748 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4132, 37, 403eqtrd 2730 . . . . . . . 8 (𝜑 → (𝑀 − 1) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4241oveq1d 6748 . . . . . . 7 (𝜑 → ((𝑀 − 1) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2))
43 2cnd 11174 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
44 2ne0 11194 . . . . . . . . 9 2 ≠ 0
4544a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
4633, 36, 43, 45divdird 10920 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)))
4716, 20, 43, 45divassd 10917 . . . . . . . . 9 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
4816, 43, 45divcan2d 10884 . . . . . . . . . 10 (𝜑 → (2 · ((𝐴 − 1) / 2)) = (𝐴 − 1))
4948oveq1d 6748 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
50 lgsquad2.2 . . . . . . . . . . . . . 14 (𝜑 → ¬ 2 ∥ 𝑀)
51 dvdsmul1 15094 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
523, 9, 51syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∥ (𝐴 · 𝐵))
5352, 1breqtrd 4754 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑀)
54 2z 11490 . . . . . . . . . . . . . . . . 17 2 ∈ ℤ
5554a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℤ)
56 lgsquad2.1 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5756nnzd 11562 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
58 dvdstr 15109 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5955, 3, 57, 58syl3anc 1407 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
6053, 59mpan2d 712 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐴 → 2 ∥ 𝑀))
6150, 60mtod 189 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐴)
62 1zzd 11489 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
63 2prm 15496 . . . . . . . . . . . . . 14 2 ∈ ℙ
64 nprmdvds1 15509 . . . . . . . . . . . . . 14 (2 ∈ ℙ → ¬ 2 ∥ 1)
6563, 64mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 1)
66 omoe 15179 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐴 − 1))
673, 61, 62, 65, 66syl22anc 1408 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐴 − 1))
68 dvdsval2 15074 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐴 − 1) ∈ ℤ) → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6955, 45, 15, 68syl3anc 1407 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
7067, 69mpbid 222 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) / 2) ∈ ℤ)
7170zcnd 11564 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) / 2) ∈ ℂ)
72 dvdsmul2 15095 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∥ (𝐴 · 𝐵))
733, 9, 72syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∥ (𝐴 · 𝐵))
7473, 1breqtrd 4754 . . . . . . . . . . . . . . 15 (𝜑𝐵𝑀)
75 dvdstr 15109 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7655, 9, 57, 75syl3anc 1407 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7774, 76mpan2d 712 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐵 → 2 ∥ 𝑀))
7850, 77mtod 189 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐵)
79 omoe 15179 . . . . . . . . . . . . 13 (((𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐵 − 1))
809, 78, 62, 65, 79syl22anc 1408 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐵 − 1))
81 dvdsval2 15074 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐵 − 1) ∈ ℤ) → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8255, 45, 19, 81syl3anc 1407 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8380, 82mpbid 222 . . . . . . . . . . 11 (𝜑 → ((𝐵 − 1) / 2) ∈ ℤ)
8483zcnd 11564 . . . . . . . . . 10 (𝜑 → ((𝐵 − 1) / 2) ∈ ℂ)
8543, 71, 84mulassd 10144 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8647, 49, 853eqtr2d 2732 . . . . . . . 8 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8716, 20, 43, 45divdird 10920 . . . . . . . 8 (𝜑 → (((𝐴 − 1) + (𝐵 − 1)) / 2) = (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)))
8886, 87oveq12d 6751 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8942, 46, 883eqtrd 2730 . . . . . 6 (𝜑 → ((𝑀 − 1) / 2) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
9089oveq1d 6748 . . . . 5 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)))
9170, 83zmulcld 11569 . . . . . . . 8 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℤ)
9255, 91zmulcld 11569 . . . . . . 7 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℤ)
9392zcnd 11564 . . . . . 6 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℂ)
9470, 83zaddcld 11567 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℤ)
9594zcnd 11564 . . . . . 6 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℂ)
96 lgsquad2.3 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
9796nnzd 11562 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
98 lgsquad2.4 . . . . . . . . 9 (𝜑 → ¬ 2 ∥ 𝑁)
99 omoe 15179 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1))
10097, 98, 62, 65, 99syl22anc 1408 . . . . . . . 8 (𝜑 → 2 ∥ (𝑁 − 1))
101 peano2zm 11501 . . . . . . . . . 10 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10297, 101syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ ℤ)
103 dvdsval2 15074 . . . . . . . . 9 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
10455, 45, 102, 103syl3anc 1407 . . . . . . . 8 (𝜑 → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
105100, 104mpbid 222 . . . . . . 7 (𝜑 → ((𝑁 − 1) / 2) ∈ ℤ)
106105zcnd 11564 . . . . . 6 (𝜑 → ((𝑁 − 1) / 2) ∈ ℂ)
10793, 95, 106adddird 10146 . . . . 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 11564 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℂ)
10943, 108, 106mulassd 10144 . . . . . 6 (𝜑 → ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) = (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
110109oveq1d 6748 . . . . 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 2730 . . . 4 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
112111oveq2d 6749 . . 3 (𝜑 → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
113 neg1cn 11205 . . . . . 6 -1 ∈ ℂ
114113a1i 11 . . . . 5 (𝜑 → -1 ∈ ℂ)
115 neg1ne0 11207 . . . . . 6 -1 ≠ 0
116115a1i 11 . . . . 5 (𝜑 → -1 ≠ 0)
11791, 105zmulcld 11569 . . . . . 6 (𝜑 → ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
11855, 117zmulcld 11569 . . . . 5 (𝜑 → (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℤ)
11994, 105zmulcld 11569 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
120 expaddz 12987 . . . . 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 1408 . . . 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 12989 . . . . . . 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 1408 . . . . . 6 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
124 neg1sqe1 13042 . . . . . . . 8 (-1↑2) = 1
125124oveq1i 6743 . . . . . . 7 ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))
126 1exp 12972 . . . . . . . 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 2738 . . . . . 6 (𝜑 → ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
129123, 128eqtrd 2726 . . . . 5 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = 1)
130129oveq1d 6748 . . . 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 2726 . . 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 13096 . . . . 5 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℂ)
133132mulid2d 10139 . . . 4 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
13471, 84, 106adddird 10146 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) = ((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
135134oveq2d 6749 . . . 4 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
136133, 135eqtrd 2726 . . 3 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
137112, 131, 1363eqtrd 2730 . 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 6751 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
14170, 105zmulcld 11569 . . . 4 (𝜑 → (((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
14283, 105zmulcld 11569 . . . 4 (𝜑 → (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
143 expaddz 12987 . . . 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 1408 . . 3 (𝜑 → (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
145140, 144eqtr4d 2729 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
146 lgscl 25124 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
1473, 97, 146syl2anc 696 . . . . 5 (𝜑 → (𝐴 /L 𝑁) ∈ ℤ)
148147zcnd 11564 . . . 4 (𝜑 → (𝐴 /L 𝑁) ∈ ℂ)
149 lgscl 25124 . . . . . 6 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈ ℤ)
1509, 97, 149syl2anc 696 . . . . 5 (𝜑 → (𝐵 /L 𝑁) ∈ ℤ)
151150zcnd 11564 . . . 4 (𝜑 → (𝐵 /L 𝑁) ∈ ℂ)
152 lgscl 25124 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 /L 𝐴) ∈ ℤ)
15397, 3, 152syl2anc 696 . . . . 5 (𝜑 → (𝑁 /L 𝐴) ∈ ℤ)
154153zcnd 11564 . . . 4 (𝜑 → (𝑁 /L 𝐴) ∈ ℂ)
155 lgscl 25124 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 /L 𝐵) ∈ ℤ)
15697, 9, 155syl2anc 696 . . . . 5 (𝜑 → (𝑁 /L 𝐵) ∈ ℤ)
157156zcnd 11564 . . . 4 (𝜑 → (𝑁 /L 𝐵) ∈ ℂ)
158148, 151, 154, 157mul4d 10329 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))))
1592nnne0d 11146 . . . . . 6 (𝜑𝐴 ≠ 0)
1608nnne0d 11146 . . . . . 6 (𝜑𝐵 ≠ 0)
161 lgsdir 25145 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1623, 9, 97, 159, 160, 161syl32anc 1415 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1631oveq1d 6748 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = (𝑀 /L 𝑁))
164162, 163eqtr3d 2728 . . . 4 (𝜑 → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (𝑀 /L 𝑁))
165 lgsdi 25147 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
16697, 3, 9, 159, 160, 165syl32anc 1415 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
1671oveq2d 6749 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = (𝑁 /L 𝑀))
168166, 167eqtr3d 2728 . . . 4 (𝜑 → ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)) = (𝑁 /L 𝑀))
169164, 168oveq12d 6751 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
170158, 169eqtr3d 2728 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
171137, 145, 1703eqtr2rd 2733 1 (𝜑 → ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)) = (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1564  wcel 2071  wne 2864   class class class wbr 4728  (class class class)co 6733  cc 10015  0cc0 10017  1c1 10018   + caddc 10020   · cmul 10022  cmin 10347  -cneg 10348   / cdiv 10765  cn 11101  2c2 11151  cz 11458  cexp 12943  cdvds 15071   gcd cgcd 15307  cprime 15476   /L clgs 25107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-rep 4847  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-cnex 10073  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093  ax-pre-mulgt0 10094  ax-pre-sup 10095
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rmo 2990  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-pss 3664  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-tp 4258  df-op 4260  df-uni 4513  df-int 4552  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-tr 4829  df-id 5096  df-eprel 5101  df-po 5107  df-so 5108  df-fr 5145  df-we 5147  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-pred 5761  df-ord 5807  df-on 5808  df-lim 5809  df-suc 5810  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-om 7151  df-1st 7253  df-2nd 7254  df-wrecs 7495  df-recs 7556  df-rdg 7594  df-1o 7648  df-2o 7649  df-oadd 7652  df-er 7830  df-map 7944  df-en 8041  df-dom 8042  df-sdom 8043  df-fin 8044  df-sup 8432  df-inf 8433  df-card 8846  df-cda 9071  df-pnf 10157  df-mnf 10158  df-xr 10159  df-ltxr 10160  df-le 10161  df-sub 10349  df-neg 10350  df-div 10766  df-nn 11102  df-2 11160  df-3 11161  df-4 11162  df-5 11163  df-6 11164  df-7 11165  df-8 11166  df-9 11167  df-n0 11374  df-xnn0 11445  df-z 11459  df-uz 11769  df-q 11871  df-rp 11915  df-fz 12409  df-fzo 12549  df-fl 12676  df-mod 12752  df-seq 12885  df-exp 12944  df-hash 13201  df-cj 13927  df-re 13928  df-im 13929  df-sqrt 14063  df-abs 14064  df-dvds 15072  df-gcd 15308  df-prm 15477  df-phi 15562  df-pc 15633  df-lgs 25108
This theorem is referenced by:  lgsquad2lem2  25198
  Copyright terms: Public domain W3C validator