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

Theorem lgsquad2lem1 26732
Description: Lemma for lgsquad2 26734. (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 12526 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℤ)
43zcnd 12608 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℂ)
5 ax-1cn 11109 . . . . . . . . . . . . . 14 1 ∈ ℂ
6 npcan 11410 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 − 1) + 1) = 𝐴)
74, 5, 6sylancl 586 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 − 1) + 1) = 𝐴)
8 lgsquad2lem1.b . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℕ)
98nnzd 12526 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℤ)
109zcnd 12608 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℂ)
11 npcan 11410 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐵 − 1) + 1) = 𝐵)
1210, 5, 11sylancl 586 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 − 1) + 1) = 𝐵)
137, 12oveq12d 7375 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = (𝐴 · 𝐵))
14 peano2zm 12546 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
153, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 − 1) ∈ ℤ)
1615zcnd 12608 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 − 1) ∈ ℂ)
175a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
18 peano2zm 12546 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
199, 18syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 − 1) ∈ ℤ)
2019zcnd 12608 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 1) ∈ ℂ)
2116, 17, 20, 17muladdd 11613 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))))
22 1t1e1 12315 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
2322a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 1) = 1)
2423oveq2d 7373 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) = (((𝐴 − 1) · (𝐵 − 1)) + 1))
2516mulid1d 11172 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 − 1) · 1) = (𝐴 − 1))
2620mulid1d 11172 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 − 1) · 1) = (𝐵 − 1))
2725, 26oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1)) = ((𝐴 − 1) + (𝐵 − 1)))
2824, 27oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + (1 · 1)) + (((𝐴 − 1) · 1) + ((𝐵 − 1) · 1))) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
2921, 28eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → (((𝐴 − 1) + 1) · ((𝐵 − 1) + 1)) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3013, 29eqtr3d 2778 . . . . . . . . . . 11 (𝜑 → (𝐴 · 𝐵) = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
311, 30eqtr3d 2778 . . . . . . . . . 10 (𝜑𝑀 = ((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))))
3231oveq1d 7372 . . . . . . . . 9 (𝜑 → (𝑀 − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1))
3316, 20mulcld 11175 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ)
34 addcl 11133 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3533, 5, 34sylancl 586 . . . . . . . . . 10 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) + 1) ∈ ℂ)
3616, 20addcld 11174 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) + (𝐵 − 1)) ∈ ℂ)
3735, 36, 17addsubd 11533 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) + ((𝐴 − 1) + (𝐵 − 1))) − 1) = (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))))
38 pncan 11407 . . . . . . . . . . 11 ((((𝐴 − 1) · (𝐵 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
3933, 5, 38sylancl 586 . . . . . . . . . 10 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) = ((𝐴 − 1) · (𝐵 − 1)))
4039oveq1d 7372 . . . . . . . . 9 (𝜑 → (((((𝐴 − 1) · (𝐵 − 1)) + 1) − 1) + ((𝐴 − 1) + (𝐵 − 1))) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4132, 37, 403eqtrd 2780 . . . . . . . 8 (𝜑 → (𝑀 − 1) = (((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))))
4241oveq1d 7372 . . . . . . 7 (𝜑 → ((𝑀 − 1) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2))
43 2cnd 12231 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
44 2ne0 12257 . . . . . . . . 9 2 ≠ 0
4544a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
4633, 36, 43, 45divdird 11969 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) + ((𝐴 − 1) + (𝐵 − 1))) / 2) = ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)))
4716, 20, 43, 45divassd 11966 . . . . . . . . 9 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
4816, 43, 45divcan2d 11933 . . . . . . . . . 10 (𝜑 → (2 · ((𝐴 − 1) / 2)) = (𝐴 − 1))
4948oveq1d 7372 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = ((𝐴 − 1) · ((𝐵 − 1) / 2)))
50 lgsquad2.2 . . . . . . . . . . . . . 14 (𝜑 → ¬ 2 ∥ 𝑀)
51 dvdsmul1 16160 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
523, 9, 51syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∥ (𝐴 · 𝐵))
5352, 1breqtrd 5131 . . . . . . . . . . . . . . 15 (𝜑𝐴𝑀)
54 2z 12535 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
55 lgsquad2.1 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5655nnzd 12526 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
57 dvdstr 16176 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5854, 3, 56, 57mp3an2i 1466 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐴𝐴𝑀) → 2 ∥ 𝑀))
5953, 58mpan2d 692 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐴 → 2 ∥ 𝑀))
6050, 59mtod 197 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐴)
61 1zzd 12534 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
62 2prm 16568 . . . . . . . . . . . . . 14 2 ∈ ℙ
63 nprmdvds1 16582 . . . . . . . . . . . . . 14 (2 ∈ ℙ → ¬ 2 ∥ 1)
6462, 63mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 1)
65 omoe 16246 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐴 − 1))
663, 60, 61, 64, 65syl22anc 837 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐴 − 1))
67 dvdsval2 16139 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐴 − 1) ∈ ℤ) → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6854, 45, 15, 67mp3an2i 1466 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐴 − 1) ↔ ((𝐴 − 1) / 2) ∈ ℤ))
6966, 68mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝐴 − 1) / 2) ∈ ℤ)
7069zcnd 12608 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) / 2) ∈ ℂ)
71 dvdsmul2 16161 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∥ (𝐴 · 𝐵))
723, 9, 71syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∥ (𝐴 · 𝐵))
7372, 1breqtrd 5131 . . . . . . . . . . . . . . 15 (𝜑𝐵𝑀)
74 dvdstr 16176 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7554, 9, 56, 74mp3an2i 1466 . . . . . . . . . . . . . . 15 (𝜑 → ((2 ∥ 𝐵𝐵𝑀) → 2 ∥ 𝑀))
7673, 75mpan2d 692 . . . . . . . . . . . . . 14 (𝜑 → (2 ∥ 𝐵 → 2 ∥ 𝑀))
7750, 76mtod 197 . . . . . . . . . . . . 13 (𝜑 → ¬ 2 ∥ 𝐵)
78 omoe 16246 . . . . . . . . . . . . 13 (((𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐵 − 1))
799, 77, 61, 64, 78syl22anc 837 . . . . . . . . . . . 12 (𝜑 → 2 ∥ (𝐵 − 1))
80 dvdsval2 16139 . . . . . . . . . . . . 13 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝐵 − 1) ∈ ℤ) → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8154, 45, 19, 80mp3an2i 1466 . . . . . . . . . . . 12 (𝜑 → (2 ∥ (𝐵 − 1) ↔ ((𝐵 − 1) / 2) ∈ ℤ))
8279, 81mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝐵 − 1) / 2) ∈ ℤ)
8382zcnd 12608 . . . . . . . . . 10 (𝜑 → ((𝐵 − 1) / 2) ∈ ℂ)
8443, 70, 83mulassd 11178 . . . . . . . . 9 (𝜑 → ((2 · ((𝐴 − 1) / 2)) · ((𝐵 − 1) / 2)) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8547, 49, 843eqtr2d 2782 . . . . . . . 8 (𝜑 → (((𝐴 − 1) · (𝐵 − 1)) / 2) = (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))))
8616, 20, 43, 45divdird 11969 . . . . . . . 8 (𝜑 → (((𝐴 − 1) + (𝐵 − 1)) / 2) = (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)))
8785, 86oveq12d 7375 . . . . . . 7 (𝜑 → ((((𝐴 − 1) · (𝐵 − 1)) / 2) + (((𝐴 − 1) + (𝐵 − 1)) / 2)) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8842, 46, 873eqtrd 2780 . . . . . 6 (𝜑 → ((𝑀 − 1) / 2) = ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))))
8988oveq1d 7372 . . . . 5 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = (((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) + (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)))
9054a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
9169, 82zmulcld 12613 . . . . . . . 8 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℤ)
9290, 91zmulcld 12613 . . . . . . 7 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℤ)
9392zcnd 12608 . . . . . 6 (𝜑 → (2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) ∈ ℂ)
9469, 82zaddcld 12611 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℤ)
9594zcnd 12608 . . . . . 6 (𝜑 → (((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) ∈ ℂ)
96 lgsquad2.3 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
9796nnzd 12526 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
98 lgsquad2.4 . . . . . . . . 9 (𝜑 → ¬ 2 ∥ 𝑁)
99 omoe 16246 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝑁 − 1))
10097, 98, 61, 64, 99syl22anc 837 . . . . . . . 8 (𝜑 → 2 ∥ (𝑁 − 1))
101 peano2zm 12546 . . . . . . . . . 10 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10297, 101syl 17 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ ℤ)
103 dvdsval2 16139 . . . . . . . . 9 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
10454, 45, 102, 103mp3an2i 1466 . . . . . . . 8 (𝜑 → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈ ℤ))
105100, 104mpbid 231 . . . . . . 7 (𝜑 → ((𝑁 − 1) / 2) ∈ ℤ)
106105zcnd 12608 . . . . . 6 (𝜑 → ((𝑁 − 1) / 2) ∈ ℂ)
10793, 95, 106adddird 11180 . . . . 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 12608 . . . . . . 7 (𝜑 → (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) ∈ ℂ)
10943, 108, 106mulassd 11178 . . . . . 6 (𝜑 → ((2 · (((𝐴 − 1) / 2) · ((𝐵 − 1) / 2))) · ((𝑁 − 1) / 2)) = (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
110109oveq1d 7372 . . . . 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 2780 . . . 4 (𝜑 → (((𝑀 − 1) / 2) · ((𝑁 − 1) / 2)) = ((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
112111oveq2d 7373 . . 3 (𝜑 → (-1↑(((𝑀 − 1) / 2) · ((𝑁 − 1) / 2))) = (-1↑((2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) + ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))))
113 neg1cn 12267 . . . . . 6 -1 ∈ ℂ
114113a1i 11 . . . . 5 (𝜑 → -1 ∈ ℂ)
115 neg1ne0 12269 . . . . . 6 -1 ≠ 0
116115a1i 11 . . . . 5 (𝜑 → -1 ≠ 0)
11791, 105zmulcld 12613 . . . . . 6 (𝜑 → ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
11890, 117zmulcld 12613 . . . . 5 (𝜑 → (2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℤ)
11994, 105zmulcld 12613 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) ∈ ℤ)
120 expaddz 14012 . . . . 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 837 . . . 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 14014 . . . . . . 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 837 . . . . . 6 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
124 neg1sqe1 14100 . . . . . . . 8 (-1↑2) = 1
125124oveq1i 7367 . . . . . . 7 ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (1↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))
126 1exp 13997 . . . . . . . 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 2788 . . . . . 6 (𝜑 → ((-1↑2)↑((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = 1)
129123, 128eqtrd 2776 . . . . 5 (𝜑 → (-1↑(2 · ((((𝐴 − 1) / 2) · ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = 1)
130129oveq1d 7372 . . . 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 2776 . . 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 14056 . . . . 5 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) ∈ ℂ)
133132mulid2d 11173 . . . 4 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))))
13470, 83, 106adddird 11180 . . . . 5 (𝜑 → ((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)) = ((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2))))
135134oveq2d 7373 . . . 4 (𝜑 → (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
136133, 135eqtrd 2776 . . 3 (𝜑 → (1 · (-1↑((((𝐴 − 1) / 2) + ((𝐵 − 1) / 2)) · ((𝑁 − 1) / 2)))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
137112, 131, 1363eqtrd 2780 . 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 7375 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
14169, 105zmulcld 12613 . . . 4 (𝜑 → (((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
14282, 105zmulcld 12613 . . . 4 (𝜑 → (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)) ∈ ℤ)
143 expaddz 14012 . . . 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 837 . . 3 (𝜑 → (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))) = ((-1↑(((𝐴 − 1) / 2) · ((𝑁 − 1) / 2))) · (-1↑(((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
145140, 144eqtr4d 2779 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = (-1↑((((𝐴 − 1) / 2) · ((𝑁 − 1) / 2)) + (((𝐵 − 1) / 2) · ((𝑁 − 1) / 2)))))
146 lgscl 26659 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
1473, 97, 146syl2anc 584 . . . . 5 (𝜑 → (𝐴 /L 𝑁) ∈ ℤ)
148147zcnd 12608 . . . 4 (𝜑 → (𝐴 /L 𝑁) ∈ ℂ)
149 lgscl 26659 . . . . . 6 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐵 /L 𝑁) ∈ ℤ)
1509, 97, 149syl2anc 584 . . . . 5 (𝜑 → (𝐵 /L 𝑁) ∈ ℤ)
151150zcnd 12608 . . . 4 (𝜑 → (𝐵 /L 𝑁) ∈ ℂ)
152 lgscl 26659 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁 /L 𝐴) ∈ ℤ)
15397, 3, 152syl2anc 584 . . . . 5 (𝜑 → (𝑁 /L 𝐴) ∈ ℤ)
154153zcnd 12608 . . . 4 (𝜑 → (𝑁 /L 𝐴) ∈ ℂ)
155 lgscl 26659 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 /L 𝐵) ∈ ℤ)
15697, 9, 155syl2anc 584 . . . . 5 (𝜑 → (𝑁 /L 𝐵) ∈ ℤ)
157156zcnd 12608 . . . 4 (𝜑 → (𝑁 /L 𝐵) ∈ ℂ)
158148, 151, 154, 157mul4d 11367 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))))
1592nnne0d 12203 . . . . . 6 (𝜑𝐴 ≠ 0)
1608nnne0d 12203 . . . . . 6 (𝜑𝐵 ≠ 0)
161 lgsdir 26680 . . . . . 6 (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1623, 9, 97, 159, 160, 161syl32anc 1378 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
1631oveq1d 7372 . . . . 5 (𝜑 → ((𝐴 · 𝐵) /L 𝑁) = (𝑀 /L 𝑁))
164162, 163eqtr3d 2778 . . . 4 (𝜑 → ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) = (𝑀 /L 𝑁))
165 lgsdi 26682 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
16697, 3, 9, 159, 160, 165syl32anc 1378 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)))
1671oveq2d 7373 . . . . 5 (𝜑 → (𝑁 /L (𝐴 · 𝐵)) = (𝑁 /L 𝑀))
168166, 167eqtr3d 2778 . . . 4 (𝜑 → ((𝑁 /L 𝐴) · (𝑁 /L 𝐵)) = (𝑁 /L 𝑀))
169164, 168oveq12d 7375 . . 3 (𝜑 → (((𝐴 /L 𝑁) · (𝐵 /L 𝑁)) · ((𝑁 /L 𝐴) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
170158, 169eqtr3d 2778 . 2 (𝜑 → (((𝐴 /L 𝑁) · (𝑁 /L 𝐴)) · ((𝐵 /L 𝑁) · (𝑁 /L 𝐵))) = ((𝑀 /L 𝑁) · (𝑁 /L 𝑀)))
171137, 145, 1703eqtr2rd 2783 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 1541  wcel 2106  wne 2943   class class class wbr 5105  (class class class)co 7357  cc 11049  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  cz 12499  cexp 13967  cdvds 16136   gcd cgcd 16374  cprime 16547   /L clgs 26642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-dvds 16137  df-gcd 16375  df-prm 16548  df-phi 16638  df-pc 16709  df-lgs 26643
This theorem is referenced by:  lgsquad2lem2  26733
  Copyright terms: Public domain W3C validator