Theorem ostth3

Description: - Lemma for ostth : p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
	padic.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
	ostth.k	⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
	ostth.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
	ostth3.2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) )
	ostth3.3	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	ostth3.4	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) < 1 )
	ostth3.5	⊢ 𝑅 = - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) )
	ostth3.6	⊢ 𝑆 = if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) )
Assertion	ostth3	⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		padic.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4		ostth.k	⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		ostth.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
6		ostth3.2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) )
7		ostth3.3	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
8		ostth3.4	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) < 1 )
9		ostth3.5	⊢ 𝑅 = - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) )
10		ostth3.6	⊢ 𝑆 = if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) )
11		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
12	7 11	syl	⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
13		eluz2b2	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
14	12 13	sylib	⊢ ( 𝜑 → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
15	14	simpld	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
16		nnq	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℚ )
17	15 16	syl	⊢ ( 𝜑 → 𝑃 ∈ ℚ )
18	1	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )
19	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ) → ( 𝐹 ‘ 𝑃 ) ∈ ℝ )
20	5 17 19	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ ℝ )
21	15	nnne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
22	1	qrng0	⊢ 0 = ( 0g ‘ 𝑄 )
23	2 18 22	abvgt0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑃 ) )
24	5 17 21 23	syl3anc	⊢ ( 𝜑 → 0 < ( 𝐹 ‘ 𝑃 ) )
25	20 24	elrpd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ ℝ+ )
26	25	relogcld	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ ℝ )
27	15	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
28	14	simprd	⊢ ( 𝜑 → 1 < 𝑃 )
29	27 28	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑃 ) ∈ ℝ+ )
30	26 29	rerpdivcld	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ∈ ℝ )
31	30	renegcld	⊢ ( 𝜑 → - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ∈ ℝ )
32	9 31	eqeltrid	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
33		1rp	⊢ 1 ∈ ℝ+
34		logltb	⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑃 ) < 1 ↔ ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < ( log ‘ 1 ) ) )
35	25 33 34	sylancl	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) < 1 ↔ ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < ( log ‘ 1 ) ) )
36	8 35	mpbid	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < ( log ‘ 1 ) )
37		log1	⊢ ( log ‘ 1 ) = 0
38	36 37	breqtrdi	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < 0 )
39	29	rpcnd	⊢ ( 𝜑 → ( log ‘ 𝑃 ) ∈ ℂ )
40	39	mul01d	⊢ ( 𝜑 → ( ( log ‘ 𝑃 ) · 0 ) = 0 )
41	38 40	breqtrrd	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < ( ( log ‘ 𝑃 ) · 0 ) )
42		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
43	26 42 29	ltdivmuld	⊢ ( 𝜑 → ( ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) < 0 ↔ ( log ‘ ( 𝐹 ‘ 𝑃 ) ) < ( ( log ‘ 𝑃 ) · 0 ) ) )
44	41 43	mpbird	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) < 0 )
45	30	lt0neg1d	⊢ ( 𝜑 → ( ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) < 0 ↔ 0 < - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ) )
46	44 45	mpbid	⊢ ( 𝜑 → 0 < - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) )
47	46 9	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑅 )
48	32 47	elrpd	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
49	1 2 3	padicabvcxp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )
50	7 48 49	syl2anc	⊢ ( 𝜑 → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )
51		fveq2	⊢ ( 𝑦 = 𝑃 → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) )
52	51	oveq1d	⊢ ( 𝑦 = 𝑃 → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) ↑𝑐 𝑅 ) )
53		eqid	⊢ ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) )
54		ovex	⊢ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) ↑𝑐 𝑅 ) ∈ V
55	52 53 54	fvmpt	⊢ ( 𝑃 ∈ ℚ → ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) ↑𝑐 𝑅 ) )
56	17 55	syl	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) ↑𝑐 𝑅 ) )
57	3	padicval	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ ℚ ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) = if ( 𝑃 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) ) )
58	7 17 57	syl2anc	⊢ ( 𝜑 → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) = if ( 𝑃 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) ) )
59	21	neneqd	⊢ ( 𝜑 → ¬ 𝑃 = 0 )
60	59	iffalsed	⊢ ( 𝜑 → if ( 𝑃 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) ) = ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) )
61	15	nncnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
62	61	exp1d	⊢ ( 𝜑 → ( 𝑃 ↑ 1 ) = 𝑃 )
63	62	oveq2d	⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = ( 𝑃 pCnt 𝑃 ) )
64		1z	⊢ 1 ∈ ℤ
65		pcid	⊢ ( ( 𝑃 ∈ ℙ ∧ 1 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
66	7 64 65	sylancl	⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
67	63 66	eqtr3d	⊢ ( 𝜑 → ( 𝑃 pCnt 𝑃 ) = 1 )
68	67	negeqd	⊢ ( 𝜑 → - ( 𝑃 pCnt 𝑃 ) = - 1 )
69	68	oveq2d	⊢ ( 𝜑 → ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) = ( 𝑃 ↑ - 1 ) )
70		neg1z	⊢ - 1 ∈ ℤ
71	70	a1i	⊢ ( 𝜑 → - 1 ∈ ℤ )
72	61 21 71	cxpexpzd	⊢ ( 𝜑 → ( 𝑃 ↑𝑐 - 1 ) = ( 𝑃 ↑ - 1 ) )
73	69 72	eqtr4d	⊢ ( 𝜑 → ( 𝑃 ↑ - ( 𝑃 pCnt 𝑃 ) ) = ( 𝑃 ↑𝑐 - 1 ) )
74	58 60 73	3eqtrd	⊢ ( 𝜑 → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) = ( 𝑃 ↑𝑐 - 1 ) )
75	74	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑃 ) ↑𝑐 𝑅 ) = ( ( 𝑃 ↑𝑐 - 1 ) ↑𝑐 𝑅 ) )
76	32	recnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
77	76	mulm1d	⊢ ( 𝜑 → ( - 1 · 𝑅 ) = - 𝑅 )
78	9	negeqi	⊢ - 𝑅 = - - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) )
79	30	recnd	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ∈ ℂ )
80	79	negnegd	⊢ ( 𝜑 → - - ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) = ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) )
81	78 80	eqtrid	⊢ ( 𝜑 → - 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) )
82	77 81	eqtrd	⊢ ( 𝜑 → ( - 1 · 𝑅 ) = ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) )
83	82	oveq2d	⊢ ( 𝜑 → ( 𝑃 ↑𝑐 ( - 1 · 𝑅 ) ) = ( 𝑃 ↑𝑐 ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ) )
84	15	nnrpd	⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
85		neg1rr	⊢ - 1 ∈ ℝ
86	85	a1i	⊢ ( 𝜑 → - 1 ∈ ℝ )
87	84 86 76	cxpmuld	⊢ ( 𝜑 → ( 𝑃 ↑𝑐 ( - 1 · 𝑅 ) ) = ( ( 𝑃 ↑𝑐 - 1 ) ↑𝑐 𝑅 ) )
88	61 21 79	cxpefd	⊢ ( 𝜑 → ( 𝑃 ↑𝑐 ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ) = ( exp ‘ ( ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) · ( log ‘ 𝑃 ) ) ) )
89	26	recnd	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ ℂ )
90	29	rpne0d	⊢ ( 𝜑 → ( log ‘ 𝑃 ) ≠ 0 )
91	89 39 90	divcan1d	⊢ ( 𝜑 → ( ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) · ( log ‘ 𝑃 ) ) = ( log ‘ ( 𝐹 ‘ 𝑃 ) ) )
92	91	fveq2d	⊢ ( 𝜑 → ( exp ‘ ( ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) · ( log ‘ 𝑃 ) ) ) = ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑃 ) ) ) )
93	25	reeflogd	⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑃 ) ) ) = ( 𝐹 ‘ 𝑃 ) )
94	88 92 93	3eqtrd	⊢ ( 𝜑 → ( 𝑃 ↑𝑐 ( ( log ‘ ( 𝐹 ‘ 𝑃 ) ) / ( log ‘ 𝑃 ) ) ) = ( 𝐹 ‘ 𝑃 ) )
95	83 87 94	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑃 ↑𝑐 - 1 ) ↑𝑐 𝑅 ) = ( 𝐹 ‘ 𝑃 ) )
96	56 75 95	3eqtrrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑃 ) )
97		fveq2	⊢ ( 𝑃 = 𝑝 → ( 𝐹 ‘ 𝑃 ) = ( 𝐹 ‘ 𝑝 ) )
98		fveq2	⊢ ( 𝑃 = 𝑝 → ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑃 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) )
99	97 98	eqeq12d	⊢ ( 𝑃 = 𝑝 → ( ( 𝐹 ‘ 𝑃 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑃 ) ↔ ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) ) )
100	96 99	syl5ibcom	⊢ ( 𝜑 → ( 𝑃 = 𝑝 → ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) ) )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑃 = 𝑝 → ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) ) )
102		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
103	102	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑝 ∈ ℕ )
104		nnq	⊢ ( 𝑝 ∈ ℕ → 𝑝 ∈ ℚ )
105	103 104	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑝 ∈ ℚ )
106		fveq2	⊢ ( 𝑦 = 𝑝 → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) )
107	106	oveq1d	⊢ ( 𝑦 = 𝑝 → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) )
108		ovex	⊢ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) ∈ V
109	107 53 108	fvmpt	⊢ ( 𝑝 ∈ ℚ → ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) )
110	105 109	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) )
111	76	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑅 ∈ ℂ )
112	111	1cxpd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 1 ↑𝑐 𝑅 ) = 1 )
113	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑃 ∈ ℙ )
114	3	padicval	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑝 ∈ ℚ ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) = if ( 𝑝 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) ) )
115	113 105 114	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) = if ( 𝑝 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) ) )
116	103	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑝 ≠ 0 )
117	116	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ¬ 𝑝 = 0 )
118	117	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → if ( 𝑝 = 0 , 0 , ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) ) = ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) )
119		pceq0	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑝 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑝 ) = 0 ↔ ¬ 𝑃 ∥ 𝑝 ) )
120	7 102 119	syl2an	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑃 pCnt 𝑝 ) = 0 ↔ ¬ 𝑃 ∥ 𝑝 ) )
121		dvdsprm	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝 ) )
122	12 121	sylan	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝 ) )
123	122	necon3bbid	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ¬ 𝑃 ∥ 𝑝 ↔ 𝑃 ≠ 𝑝 ) )
124	120 123	bitrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑃 pCnt 𝑝 ) = 0 ↔ 𝑃 ≠ 𝑝 ) )
125	124	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝑃 pCnt 𝑝 ) = 0 )
126	125	negeqd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → - ( 𝑃 pCnt 𝑝 ) = - 0 )
127		neg0	⊢ - 0 = 0
128	126 127	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → - ( 𝑃 pCnt 𝑝 ) = 0 )
129	128	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) = ( 𝑃 ↑ 0 ) )
130	61	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝑃 ∈ ℂ )
131	130	exp0d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝑃 ↑ 0 ) = 1 )
132	129 131	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝑃 ↑ - ( 𝑃 pCnt 𝑝 ) ) = 1 )
133	115 118 132	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) = 1 )
134	133	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) = ( 1 ↑𝑐 𝑅 ) )
135		2re	⊢ 2 ∈ ℝ
136	135	a1i	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 2 ∈ ℝ )
137	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 𝐹 ∈ 𝐴 )
138	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ )
139	137 105 138	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ )
140	2 18 22	abvgt0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑝 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑝 ) )
141	137 105 116 140	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → 0 < ( 𝐹 ‘ 𝑝 ) )
142	139 141	elrpd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ+ )
143	142	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ+ )
144	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ℝ+ )
145	143 144	ifcld	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) ∈ ℝ+ )
146	10 145	eqeltrid	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑆 ∈ ℝ+ )
147	146	rprecred	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 1 / 𝑆 ) ∈ ℝ )
148		simprr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 ‘ 𝑝 ) < 1 )
149	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 ‘ 𝑃 ) < 1 )
150		breq1	⊢ ( ( 𝐹 ‘ 𝑝 ) = if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) → ( ( 𝐹 ‘ 𝑝 ) < 1 ↔ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) < 1 ) )
151		breq1	⊢ ( ( 𝐹 ‘ 𝑃 ) = if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) → ( ( 𝐹 ‘ 𝑃 ) < 1 ↔ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) < 1 ) )
152	150 151	ifboth	⊢ ( ( ( 𝐹 ‘ 𝑝 ) < 1 ∧ ( 𝐹 ‘ 𝑃 ) < 1 ) → if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) < 1 )
153	148 149 152	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) < 1 )
154	10 153	eqbrtrid	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑆 < 1 )
155	146	reclt1d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝑆 < 1 ↔ 1 < ( 1 / 𝑆 ) ) )
156	154 155	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 1 < ( 1 / 𝑆 ) )
157		expnbnd	⊢ ( ( 2 ∈ ℝ ∧ ( 1 / 𝑆 ) ∈ ℝ ∧ 1 < ( 1 / 𝑆 ) ) → ∃ 𝑘 ∈ ℕ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) )
158	136 147 156 157	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∃ 𝑘 ∈ ℕ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) )
159	146	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑆 ∈ ℂ )
160	159	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑆 ∈ ℂ )
161	146	rpne0d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑆 ≠ 0 )
162	161	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑆 ≠ 0 )
163		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
164	163	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
165	160 162 164	exprecd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑆 ) ↑ 𝑘 ) = ( 1 / ( 𝑆 ↑ 𝑘 ) ) )
166	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝐹 ∈ 𝐴 )
167		ax-1ne0	⊢ 1 ≠ 0
168	1	qrng1	⊢ 1 = ( 1r ‘ 𝑄 )
169	2 168 22	abv1z	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )
170	166 167 169	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 1 ) = 1 )
171	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑃 ∈ ℕ )
172		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
173		nnexpcl	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ )
174	171 172 173	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ )
175	174	nnzd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ↑ 𝑘 ) ∈ ℤ )
176	102	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑝 ∈ ℕ )
177		nnexpcl	⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
178	176 172 177	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
179	178	nnzd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
180		bezout	⊢ ( ( ( 𝑃 ↑ 𝑘 ) ∈ ℤ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) )
181	175 179 180	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) )
182		simprl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑃 ≠ 𝑝 )
183	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑃 ∈ ℙ )
184		simplr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑝 ∈ ℙ )
185		prmrp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑃 gcd 𝑝 ) = 1 ↔ 𝑃 ≠ 𝑝 ) )
186	183 184 185	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( ( 𝑃 gcd 𝑝 ) = 1 ↔ 𝑃 ≠ 𝑝 ) )
187	182 186	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝑃 gcd 𝑝 ) = 1 )
188	187	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 gcd 𝑝 ) = 1 )
189	171	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑃 ∈ ℕ )
190	176	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
191		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
192		rppwr	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 gcd 𝑝 ) = 1 → ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = 1 ) )
193	189 190 191 192	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 gcd 𝑝 ) = 1 → ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = 1 ) )
194	188 193	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = 1 )
195	194	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = 1 )
196	195	eqeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ↔ 1 = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) )
197	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝐹 ∈ 𝐴 )
198	174	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ )
199		nnq	⊢ ( ( 𝑃 ↑ 𝑘 ) ∈ ℕ → ( 𝑃 ↑ 𝑘 ) ∈ ℚ )
200	198 199	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝑃 ↑ 𝑘 ) ∈ ℚ )
201		simprrl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑎 ∈ ℤ )
202		zq	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℚ )
203	201 202	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑎 ∈ ℚ )
204		qmulcl	⊢ ( ( ( 𝑃 ↑ 𝑘 ) ∈ ℚ ∧ 𝑎 ∈ ℚ ) → ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ∈ ℚ )
205	200 203 204	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ∈ ℚ )
206	178	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
207		nnq	⊢ ( ( 𝑝 ↑ 𝑘 ) ∈ ℕ → ( 𝑝 ↑ 𝑘 ) ∈ ℚ )
208	206 207	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℚ )
209		simprrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑏 ∈ ℤ )
210		zq	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℚ )
211	209 210	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑏 ∈ ℚ )
212		qmulcl	⊢ ( ( ( 𝑝 ↑ 𝑘 ) ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ∈ ℚ )
213	208 211 212	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ∈ ℚ )
214		qaddcl	⊢ ( ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ∈ ℚ ∧ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ∈ ℚ ) → ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ∈ ℚ )
215	205 213 214	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ∈ ℚ )
216	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ∈ ℚ ) → ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ∈ ℝ )
217	197 215 216	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ∈ ℝ )
218	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) ∈ ℝ )
219	197 205 218	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) ∈ ℝ )
220	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ∈ ℝ )
221	197 213 220	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ∈ ℝ )
222	219 221	readdcld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) + ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ∈ ℝ )
223		rpexpcl	⊢ ( ( 𝑆 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( 𝑆 ↑ 𝑘 ) ∈ ℝ+ )
224	146 163 223	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ↑ 𝑘 ) ∈ ℝ+ )
225	224	rpred	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ↑ 𝑘 ) ∈ ℝ )
226	225	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝑆 ↑ 𝑘 ) ∈ ℝ )
227		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( 𝑆 ↑ 𝑘 ) ∈ ℝ ) → ( 2 · ( 𝑆 ↑ 𝑘 ) ) ∈ ℝ )
228	135 226 227	sylancr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 2 · ( 𝑆 ↑ 𝑘 ) ) ∈ ℝ )
229		qex	⊢ ℚ ∈ V
230		cnfldadd	⊢ + = ( +g ‘ ℂfld )
231	1 230	ressplusg	⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) )
232	229 231	ax-mp	⊢ + = ( +g ‘ 𝑄 )
233	2 18 232	abvtri	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ∈ ℚ ∧ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ∈ ℚ ) → ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) + ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) )
234	197 205 213 233	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) + ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) )
235		cnfldmul	⊢ · = ( .r ‘ ℂfld )
236	1 235	ressmulr	⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) )
237	229 236	ax-mp	⊢ · = ( .r ‘ 𝑄 )
238	2 18 237	abvmul	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑃 ↑ 𝑘 ) ∈ ℚ ∧ 𝑎 ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) = ( ( 𝐹 ‘ ( 𝑃 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑎 ) ) )
239	197 200 203 238	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) = ( ( 𝐹 ‘ ( 𝑃 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑎 ) ) )
240	17	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑃 ∈ ℚ )
241	172	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑘 ∈ ℕ0 )
242	1 2	qabvexp	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑃 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
243	197 240 241 242	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( 𝑃 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
244	243	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ ( 𝑃 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑎 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) )
245	239 244	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) )
246	197 240 19	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ℝ )
247	246 241	reexpcld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ∈ ℝ )
248	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
249	197 203 248	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
250	247 249	remulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ∈ ℝ )
251		elz	⊢ ( 𝑎 ∈ ℤ ↔ ( 𝑎 ∈ ℝ ∧ ( 𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ - 𝑎 ∈ ℕ ) ) )
252	251	simprbi	⊢ ( 𝑎 ∈ ℤ → ( 𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ - 𝑎 ∈ ℕ ) )
253	252	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( 𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ - 𝑎 ∈ ℕ ) )
254	2 22	abv0	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )
255	5 254	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
256		0le1	⊢ 0 ≤ 1
257	255 256	eqbrtrdi	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≤ 1 )
258	257	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( 𝐹 ‘ 0 ) ≤ 1 )
259		fveq2	⊢ ( 𝑎 = 0 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 0 ) )
260	259	breq1d	⊢ ( 𝑎 = 0 → ( ( 𝐹 ‘ 𝑎 ) ≤ 1 ↔ ( 𝐹 ‘ 0 ) ≤ 1 ) )
261	258 260	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( 𝑎 = 0 → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
262		nnq	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℚ )
263	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
264	5 262 263	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
265		1re	⊢ 1 ∈ ℝ
266		lenlt	⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ≤ 1 ↔ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) )
267	264 265 266	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ≤ 1 ↔ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) )
268	267	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ≤ 1 ↔ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) )
269	6 268	mpbird	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ≤ 1 )
270		fveq2	⊢ ( 𝑛 = 𝑎 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑎 ) )
271	270	breq1d	⊢ ( 𝑛 = 𝑎 → ( ( 𝐹 ‘ 𝑛 ) ≤ 1 ↔ ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
272	271	rspccv	⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ≤ 1 → ( 𝑎 ∈ ℕ → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
273	269 272	syl	⊢ ( 𝜑 → ( 𝑎 ∈ ℕ → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
274	273	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ∈ ℕ → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
275	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → 𝐹 ∈ 𝐴 )
276	202	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → 𝑎 ∈ ℚ )
277		eqid	⊢ ( invg ‘ 𝑄 ) = ( invg ‘ 𝑄 )
278	2 18 277	abvneg	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
279	275 276 278	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
280		fveq2	⊢ ( 𝑛 = ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ) )
281	280	breq1d	⊢ ( 𝑛 = ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) → ( ( 𝐹 ‘ 𝑛 ) ≤ 1 ↔ ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ) ≤ 1 ) )
282	269	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ≤ 1 )
283	1	qrngneg	⊢ ( 𝑎 ∈ ℚ → ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) = - 𝑎 )
284	276 283	syl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) = - 𝑎 )
285		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → - 𝑎 ∈ ℕ )
286	284 285	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ∈ ℕ )
287	281 282 286	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑎 ) ) ≤ 1 )
288	279 287	eqbrtrrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℤ ∧ - 𝑎 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑎 ) ≤ 1 )
289	288	expr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( - 𝑎 ∈ ℕ → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
290	261 274 289	3jaod	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ - 𝑎 ∈ ℕ ) → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
291	253 290	mpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( 𝐹 ‘ 𝑎 ) ≤ 1 )
292	291	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℤ ( 𝐹 ‘ 𝑎 ) ≤ 1 )
293	292	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ∀ 𝑎 ∈ ℤ ( 𝐹 ‘ 𝑎 ) ≤ 1 )
294		rsp	⊢ ( ∀ 𝑎 ∈ ℤ ( 𝐹 ‘ 𝑎 ) ≤ 1 → ( 𝑎 ∈ ℤ → ( 𝐹 ‘ 𝑎 ) ≤ 1 ) )
295	293 201 294	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑎 ) ≤ 1 )
296	265	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 1 ∈ ℝ )
297	163	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑘 ∈ ℤ )
298	24	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 < ( 𝐹 ‘ 𝑃 ) )
299		expgt0	⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < ( 𝐹 ‘ 𝑃 ) ) → 0 < ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
300	246 297 298 299	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 < ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
301		lemul2	⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ≤ 1 ↔ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ≤ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · 1 ) ) )
302	249 296 247 300 301	syl112anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ≤ 1 ↔ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ≤ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · 1 ) ) )
303	295 302	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ≤ ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · 1 ) )
304	247	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ∈ ℂ )
305	304	mulridd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · 1 ) = ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
306	303 305	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ≤ ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) )
307	146	rpred	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑆 ∈ ℝ )
308	307	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑆 ∈ ℝ )
309	144	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ℝ+ )
310	309	rpge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑃 ) )
311	176	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑝 ∈ ℕ )
312	311 104	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑝 ∈ ℚ )
313	197 312 138	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ )
314		max1	⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑝 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑃 ) ≤ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) )
315	246 313 314	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) )
316	315 10	breqtrrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ 𝑆 )
317		leexp1a	⊢ ( ( ( ( 𝐹 ‘ 𝑃 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) ≤ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ≤ ( 𝑆 ↑ 𝑘 ) )
318	246 308 241 310 316 317	syl32anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) ≤ ( 𝑆 ↑ 𝑘 ) )
319	250 247 226 306 318	letrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑎 ) ) ≤ ( 𝑆 ↑ 𝑘 ) )
320	245 319	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) ≤ ( 𝑆 ↑ 𝑘 ) )
321	2 18 237	abvmul	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑝 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑏 ) ) )
322	197 208 211 321	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑝 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑏 ) ) )
323	1 2	qabvexp	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑝 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
324	197 312 241 323	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( 𝑝 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
325	324	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ ( 𝑝 ↑ 𝑘 ) ) · ( 𝐹 ‘ 𝑏 ) ) = ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) )
326	322 325	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) = ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) )
327	313 241	reexpcld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ∈ ℝ )
328	2 18	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑏 ∈ ℚ ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
329	197 211 328	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
330	327 329	remulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ∈ ℝ )
331		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
332	331	breq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ 𝑎 ) ≤ 1 ↔ ( 𝐹 ‘ 𝑏 ) ≤ 1 ) )
333	332 293 209	rspcdva	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑏 ) ≤ 1 )
334	311	nnne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 𝑝 ≠ 0 )
335	197 312 334 140	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 < ( 𝐹 ‘ 𝑝 ) )
336		expgt0	⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < ( 𝐹 ‘ 𝑝 ) ) → 0 < ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
337	313 297 335 336	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 < ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
338		lemul2	⊢ ( ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑏 ) ≤ 1 ↔ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · 1 ) ) )
339	329 296 327 337 338	syl112anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑏 ) ≤ 1 ↔ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · 1 ) ) )
340	333 339	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · 1 ) )
341	327	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
342	341	mulridd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · 1 ) = ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
343	340 342	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ≤ ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) )
344	143	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑝 ) ∈ ℝ+ )
345	344	rpge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑝 ) )
346		max2	⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑝 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑝 ) ≤ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) )
347	246 313 346	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑝 ) ≤ if ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑃 ) ) )
348	347 10	breqtrrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ 𝑝 ) ≤ 𝑆 )
349		leexp1a	⊢ ( ( ( ( 𝐹 ‘ 𝑝 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑝 ) ≤ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ≤ ( 𝑆 ↑ 𝑘 ) )
350	313 308 241 345 348 349	syl32anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) ≤ ( 𝑆 ↑ 𝑘 ) )
351	330 327 226 343 350	letrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ↑ 𝑘 ) · ( 𝐹 ‘ 𝑏 ) ) ≤ ( 𝑆 ↑ 𝑘 ) )
352	326 351	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ≤ ( 𝑆 ↑ 𝑘 ) )
353	219 221 226 226 320 352	le2addd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) + ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( ( 𝑆 ↑ 𝑘 ) + ( 𝑆 ↑ 𝑘 ) ) )
354	224	rpcnd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ↑ 𝑘 ) ∈ ℂ )
355	354	2timesd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 2 · ( 𝑆 ↑ 𝑘 ) ) = ( ( 𝑆 ↑ 𝑘 ) + ( 𝑆 ↑ 𝑘 ) ) )
356	355	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 2 · ( 𝑆 ↑ 𝑘 ) ) = ( ( 𝑆 ↑ 𝑘 ) + ( 𝑆 ↑ 𝑘 ) ) )
357	353 356	breqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( 𝐹 ‘ ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) ) + ( 𝐹 ‘ ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) )
358	217 222 228 234 357	letrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) )
359		fveq2	⊢ ( 1 = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( 𝐹 ‘ 1 ) = ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) )
360	359	breq1d	⊢ ( 1 = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ↔ ( 𝐹 ‘ ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
361	358 360	syl5ibrcom	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( 1 = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
362	196 361	sylbid	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ) → ( ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
363	362	anassrs	⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
364	363	rexlimdvva	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ↑ 𝑘 ) gcd ( 𝑝 ↑ 𝑘 ) ) = ( ( ( 𝑃 ↑ 𝑘 ) · 𝑎 ) + ( ( 𝑝 ↑ 𝑘 ) · 𝑏 ) ) → ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
365	181 364	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 1 ) ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) )
366	170 365	eqbrtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → 1 ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) )
367	224	rpregt0d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑆 ↑ 𝑘 ) ) )
368		ledivmul2	⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ( 𝑆 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑆 ↑ 𝑘 ) ) ) → ( ( 1 / ( 𝑆 ↑ 𝑘 ) ) ≤ 2 ↔ 1 ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
369	265 135 367 368	mp3an12i	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( 𝑆 ↑ 𝑘 ) ) ≤ 2 ↔ 1 ≤ ( 2 · ( 𝑆 ↑ 𝑘 ) ) ) )
370	366 369	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑆 ↑ 𝑘 ) ) ≤ 2 )
371	165 370	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑆 ) ↑ 𝑘 ) ≤ 2 )
372		reexpcl	⊢ ( ( ( 1 / 𝑆 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝑆 ) ↑ 𝑘 ) ∈ ℝ )
373	147 172 372	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑆 ) ↑ 𝑘 ) ∈ ℝ )
374		lenlt	⊢ ( ( ( ( 1 / 𝑆 ) ↑ 𝑘 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( 1 / 𝑆 ) ↑ 𝑘 ) ≤ 2 ↔ ¬ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) ) )
375	373 135 374	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / 𝑆 ) ↑ 𝑘 ) ≤ 2 ↔ ¬ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) ) )
376	371 375	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ¬ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) )
377	376	pm2.21d	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) → ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) )
378	377	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( ∃ 𝑘 ∈ ℕ 2 < ( ( 1 / 𝑆 ) ↑ 𝑘 ) → ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) )
379	158 378	mpd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ¬ ( 𝐹 ‘ 𝑝 ) < 1 )
380	379	expr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( 𝐹 ‘ 𝑝 ) < 1 → ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) )
381	380	pm2.01d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ¬ ( 𝐹 ‘ 𝑝 ) < 1 )
382		fveq2	⊢ ( 𝑛 = 𝑝 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑝 ) )
383	382	breq2d	⊢ ( 𝑛 = 𝑝 → ( 1 < ( 𝐹 ‘ 𝑛 ) ↔ 1 < ( 𝐹 ‘ 𝑝 ) ) )
384	383	notbid	⊢ ( 𝑛 = 𝑝 → ( ¬ 1 < ( 𝐹 ‘ 𝑛 ) ↔ ¬ 1 < ( 𝐹 ‘ 𝑝 ) ) )
385	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) )
386	384 385 103	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ¬ 1 < ( 𝐹 ‘ 𝑝 ) )
387		lttri3	⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑝 ) = 1 ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) < 1 ∧ ¬ 1 < ( 𝐹 ‘ 𝑝 ) ) ) )
388	139 265 387	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( 𝐹 ‘ 𝑝 ) = 1 ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) < 1 ∧ ¬ 1 < ( 𝐹 ‘ 𝑝 ) ) ) )
389	381 386 388	mpbir2and	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 1 )
390	112 134 389	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑝 ) ↑𝑐 𝑅 ) = ( 𝐹 ‘ 𝑝 ) )
391	110 390	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑃 ≠ 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) )
392	391	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ≠ 𝑝 → ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) ) )
393	101 392	pm2.61dne	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐹 ‘ 𝑝 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑝 ) )
394	1 2 5 50 393	ostthlem2	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) )
395		oveq2	⊢ ( 𝑎 = 𝑅 → ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) = ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) )
396	395	mpteq2dv	⊢ ( 𝑎 = 𝑅 → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) )
397	396	rspceeqv	⊢ ( ( 𝑅 ∈ ℝ+ ∧ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ) → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
398	48 394 397	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )