jm2.22

Description: Lemma for jm2.20nn . Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014) (Revised by Stefan O'Rear, 6-May-2015)

		Ref	Expression
	Assertion	jm2.22	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ J \in ℕ_{0} \to J \in ℤ$
2		jm2.21	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℤ) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J}$
3	1 2	syl3an3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J}$
4		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
5	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
6	5	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A X_{rm} N \in ℕ_{0}$
7	6	nn0cnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A X_{rm} N \in ℂ$
8		eluzelz	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ$
9		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
10		peano2zm	$⊢ A^{2} \in ℤ \to A^{2} - 1 \in ℤ$
11	8 9 10	3syl	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℤ$
12	11	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A^{2} - 1 \in ℤ$
13	12	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A^{2} - 1 \in ℂ$
14	13	sqrtcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sqrt{A^{2} - 1} \in ℂ$
15		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
16	15	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
17	16	3adant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \in ℤ$
18	17	zcnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \in ℂ$
19	14 18	mulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ$
20		simp3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to J \in ℕ_{0}$
21		binom	$⊢ (A X_{rm} N \in ℂ \land \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ \land J \in ℕ_{0}) \to {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J} = \sum_{i = 0}^{J} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
22	7 19 20 21	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to {((A X_{rm} N) + \sqrt{A^{2} - 1} (A Y_{rm} N))}^{J} = \sum_{i = 0}^{J} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
23		rabnc	$⊢ \{x \in (0 \dots J) \| 2 ∥ x\} \cap \{x \in (0 \dots J) \| \neg 2 ∥ x\} = \emptyset$
24	23	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \{x \in (0 \dots J) \| 2 ∥ x\} \cap \{x \in (0 \dots J) \| \neg 2 ∥ x\} = \emptyset$
25		rabxm	$⊢ (0 \dots J) = \{x \in (0 \dots J) \| 2 ∥ x\} \cup \{x \in (0 \dots J) \| \neg 2 ∥ x\}$
26	25	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to (0 \dots J) = \{x \in (0 \dots J) \| 2 ∥ x\} \cup \{x \in (0 \dots J) \| \neg 2 ∥ x\}$
27		fzfid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to (0 \dots J) \in Fin$
28		simpl3	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to J \in ℕ_{0}$
29		elfzelz	$⊢ i \in (0 \dots J) \to i \in ℤ$
30	29	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to i \in ℤ$
31		bccl	$⊢ (J \in ℕ_{0} \land i \in ℤ) \to (\binom{J}{i}) \in ℕ_{0}$
32	31	nn0zd	$⊢ (J \in ℕ_{0} \land i \in ℤ) \to (\binom{J}{i}) \in ℤ$
33	28 30 32	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to (\binom{J}{i}) \in ℤ$
34	33	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to (\binom{J}{i}) \in ℂ$
35	6	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A X_{rm} N \in ℤ$
36	35	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A X_{rm} N \in ℤ$
37	36	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A X_{rm} N \in ℂ$
38		fznn0sub	$⊢ i \in (0 \dots J) \to J - i \in ℕ_{0}$
39	38	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to J - i \in ℕ_{0}$
40	37 39	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {(A X_{rm} N)}^{J - i} \in ℂ$
41	12	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A^{2} - 1 \in ℤ$
42	41	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A^{2} - 1 \in ℂ$
43	42	sqrtcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to \sqrt{A^{2} - 1} \in ℂ$
44	17	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A Y_{rm} N \in ℤ$
45	44	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to A Y_{rm} N \in ℂ$
46	43 45	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to \sqrt{A^{2} - 1} (A Y_{rm} N) \in ℂ$
47		elfznn0	$⊢ i \in (0 \dots J) \to i \in ℕ_{0}$
48	47	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to i \in ℕ_{0}$
49	46 48	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℂ$
50	40 49	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℂ$
51	34 50	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℂ$
52	24 26 27 51	fsumsplit	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i = 0}^{J} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
53		fzfi	$⊢ (0 \dots J) \in Fin$
54		ssrab2	$⊢ \{x \in (0 \dots J) \| \neg 2 ∥ x\} \subseteq (0 \dots J)$
55		ssfi	$⊢ ((0 \dots J) \in Fin \land \{x \in (0 \dots J) \| \neg 2 ∥ x\} \subseteq (0 \dots J)) \to \{x \in (0 \dots J) \| \neg 2 ∥ x\} \in Fin$
56	53 54 55	mp2an	$⊢ \{x \in (0 \dots J) \| \neg 2 ∥ x\} \in Fin$
57	56	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \{x \in (0 \dots J) \| \neg 2 ∥ x\} \in Fin$
58		breq2	$⊢ x = i \to (2 ∥ x \leftrightarrow 2 ∥ i)$
59	58	notbid	$⊢ x = i \to (\neg 2 ∥ x \leftrightarrow \neg 2 ∥ i)$
60	59	elrab	$⊢ i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\} \leftrightarrow (i \in (0 \dots J) \land \neg 2 ∥ i)$
61	34	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to (\binom{J}{i}) \in ℂ$
62	40	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} \in ℂ$
63		zexpcl	$⊢ (A Y_{rm} N \in ℤ \land i \in ℕ_{0}) \to {(A Y_{rm} N)}^{i} \in ℤ$
64	17 47 63	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {(A Y_{rm} N)}^{i} \in ℤ$
65	64	zcnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {(A Y_{rm} N)}^{i} \in ℂ$
66	65	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} \in ℂ$
67	42	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to A^{2} - 1 \in ℂ$
68	29	adantr	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i \in ℤ$
69		simpr	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to \neg 2 ∥ i$
70		1zzd	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 1 \in ℤ$
71		n2dvds1	$⊢ \neg 2 ∥ 1$
72	71	a1i	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to \neg 2 ∥ 1$
73		omoe	$⊢ ((i \in ℤ \land \neg 2 ∥ i) \land (1 \in ℤ \land \neg 2 ∥ 1)) \to 2 ∥ (i - 1)$
74	68 69 70 72 73	syl22anc	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 2 ∥ (i - 1)$
75		2z	$⊢ 2 \in ℤ$
76	75	a1i	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 2 \in ℤ$
77		2ne0	$⊢ 2 \neq 0$
78	77	a1i	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 2 \neq 0$
79		peano2zm	$⊢ i \in ℤ \to i - 1 \in ℤ$
80	29 79	syl	$⊢ i \in (0 \dots J) \to i - 1 \in ℤ$
81	80	adantr	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i - 1 \in ℤ$
82		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land i - 1 \in ℤ) \to (2 ∥ (i - 1) \leftrightarrow \frac{i - 1}{2} \in ℤ)$
83	76 78 81 82	syl3anc	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to (2 ∥ (i - 1) \leftrightarrow \frac{i - 1}{2} \in ℤ)$
84	74 83	mpbid	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to \frac{i - 1}{2} \in ℤ$
85	80	zred	$⊢ i \in (0 \dots J) \to i - 1 \in ℝ$
86	85	adantr	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i - 1 \in ℝ$
87		dvds0	$⊢ 2 \in ℤ \to 2 ∥ 0$
88	75 87	ax-mp	$⊢ 2 ∥ 0$
89		breq2	$⊢ i = 0 \to (2 ∥ i \leftrightarrow 2 ∥ 0)$
90	88 89	mpbiri	$⊢ i = 0 \to 2 ∥ i$
91	90	con3i	$⊢ \neg 2 ∥ i \to \neg i = 0$
92	91	adantl	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to \neg i = 0$
93	47	adantr	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i \in ℕ_{0}$
94		elnn0	$⊢ i \in ℕ_{0} \leftrightarrow (i \in ℕ \lor i = 0)$
95	93 94	sylib	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to (i \in ℕ \lor i = 0)$
96		orel2	$⊢ \neg i = 0 \to ((i \in ℕ \lor i = 0) \to i \in ℕ)$
97	92 95 96	sylc	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i \in ℕ$
98		nnm1nn0	$⊢ i \in ℕ \to i - 1 \in ℕ_{0}$
99	97 98	syl	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to i - 1 \in ℕ_{0}$
100	99	nn0ge0d	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 0 \leq i - 1$
101		2re	$⊢ 2 \in ℝ$
102	101	a1i	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 2 \in ℝ$
103		2pos	$⊢ 0 < 2$
104	103	a1i	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 0 < 2$
105		divge0	$⊢ ((i - 1 \in ℝ \land 0 \leq i - 1) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{i - 1}{2}$
106	86 100 102 104 105	syl22anc	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to 0 \leq \frac{i - 1}{2}$
107		elnn0z	$⊢ \frac{i - 1}{2} \in ℕ_{0} \leftrightarrow (\frac{i - 1}{2} \in ℤ \land 0 \leq \frac{i - 1}{2})$
108	84 106 107	sylanbrc	$⊢ (i \in (0 \dots J) \land \neg 2 ∥ i) \to \frac{i - 1}{2} \in ℕ_{0}$
109	108	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \frac{i - 1}{2} \in ℕ_{0}$
110	67 109	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℂ$
111	66 110	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℂ$
112	62 111	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℂ$
113	61 112	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℂ$
114	60 113	sylan2b	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℂ$
115	57 14 114	fsummulc2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} \sqrt{A^{2} - 1} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
116	43	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} \in ℂ$
117	116 61 112	mul12d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = (\binom{J}{i}) \sqrt{A^{2} - 1} {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
118	116 62 111	mul12d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A X_{rm} N)}^{J - i} \sqrt{A^{2} - 1} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
119	43 48	expcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {\sqrt{A^{2} - 1}}^{i} \in ℂ$
120	119	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{i} \in ℂ$
121	66 120	mulcomd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} {\sqrt{A^{2} - 1}}^{i} = {\sqrt{A^{2} - 1}}^{i} {(A Y_{rm} N)}^{i}$
122	116 66 110	mul12d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A Y_{rm} N)}^{i} \sqrt{A^{2} - 1} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
123		2nn0	$⊢ 2 \in ℕ_{0}$
124	123	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to 2 \in ℕ_{0}$
125	116 109 124	expmuld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{2 (\frac{i - 1}{2})} = {({\sqrt{A^{2} - 1}}^{2})}^{\frac{i - 1}{2}}$
126	80	zcnd	$⊢ i \in (0 \dots J) \to i - 1 \in ℂ$
127	126	ad2antrl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to i - 1 \in ℂ$
128		2cnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to 2 \in ℂ$
129	77	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to 2 \neq 0$
130	127 128 129	divcan2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to 2 (\frac{i - 1}{2}) = i - 1$
131	130	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{2 (\frac{i - 1}{2})} = {\sqrt{A^{2} - 1}}^{i - 1}$
132	67	sqsqrtd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{2} = A^{2} - 1$
133	132	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {({\sqrt{A^{2} - 1}}^{2})}^{\frac{i - 1}{2}} = {(A^{2} - 1)}^{\frac{i - 1}{2}}$
134	125 131 133	3eqtr3rd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i - 1}{2}} = {\sqrt{A^{2} - 1}}^{i - 1}$
135	134	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i - 1}{2}} \sqrt{A^{2} - 1} = {\sqrt{A^{2} - 1}}^{i - 1} \sqrt{A^{2} - 1}$
136	116 110	mulcomd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A^{2} - 1)}^{\frac{i - 1}{2}} \sqrt{A^{2} - 1}$
137	97	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to i \in ℕ$
138		expm1t	$⊢ (\sqrt{A^{2} - 1} \in ℂ \land i \in ℕ) \to {\sqrt{A^{2} - 1}}^{i} = {\sqrt{A^{2} - 1}}^{i - 1} \sqrt{A^{2} - 1}$
139	116 137 138	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{i} = {\sqrt{A^{2} - 1}}^{i - 1} \sqrt{A^{2} - 1}$
140	135 136 139	3eqtr4d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {\sqrt{A^{2} - 1}}^{i}$
141	140	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} \sqrt{A^{2} - 1} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A Y_{rm} N)}^{i} {\sqrt{A^{2} - 1}}^{i}$
142	122 141	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A Y_{rm} N)}^{i} {\sqrt{A^{2} - 1}}^{i}$
143	43 45 48	mulexpd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = {\sqrt{A^{2} - 1}}^{i} {(A Y_{rm} N)}^{i}$
144	143	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = {\sqrt{A^{2} - 1}}^{i} {(A Y_{rm} N)}^{i}$
145	121 142 144	3eqtr4d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
146	145	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} \sqrt{A^{2} - 1} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
147	118 146	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
148	147	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to (\binom{J}{i}) \sqrt{A^{2} - 1} {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
149	117 148	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to \sqrt{A^{2} - 1} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
150	60 149	sylan2b	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}) \to \sqrt{A^{2} - 1} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
151	150	sumeq2dv	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} \sqrt{A^{2} - 1} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i}$
152	115 151	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
153	152	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
154	52 153	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i = 0}^{J} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
155	3 22 154	3eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to (A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$
156		rmspecsqrtnq	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
157	156	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
158		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
159		simp1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A \in ℤ_{\geq 2}$
160		simp2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to N \in ℤ$
161	1	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to J \in ℤ$
162	160 161	zmulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to N \cdot J \in ℤ$
163	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \cdot J \in ℤ) \to A X_{rm} N \cdot J \in ℕ_{0}$
164	159 162 163	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A X_{rm} N \cdot J \in ℕ_{0}$
165	158 164	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A X_{rm} N \cdot J \in ℚ$
166		zssq	$⊢ ℤ \subseteq ℚ$
167	15	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \cdot J \in ℤ) \to A Y_{rm} N \cdot J \in ℤ$
168	159 162 167	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \cdot J \in ℤ$
169	166 168	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \cdot J \in ℚ$
170		ssrab2	$⊢ \{x \in (0 \dots J) \| 2 ∥ x\} \subseteq (0 \dots J)$
171		ssfi	$⊢ ((0 \dots J) \in Fin \land \{x \in (0 \dots J) \| 2 ∥ x\} \subseteq (0 \dots J)) \to \{x \in (0 \dots J) \| 2 ∥ x\} \in Fin$
172	53 170 171	mp2an	$⊢ \{x \in (0 \dots J) \| 2 ∥ x\} \in Fin$
173	172	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \{x \in (0 \dots J) \| 2 ∥ x\} \in Fin$
174	58	elrab	$⊢ i \in \{x \in (0 \dots J) \| 2 ∥ x\} \leftrightarrow (i \in (0 \dots J) \land 2 ∥ i)$
175	33	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to (\binom{J}{i}) \in ℤ$
176		zexpcl	$⊢ (A X_{rm} N \in ℤ \land J - i \in ℕ_{0}) \to {(A X_{rm} N)}^{J - i} \in ℤ$
177	36 39 176	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to {(A X_{rm} N)}^{J - i} \in ℤ$
178	177	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} \in ℤ$
179	43	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to \sqrt{A^{2} - 1} \in ℂ$
180	45	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to A Y_{rm} N \in ℂ$
181	47	ad2antrl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to i \in ℕ_{0}$
182	179 180 181	mulexpd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = {\sqrt{A^{2} - 1}}^{i} {(A Y_{rm} N)}^{i}$
183	29	zcnd	$⊢ i \in (0 \dots J) \to i \in ℂ$
184	183	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to i \in ℂ$
185		2cnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to 2 \in ℂ$
186	77	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to 2 \neq 0$
187	184 185 186	divcan2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to 2 (\frac{i}{2}) = i$
188	187	eqcomd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in (0 \dots J)) \to i = 2 (\frac{i}{2})$
189	188	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to i = 2 (\frac{i}{2})$
190	189	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{i} = {\sqrt{A^{2} - 1}}^{2 (\frac{i}{2})}$
191	75	a1i	$⊢ i \in ℕ_{0} \to 2 \in ℤ$
192	77	a1i	$⊢ i \in ℕ_{0} \to 2 \neq 0$
193		nn0z	$⊢ i \in ℕ_{0} \to i \in ℤ$
194		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land i \in ℤ) \to (2 ∥ i \leftrightarrow \frac{i}{2} \in ℤ)$
195	191 192 193 194	syl3anc	$⊢ i \in ℕ_{0} \to (2 ∥ i \leftrightarrow \frac{i}{2} \in ℤ)$
196	195	biimpa	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to \frac{i}{2} \in ℤ$
197		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
198	197	adantr	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to i \in ℝ$
199		nn0ge0	$⊢ i \in ℕ_{0} \to 0 \leq i$
200	199	adantr	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to 0 \leq i$
201	101	a1i	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to 2 \in ℝ$
202	103	a1i	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to 0 < 2$
203		divge0	$⊢ ((i \in ℝ \land 0 \leq i) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{i}{2}$
204	198 200 201 202 203	syl22anc	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to 0 \leq \frac{i}{2}$
205		elnn0z	$⊢ \frac{i}{2} \in ℕ_{0} \leftrightarrow (\frac{i}{2} \in ℤ \land 0 \leq \frac{i}{2})$
206	196 204 205	sylanbrc	$⊢ (i \in ℕ_{0} \land 2 ∥ i) \to \frac{i}{2} \in ℕ_{0}$
207	47 206	sylan	$⊢ (i \in (0 \dots J) \land 2 ∥ i) \to \frac{i}{2} \in ℕ_{0}$
208	207	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to \frac{i}{2} \in ℕ_{0}$
209	123	a1i	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to 2 \in ℕ_{0}$
210	179 208 209	expmuld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{2 (\frac{i}{2})} = {({\sqrt{A^{2} - 1}}^{2})}^{\frac{i}{2}}$
211	42	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to A^{2} - 1 \in ℂ$
212	211	sqsqrtd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{2} = A^{2} - 1$
213	212	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {({\sqrt{A^{2} - 1}}^{2})}^{\frac{i}{2}} = {(A^{2} - 1)}^{\frac{i}{2}}$
214	190 210 213	3eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{i} = {(A^{2} - 1)}^{\frac{i}{2}}$
215	214	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1}}^{i} {(A Y_{rm} N)}^{i} = {(A^{2} - 1)}^{\frac{i}{2}} {(A Y_{rm} N)}^{i}$
216	182 215	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} = {(A^{2} - 1)}^{\frac{i}{2}} {(A Y_{rm} N)}^{i}$
217		zexpcl	$⊢ (A^{2} - 1 \in ℤ \land \frac{i}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{i}{2}} \in ℤ$
218	12 207 217	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i}{2}} \in ℤ$
219	64	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {(A Y_{rm} N)}^{i} \in ℤ$
220	218 219	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i}{2}} {(A Y_{rm} N)}^{i} \in ℤ$
221	216 220	eqeltrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℤ$
222	178 221	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℤ$
223	175 222	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land 2 ∥ i)) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℤ$
224	174 223	sylan2b	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in \{x \in (0 \dots J) \| 2 ∥ x\}) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℤ$
225	173 224	fsumzcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℤ$
226	166 225	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℚ$
227	33	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to (\binom{J}{i}) \in ℤ$
228	177	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} \in ℤ$
229	64	adantrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} \in ℤ$
230		zexpcl	$⊢ (A^{2} - 1 \in ℤ \land \frac{i - 1}{2} \in ℕ_{0}) \to {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
231	12 108 230	syl2an	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
232	229 231	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
233	228 232	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
234	227 233	zmulcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land (i \in (0 \dots J) \land \neg 2 ∥ i)) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
235	60 234	sylan2b	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \land i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}) \to (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
236	57 235	fsumzcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℤ$
237	166 236	sseldi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℚ$
238		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (A X_{rm} N \cdot J \in ℚ \land A Y_{rm} N \cdot J \in ℚ) \land (\sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \in ℚ \land \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \in ℚ)) \to ((A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \leftrightarrow (A X_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \land A Y_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}))$
239	157 165 169 226 237 238	syl122anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to ((A X_{rm} N \cdot J) + \sqrt{A^{2} - 1} (A Y_{rm} N \cdot J) = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} + \sqrt{A^{2} - 1} \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}} \leftrightarrow (A X_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \land A Y_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}))$
240	155 239	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to (A X_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {\sqrt{A^{2} - 1} (A Y_{rm} N)}^{i} \land A Y_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}})$
241	240	simprd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land J \in ℕ_{0}) \to A Y_{rm} N \cdot J = \sum_{i \in \{x \in (0 \dots J) \| \neg 2 ∥ x\}} (\binom{J}{i}) {(A X_{rm} N)}^{J - i} {(A Y_{rm} N)}^{i} {(A^{2} - 1)}^{\frac{i - 1}{2}}$

Metamath Proof Explorer

Theorem jm2.22

Proof