jm2.23

Description: Lemma for jm2.20nn . Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014)

		Ref	Expression
	Assertion	jm2.23	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} ∥ ((A Y_{rm} N \cdot J) - J {(A X_{rm} N)}^{J - 1} (A Y_{rm} N))$

Proof

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (3 \dots J) \in Fin$
2		ssrab2	$⊢ \{b \in (3 \dots J) \| \neg 2 ∥ b\} \subseteq (3 \dots J)$
3		ssfi	$⊢ ((3 \dots J) \in Fin \land \{b \in (3 \dots J) \| \neg 2 ∥ b\} \subseteq (3 \dots J)) \to \{b \in (3 \dots J) \| \neg 2 ∥ b\} \in Fin$
4	1 2 3	mp2an	$⊢ \{b \in (3 \dots J) \| \neg 2 ∥ b\} \in Fin$
5	4	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \{b \in (3 \dots J) \| \neg 2 ∥ b\} \in Fin$
6		nnnn0	$⊢ J \in ℕ \to J \in ℕ_{0}$
7	6	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J \in ℕ_{0}$
8	2	sseli	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to a \in (3 \dots J)$
9		elfzelz	$⊢ a \in (3 \dots J) \to a \in ℤ$
10	8 9	syl	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to a \in ℤ$
11		bccl	$⊢ (J \in ℕ_{0} \land a \in ℤ) \to (\binom{J}{a}) \in ℕ_{0}$
12	7 10 11	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) \in ℕ_{0}$
13	12	nn0zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) \in ℤ$
14		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A \in ℤ_{\geq 2}$
15		simpl2	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to N \in ℤ$
16		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
17	16	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
18	14 15 17	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A X_{rm} N \in ℕ_{0}$
19	18	nn0zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A X_{rm} N \in ℤ$
20	8	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to a \in (3 \dots J)$
21		fznn0sub	$⊢ a \in (3 \dots J) \to J - a \in ℕ_{0}$
22	20 21	syl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to J - a \in ℕ_{0}$
23		zexpcl	$⊢ (A X_{rm} N \in ℤ \land J - a \in ℕ_{0}) \to {(A X_{rm} N)}^{J - a} \in ℤ$
24	19 22 23	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} \in ℤ$
25		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
26	25	eldifad	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℕ$
27	26	nnzd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℤ$
28	27	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A^{2} - 1 \in ℤ$
29		breq2	$⊢ b = a \to (2 ∥ b \leftrightarrow 2 ∥ a)$
30	29	notbid	$⊢ b = a \to (\neg 2 ∥ b \leftrightarrow \neg 2 ∥ a)$
31	30	elrab	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \leftrightarrow (a \in (3 \dots J) \land \neg 2 ∥ a)$
32	31	simprbi	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ a$
33		1zzd	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 1 \in ℤ$
34		n2dvds1	$⊢ \neg 2 ∥ 1$
35	34	a1i	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ 1$
36		omoe	$⊢ ((a \in ℤ \land \neg 2 ∥ a) \land (1 \in ℤ \land \neg 2 ∥ 1)) \to 2 ∥ (a - 1)$
37	10 32 33 35 36	syl22anc	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 2 ∥ (a - 1)$
38		2z	$⊢ 2 \in ℤ$
39	38	a1i	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℤ$
40		2ne0	$⊢ 2 \neq 0$
41	40	a1i	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 2 \neq 0$
42		peano2zm	$⊢ a \in ℤ \to a - 1 \in ℤ$
43	10 42	syl	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℤ$
44		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land a - 1 \in ℤ) \to (2 ∥ (a - 1) \leftrightarrow \frac{a - 1}{2} \in ℤ)$
45	39 41 43 44	syl3anc	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to (2 ∥ (a - 1) \leftrightarrow \frac{a - 1}{2} \in ℤ)$
46	37 45	mpbid	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℤ$
47	43	zred	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℝ$
48		0red	$⊢ a \in (3 \dots J) \to 0 \in ℝ$
49		3re	$⊢ 3 \in ℝ$
50	49	a1i	$⊢ a \in (3 \dots J) \to 3 \in ℝ$
51	9	zred	$⊢ a \in (3 \dots J) \to a \in ℝ$
52		3pos	$⊢ 0 < 3$
53	52	a1i	$⊢ a \in (3 \dots J) \to 0 < 3$
54		elfzle1	$⊢ a \in (3 \dots J) \to 3 \leq a$
55	48 50 51 53 54	ltletrd	$⊢ a \in (3 \dots J) \to 0 < a$
56		elnnz	$⊢ a \in ℕ \leftrightarrow (a \in ℤ \land 0 < a)$
57	9 55 56	sylanbrc	$⊢ a \in (3 \dots J) \to a \in ℕ$
58		nnm1nn0	$⊢ a \in ℕ \to a - 1 \in ℕ_{0}$
59	57 58	syl	$⊢ a \in (3 \dots J) \to a - 1 \in ℕ_{0}$
60	59	nn0ge0d	$⊢ a \in (3 \dots J) \to 0 \leq a - 1$
61	8 60	syl	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 0 \leq a - 1$
62		2re	$⊢ 2 \in ℝ$
63	62	a1i	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℝ$
64		2pos	$⊢ 0 < 2$
65	64	a1i	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 0 < 2$
66		divge0	$⊢ ((a - 1 \in ℝ \land 0 \leq a - 1) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{a - 1}{2}$
67	47 61 63 65 66	syl22anc	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to 0 \leq \frac{a - 1}{2}$
68		elnn0z	$⊢ \frac{a - 1}{2} \in ℕ_{0} \leftrightarrow (\frac{a - 1}{2} \in ℤ \land 0 \leq \frac{a - 1}{2})$
69	46 67 68	sylanbrc	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℕ_{0}$
70		zexpcl	$⊢ (A^{2} - 1 \in ℤ \land \frac{a - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℤ$
71	28 69 70	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℤ$
72		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
73	72	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
74	14 15 73	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A Y_{rm} N \in ℤ$
75		elfzel1	$⊢ a \in (3 \dots J) \to 3 \in ℤ$
76	9 75	zsubcld	$⊢ a \in (3 \dots J) \to a - 3 \in ℤ$
77		subge0	$⊢ (a \in ℝ \land 3 \in ℝ) \to (0 \leq a - 3 \leftrightarrow 3 \leq a)$
78	51 49 77	sylancl	$⊢ a \in (3 \dots J) \to (0 \leq a - 3 \leftrightarrow 3 \leq a)$
79	54 78	mpbird	$⊢ a \in (3 \dots J) \to 0 \leq a - 3$
80		elnn0z	$⊢ a - 3 \in ℕ_{0} \leftrightarrow (a - 3 \in ℤ \land 0 \leq a - 3)$
81	76 79 80	sylanbrc	$⊢ a \in (3 \dots J) \to a - 3 \in ℕ_{0}$
82	8 81	syl	$⊢ a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \to a - 3 \in ℕ_{0}$
83	82	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to a - 3 \in ℕ_{0}$
84		zexpcl	$⊢ (A Y_{rm} N \in ℤ \land a - 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{a - 3} \in ℤ$
85	74 83 84	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3} \in ℤ$
86	71 85	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℤ$
87	24 86	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℤ$
88	13 87	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℤ$
89	5 88	fsumzcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℤ$
90	73	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N \in ℤ$
91		3nn0	$⊢ 3 \in ℕ_{0}$
92		zexpcl	$⊢ (A Y_{rm} N \in ℤ \land 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{3} \in ℤ$
93	90 91 92	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} \in ℤ$
94		dvdsmul2	$⊢ (\sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℤ \land {(A Y_{rm} N)}^{3} \in ℤ) \to {(A Y_{rm} N)}^{3} ∥ \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
95	89 93 94	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} ∥ \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
96		jm2.22	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \cdot J = \sum_{a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
97	6 96	syl3an3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N \cdot J = \sum_{a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
98		1lt3	$⊢ 1 < 3$
99		1re	$⊢ 1 \in ℝ$
100	99 49	ltnlei	$⊢ 1 < 3 \leftrightarrow \neg 3 \leq 1$
101	98 100	mpbi	$⊢ \neg 3 \leq 1$
102		elfzle1	$⊢ 1 \in (3 \dots J) \to 3 \leq 1$
103	101 102	mto	$⊢ \neg 1 \in (3 \dots J)$
104	103	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \neg 1 \in (3 \dots J)$
105	104	intnanrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \neg (1 \in (3 \dots J) \land \neg 2 ∥ 1)$
106		breq2	$⊢ b = 1 \to (2 ∥ b \leftrightarrow 2 ∥ 1)$
107	106	notbid	$⊢ b = 1 \to (\neg 2 ∥ b \leftrightarrow \neg 2 ∥ 1)$
108	107	elrab	$⊢ 1 \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \leftrightarrow (1 \in (3 \dots J) \land \neg 2 ∥ 1)$
109	105 108	sylnibr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \neg 1 \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}$
110		disjsn	$⊢ \{b \in (3 \dots J) \| \neg 2 ∥ b\} \cap \{1\} = \emptyset \leftrightarrow \neg 1 \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}$
111	109 110	sylibr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \{b \in (3 \dots J) \| \neg 2 ∥ b\} \cap \{1\} = \emptyset$
112		simpr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a = 1) \to a = 1$
113	112	olcd	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a = 1) \to ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)$
114		elfznn0	$⊢ a \in (0 \dots J) \to a \in ℕ_{0}$
115	114	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \in ℕ_{0}$
116	115	ad2antlr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to a \in ℕ_{0}$
117		simplrr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to \neg 2 ∥ a$
118		simpr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to a \neq 1$
119		elnn1uz2	$⊢ a \in ℕ \leftrightarrow (a = 1 \lor a \in ℤ_{\geq 2})$
120		df-ne	$⊢ a \neq 1 \leftrightarrow \neg a = 1$
121	120	biimpi	$⊢ a \neq 1 \to \neg a = 1$
122	121	3ad2ant3	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to \neg a = 1$
123	122	pm2.21d	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to (a = 1 \to 3 \leq a)$
124	123	imp	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 1) \to 3 \leq a$
125		uzp1	$⊢ a \in ℤ_{\geq 2} \to (a = 2 \lor a \in ℤ_{\geq (2 + 1)})$
126		1z	$⊢ 1 \in ℤ$
127		dvdsmul1	$⊢ (2 \in ℤ \land 1 \in ℤ) \to 2 ∥ 2 \cdot 1$
128	38 126 127	mp2an	$⊢ 2 ∥ 2 \cdot 1$
129		2t1e2	$⊢ 2 \cdot 1 = 2$
130	128 129	breqtri	$⊢ 2 ∥ 2$
131		breq2	$⊢ a = 2 \to (2 ∥ a \leftrightarrow 2 ∥ 2)$
132	131	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to (2 ∥ a \leftrightarrow 2 ∥ 2)$
133	130 132	mpbiri	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to 2 ∥ a$
134		simpl2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to \neg 2 ∥ a$
135	133 134	pm2.21dd	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to 3 \leq a$
136		eluzle	$⊢ a \in ℤ_{\geq 3} \to 3 \leq a$
137		2p1e3	$⊢ 2 + 1 = 3$
138	137	fveq2i	$⊢ ℤ_{\geq (2 + 1)} = ℤ_{\geq 3}$
139	136 138	eleq2s	$⊢ a \in ℤ_{\geq (2 + 1)} \to 3 \leq a$
140	139	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℤ_{\geq (2 + 1)}) \to 3 \leq a$
141	135 140	jaodan	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land (a = 2 \lor a \in ℤ_{\geq (2 + 1)})) \to 3 \leq a$
142	125 141	sylan2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℤ_{\geq 2}) \to 3 \leq a$
143	124 142	jaodan	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land (a = 1 \lor a \in ℤ_{\geq 2})) \to 3 \leq a$
144	119 143	sylan2b	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℕ) \to 3 \leq a$
145		dvds0	$⊢ 2 \in ℤ \to 2 ∥ 0$
146	38 145	ax-mp	$⊢ 2 ∥ 0$
147		breq2	$⊢ a = 0 \to (2 ∥ a \leftrightarrow 2 ∥ 0)$
148	146 147	mpbiri	$⊢ a = 0 \to 2 ∥ a$
149	148	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to 2 ∥ a$
150		simpl2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to \neg 2 ∥ a$
151	149 150	pm2.21dd	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to 3 \leq a$
152		elnn0	$⊢ a \in ℕ_{0} \leftrightarrow (a \in ℕ \lor a = 0)$
153	152	biimpi	$⊢ a \in ℕ_{0} \to (a \in ℕ \lor a = 0)$
154	153	3ad2ant1	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to (a \in ℕ \lor a = 0)$
155	144 151 154	mpjaodan	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to 3 \leq a$
156	116 117 118 155	syl3anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to 3 \leq a$
157		elfzle2	$⊢ a \in (0 \dots J) \to a \leq J$
158	157	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \leq J$
159	158	ad2antlr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to a \leq J$
160		elfzelz	$⊢ a \in (0 \dots J) \to a \in ℤ$
161	160	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \in ℤ$
162	161	ad2antlr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to a \in ℤ$
163		3z	$⊢ 3 \in ℤ$
164	163	a1i	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to 3 \in ℤ$
165		nnz	$⊢ J \in ℕ \to J \in ℤ$
166	165	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J \in ℤ$
167	166	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to J \in ℤ$
168		elfz	$⊢ (a \in ℤ \land 3 \in ℤ \land J \in ℤ) \to (a \in (3 \dots J) \leftrightarrow (3 \leq a \land a \leq J))$
169	162 164 167 168	syl3anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to (a \in (3 \dots J) \leftrightarrow (3 \leq a \land a \leq J))$
170	156 159 169	mpbir2and	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to a \in (3 \dots J)$
171	170 117	jca	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to (a \in (3 \dots J) \land \neg 2 ∥ a)$
172	171	orcd	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \land a \neq 1) \to ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)$
173	113 172	pm2.61dane	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (0 \dots J) \land \neg 2 ∥ a)) \to ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)$
174		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
175	91 174	eleqtri	$⊢ 3 \in ℤ_{\geq 0}$
176		fzss1	$⊢ 3 \in ℤ_{\geq 0} \to (3 \dots J) \subseteq (0 \dots J)$
177	175 176	ax-mp	$⊢ (3 \dots J) \subseteq (0 \dots J)$
178	177	sseli	$⊢ a \in (3 \dots J) \to a \in (0 \dots J)$
179	178	anim1i	$⊢ (a \in (3 \dots J) \land \neg 2 ∥ a) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
180	179	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land (a \in (3 \dots J) \land \neg 2 ∥ a)) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
181		0le1	$⊢ 0 \leq 1$
182	181	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 0 \leq 1$
183		nnge1	$⊢ J \in ℕ \to 1 \leq J$
184	183	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to 1 \leq J$
185	184	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \leq J$
186		1zzd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \in ℤ$
187		0zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 0 \in ℤ$
188	166	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to J \in ℤ$
189		elfz	$⊢ (1 \in ℤ \land 0 \in ℤ \land J \in ℤ) \to (1 \in (0 \dots J) \leftrightarrow (0 \leq 1 \land 1 \leq J))$
190	186 187 188 189	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to (1 \in (0 \dots J) \leftrightarrow (0 \leq 1 \land 1 \leq J))$
191	182 185 190	mpbir2and	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \in (0 \dots J)$
192	34	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to \neg 2 ∥ 1$
193		eleq1	$⊢ a = 1 \to (a \in (0 \dots J) \leftrightarrow 1 \in (0 \dots J))$
194		breq2	$⊢ a = 1 \to (2 ∥ a \leftrightarrow 2 ∥ 1)$
195	194	notbid	$⊢ a = 1 \to (\neg 2 ∥ a \leftrightarrow \neg 2 ∥ 1)$
196	193 195	anbi12d	$⊢ a = 1 \to ((a \in (0 \dots J) \land \neg 2 ∥ a) \leftrightarrow (1 \in (0 \dots J) \land \neg 2 ∥ 1))$
197	196	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to ((a \in (0 \dots J) \land \neg 2 ∥ a) \leftrightarrow (1 \in (0 \dots J) \land \neg 2 ∥ 1))$
198	191 192 197	mpbir2and	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
199	180 198	jaodan	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
200	173 199	impbida	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to ((a \in (0 \dots J) \land \neg 2 ∥ a) \leftrightarrow ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1))$
201	30	elrab	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \leftrightarrow (a \in (0 \dots J) \land \neg 2 ∥ a)$
202		elun	$⊢ a \in (\{b \in (3 \dots J) \| \neg 2 ∥ b\} \cup \{1\}) \leftrightarrow (a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \lor a \in \{1\})$
203		velsn	$⊢ a \in \{1\} \leftrightarrow a = 1$
204	31 203	orbi12i	$⊢ (a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\} \lor a \in \{1\}) \leftrightarrow ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)$
205	202 204	bitri	$⊢ a \in (\{b \in (3 \dots J) \| \neg 2 ∥ b\} \cup \{1\}) \leftrightarrow ((a \in (3 \dots J) \land \neg 2 ∥ a) \lor a = 1)$
206	200 201 205	3bitr4g	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \leftrightarrow a \in (\{b \in (3 \dots J) \| \neg 2 ∥ b\} \cup \{1\}))$
207	206	eqrdv	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \{b \in (0 \dots J) \| \neg 2 ∥ b\} = \{b \in (3 \dots J) \| \neg 2 ∥ b\} \cup \{1\}$
208		fzfi	$⊢ (0 \dots J) \in Fin$
209		ssrab2	$⊢ \{b \in (0 \dots J) \| \neg 2 ∥ b\} \subseteq (0 \dots J)$
210		ssfi	$⊢ ((0 \dots J) \in Fin \land \{b \in (0 \dots J) \| \neg 2 ∥ b\} \subseteq (0 \dots J)) \to \{b \in (0 \dots J) \| \neg 2 ∥ b\} \in Fin$
211	208 209 210	mp2an	$⊢ \{b \in (0 \dots J) \| \neg 2 ∥ b\} \in Fin$
212	211	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \{b \in (0 \dots J) \| \neg 2 ∥ b\} \in Fin$
213	209	sseli	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in (0 \dots J)$
214	213 160	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℤ$
215	7 214 11	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) \in ℕ_{0}$
216	215	nn0cnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) \in ℂ$
217	17	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A X_{rm} N \in ℕ_{0}$
218	217	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A X_{rm} N \in ℂ$
219	218	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to A X_{rm} N \in ℂ$
220	213	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to a \in (0 \dots J)$
221		fznn0sub	$⊢ a \in (0 \dots J) \to J - a \in ℕ_{0}$
222	220 221	syl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to J - a \in ℕ_{0}$
223	219 222	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} \in ℂ$
224	90	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N \in ℂ$
225	213 114	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℕ_{0}$
226		expcl	$⊢ (A Y_{rm} N \in ℂ \land a \in ℕ_{0}) \to {(A Y_{rm} N)}^{a} \in ℂ$
227	224 225 226	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a} \in ℂ$
228		rmspecpos	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℝ^{+}$
229	228	rpcnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
230	229	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A^{2} - 1 \in ℂ$
231	201	simprbi	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ a$
232		1zzd	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 1 \in ℤ$
233	34	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ 1$
234	214 231 232 233 36	syl22anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 ∥ (a - 1)$
235	38	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℤ$
236	40	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \neq 0$
237	214 42	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℤ$
238	235 236 237 44	syl3anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to (2 ∥ (a - 1) \leftrightarrow \frac{a - 1}{2} \in ℤ)$
239	234 238	mpbid	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℤ$
240	237	zred	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℝ$
241	148	a1i	$⊢ a \in (0 \dots J) \to (a = 0 \to 2 ∥ a)$
242	241	con3dimp	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to \neg a = 0$
243	201 242	sylbi	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg a = 0$
244	225 153	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to (a \in ℕ \lor a = 0)$
245		orel2	$⊢ \neg a = 0 \to ((a \in ℕ \lor a = 0) \to a \in ℕ)$
246	243 244 245	sylc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℕ$
247	246 58	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℕ_{0}$
248	247	nn0ge0d	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 \leq a - 1$
249	62	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℝ$
250	64	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 < 2$
251	240 248 249 250 66	syl22anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 \leq \frac{a - 1}{2}$
252	239 251 68	sylanbrc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℕ_{0}$
253		expcl	$⊢ (A^{2} - 1 \in ℂ \land \frac{a - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
254	230 252 253	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
255	227 254	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
256	223 255	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
257	216 256	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
258	111 207 212 257	fsumsplit	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} + \sum_{a \in \{1\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
259		expcl	$⊢ (A Y_{rm} N \in ℂ \land 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{3} \in ℂ$
260	224 91 259	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} \in ℂ$
261	88	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℂ$
262	5 260 261	fsummulc1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
263	12	nn0cnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) \in ℂ$
264	218	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A X_{rm} N \in ℂ$
265	264 22	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} \in ℂ$
266	230 69 253	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
267		expcl	$⊢ (A Y_{rm} N \in ℂ \land a - 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{a - 3} \in ℂ$
268	224 82 267	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3} \in ℂ$
269	266 268	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℂ$
270	265 269	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℂ$
271	260	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{3} \in ℂ$
272	263 270 271	mulassd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
273	265 269 271	mulassd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
274	266 268 271	mulassd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
275	268 271	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} \in ℂ$
276	266 275	mulcomd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
277	224	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to A Y_{rm} N \in ℂ$
278	91	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to 3 \in ℕ_{0}$
279	277 278 83	expaddd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3 + 3} = {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
280	10	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to a \in ℤ$
281	280	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to a \in ℂ$
282		3cn	$⊢ 3 \in ℂ$
283		npcan	$⊢ (a \in ℂ \land 3 \in ℂ) \to a - 3 + 3 = a$
284	281 282 283	sylancl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to a - 3 + 3 = a$
285	284	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3 + 3} = {(A Y_{rm} N)}^{a}$
286	279 285	eqtr3d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A Y_{rm} N)}^{a}$
287	286	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} {(A^{2} - 1)}^{\frac{a - 1}{2}} = {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
288	274 276 287	3eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
289	288	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
290	273 289	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
291	290	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
292	272 291	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}) \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
293	292	sumeq2dv	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}}$
294	262 293	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
295		1nn	$⊢ 1 \in ℕ$
296		bccl	$⊢ (J \in ℕ_{0} \land 1 \in ℤ) \to (\binom{J}{1}) \in ℕ_{0}$
297	6 126 296	sylancl	$⊢ J \in ℕ \to (\binom{J}{1}) \in ℕ_{0}$
298	297	nn0cnd	$⊢ J \in ℕ \to (\binom{J}{1}) \in ℂ$
299	298	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (\binom{J}{1}) \in ℂ$
300		nnm1nn0	$⊢ J \in ℕ \to J - 1 \in ℕ_{0}$
301	300	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J - 1 \in ℕ_{0}$
302	218 301	expcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A X_{rm} N)}^{J - 1} \in ℂ$
303		1nn0	$⊢ 1 \in ℕ_{0}$
304		expcl	$⊢ (A Y_{rm} N \in ℂ \land 1 \in ℕ_{0}) \to {(A Y_{rm} N)}^{1} \in ℂ$
305	224 303 304	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} \in ℂ$
306		1m1e0	$⊢ 1 - 1 = 0$
307	306	oveq1i	$⊢ \frac{1 - 1}{2} = \frac{0}{2}$
308		2cn	$⊢ 2 \in ℂ$
309	308 40	div0i	$⊢ \frac{0}{2} = 0$
310	307 309	eqtri	$⊢ \frac{1 - 1}{2} = 0$
311		0nn0	$⊢ 0 \in ℕ_{0}$
312	310 311	eqeltri	$⊢ \frac{1 - 1}{2} \in ℕ_{0}$
313		expcl	$⊢ (A^{2} - 1 \in ℂ \land \frac{1 - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
314	230 312 313	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
315	305 314	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
316	302 315	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
317	299 316	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
318		oveq2	$⊢ a = 1 \to (\binom{J}{a}) = (\binom{J}{1})$
319		oveq2	$⊢ a = 1 \to J - a = J - 1$
320	319	oveq2d	$⊢ a = 1 \to {(A X_{rm} N)}^{J - a} = {(A X_{rm} N)}^{J - 1}$
321		oveq2	$⊢ a = 1 \to {(A Y_{rm} N)}^{a} = {(A Y_{rm} N)}^{1}$
322		oveq1	$⊢ a = 1 \to a - 1 = 1 - 1$
323	322	oveq1d	$⊢ a = 1 \to \frac{a - 1}{2} = \frac{1 - 1}{2}$
324	323	oveq2d	$⊢ a = 1 \to {(A^{2} - 1)}^{\frac{a - 1}{2}} = {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
325	321 324	oveq12d	$⊢ a = 1 \to {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
326	320 325	oveq12d	$⊢ a = 1 \to {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
327	318 326	oveq12d	$⊢ a = 1 \to (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
328	327	sumsn	$⊢ (1 \in ℕ \land (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ) \to \sum_{a \in \{1\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
329	295 317 328	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{1\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
330	294 329	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} + \sum_{a \in \{1\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A Y_{rm} N)}^{a} {(A^{2} - 1)}^{\frac{a - 1}{2}} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} + (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
331	97 258 330	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N \cdot J = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} + (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
332		bcn1	$⊢ J \in ℕ_{0} \to (\binom{J}{1}) = J$
333	7 332	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (\binom{J}{1}) = J$
334	333	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J = (\binom{J}{1})$
335	224	exp1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} = A Y_{rm} N$
336	310	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \frac{1 - 1}{2} = 0$
337	336	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} = {(A^{2} - 1)}^{0}$
338	230	exp0d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{0} = 1$
339	337 338	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} = 1$
340	335 339	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} = (A Y_{rm} N) \cdot 1$
341	224	mulid1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (A Y_{rm} N) \cdot 1 = A Y_{rm} N$
342	340 341	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N = {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
343	342	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A X_{rm} N)}^{J - 1} (A Y_{rm} N) = {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
344	334 343	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J {(A X_{rm} N)}^{J - 1} (A Y_{rm} N) = (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
345	331 344	oveq12d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (A Y_{rm} N \cdot J) - J {(A X_{rm} N)}^{J - 1} (A Y_{rm} N) = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} + (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} - (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
346	5 261	fsumcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} \in ℂ$
347	346 260	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} \in ℂ$
348	347 317	pncand	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3} + (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} - (\binom{J}{1}) {(A X_{rm} N)}^{J - 1} {(A Y_{rm} N)}^{1} {(A^{2} - 1)}^{\frac{1 - 1}{2}} = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
349	345 348	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (A Y_{rm} N \cdot J) - J {(A X_{rm} N)}^{J - 1} (A Y_{rm} N) = \sum_{a \in \{b \in (3 \dots J) \| \neg 2 ∥ b\}} (\binom{J}{a}) {(A X_{rm} N)}^{J - a} {(A^{2} - 1)}^{\frac{a - 1}{2}} {(A Y_{rm} N)}^{a - 3} {(A Y_{rm} N)}^{3}$
350	95 349	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} ∥ ((A Y_{rm} N \cdot J) - J {(A X_{rm} N)}^{J - 1} (A Y_{rm} N))$

Metamath Proof Explorer

Theorem jm2.23

Proof