Metamath Proof Explorer

Theorem lgsquad2lem1

Description: Lemma for lgsquad2 . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 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 lgsquad2lem1 ( 𝜑 → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsquad2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lgsquad2.2 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
3 lgsquad2.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 lgsquad2.4 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
5 lgsquad2.5 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
6 lgsquad2lem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
7 lgsquad2lem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
8 lgsquad2lem1.m ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = 𝑀 )
9 lgsquad2lem1.1 ⊢ ( 𝜑 → ( ( 𝐴 /L 𝑁 ) · ( 𝑁 /L 𝐴 ) ) = ( - 1 ↑ ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
10 lgsquad2lem1.2 ⊢ ( 𝜑 → ( ( 𝐵 /L 𝑁 ) · ( 𝑁 /L 𝐵 ) ) = ( - 1 ↑ ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
11 6 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
12 11 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13 ax-1cn ⊢ 1 ∈ ℂ
14 npcan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
15 12 13 14 sylancl ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
16 7 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
17 16 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
18 npcan ⊢ ( ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
19 17 13 18 sylancl ⊢ ( 𝜑 → ( ( 𝐵 − 1 ) + 1 ) = 𝐵 )
20 15 19 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) + 1 ) · ( ( 𝐵 − 1 ) + 1 ) ) = ( 𝐴 · 𝐵 ) )
21 peano2zm ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℤ )
22 11 21 syl ⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℤ )
23 22 zcnd ⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℂ )
24 13 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
25 peano2zm ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 − 1 ) ∈ ℤ )
26 16 25 syl ⊢ ( 𝜑 → ( 𝐵 − 1 ) ∈ ℤ )
27 26 zcnd ⊢ ( 𝜑 → ( 𝐵 − 1 ) ∈ ℂ )
28 23 24 27 24 muladdd ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) + 1 ) · ( ( 𝐵 − 1 ) + 1 ) ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( 1 · 1 ) ) + ( ( ( 𝐴 − 1 ) · 1 ) + ( ( 𝐵 − 1 ) · 1 ) ) ) )
29 1t1e1 ⊢ ( 1 · 1 ) = 1
30 29 a1i ⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
31 30 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( 1 · 1 ) ) = ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) )
32 23 mulridd ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) · 1 ) = ( 𝐴 − 1 ) )
33 27 mulridd ⊢ ( 𝜑 → ( ( 𝐵 − 1 ) · 1 ) = ( 𝐵 − 1 ) )
34 32 33 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) · 1 ) + ( ( 𝐵 − 1 ) · 1 ) ) = ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) )
35 31 34 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( 1 · 1 ) ) + ( ( ( 𝐴 − 1 ) · 1 ) + ( ( 𝐵 − 1 ) · 1 ) ) ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
36 28 35 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) + 1 ) · ( ( 𝐵 − 1 ) + 1 ) ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
37 20 36 eqtr3d ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
38 8 37 eqtr3d ⊢ ( 𝜑 → 𝑀 = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
39 38 oveq1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) = ( ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) − 1 ) )
40 23 27 mulcld ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ∈ ℂ )
41 addcl ⊢ ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) ∈ ℂ )
42 40 13 41 sylancl ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) ∈ ℂ )
43 23 27 addcld ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ∈ ℂ )
44 42 43 24 addsubd ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) − 1 ) = ( ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) − 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
45 pncan ⊢ ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) − 1 ) = ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
46 40 13 45 sylancl ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) − 1 ) = ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
47 46 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + 1 ) − 1 ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) = ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
48 39 44 47 3eqtrd ⊢ ( 𝜑 → ( 𝑀 − 1 ) = ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) )
49 48 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) / 2 ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) / 2 ) )
50 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
51 2ne0 ⊢ 2 ≠ 0
52 51 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
53 40 43 50 52 divdird ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) + ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) ) / 2 ) = ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) / 2 ) + ( ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) / 2 ) ) )
54 23 27 50 52 divassd ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) / 2 ) = ( ( 𝐴 − 1 ) · ( ( 𝐵 − 1 ) / 2 ) ) )
55 23 50 52 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 − 1 ) / 2 ) ) = ( 𝐴 − 1 ) )
56 55 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 𝐴 − 1 ) / 2 ) ) · ( ( 𝐵 − 1 ) / 2 ) ) = ( ( 𝐴 − 1 ) · ( ( 𝐵 − 1 ) / 2 ) ) )
57 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
58 11 16 57 syl2anc ⊢ ( 𝜑 → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
59 58 8 breqtrd ⊢ ( 𝜑 → 𝐴 ∥ 𝑀 )
60 2z ⊢ 2 ∈ ℤ
61 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
62 dvdstr ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ 𝐴 ∥ 𝑀 ) → 2 ∥ 𝑀 ) )
63 60 11 61 62 mp3an2i ⊢ ( 𝜑 → ( ( 2 ∥ 𝐴 ∧ 𝐴 ∥ 𝑀 ) → 2 ∥ 𝑀 ) )
64 59 63 mpan2d ⊢ ( 𝜑 → ( 2 ∥ 𝐴 → 2 ∥ 𝑀 ) )
65 2 64 mtod ⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
66 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
67 2prm ⊢ 2 ∈ ℙ
68 nprmdvds1 ⊢ ( 2 ∈ ℙ → ¬ 2 ∥ 1 )
69 67 68 mp1i ⊢ ( 𝜑 → ¬ 2 ∥ 1 )
70 omoe ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝐴 − 1 ) )
71 11 65 66 69 70 syl22anc ⊢ ( 𝜑 → 2 ∥ ( 𝐴 − 1 ) )
72 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝐴 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝐴 − 1 ) ↔ ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ) )
73 60 52 22 72 mp3an2i ⊢ ( 𝜑 → ( 2 ∥ ( 𝐴 − 1 ) ↔ ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ) )
74 71 73 mpbid ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ )
75 74 zcnd ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) / 2 ) ∈ ℂ )
76 dvdsmul2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∥ ( 𝐴 · 𝐵 ) )
77 11 16 76 syl2anc ⊢ ( 𝜑 → 𝐵 ∥ ( 𝐴 · 𝐵 ) )
78 77 8 breqtrd ⊢ ( 𝜑 → 𝐵 ∥ 𝑀 )
79 dvdstr ⊢ ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 2 ∥ 𝐵 ∧ 𝐵 ∥ 𝑀 ) → 2 ∥ 𝑀 ) )
80 60 16 61 79 mp3an2i ⊢ ( 𝜑 → ( ( 2 ∥ 𝐵 ∧ 𝐵 ∥ 𝑀 ) → 2 ∥ 𝑀 ) )
81 78 80 mpan2d ⊢ ( 𝜑 → ( 2 ∥ 𝐵 → 2 ∥ 𝑀 ) )
82 2 81 mtod ⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )
83 omoe ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝐵 − 1 ) )
84 16 82 66 69 83 syl22anc ⊢ ( 𝜑 → 2 ∥ ( 𝐵 − 1 ) )
85 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝐵 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝐵 − 1 ) ↔ ( ( 𝐵 − 1 ) / 2 ) ∈ ℤ ) )
86 60 52 26 85 mp3an2i ⊢ ( 𝜑 → ( 2 ∥ ( 𝐵 − 1 ) ↔ ( ( 𝐵 − 1 ) / 2 ) ∈ ℤ ) )
87 84 86 mpbid ⊢ ( 𝜑 → ( ( 𝐵 − 1 ) / 2 ) ∈ ℤ )
88 87 zcnd ⊢ ( 𝜑 → ( ( 𝐵 − 1 ) / 2 ) ∈ ℂ )
89 50 75 88 mulassd ⊢ ( 𝜑 → ( ( 2 · ( ( 𝐴 − 1 ) / 2 ) ) · ( ( 𝐵 − 1 ) / 2 ) ) = ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) )
90 54 56 89 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) / 2 ) = ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) )
91 23 27 50 52 divdird ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) / 2 ) = ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) )
92 90 91 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) / 2 ) + ( ( ( 𝐴 − 1 ) + ( 𝐵 − 1 ) ) / 2 ) ) = ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) + ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ) )
93 49 53 92 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) / 2 ) = ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) + ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ) )
94 93 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) + ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ) · ( ( 𝑁 − 1 ) / 2 ) ) )
95 60 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
96 74 87 zmulcld ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ∈ ℤ )
97 95 96 zmulcld ⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) ∈ ℤ )
98 97 zcnd ⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) ∈ ℂ )
99 74 87 zaddcld ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ∈ ℤ )
100 99 zcnd ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ∈ ℂ )
101 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
102 omoe ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝑁 − 1 ) )
103 101 4 66 69 102 syl22anc ⊢ ( 𝜑 → 2 ∥ ( 𝑁 − 1 ) )
104 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
105 101 104 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
106 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
107 60 52 105 106 mp3an2i ⊢ ( 𝜑 → ( 2 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
108 103 107 mpbid ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ )
109 108 zcnd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / 2 ) ∈ ℂ )
110 98 100 109 adddird ⊢ ( 𝜑 → ( ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) + ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
111 96 zcnd ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ∈ ℂ )
112 50 111 109 mulassd ⊢ ( 𝜑 → ( ( 2 · ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
113 112 oveq1d ⊢ ( 𝜑 → ( ( ( 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 ) ) ) )
114 94 110 113 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) + ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
115 114 oveq2d ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = ( - 1 ↑ ( ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) + ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
116 neg1cn ⊢ - 1 ∈ ℂ
117 116 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
118 neg1ne0 ⊢ - 1 ≠ 0
119 118 a1i ⊢ ( 𝜑 → - 1 ≠ 0 )
120 96 108 zmulcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ )
121 95 120 zmulcld ⊢ ( 𝜑 → ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ∈ ℤ )
122 99 108 zmulcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ )
123 expaddz ⊢ ( ( ( - 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 ) ) ) ) )
124 117 119 121 122 123 syl22anc ⊢ ( 𝜑 → ( - 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 ) ) ) ) )
125 expmulz ⊢ ( ( ( - 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 ) ) ) )
126 117 119 95 120 125 syl22anc ⊢ ( 𝜑 → ( - 1 ↑ ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
127 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
128 127 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = ( 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) )
129 1exp ⊢ ( ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ → ( 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = 1 )
130 120 129 syl ⊢ ( 𝜑 → ( 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = 1 )
131 128 130 eqtrid ⊢ ( 𝜑 → ( ( - 1 ↑ 2 ) ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = 1 )
132 126 131 eqtrd ⊢ ( 𝜑 → ( - 1 ↑ ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = 1 )
133 132 oveq1d ⊢ ( 𝜑 → ( ( - 1 ↑ ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) · ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( 1 · ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
134 124 133 eqtrd ⊢ ( 𝜑 → ( - 1 ↑ ( ( 2 · ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) + ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( 1 · ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
135 117 119 122 expclzd ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ∈ ℂ )
136 135 mullidd ⊢ ( 𝜑 → ( 1 · ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
137 75 88 109 adddird ⊢ ( 𝜑 → ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) = ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )
138 137 oveq2d ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
139 136 138 eqtrd ⊢ ( 𝜑 → ( 1 · ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) + ( ( 𝐵 − 1 ) / 2 ) ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
140 115 134 139 3eqtrd ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) = ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
141 9 10 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 /L 𝑁 ) · ( 𝑁 /L 𝐴 ) ) · ( ( 𝐵 /L 𝑁 ) · ( 𝑁 /L 𝐵 ) ) ) = ( ( - 1 ↑ ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( - 1 ↑ ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
142 74 108 zmulcld ⊢ ( 𝜑 → ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ )
143 87 108 zmulcld ⊢ ( 𝜑 → ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ∈ ℤ )
144 expaddz ⊢ ( ( ( - 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 ) ) ) ) )
145 117 119 142 143 144 syl22anc ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) = ( ( - 1 ↑ ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) · ( - 1 ↑ ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
146 141 145 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 /L 𝑁 ) · ( 𝑁 /L 𝐴 ) ) · ( ( 𝐵 /L 𝑁 ) · ( 𝑁 /L 𝐵 ) ) ) = ( - 1 ↑ ( ( ( ( 𝐴 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) + ( ( ( 𝐵 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) ) )
147 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
148 11 101 147 syl2anc ⊢ ( 𝜑 → ( 𝐴 /L 𝑁 ) ∈ ℤ )
149 148 zcnd ⊢ ( 𝜑 → ( 𝐴 /L 𝑁 ) ∈ ℂ )
150 lgscl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 /L 𝑁 ) ∈ ℤ )
151 16 101 150 syl2anc ⊢ ( 𝜑 → ( 𝐵 /L 𝑁 ) ∈ ℤ )
152 151 zcnd ⊢ ( 𝜑 → ( 𝐵 /L 𝑁 ) ∈ ℂ )
153 lgscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑁 /L 𝐴 ) ∈ ℤ )
154 101 11 153 syl2anc ⊢ ( 𝜑 → ( 𝑁 /L 𝐴 ) ∈ ℤ )
155 154 zcnd ⊢ ( 𝜑 → ( 𝑁 /L 𝐴 ) ∈ ℂ )
156 lgscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 /L 𝐵 ) ∈ ℤ )
157 101 16 156 syl2anc ⊢ ( 𝜑 → ( 𝑁 /L 𝐵 ) ∈ ℤ )
158 157 zcnd ⊢ ( 𝜑 → ( 𝑁 /L 𝐵 ) ∈ ℂ )
159 149 152 155 158 mul4d ⊢ ( 𝜑 → ( ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) · ( ( 𝑁 /L 𝐴 ) · ( 𝑁 /L 𝐵 ) ) ) = ( ( ( 𝐴 /L 𝑁 ) · ( 𝑁 /L 𝐴 ) ) · ( ( 𝐵 /L 𝑁 ) · ( 𝑁 /L 𝐵 ) ) ) )
160 6 nnne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
161 7 nnne0d ⊢ ( 𝜑 → 𝐵 ≠ 0 )
162 lgsdir ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
163 11 16 101 160 161 162 syl32anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
164 8 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /L 𝑁 ) = ( 𝑀 /L 𝑁 ) )
165 163 164 eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) = ( 𝑀 /L 𝑁 ) )
166 lgsdi ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝑁 /L ( 𝐴 · 𝐵 ) ) = ( ( 𝑁 /L 𝐴 ) · ( 𝑁 /L 𝐵 ) ) )
167 101 11 16 160 161 166 syl32anc ⊢ ( 𝜑 → ( 𝑁 /L ( 𝐴 · 𝐵 ) ) = ( ( 𝑁 /L 𝐴 ) · ( 𝑁 /L 𝐵 ) ) )
168 8 oveq2d ⊢ ( 𝜑 → ( 𝑁 /L ( 𝐴 · 𝐵 ) ) = ( 𝑁 /L 𝑀 ) )
169 167 168 eqtr3d ⊢ ( 𝜑 → ( ( 𝑁 /L 𝐴 ) · ( 𝑁 /L 𝐵 ) ) = ( 𝑁 /L 𝑀 ) )
170 165 169 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) · ( ( 𝑁 /L 𝐴 ) · ( 𝑁 /L 𝐵 ) ) ) = ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) )
171 159 170 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐴 /L 𝑁 ) · ( 𝑁 /L 𝐴 ) ) · ( ( 𝐵 /L 𝑁 ) · ( 𝑁 /L 𝐵 ) ) ) = ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) )
172 140 146 171 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝑀 /L 𝑁 ) · ( 𝑁 /L 𝑀 ) ) = ( - 1 ↑ ( ( ( 𝑀 − 1 ) / 2 ) · ( ( 𝑁 − 1 ) / 2 ) ) ) )