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		3z	$⊢ 3 \in ℤ$
115	114	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 ℤ$
116		nnz	$⊢ J \in ℕ \to J \in ℤ$
117	116	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J \in ℤ$
118	117	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 ℤ$
119		elfzelz	$⊢ a \in (0 \dots J) \to a \in ℤ$
120	119	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \in ℤ$
121	120	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 ℤ$
122		elfznn0	$⊢ a \in (0 \dots J) \to a \in ℕ_{0}$
123	122	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \in ℕ_{0}$
124	123	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}$
125		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$
126		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$
127		elnn1uz2	$⊢ a \in ℕ \leftrightarrow (a = 1 \lor a \in ℤ_{\geq 2})$
128		df-ne	$⊢ a \neq 1 \leftrightarrow \neg a = 1$
129	128	biimpi	$⊢ a \neq 1 \to \neg a = 1$
130	129	3ad2ant3	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to \neg a = 1$
131	130	pm2.21d	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to (a = 1 \to 3 \leq a)$
132	131	imp	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 1) \to 3 \leq a$
133		uzp1	$⊢ a \in ℤ_{\geq 2} \to (a = 2 \lor a \in ℤ_{\geq (2 + 1)})$
134		1z	$⊢ 1 \in ℤ$
135		dvdsmul1	$⊢ (2 \in ℤ \land 1 \in ℤ) \to 2 ∥ 2 \cdot 1$
136	38 134 135	mp2an	$⊢ 2 ∥ 2 \cdot 1$
137		2t1e2	$⊢ 2 \cdot 1 = 2$
138	136 137	breqtri	$⊢ 2 ∥ 2$
139		breq2	$⊢ a = 2 \to (2 ∥ a \leftrightarrow 2 ∥ 2)$
140	139	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to (2 ∥ a \leftrightarrow 2 ∥ 2)$
141	138 140	mpbiri	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to 2 ∥ a$
142		simpl2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to \neg 2 ∥ a$
143	141 142	pm2.21dd	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 2) \to 3 \leq a$
144		eluzle	$⊢ a \in ℤ_{\geq 3} \to 3 \leq a$
145		2p1e3	$⊢ 2 + 1 = 3$
146	145	fveq2i	$⊢ ℤ_{\geq (2 + 1)} = ℤ_{\geq 3}$
147	144 146	eleq2s	$⊢ a \in ℤ_{\geq (2 + 1)} \to 3 \leq a$
148	147	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℤ_{\geq (2 + 1)}) \to 3 \leq a$
149	143 148	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$
150	133 149	sylan2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℤ_{\geq 2}) \to 3 \leq a$
151	132 150	jaodan	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land (a = 1 \lor a \in ℤ_{\geq 2})) \to 3 \leq a$
152	127 151	sylan2b	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a \in ℕ) \to 3 \leq a$
153		dvds0	$⊢ 2 \in ℤ \to 2 ∥ 0$
154	38 153	ax-mp	$⊢ 2 ∥ 0$
155		breq2	$⊢ a = 0 \to (2 ∥ a \leftrightarrow 2 ∥ 0)$
156	154 155	mpbiri	$⊢ a = 0 \to 2 ∥ a$
157	156	adantl	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to 2 ∥ a$
158		simpl2	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to \neg 2 ∥ a$
159	157 158	pm2.21dd	$⊢ ((a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \land a = 0) \to 3 \leq a$
160		elnn0	$⊢ a \in ℕ_{0} \leftrightarrow (a \in ℕ \lor a = 0)$
161	160	biimpi	$⊢ a \in ℕ_{0} \to (a \in ℕ \lor a = 0)$
162	161	3ad2ant1	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to (a \in ℕ \lor a = 0)$
163	152 159 162	mpjaodan	$⊢ (a \in ℕ_{0} \land \neg 2 ∥ a \land a \neq 1) \to 3 \leq a$
164	124 125 126 163	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$
165		elfzle2	$⊢ a \in (0 \dots J) \to a \leq J$
166	165	adantr	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to a \leq J$
167	166	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$
168	115 118 121 164 167	elfzd	$⊢ (((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)$
169	168 125	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)$
170	169	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)$
171	113 170	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)$
172		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
173	91 172	eleqtri	$⊢ 3 \in ℤ_{\geq 0}$
174		fzss1	$⊢ 3 \in ℤ_{\geq 0} \to (3 \dots J) \subseteq (0 \dots J)$
175	173 174	ax-mp	$⊢ (3 \dots J) \subseteq (0 \dots J)$
176	175	sseli	$⊢ a \in (3 \dots J) \to a \in (0 \dots J)$
177	176	anim1i	$⊢ (a \in (3 \dots J) \land \neg 2 ∥ a) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
178	177	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)$
179		0zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 0 \in ℤ$
180	117	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to J \in ℤ$
181		1zzd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \in ℤ$
182		0le1	$⊢ 0 \leq 1$
183	182	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 0 \leq 1$
184		nnge1	$⊢ J \in ℕ \to 1 \leq J$
185	184	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to 1 \leq J$
186	185	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \leq J$
187	179 180 181 183 186	elfzd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to 1 \in (0 \dots J)$
188	34	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to \neg 2 ∥ 1$
189		eleq1	$⊢ a = 1 \to (a \in (0 \dots J) \leftrightarrow 1 \in (0 \dots J))$
190		breq2	$⊢ a = 1 \to (2 ∥ a \leftrightarrow 2 ∥ 1)$
191	190	notbid	$⊢ a = 1 \to (\neg 2 ∥ a \leftrightarrow \neg 2 ∥ 1)$
192	189 191	anbi12d	$⊢ a = 1 \to ((a \in (0 \dots J) \land \neg 2 ∥ a) \leftrightarrow (1 \in (0 \dots J) \land \neg 2 ∥ 1))$
193	192	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))$
194	187 188 193	mpbir2and	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \land a = 1) \to (a \in (0 \dots J) \land \neg 2 ∥ a)$
195	178 194	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)$
196	171 195	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))$
197	30	elrab	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \leftrightarrow (a \in (0 \dots J) \land \neg 2 ∥ a)$
198		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\})$
199		velsn	$⊢ a \in \{1\} \leftrightarrow a = 1$
200	31 199	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)$
201	198 200	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)$
202	196 197 201	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\}))$
203	202	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\}$
204		fzfi	$⊢ (0 \dots J) \in Fin$
205		ssrab2	$⊢ \{b \in (0 \dots J) \| \neg 2 ∥ b\} \subseteq (0 \dots J)$
206		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$
207	204 205 206	mp2an	$⊢ \{b \in (0 \dots J) \| \neg 2 ∥ b\} \in Fin$
208	207	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \{b \in (0 \dots J) \| \neg 2 ∥ b\} \in Fin$
209	205	sseli	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in (0 \dots J)$
210	209 119	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℤ$
211	7 210 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}$
212	211	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 ℂ$
213	17	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A X_{rm} N \in ℕ_{0}$
214	213	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A X_{rm} N \in ℂ$
215	214	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 ℂ$
216	209	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)$
217		fznn0sub	$⊢ a \in (0 \dots J) \to J - a \in ℕ_{0}$
218	216 217	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}$
219	215 218	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 ℂ$
220	90	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A Y_{rm} N \in ℂ$
221	209 122	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℕ_{0}$
222		expcl	$⊢ (A Y_{rm} N \in ℂ \land a \in ℕ_{0}) \to {(A Y_{rm} N)}^{a} \in ℂ$
223	220 221 222	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 ℂ$
224		rmspecpos	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℝ^{+}$
225	224	rpcnd	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℂ$
226	225	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to A^{2} - 1 \in ℂ$
227	197	simprbi	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ a$
228		1zzd	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 1 \in ℤ$
229	34	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg 2 ∥ 1$
230	210 227 228 229 36	syl22anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 ∥ (a - 1)$
231	38	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℤ$
232	40	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \neq 0$
233	210 42	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℤ$
234	231 232 233 44	syl3anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to (2 ∥ (a - 1) \leftrightarrow \frac{a - 1}{2} \in ℤ)$
235	230 234	mpbid	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℤ$
236	233	zred	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℝ$
237	156	a1i	$⊢ a \in (0 \dots J) \to (a = 0 \to 2 ∥ a)$
238	237	con3dimp	$⊢ (a \in (0 \dots J) \land \neg 2 ∥ a) \to \neg a = 0$
239	197 238	sylbi	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \neg a = 0$
240	221 161	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to (a \in ℕ \lor a = 0)$
241		orel2	$⊢ \neg a = 0 \to ((a \in ℕ \lor a = 0) \to a \in ℕ)$
242	239 240 241	sylc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a \in ℕ$
243	242 58	syl	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to a - 1 \in ℕ_{0}$
244	243	nn0ge0d	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 \leq a - 1$
245	62	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 2 \in ℝ$
246	64	a1i	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 < 2$
247	236 244 245 246 66	syl22anc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to 0 \leq \frac{a - 1}{2}$
248	235 247 68	sylanbrc	$⊢ a \in \{b \in (0 \dots J) \| \neg 2 ∥ b\} \to \frac{a - 1}{2} \in ℕ_{0}$
249		expcl	$⊢ (A^{2} - 1 \in ℂ \land \frac{a - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{a - 1}{2}} \in ℂ$
250	226 248 249	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 ℂ$
251	223 250	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 ℂ$
252	219 251	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 ℂ$
253	212 252	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 ℂ$
254	111 203 208 253	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}}$
255		expcl	$⊢ (A Y_{rm} N \in ℂ \land 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{3} \in ℂ$
256	220 91 255	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{3} \in ℂ$
257	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 ℂ$
258	5 256 257	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}$
259	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 ℂ$
260	214	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 ℂ$
261	260 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 ℂ$
262	226 69 249	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 ℂ$
263		expcl	$⊢ (A Y_{rm} N \in ℂ \land a - 3 \in ℕ_{0}) \to {(A Y_{rm} N)}^{a - 3} \in ℂ$
264	220 82 263	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 ℂ$
265	262 264	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 ℂ$
266	261 265	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 ℂ$
267	256	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 ℂ$
268	259 266 267	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}$
269	261 265 267	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}$
270	262 264 267	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}$
271	264 267	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 ℂ$
272	262 271	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}}$
273	220	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 ℂ$
274	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}$
275	273 274 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}$
276	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 ℤ$
277	276	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 ℂ$
278		3cn	$⊢ 3 \in ℂ$
279		npcan	$⊢ (a \in ℂ \land 3 \in ℂ) \to a - 3 + 3 = a$
280	277 278 279	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$
281	280	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}$
282	275 281	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}$
283	282	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}}$
284	270 272 283	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}}$
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 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}}$
286	269 285	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}}$
287	286	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}}$
288	268 287	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}}$
289	288	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}}$
290	258 289	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}$
291		1nn	$⊢ 1 \in ℕ$
292		bccl	$⊢ (J \in ℕ_{0} \land 1 \in ℤ) \to (\binom{J}{1}) \in ℕ_{0}$
293	6 134 292	sylancl	$⊢ J \in ℕ \to (\binom{J}{1}) \in ℕ_{0}$
294	293	nn0cnd	$⊢ J \in ℕ \to (\binom{J}{1}) \in ℂ$
295	294	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (\binom{J}{1}) \in ℂ$
296		nnm1nn0	$⊢ J \in ℕ \to J - 1 \in ℕ_{0}$
297	296	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J - 1 \in ℕ_{0}$
298	214 297	expcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A X_{rm} N)}^{J - 1} \in ℂ$
299		1nn0	$⊢ 1 \in ℕ_{0}$
300		expcl	$⊢ (A Y_{rm} N \in ℂ \land 1 \in ℕ_{0}) \to {(A Y_{rm} N)}^{1} \in ℂ$
301	220 299 300	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} \in ℂ$
302		1m1e0	$⊢ 1 - 1 = 0$
303	302	oveq1i	$⊢ \frac{1 - 1}{2} = \frac{0}{2}$
304		2cn	$⊢ 2 \in ℂ$
305	304 40	div0i	$⊢ \frac{0}{2} = 0$
306	303 305	eqtri	$⊢ \frac{1 - 1}{2} = 0$
307		0nn0	$⊢ 0 \in ℕ_{0}$
308	306 307	eqeltri	$⊢ \frac{1 - 1}{2} \in ℕ_{0}$
309		expcl	$⊢ (A^{2} - 1 \in ℂ \land \frac{1 - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
310	226 308 309	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} \in ℂ$
311	301 310	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 ℂ$
312	298 311	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 ℂ$
313	295 312	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 ℂ$
314		oveq2	$⊢ a = 1 \to (\binom{J}{a}) = (\binom{J}{1})$
315		oveq2	$⊢ a = 1 \to J - a = J - 1$
316	315	oveq2d	$⊢ a = 1 \to {(A X_{rm} N)}^{J - a} = {(A X_{rm} N)}^{J - 1}$
317		oveq2	$⊢ a = 1 \to {(A Y_{rm} N)}^{a} = {(A Y_{rm} N)}^{1}$
318		oveq1	$⊢ a = 1 \to a - 1 = 1 - 1$
319	318	oveq1d	$⊢ a = 1 \to \frac{a - 1}{2} = \frac{1 - 1}{2}$
320	319	oveq2d	$⊢ a = 1 \to {(A^{2} - 1)}^{\frac{a - 1}{2}} = {(A^{2} - 1)}^{\frac{1 - 1}{2}}$
321	317 320	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}}$
322	316 321	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}}$
323	314 322	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}}$
324	323	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}}$
325	291 313 324	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}}$
326	290 325	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}}$
327	97 254 326	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}}$
328		bcn1	$⊢ J \in ℕ_{0} \to (\binom{J}{1}) = J$
329	7 328	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (\binom{J}{1}) = J$
330	329	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to J = (\binom{J}{1})$
331	220	exp1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A Y_{rm} N)}^{1} = A Y_{rm} N$
332	306	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to \frac{1 - 1}{2} = 0$
333	332	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} = {(A^{2} - 1)}^{0}$
334	226	exp0d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{0} = 1$
335	333 334	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to {(A^{2} - 1)}^{\frac{1 - 1}{2}} = 1$
336	331 335	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$
337	220	mulridd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ) \to (A Y_{rm} N) \cdot 1 = A Y_{rm} N$
338	336 337	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}}$
339	338	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}}$
340	330 339	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}}$
341	327 340	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}}$
342	5 257	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 ℂ$
343	342 256	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 ℂ$
344	343 313	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}$
345	341 344	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}$
346	95 345	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