Theorem 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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑁 · 𝐽 ) ) = Σ 𝑖 ∈ { 𝑥 ∈ ( 0 ... 𝐽 ) ∣ ¬ 2 ∥ 𝑥 } ( ( 𝐽 C 𝑖 ) · ( ( ( 𝐴 Xrm 𝑁 ) ↑ ( 𝐽 − 𝑖 ) ) · ( ( ( 𝐴 Yrm 𝑁 ) ↑ 𝑖 ) · ( ( ( 𝐴 ↑ 2 ) − 1 ) ↑ ( ( 𝑖 − 1 ) / 2 ) ) ) ) ) )

Proof

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