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 ) ) ) )