Theorem dchrisum0flblem1

Description: Lemma for dchrisum0flb . Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
	dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum0flb.r	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
	dchrisum0flblem1.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	dchrisum0flblem1.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
Assertion	dchrisum0flblem1	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
8		dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		dchrisum0flb.r	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
10		dchrisum0flblem1.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
11		dchrisum0flblem1.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
12		1red	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 1 ∈ ℝ )
13		0red	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ ¬ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 0 ∈ ℝ )
14	12 13	ifclda	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
15		1red	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ∈ ℝ )
16		fzfid	⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ Fin )
17	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
18		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
19	1 18 2	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
20		fof	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
21	17 19 20	3syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
22		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
23	10 22	syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
24	21 23	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) )
25	9 24	ffvelcdmd	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ )
26		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℕ0 )
27		reexpcl	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ )
28	25 26 27	syl2an	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ )
29	16 28	fsumrecl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ )
30	29	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ )
31		breq1	⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 1 ≤ 1 ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 ) )
32		breq1	⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 ) )
33		1le1	⊢ 1 ≤ 1
34		0le1	⊢ 0 ≤ 1
35	31 32 33 34	keephyp	⊢ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1
36	35	a1i	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 )
37		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
38	11 37	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 0 ) )
39		fzn0	⊢ ( ( 0 ... 𝐴 ) ≠ ∅ ↔ 𝐴 ∈ ( ℤ≥ ‘ 0 ) )
40	38 39	sylibr	⊢ ( 𝜑 → ( 0 ... 𝐴 ) ≠ ∅ )
41		hashnncl	⊢ ( ( 0 ... 𝐴 ) ∈ Fin → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ↔ ( 0 ... 𝐴 ) ≠ ∅ ) )
42	16 41	syl	⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ↔ ( 0 ... 𝐴 ) ≠ ∅ ) )
43	40 42	mpbird	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ )
44	43	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ )
45	44	nnge1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ≤ ( ♯ ‘ ( 0 ... 𝐴 ) ) )
46		simpr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 )
47	46	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( 1 ↑ 𝑖 ) )
48		elfzelz	⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℤ )
49		1exp	⊢ ( 𝑖 ∈ ℤ → ( 1 ↑ 𝑖 ) = 1 )
50	48 49	syl	⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → ( 1 ↑ 𝑖 ) = 1 )
51	47 50	sylan9eq	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = 1 )
52	51	sumeq2dv	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 )
53		fzfid	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( 0 ... 𝐴 ) ∈ Fin )
54		ax-1cn	⊢ 1 ∈ ℂ
55		fsumconst	⊢ ( ( ( 0 ... 𝐴 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 = ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) )
56	53 54 55	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 = ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) )
57	44	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℂ )
58	57	mulridd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) = ( ♯ ‘ ( 0 ... 𝐴 ) ) )
59	52 56 58	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ♯ ‘ ( 0 ... 𝐴 ) ) )
60	45 59	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
61	14 15 30 36 60	letrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
62		oveq1	⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
63	62	breq1d	⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) )
64		oveq1	⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
65	64	breq1d	⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) )
66		1re	⊢ 1 ∈ ℝ
67	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ )
68		resubcl	⊢ ( ( 1 ∈ ℝ ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ )
69	66 67 68	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ )
70	69	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ )
71	70	leidd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
72	69	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℂ )
73	72	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℂ )
74	73	mullidd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
75		nn0p1nn	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ )
76	11 75	syl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ )
77	76	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 𝐴 + 1 ) ∈ ℕ )
78	77	0expd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 0 ↑ ( 𝐴 + 1 ) ) = 0 )
79		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 )
80	79	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 0 ↑ ( 𝐴 + 1 ) ) )
81	78 80 79	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
82		neg1cn	⊢ - 1 ∈ ℂ
83	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 ∈ ℕ0 )
84		expp1	⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = ( ( - 1 ↑ 𝐴 ) · - 1 ) )
85	82 83 84	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = ( ( - 1 ↑ 𝐴 ) · - 1 ) )
86		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
87	10 86	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
88	87 11	nnexpcld	⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) ∈ ℕ )
89	88	nncnd	⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) ∈ ℂ )
90	89	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 ↑ 𝐴 ) ∈ ℂ )
91	90	sqsqrtd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) = ( 𝑃 ↑ 𝐴 ) )
92	91	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) )
93	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝑃 ∈ ℙ )
94		nnq	⊢ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ )
95	94	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ )
96		nnne0	⊢ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 )
97	96	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 )
98		2z	⊢ 2 ∈ ℤ
99	98	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 2 ∈ ℤ )
100		pcexp	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 ) ∧ 2 ∈ ℤ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) )
101	93 95 97 99 100	syl121anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) )
102	83	nn0zd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 ∈ ℤ )
103		pcid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )
104	93 102 103	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )
105	92 101 104	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) )
106	105	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ 𝐴 ) = ( - 1 ↑ ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) )
107	82	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → - 1 ∈ ℂ )
108		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ )
109	93 108	pccld	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℕ0 )
110		2nn0	⊢ 2 ∈ ℕ0
111	110	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 2 ∈ ℕ0 )
112	107 109 111	expmuld	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) )
113		neg1sqe1	⊢ ( - 1 ↑ 2 ) = 1
114	113	oveq1i	⊢ ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) )
115	109	nn0zd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ )
116		1exp	⊢ ( ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ → ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 )
117	115 116	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 )
118	114 117	eqtrid	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 )
119	106 112 118	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ 𝐴 ) = 1 )
120	119	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 𝐴 ) · - 1 ) = ( 1 · - 1 ) )
121	82	mullidi	⊢ ( 1 · - 1 ) = - 1
122	120 121	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 𝐴 ) · - 1 ) = - 1 )
123	85 122	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = - 1 )
124	123	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = - 1 )
125	25	recnd	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ )
126	125	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ )
127	126	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ )
128	127	negnegd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
129		simpr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 )
130	129	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 )
131	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → 𝑋 ∈ 𝐷 )
132		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
133	4 1 5 18 132 8 24	dchrn0	⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ↔ ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) ) )
134	133	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ↔ ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) ) )
135	134	biimpa	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) )
136	4 5 131 1 132 135	dchrabs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = 1 )
137		eqeq1	⊢ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = 1 ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) )
138	136 137	syl5ibcom	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) )
139	138	necon3ad	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 → ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
140	130 139	mpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
141	67	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ )
142	141	absord	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∨ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
143	142	ord	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
144	140 143	mpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
145	144 136	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 )
146	145	negeqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = - 1 )
147	128 146	eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = - 1 )
148	147	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( - 1 ↑ ( 𝐴 + 1 ) ) )
149	124 148 147	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
150	81 149	pm2.61dane	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
151	150	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
152	71 74 151	3brtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
153	72	mul02d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = 0 )
154		peano2nn0	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ0 )
155	11 154	syl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ0 )
156	25 155	reexpcld	⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ )
157	156	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ )
158	157	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℂ )
159	158	abscld	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ )
160		1red	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 1 ∈ ℝ )
161	157	leabsd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
162	155	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝐴 + 1 ) ∈ ℕ0 )
163	126 162	absexpd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) )
164	126	abscld	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ )
165	126	absge0d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
166	4 5 1 18 8 24	dchrabs2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 )
167	166	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 )
168		exple1	⊢ ( ( ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∧ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 ) ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 )
169	164 165 167 162 168	syl31anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 )
170	163 169	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ≤ 1 )
171	157 159 160 161 170	letrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 )
172		subge0	⊢ ( ( 1 ∈ ℝ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) )
173	66 157 172	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) )
174	171 173	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
175	153 174	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
176	175	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ¬ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
177	63 65 152 176	ifbothda	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
178		0re	⊢ 0 ∈ ℝ
179	66 178	ifcli	⊢ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ
180	179	a1i	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ )
181		resubcl	⊢ ( ( 1 ∈ ℝ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ )
182	66 157 181	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ )
183	67	leabsd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
184	67 164 160 183 167	letrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≤ 1 )
185	129	necomd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 1 ≠ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) )
186	67 160 184 185	leneltd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 )
187		posdif	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 ↔ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
188	67 66 187	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 ↔ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
189	186 188	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
190		lemuldiv	⊢ ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ ∧ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ∧ ( ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ∧ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) → ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) )
191	180 182 69 189 190	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) )
192	177 191	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
193	11	nn0zd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
194		fzval3	⊢ ( 𝐴 ∈ ℤ → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) )
195	193 194	syl	⊢ ( 𝜑 → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) )
196	195	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) )
197	196	sumeq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = Σ 𝑖 ∈ ( 0 ..^ ( 𝐴 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
198		0nn0	⊢ 0 ∈ ℕ0
199	198	a1i	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ∈ ℕ0 )
200	155 37	eleqtrdi	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
201	200	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
202	126 129 199 201	geoserg	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ..^ ( 𝐴 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
203	126	exp0d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) = 1 )
204	203	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) )
205	204	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
206	197 202 205	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) )
207	192 206	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
208	61 207	pm2.61dane	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
209	1 2 3 4 5 6 7	dchrisum0fval	⊢ ( ( 𝑃 ↑ 𝐴 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) )
210	88 209	syl	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) )
211		2fveq3	⊢ ( 𝑘 = ( 𝑃 ↑ 𝑖 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) )
212		eqid	⊢ ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) = ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) )
213	212	dvdsppwf1o	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } )
214	10 11 213	syl2anc	⊢ ( 𝜑 → ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } )
215		oveq2	⊢ ( 𝑏 = 𝑖 → ( 𝑃 ↑ 𝑏 ) = ( 𝑃 ↑ 𝑖 ) )
216		ovex	⊢ ( 𝑃 ↑ 𝑏 ) ∈ V
217	215 212 216	fvmpt3i	⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → ( ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) ‘ 𝑖 ) = ( 𝑃 ↑ 𝑖 ) )
218	217	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) ‘ 𝑖 ) = ( 𝑃 ↑ 𝑖 ) )
219	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
220		elrabi	⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑘 ∈ ℕ )
221	220	nnzd	⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑘 ∈ ℤ )
222		ffvelcdm	⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) )
223	21 221 222	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) )
224	219 223	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℝ )
225	224	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
226	211 16 214 218 225	fsumf1o	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) )
227		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
228		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
229	228	subrgsubm	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
230	227 229	mp1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
231	26	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑖 ∈ ℕ0 )
232	23	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑃 ∈ ℤ )
233		eqid	⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
234		zringmpg	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )
235	234	eqcomi	⊢ ( mulGrp ‘ ℤring ) = ( ( mulGrp ‘ ℂfld ) ↾s ℤ )
236		eqid	⊢ ( .g ‘ ( mulGrp ‘ ℤring ) ) = ( .g ‘ ( mulGrp ‘ ℤring ) )
237	233 235 236	submmulg	⊢ ( ( ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ 𝑖 ∈ ℕ0 ∧ 𝑃 ∈ ℤ ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) )
238	230 231 232 237	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) )
239	87	nncnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
240		cnfldexp	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) )
241	239 26 240	syl2an	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) )
242	238 241	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) )
243	242	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) )
244	1	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
245		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
246	17 244 245	3syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
247	2	zrhrhm	⊢ ( 𝑍 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
248		eqid	⊢ ( mulGrp ‘ ℤring ) = ( mulGrp ‘ ℤring )
249		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
250	248 249	rhmmhm	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) )
251	246 247 250	3syl	⊢ ( 𝜑 → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) )
252	251	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) )
253		zringbas	⊢ ℤ = ( Base ‘ ℤring )
254	248 253	mgpbas	⊢ ℤ = ( Base ‘ ( mulGrp ‘ ℤring ) )
255		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑍 ) ) = ( .g ‘ ( mulGrp ‘ 𝑍 ) )
256	254 236 255	mhmmulg	⊢ ( ( 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) ∧ 𝑖 ∈ ℕ0 ∧ 𝑃 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) )
257	252 231 232 256	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) )
258	243 257	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) )
259	258	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) )
260	4 1 5	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
261	260 8	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
262	261	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
263	24	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) )
264	249 18	mgpbas	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
265	264 255 233	mhmmulg	⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑖 ∈ ℕ0 ∧ ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
266	262 231 263 265	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) )
267		cnfldexp	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
268	125 26 267	syl2an	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
269	259 266 268	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
270	269	sumeq2dv	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
271	210 226 270	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) )
272	208 271	breqtrrd	⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) )