Metamath Proof Explorer

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 syl5eq ⊢ ( 𝜑 → - 𝑅 = ( ( 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 mulid1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 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 mulid1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑃 ≠ 𝑝 ∧ ( 𝐹 ‘ 𝑝 ) < 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 ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑃 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )