Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ostth3 Structured version   Visualization version   GIF version

Theorem ostth3 26206
 Description: - Lemma for ostth 26207: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
qrng.q 𝑄 = (ℂflds ℚ)
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
Ref Expression
ostth3 (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)))
Distinct variable groups:   𝑛,𝑝,𝑦   𝑛,𝐾   𝑥,𝑛,𝑎,𝑝,𝑞,𝑦,𝜑   𝐽,𝑎,𝑝,𝑦   𝑆,𝑎   𝐴,𝑎,𝑛,𝑝,𝑞,𝑥,𝑦   𝑄,𝑛,𝑥,𝑦   𝐹,𝑎,𝑛,𝑝,𝑞,𝑦   𝑃,𝑎,𝑝,𝑞,𝑥,𝑦   𝑅,𝑎,𝑝,𝑞,𝑦   𝑥,𝐹
Allowed substitution hints:   𝑃(𝑛)   𝑄(𝑞,𝑝,𝑎)   𝑅(𝑥,𝑛)   𝑆(𝑥,𝑦,𝑛,𝑞,𝑝)   𝐽(𝑥,𝑛,𝑞)   𝐾(𝑥,𝑦,𝑞,𝑝,𝑎)

Proof of Theorem ostth3
Dummy variables 𝑘 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ostth3.5 . . . 4 𝑅 = -((log‘(𝐹𝑃)) / (log‘𝑃))
2 ostth.1 . . . . . . . . 9 (𝜑𝐹𝐴)
3 ostth3.3 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
4 prmuz2 16032 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
53, 4syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ (ℤ‘2))
6 eluz2b2 12313 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
75, 6sylib 220 . . . . . . . . . . 11 (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃))
87simpld 497 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
9 nnq 12353 . . . . . . . . . 10 (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
108, 9syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℚ)
11 qabsabv.a . . . . . . . . . 10 𝐴 = (AbsVal‘𝑄)
12 qrng.q . . . . . . . . . . 11 𝑄 = (ℂflds ℚ)
1312qrngbas 26187 . . . . . . . . . 10 ℚ = (Base‘𝑄)
1411, 13abvcl 19587 . . . . . . . . 9 ((𝐹𝐴𝑃 ∈ ℚ) → (𝐹𝑃) ∈ ℝ)
152, 10, 14syl2anc 586 . . . . . . . 8 (𝜑 → (𝐹𝑃) ∈ ℝ)
168nnne0d 11679 . . . . . . . . 9 (𝜑𝑃 ≠ 0)
1712qrng0 26189 . . . . . . . . . 10 0 = (0g𝑄)
1811, 13, 17abvgt0 19591 . . . . . . . . 9 ((𝐹𝐴𝑃 ∈ ℚ ∧ 𝑃 ≠ 0) → 0 < (𝐹𝑃))
192, 10, 16, 18syl3anc 1365 . . . . . . . 8 (𝜑 → 0 < (𝐹𝑃))
2015, 19elrpd 12420 . . . . . . 7 (𝜑 → (𝐹𝑃) ∈ ℝ+)
2120relogcld 25198 . . . . . 6 (𝜑 → (log‘(𝐹𝑃)) ∈ ℝ)
228nnred 11645 . . . . . . 7 (𝜑𝑃 ∈ ℝ)
237simprd 498 . . . . . . 7 (𝜑 → 1 < 𝑃)
2422, 23rplogcld 25204 . . . . . 6 (𝜑 → (log‘𝑃) ∈ ℝ+)
2521, 24rerpdivcld 12454 . . . . 5 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℝ)
2625renegcld 11059 . . . 4 (𝜑 → -((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℝ)
271, 26eqeltrid 2915 . . 3 (𝜑𝑅 ∈ ℝ)
28 ostth3.4 . . . . . . . . 9 (𝜑 → (𝐹𝑃) < 1)
29 1rp 12385 . . . . . . . . . 10 1 ∈ ℝ+
30 logltb 25175 . . . . . . . . . 10 (((𝐹𝑃) ∈ ℝ+ ∧ 1 ∈ ℝ+) → ((𝐹𝑃) < 1 ↔ (log‘(𝐹𝑃)) < (log‘1)))
3120, 29, 30sylancl 588 . . . . . . . . 9 (𝜑 → ((𝐹𝑃) < 1 ↔ (log‘(𝐹𝑃)) < (log‘1)))
3228, 31mpbid 234 . . . . . . . 8 (𝜑 → (log‘(𝐹𝑃)) < (log‘1))
33 log1 25161 . . . . . . . 8 (log‘1) = 0
3432, 33breqtrdi 5098 . . . . . . 7 (𝜑 → (log‘(𝐹𝑃)) < 0)
3524rpcnd 12425 . . . . . . . 8 (𝜑 → (log‘𝑃) ∈ ℂ)
3635mul01d 10831 . . . . . . 7 (𝜑 → ((log‘𝑃) · 0) = 0)
3734, 36breqtrrd 5085 . . . . . 6 (𝜑 → (log‘(𝐹𝑃)) < ((log‘𝑃) · 0))
38 0red 10636 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
3921, 38, 24ltdivmuld 12474 . . . . . 6 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) < 0 ↔ (log‘(𝐹𝑃)) < ((log‘𝑃) · 0)))
4037, 39mpbird 259 . . . . 5 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) < 0)
4125lt0neg1d 11201 . . . . 5 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) < 0 ↔ 0 < -((log‘(𝐹𝑃)) / (log‘𝑃))))
4240, 41mpbid 234 . . . 4 (𝜑 → 0 < -((log‘(𝐹𝑃)) / (log‘𝑃)))
4342, 1breqtrrdi 5099 . . 3 (𝜑 → 0 < 𝑅)
4427, 43elrpd 12420 . 2 (𝜑𝑅 ∈ ℝ+)
45 padic.j . . . . 5 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))
4612, 11, 45padicabvcxp 26200 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+) → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
473, 44, 46syl2anc 586 . . 3 (𝜑 → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
48 fveq2 6663 . . . . . . . . . 10 (𝑦 = 𝑃 → ((𝐽𝑃)‘𝑦) = ((𝐽𝑃)‘𝑃))
4948oveq1d 7163 . . . . . . . . 9 (𝑦 = 𝑃 → (((𝐽𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
50 eqid 2819 . . . . . . . . 9 (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))
51 ovex 7181 . . . . . . . . 9 (((𝐽𝑃)‘𝑃)↑𝑐𝑅) ∈ V
5249, 50, 51fvmpt 6761 . . . . . . . 8 (𝑃 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
5310, 52syl 17 . . . . . . 7 (𝜑 → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
5445padicval 26185 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝑃 ∈ ℚ) → ((𝐽𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
553, 10, 54syl2anc 586 . . . . . . . . 9 (𝜑 → ((𝐽𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
5616neneqd 3019 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
5756iffalsed 4476 . . . . . . . . 9 (𝜑 → if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))) = (𝑃↑-(𝑃 pCnt 𝑃)))
588nncnd 11646 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℂ)
5958exp1d 13497 . . . . . . . . . . . . . 14 (𝜑 → (𝑃↑1) = 𝑃)
6059oveq2d 7164 . . . . . . . . . . . . 13 (𝜑 → (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃))
61 1z 12004 . . . . . . . . . . . . . 14 1 ∈ ℤ
62 pcid 16201 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℙ ∧ 1 ∈ ℤ) → (𝑃 pCnt (𝑃↑1)) = 1)
633, 61, 62sylancl 588 . . . . . . . . . . . . 13 (𝜑 → (𝑃 pCnt (𝑃↑1)) = 1)
6460, 63eqtr3d 2856 . . . . . . . . . . . 12 (𝜑 → (𝑃 pCnt 𝑃) = 1)
6564negeqd 10872 . . . . . . . . . . 11 (𝜑 → -(𝑃 pCnt 𝑃) = -1)
6665oveq2d 7164 . . . . . . . . . 10 (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑-1))
67 neg1z 12010 . . . . . . . . . . . 12 -1 ∈ ℤ
6867a1i 11 . . . . . . . . . . 11 (𝜑 → -1 ∈ ℤ)
6958, 16, 68cxpexpzd 25286 . . . . . . . . . 10 (𝜑 → (𝑃𝑐-1) = (𝑃↑-1))
7066, 69eqtr4d 2857 . . . . . . . . 9 (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃𝑐-1))
7155, 57, 703eqtrd 2858 . . . . . . . 8 (𝜑 → ((𝐽𝑃)‘𝑃) = (𝑃𝑐-1))
7271oveq1d 7163 . . . . . . 7 (𝜑 → (((𝐽𝑃)‘𝑃)↑𝑐𝑅) = ((𝑃𝑐-1)↑𝑐𝑅))
7327recnd 10661 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
7473mulm1d 11084 . . . . . . . . . 10 (𝜑 → (-1 · 𝑅) = -𝑅)
751negeqi 10871 . . . . . . . . . . 11 -𝑅 = --((log‘(𝐹𝑃)) / (log‘𝑃))
7625recnd 10661 . . . . . . . . . . . 12 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℂ)
7776negnegd 10980 . . . . . . . . . . 11 (𝜑 → --((log‘(𝐹𝑃)) / (log‘𝑃)) = ((log‘(𝐹𝑃)) / (log‘𝑃)))
7875, 77syl5eq 2866 . . . . . . . . . 10 (𝜑 → -𝑅 = ((log‘(𝐹𝑃)) / (log‘𝑃)))
7974, 78eqtrd 2854 . . . . . . . . 9 (𝜑 → (-1 · 𝑅) = ((log‘(𝐹𝑃)) / (log‘𝑃)))
8079oveq2d 7164 . . . . . . . 8 (𝜑 → (𝑃𝑐(-1 · 𝑅)) = (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))))
818nnrpd 12421 . . . . . . . . 9 (𝜑𝑃 ∈ ℝ+)
82 neg1rr 11744 . . . . . . . . . 10 -1 ∈ ℝ
8382a1i 11 . . . . . . . . 9 (𝜑 → -1 ∈ ℝ)
8481, 83, 73cxpmuld 25311 . . . . . . . 8 (𝜑 → (𝑃𝑐(-1 · 𝑅)) = ((𝑃𝑐-1)↑𝑐𝑅))
8558, 16, 76cxpefd 25287 . . . . . . . . 9 (𝜑 → (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))) = (exp‘(((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃))))
8621recnd 10661 . . . . . . . . . . 11 (𝜑 → (log‘(𝐹𝑃)) ∈ ℂ)
8724rpne0d 12428 . . . . . . . . . . 11 (𝜑 → (log‘𝑃) ≠ 0)
8886, 35, 87divcan1d 11409 . . . . . . . . . 10 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃)) = (log‘(𝐹𝑃)))
8988fveq2d 6667 . . . . . . . . 9 (𝜑 → (exp‘(((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃))) = (exp‘(log‘(𝐹𝑃))))
9020reeflogd 25199 . . . . . . . . 9 (𝜑 → (exp‘(log‘(𝐹𝑃))) = (𝐹𝑃))
9185, 89, 903eqtrd 2858 . . . . . . . 8 (𝜑 → (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))) = (𝐹𝑃))
9280, 84, 913eqtr3d 2862 . . . . . . 7 (𝜑 → ((𝑃𝑐-1)↑𝑐𝑅) = (𝐹𝑃))
9353, 72, 923eqtrrd 2859 . . . . . 6 (𝜑 → (𝐹𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃))
94 fveq2 6663 . . . . . . 7 (𝑃 = 𝑝 → (𝐹𝑃) = (𝐹𝑝))
95 fveq2 6663 . . . . . . 7 (𝑃 = 𝑝 → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
9694, 95eqeq12d 2835 . . . . . 6 (𝑃 = 𝑝 → ((𝐹𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) ↔ (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
9793, 96syl5ibcom 247 . . . . 5 (𝜑 → (𝑃 = 𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
9897adantr 483 . . . 4 ((𝜑𝑝 ∈ ℙ) → (𝑃 = 𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
99 prmnn 16010 . . . . . . . . 9 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
10099ad2antlr 725 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ∈ ℕ)
101 nnq 12353 . . . . . . . 8 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
102100, 101syl 17 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ∈ ℚ)
103 fveq2 6663 . . . . . . . . 9 (𝑦 = 𝑝 → ((𝐽𝑃)‘𝑦) = ((𝐽𝑃)‘𝑝))
104103oveq1d 7163 . . . . . . . 8 (𝑦 = 𝑝 → (((𝐽𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
105 ovex 7181 . . . . . . . 8 (((𝐽𝑃)‘𝑝)↑𝑐𝑅) ∈ V
106104, 50, 105fvmpt 6761 . . . . . . 7 (𝑝 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
107102, 106syl 17 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
10873ad2antrr 724 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑅 ∈ ℂ)
1091081cxpd 25282 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (1↑𝑐𝑅) = 1)
1103ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑃 ∈ ℙ)
11145padicval 26185 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℚ) → ((𝐽𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
112110, 102, 111syl2anc 586 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐽𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
113100nnne0d 11679 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ≠ 0)
114113neneqd 3019 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ 𝑝 = 0)
115114iffalsed 4476 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))) = (𝑃↑-(𝑃 pCnt 𝑝)))
116 pceq0 16199 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℕ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃𝑝))
1173, 99, 116syl2an 597 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃𝑝))
118 dvdsprm 16039 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℤ‘2) ∧ 𝑝 ∈ ℙ) → (𝑃𝑝𝑃 = 𝑝))
1195, 118sylan 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (𝑃𝑝𝑃 = 𝑝))
120119necon3bbid 3051 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑃𝑝𝑃𝑝))
121117, 120bitrd 281 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ 𝑃𝑝))
122121biimpar 480 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃 pCnt 𝑝) = 0)
123122negeqd 10872 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → -(𝑃 pCnt 𝑝) = -0)
124 neg0 10924 . . . . . . . . . . . 12 -0 = 0
125123, 124syl6eq 2870 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → -(𝑃 pCnt 𝑝) = 0)
126125oveq2d 7164 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = (𝑃↑0))
12758ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑃 ∈ ℂ)
128127exp0d 13496 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑0) = 1)
129126, 128eqtrd 2854 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = 1)
130112, 115, 1293eqtrd 2858 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐽𝑃)‘𝑝) = 1)
131130oveq1d 7163 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (((𝐽𝑃)‘𝑝)↑𝑐𝑅) = (1↑𝑐𝑅))
132 2re 11703 . . . . . . . . . . . . 13 2 ∈ ℝ
133132a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 2 ∈ ℝ)
134 ostth3.6 . . . . . . . . . . . . . 14 𝑆 = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃))
1352ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝐹𝐴)
13611, 13abvcl 19587 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴𝑝 ∈ ℚ) → (𝐹𝑝) ∈ ℝ)
137135, 102, 136syl2anc 586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) ∈ ℝ)
13811, 13, 17abvgt0 19591 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴𝑝 ∈ ℚ ∧ 𝑝 ≠ 0) → 0 < (𝐹𝑝))
139135, 102, 113, 138syl3anc 1365 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 0 < (𝐹𝑝))
140137, 139elrpd 12420 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) ∈ ℝ+)
141140adantrr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑝) ∈ ℝ+)
14220ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑃) ∈ ℝ+)
143141, 142ifcld 4510 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) ∈ ℝ+)
144134, 143eqeltrid 2915 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℝ+)
145144rprecred 12434 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (1 / 𝑆) ∈ ℝ)
146 simprr 771 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑝) < 1)
14728ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑃) < 1)
148 breq1 5060 . . . . . . . . . . . . . . . 16 ((𝐹𝑝) = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) → ((𝐹𝑝) < 1 ↔ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1))
149 breq1 5060 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) → ((𝐹𝑃) < 1 ↔ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1))
150148, 149ifboth 4503 . . . . . . . . . . . . . . 15 (((𝐹𝑝) < 1 ∧ (𝐹𝑃) < 1) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1)
151146, 147, 150syl2anc 586 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1)
152134, 151eqbrtrid 5092 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 < 1)
153144reclt1d 12436 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝑆 < 1 ↔ 1 < (1 / 𝑆)))
154152, 153mpbid 234 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 1 < (1 / 𝑆))
155 expnbnd 13585 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (1 / 𝑆) ∈ ℝ ∧ 1 < (1 / 𝑆)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘))
156133, 145, 154, 155syl3anc 1365 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘))
157144rpcnd 12425 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℂ)
158157adantr 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
159144rpne0d 12428 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ≠ 0)
160159adantr 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ≠ 0)
161 nnz 11996 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
162161adantl 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
163158, 160, 162exprecd 13510 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) = (1 / (𝑆𝑘)))
1642ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝐹𝐴)
165 ax-1ne0 10598 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
16612qrng1 26190 . . . . . . . . . . . . . . . . . . 19 1 = (1r𝑄)
16711, 166, 17abv1z 19595 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1)
168164, 165, 167sylancl 588 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) = 1)
1698ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃 ∈ ℕ)
170 nnnn0 11896 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
171 nnexpcl 13434 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑃𝑘) ∈ ℕ)
172169, 170, 171syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃𝑘) ∈ ℕ)
173172nnzd 12078 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃𝑘) ∈ ℤ)
17499ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑝 ∈ ℕ)
175 nnexpcl 13434 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
176174, 170, 175syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
177176nnzd 12078 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℤ)
178 bezout 15883 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑘) ∈ ℤ ∧ (𝑝𝑘) ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)))
179173, 177, 178syl2anc 586 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)))
180 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃𝑝)
1813ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃 ∈ ℙ)
182 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑝 ∈ ℙ)
183 prmrp 16048 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃𝑝))
184181, 182, 183syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃𝑝))
185180, 184mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝑃 gcd 𝑝) = 1)
186185adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃 gcd 𝑝) = 1)
187169adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℕ)
188174adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
189 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
190 rppwr 15900 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃𝑘) gcd (𝑝𝑘)) = 1))
191187, 188, 189, 190syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃𝑘) gcd (𝑝𝑘)) = 1))
192186, 191mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃𝑘) gcd (𝑝𝑘)) = 1)
193192adantrr 715 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃𝑘) gcd (𝑝𝑘)) = 1)
194193eqeq1d 2821 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ↔ 1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))))
1952ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝐹𝐴)
196172adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃𝑘) ∈ ℕ)
197 nnq 12353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃𝑘) ∈ ℕ → (𝑃𝑘) ∈ ℚ)
198196, 197syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃𝑘) ∈ ℚ)
199 simprrl 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℤ)
200 zq 12346 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ℤ → 𝑎 ∈ ℚ)
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℚ)
202 qmulcl 12358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → ((𝑃𝑘) · 𝑎) ∈ ℚ)
203198, 201, 202syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃𝑘) · 𝑎) ∈ ℚ)
204176adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝𝑘) ∈ ℕ)
205 nnq 12353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑘) ∈ ℕ → (𝑝𝑘) ∈ ℚ)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝𝑘) ∈ ℚ)
207 simprrr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℤ)
208 zq 12346 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ℤ → 𝑏 ∈ ℚ)
209207, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℚ)
210 qmulcl 12358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → ((𝑝𝑘) · 𝑏) ∈ ℚ)
211206, 209, 210syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑝𝑘) · 𝑏) ∈ ℚ)
212 qaddcl 12356 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑃𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ)
213203, 211, 212syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ)
21411, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝐴 ∧ (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ∈ ℝ)
215195, 213, 214syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ∈ ℝ)
21611, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝐴 ∧ ((𝑃𝑘) · 𝑎) ∈ ℚ) → (𝐹‘((𝑃𝑘) · 𝑎)) ∈ ℝ)
217195, 203, 216syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) ∈ ℝ)
21811, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝐴 ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (𝐹‘((𝑝𝑘) · 𝑏)) ∈ ℝ)
219195, 211, 218syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) ∈ ℝ)
220217, 219readdcld 10662 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ∈ ℝ)
221 rpexpcl 13440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 ∈ ℝ+𝑘 ∈ ℤ) → (𝑆𝑘) ∈ ℝ+)
222144, 161, 221syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ+)
223222rpred 12423 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
224223adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑆𝑘) ∈ ℝ)
225 remulcl 10614 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℝ ∧ (𝑆𝑘) ∈ ℝ) → (2 · (𝑆𝑘)) ∈ ℝ)
226132, 224, 225sylancr 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆𝑘)) ∈ ℝ)
227 qex 12352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℚ ∈ V
228 cnfldadd 20542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 + = (+g‘ℂfld)
22912, 228ressplusg 16604 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℚ ∈ V → + = (+g𝑄))
230227, 229ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 + = (+g𝑄)
23111, 13, 230abvtri 19593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝐴 ∧ ((𝑃𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))))
232195, 203, 211, 231syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))))
233 cnfldmul 20543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 · = (.r‘ℂfld)
23412, 233ressmulr 16617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ℚ ∈ V → · = (.r𝑄))
235227, 234ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 · = (.r𝑄)
23611, 13, 235abvmul 19592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝐴 ∧ (𝑃𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → (𝐹‘((𝑃𝑘) · 𝑎)) = ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)))
237195, 198, 201, 236syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) = ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)))
23810ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑃 ∈ ℚ)
239170ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℕ0)
24012, 11qabvexp 26194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑃 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑃𝑘)) = ((𝐹𝑃)↑𝑘))
241195, 238, 239, 240syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑃𝑘)) = ((𝐹𝑃)↑𝑘))
242241oveq1d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)) = (((𝐹𝑃)↑𝑘) · (𝐹𝑎)))
243237, 242eqtrd 2854 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) = (((𝐹𝑃)↑𝑘) · (𝐹𝑎)))
244195, 238, 14syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ∈ ℝ)
245244, 239reexpcld 13519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ∈ ℝ)
24611, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑎 ∈ ℚ) → (𝐹𝑎) ∈ ℝ)
247195, 201, 246syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑎) ∈ ℝ)
248245, 247remulcld 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ∈ ℝ)
249 elz 11975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)))
250249simprbi 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 ∈ ℤ → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))
251250adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑎 ∈ ℤ) → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))
25211, 17abv0 19594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐹𝐴 → (𝐹‘0) = 0)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (𝐹‘0) = 0)
254 0le1 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ≤ 1
255253, 254eqbrtrdi 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (𝐹‘0) ≤ 1)
256255adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑎 ∈ ℤ) → (𝐹‘0) ≤ 1)
257 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 0 → (𝐹𝑎) = (𝐹‘0))
258257breq1d 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 0 → ((𝐹𝑎) ≤ 1 ↔ (𝐹‘0) ≤ 1))
259256, 258syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (𝑎 = 0 → (𝐹𝑎) ≤ 1))
260 ostth3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛))
261 nnq 12353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑛 ∈ ℕ → 𝑛 ∈ ℚ)
26211, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐹𝐴𝑛 ∈ ℚ) → (𝐹𝑛) ∈ ℝ)
2632, 261, 262syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℝ)
264 1re 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 ∈ ℝ
265 lenlt 10711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐹𝑛) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐹𝑛) ≤ 1 ↔ ¬ 1 < (𝐹𝑛)))
266263, 264, 265sylancl 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) ≤ 1 ↔ ¬ 1 < (𝐹𝑛)))
267266ralbidva 3194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1 ↔ ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛)))
268260, 267mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1)
269 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = 𝑎 → (𝐹𝑛) = (𝐹𝑎))
270269breq1d 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = 𝑎 → ((𝐹𝑛) ≤ 1 ↔ (𝐹𝑎) ≤ 1))
271270rspccv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1 → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
272268, 271syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
273272adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
2742adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝐹𝐴)
275200ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝑎 ∈ ℚ)
276 eqid 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (invg𝑄) = (invg𝑄)
27711, 13, 276abvneg 19597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹𝐴𝑎 ∈ ℚ) → (𝐹‘((invg𝑄)‘𝑎)) = (𝐹𝑎))
278274, 275, 277syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg𝑄)‘𝑎)) = (𝐹𝑎))
279 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = ((invg𝑄)‘𝑎) → (𝐹𝑛) = (𝐹‘((invg𝑄)‘𝑎)))
280279breq1d 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = ((invg𝑄)‘𝑎) → ((𝐹𝑛) ≤ 1 ↔ (𝐹‘((invg𝑄)‘𝑎)) ≤ 1))
281268adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1)
28212qrngneg 26191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℚ → ((invg𝑄)‘𝑎) = -𝑎)
283275, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ((invg𝑄)‘𝑎) = -𝑎)
284 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → -𝑎 ∈ ℕ)
285283, 284eqeltrd 2911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ((invg𝑄)‘𝑎) ∈ ℕ)
286280, 281, 285rspcdva 3623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg𝑄)‘𝑎)) ≤ 1)
287278, 286eqbrtrrd 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹𝑎) ≤ 1)
288287expr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
289259, 273, 2883jaod 1422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑎 ∈ ℤ) → ((𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ) → (𝐹𝑎) ≤ 1))
290251, 289mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑎 ∈ ℤ) → (𝐹𝑎) ≤ 1)
291290ralrimiva 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1)
292291ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1)
293 rsp 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1 → (𝑎 ∈ ℤ → (𝐹𝑎) ≤ 1))
294292, 199, 293sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑎) ≤ 1)
295264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 1 ∈ ℝ)
296161ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℤ)
29719ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹𝑃))
298 expgt0 13454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑃) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹𝑃)) → 0 < ((𝐹𝑃)↑𝑘))
299244, 296, 297, 298syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹𝑃)↑𝑘))
300 lemul2 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑎) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝐹𝑃)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹𝑃)↑𝑘))) → ((𝐹𝑎) ≤ 1 ↔ (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1)))
301247, 295, 245, 299, 300syl112anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑎) ≤ 1 ↔ (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1)))
302294, 301mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1))
303245recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ∈ ℂ)
304303mulid1d 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · 1) = ((𝐹𝑃)↑𝑘))
305302, 304breqtrd 5083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ ((𝐹𝑃)↑𝑘))
306144rpred 12423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℝ)
307306adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑆 ∈ ℝ)
308142adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ∈ ℝ+)
309308rpge0d 12427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹𝑃))
310174adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℕ)
311310, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℚ)
312195, 311, 136syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ∈ ℝ)
313 max1 12570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑃) ∈ ℝ ∧ (𝐹𝑝) ∈ ℝ) → (𝐹𝑃) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
314244, 312, 313syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
315314, 134breqtrrdi 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ≤ 𝑆)
316 leexp1a 13531 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹𝑃) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑃) ∧ (𝐹𝑃) ≤ 𝑆)) → ((𝐹𝑃)↑𝑘) ≤ (𝑆𝑘))
317244, 307, 239, 309, 315, 316syl32anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ≤ (𝑆𝑘))
318248, 245, 224, 305, 317letrd 10789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (𝑆𝑘))
319243, 318eqbrtrd 5079 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) ≤ (𝑆𝑘))
32011, 13, 235abvmul 19592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝐴 ∧ (𝑝𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → (𝐹‘((𝑝𝑘) · 𝑏)) = ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)))
321195, 206, 209, 320syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) = ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)))
32212, 11qabvexp 26194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑝 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑝𝑘)) = ((𝐹𝑝)↑𝑘))
323195, 311, 239, 322syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑝𝑘)) = ((𝐹𝑝)↑𝑘))
324323oveq1d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)) = (((𝐹𝑝)↑𝑘) · (𝐹𝑏)))
325321, 324eqtrd 2854 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) = (((𝐹𝑝)↑𝑘) · (𝐹𝑏)))
326312, 239reexpcld 13519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ∈ ℝ)
32711, 13abvcl 19587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑏 ∈ ℚ) → (𝐹𝑏) ∈ ℝ)
328195, 209, 327syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑏) ∈ ℝ)
329326, 328remulcld 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ∈ ℝ)
330 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
331330breq1d 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑏 → ((𝐹𝑎) ≤ 1 ↔ (𝐹𝑏) ≤ 1))
332331, 292, 207rspcdva 3623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑏) ≤ 1)
333310nnne0d 11679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ≠ 0)
334195, 311, 333, 138syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹𝑝))
335 expgt0 13454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑝) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹𝑝)) → 0 < ((𝐹𝑝)↑𝑘))
336312, 296, 334, 335syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹𝑝)↑𝑘))
337 lemul2 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑏) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝐹𝑝)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹𝑝)↑𝑘))) → ((𝐹𝑏) ≤ 1 ↔ (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1)))
338328, 295, 326, 336, 337syl112anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑏) ≤ 1 ↔ (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1)))
339332, 338mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1))
340326recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ∈ ℂ)
341340mulid1d 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · 1) = ((𝐹𝑝)↑𝑘))
342339, 341breqtrd 5083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ ((𝐹𝑝)↑𝑘))
343141adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ∈ ℝ+)
344343rpge0d 12427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹𝑝))
345 max2 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑃) ∈ ℝ ∧ (𝐹𝑝) ∈ ℝ) → (𝐹𝑝) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
346244, 312, 345syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
347346, 134breqtrrdi 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ≤ 𝑆)
348 leexp1a 13531 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹𝑝) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑝) ∧ (𝐹𝑝) ≤ 𝑆)) → ((𝐹𝑝)↑𝑘) ≤ (𝑆𝑘))
349312, 307, 239, 344, 347, 348syl32anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ≤ (𝑆𝑘))
350329, 326, 224, 342, 349letrd 10789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (𝑆𝑘))
351325, 350eqbrtrd 5079 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) ≤ (𝑆𝑘))
352217, 219, 224, 224, 319, 351le2addd 11251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ≤ ((𝑆𝑘) + (𝑆𝑘)))
353222rpcnd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
3543532timesd 11872 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 · (𝑆𝑘)) = ((𝑆𝑘) + (𝑆𝑘)))
355354adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆𝑘)) = ((𝑆𝑘) + (𝑆𝑘)))
356352, 355breqtrrd 5085 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘)))
357215, 220, 226, 232, 356letrd 10789 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘)))
358 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) = (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))))
359358breq1d 5067 . . . . . . . . . . . . . . . . . . . . . 22 (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → ((𝐹‘1) ≤ (2 · (𝑆𝑘)) ↔ (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘))))
360357, 359syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
361194, 360sylbid 242 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
362361anassrs 470 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
363362rexlimdvva 3292 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
364179, 363mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) ≤ (2 · (𝑆𝑘)))
365168, 364eqbrtrrd 5081 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 1 ≤ (2 · (𝑆𝑘)))
366222rpregt0d 12429 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑆𝑘) ∈ ℝ ∧ 0 < (𝑆𝑘)))
367 ledivmul2 11511 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ((𝑆𝑘) ∈ ℝ ∧ 0 < (𝑆𝑘))) → ((1 / (𝑆𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆𝑘))))
368264, 132, 366, 367mp3an12i 1458 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑆𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆𝑘))))
369365, 368mpbird 259 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (1 / (𝑆𝑘)) ≤ 2)
370163, 369eqbrtrd 5079 . . . . . . . . . . . . . 14 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ≤ 2)
371 reexpcl 13438 . . . . . . . . . . . . . . . 16 (((1 / 𝑆) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 𝑆)↑𝑘) ∈ ℝ)
372145, 170, 371syl2an 597 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ∈ ℝ)
373 lenlt 10711 . . . . . . . . . . . . . . 15 ((((1 / 𝑆)↑𝑘) ∈ ℝ ∧ 2 ∈ ℝ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘)))
374372, 132, 373sylancl 588 . . . . . . . . . . . . . 14 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘)))
375370, 374mpbid 234 . . . . . . . . . . . . 13 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ¬ 2 < ((1 / 𝑆)↑𝑘))
376375pm2.21d 121 . . . . . . . . . . . 12 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹𝑝) < 1))
377376rexlimdva 3282 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹𝑝) < 1))
378156, 377mpd 15 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ¬ (𝐹𝑝) < 1)
379378expr 459 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐹𝑝) < 1 → ¬ (𝐹𝑝) < 1))
380379pm2.01d 192 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ (𝐹𝑝) < 1)
381 fveq2 6663 . . . . . . . . . . 11 (𝑛 = 𝑝 → (𝐹𝑛) = (𝐹𝑝))
382381breq2d 5069 . . . . . . . . . 10 (𝑛 = 𝑝 → (1 < (𝐹𝑛) ↔ 1 < (𝐹𝑝)))
383382notbid 320 . . . . . . . . 9 (𝑛 = 𝑝 → (¬ 1 < (𝐹𝑛) ↔ ¬ 1 < (𝐹𝑝)))
384260ad2antrr 724 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛))
385383, 384, 100rspcdva 3623 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ 1 < (𝐹𝑝))
386 lttri3 10716 . . . . . . . . 9 (((𝐹𝑝) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐹𝑝) = 1 ↔ (¬ (𝐹𝑝) < 1 ∧ ¬ 1 < (𝐹𝑝))))
387137, 264, 386sylancl 588 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐹𝑝) = 1 ↔ (¬ (𝐹𝑝) < 1 ∧ ¬ 1 < (𝐹𝑝))))
388380, 385, 387mpbir2and 711 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) = 1)
389109, 131, 3883eqtr4d 2864 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (((𝐽𝑃)‘𝑝)↑𝑐𝑅) = (𝐹𝑝))
390107, 389eqtr2d 2855 . . . . 5 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
391390ex 415 . . . 4 ((𝜑𝑝 ∈ ℙ) → (𝑃𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
39298, 391pm2.61dne 3101 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
39312, 11, 2, 47, 392ostthlem2 26196 . 2 (𝜑𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)))
394 oveq2 7156 . . . 4 (𝑎 = 𝑅 → (((𝐽𝑃)‘𝑦)↑𝑐𝑎) = (((𝐽𝑃)‘𝑦)↑𝑐𝑅))
395394mpteq2dv 5153 . . 3 (𝑎 = 𝑅 → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)) = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)))
396395rspceeqv 3636 . 2 ((𝑅 ∈ ℝ+𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))) → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)))
39744, 393, 396syl2anc 586 1 (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ w3o 1080   = wceq 1530   ∈ wcel 2107   ≠ wne 3014  ∀wral 3136  ∃wrex 3137  Vcvv 3493  ifcif 4465   class class class wbr 5057   ↦ cmpt 5137  ‘cfv 6348  (class class class)co 7148  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668  -cneg 10863   / cdiv 11289  ℕcn 11630  2c2 11684  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ℚcq 12340  ℝ+crp 12381  ↑cexp 13421  expce 15407   ∥ cdvds 15599   gcd cgcd 15835  ℙcprime 16007   pCnt cpc 16165   ↾s cress 16476  +gcplusg 16557  .rcmulr 16558  invgcminusg 18096  AbsValcabv 19579  ℂfldccnfld 20537  logclog 25130  ↑𝑐ccxp 25131 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-supp 7823  df-tpos 7884  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12885  df-fzo 13026  df-fl 13154  df-mod 13230  df-seq 13362  df-exp 13422  df-fac 13626  df-bc 13655  df-hash 13683  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-dvds 15600  df-gcd 15836  df-prm 16008  df-pc 16166  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-mulg 18217  df-subg 18268  df-cntz 18439  df-cmn 18900  df-mgp 19232  df-ur 19244  df-ring 19291  df-cring 19292  df-oppr 19365  df-dvdsr 19383  df-unit 19384  df-invr 19414  df-dvr 19425  df-drng 19496  df-subrg 19525  df-abv 19580  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-fbas 20534  df-fg 20535  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-cld 21619  df-ntr 21620  df-cls 21621  df-nei 21698  df-lp 21736  df-perf 21737  df-cn 21827  df-cnp 21828  df-haus 21915  df-tx 22162  df-hmeo 22355  df-fil 22446  df-fm 22538  df-flim 22539  df-flf 22540  df-xms 22922  df-ms 22923  df-tms 22924  df-cncf 23478  df-limc 24456  df-dv 24457  df-log 25132  df-cxp 25133 This theorem is referenced by:  ostth  26207
 Copyright terms: Public domain W3C validator