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

Theorem ostth3 27696
Description: - Lemma for ostth 27697: 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 16729 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
53, 4syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ (ℤ‘2))
6 eluz2b2 12960 . . . . . . . . . . . 12 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
75, 6sylib 218 . . . . . . . . . . 11 (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃))
87simpld 494 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
9 nnq 13001 . . . . . . . . . 10 (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
108, 9syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℚ)
11 qabsabv.a . . . . . . . . . 10 𝐴 = (AbsVal‘𝑄)
12 qrng.q . . . . . . . . . . 11 𝑄 = (ℂflds ℚ)
1312qrngbas 27677 . . . . . . . . . 10 ℚ = (Base‘𝑄)
1411, 13abvcl 20833 . . . . . . . . 9 ((𝐹𝐴𝑃 ∈ ℚ) → (𝐹𝑃) ∈ ℝ)
152, 10, 14syl2anc 584 . . . . . . . 8 (𝜑 → (𝐹𝑃) ∈ ℝ)
168nnne0d 12313 . . . . . . . . 9 (𝜑𝑃 ≠ 0)
1712qrng0 27679 . . . . . . . . . 10 0 = (0g𝑄)
1811, 13, 17abvgt0 20837 . . . . . . . . 9 ((𝐹𝐴𝑃 ∈ ℚ ∧ 𝑃 ≠ 0) → 0 < (𝐹𝑃))
192, 10, 16, 18syl3anc 1370 . . . . . . . 8 (𝜑 → 0 < (𝐹𝑃))
2015, 19elrpd 13071 . . . . . . 7 (𝜑 → (𝐹𝑃) ∈ ℝ+)
2120relogcld 26679 . . . . . 6 (𝜑 → (log‘(𝐹𝑃)) ∈ ℝ)
228nnred 12278 . . . . . . 7 (𝜑𝑃 ∈ ℝ)
237simprd 495 . . . . . . 7 (𝜑 → 1 < 𝑃)
2422, 23rplogcld 26685 . . . . . 6 (𝜑 → (log‘𝑃) ∈ ℝ+)
2521, 24rerpdivcld 13105 . . . . 5 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℝ)
2625renegcld 11687 . . . 4 (𝜑 → -((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℝ)
271, 26eqeltrid 2842 . . 3 (𝜑𝑅 ∈ ℝ)
28 ostth3.4 . . . . . . . . 9 (𝜑 → (𝐹𝑃) < 1)
29 1rp 13035 . . . . . . . . . 10 1 ∈ ℝ+
30 logltb 26656 . . . . . . . . . 10 (((𝐹𝑃) ∈ ℝ+ ∧ 1 ∈ ℝ+) → ((𝐹𝑃) < 1 ↔ (log‘(𝐹𝑃)) < (log‘1)))
3120, 29, 30sylancl 586 . . . . . . . . 9 (𝜑 → ((𝐹𝑃) < 1 ↔ (log‘(𝐹𝑃)) < (log‘1)))
3228, 31mpbid 232 . . . . . . . 8 (𝜑 → (log‘(𝐹𝑃)) < (log‘1))
33 log1 26641 . . . . . . . 8 (log‘1) = 0
3432, 33breqtrdi 5188 . . . . . . 7 (𝜑 → (log‘(𝐹𝑃)) < 0)
3524rpcnd 13076 . . . . . . . 8 (𝜑 → (log‘𝑃) ∈ ℂ)
3635mul01d 11457 . . . . . . 7 (𝜑 → ((log‘𝑃) · 0) = 0)
3734, 36breqtrrd 5175 . . . . . 6 (𝜑 → (log‘(𝐹𝑃)) < ((log‘𝑃) · 0))
38 0red 11261 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
3921, 38, 24ltdivmuld 13125 . . . . . 6 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) < 0 ↔ (log‘(𝐹𝑃)) < ((log‘𝑃) · 0)))
4037, 39mpbird 257 . . . . 5 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) < 0)
4125lt0neg1d 11829 . . . . 5 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) < 0 ↔ 0 < -((log‘(𝐹𝑃)) / (log‘𝑃))))
4240, 41mpbid 232 . . . 4 (𝜑 → 0 < -((log‘(𝐹𝑃)) / (log‘𝑃)))
4342, 1breqtrrdi 5189 . . 3 (𝜑 → 0 < 𝑅)
4427, 43elrpd 13071 . 2 (𝜑𝑅 ∈ ℝ+)
45 padic.j . . . . 5 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))
4612, 11, 45padicabvcxp 27690 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+) → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
473, 44, 46syl2anc 584 . . 3 (𝜑 → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
48 fveq2 6906 . . . . . . . . . 10 (𝑦 = 𝑃 → ((𝐽𝑃)‘𝑦) = ((𝐽𝑃)‘𝑃))
4948oveq1d 7445 . . . . . . . . 9 (𝑦 = 𝑃 → (((𝐽𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
50 eqid 2734 . . . . . . . . 9 (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))
51 ovex 7463 . . . . . . . . 9 (((𝐽𝑃)‘𝑃)↑𝑐𝑅) ∈ V
5249, 50, 51fvmpt 7015 . . . . . . . 8 (𝑃 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
5310, 52syl 17 . . . . . . 7 (𝜑 → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽𝑃)‘𝑃)↑𝑐𝑅))
5445padicval 27675 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝑃 ∈ ℚ) → ((𝐽𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
553, 10, 54syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐽𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
5616neneqd 2942 . . . . . . . . . 10 (𝜑 → ¬ 𝑃 = 0)
5756iffalsed 4541 . . . . . . . . 9 (𝜑 → if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))) = (𝑃↑-(𝑃 pCnt 𝑃)))
588nncnd 12279 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℂ)
5958exp1d 14177 . . . . . . . . . . . . . 14 (𝜑 → (𝑃↑1) = 𝑃)
6059oveq2d 7446 . . . . . . . . . . . . 13 (𝜑 → (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃))
61 1z 12644 . . . . . . . . . . . . . 14 1 ∈ ℤ
62 pcid 16906 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℙ ∧ 1 ∈ ℤ) → (𝑃 pCnt (𝑃↑1)) = 1)
633, 61, 62sylancl 586 . . . . . . . . . . . . 13 (𝜑 → (𝑃 pCnt (𝑃↑1)) = 1)
6460, 63eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 → (𝑃 pCnt 𝑃) = 1)
6564negeqd 11499 . . . . . . . . . . 11 (𝜑 → -(𝑃 pCnt 𝑃) = -1)
6665oveq2d 7446 . . . . . . . . . 10 (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑-1))
67 neg1z 12650 . . . . . . . . . . . 12 -1 ∈ ℤ
6867a1i 11 . . . . . . . . . . 11 (𝜑 → -1 ∈ ℤ)
6958, 16, 68cxpexpzd 26767 . . . . . . . . . 10 (𝜑 → (𝑃𝑐-1) = (𝑃↑-1))
7066, 69eqtr4d 2777 . . . . . . . . 9 (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃𝑐-1))
7155, 57, 703eqtrd 2778 . . . . . . . 8 (𝜑 → ((𝐽𝑃)‘𝑃) = (𝑃𝑐-1))
7271oveq1d 7445 . . . . . . 7 (𝜑 → (((𝐽𝑃)‘𝑃)↑𝑐𝑅) = ((𝑃𝑐-1)↑𝑐𝑅))
7327recnd 11286 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
7473mulm1d 11712 . . . . . . . . . 10 (𝜑 → (-1 · 𝑅) = -𝑅)
751negeqi 11498 . . . . . . . . . . 11 -𝑅 = --((log‘(𝐹𝑃)) / (log‘𝑃))
7625recnd 11286 . . . . . . . . . . . 12 (𝜑 → ((log‘(𝐹𝑃)) / (log‘𝑃)) ∈ ℂ)
7776negnegd 11608 . . . . . . . . . . 11 (𝜑 → --((log‘(𝐹𝑃)) / (log‘𝑃)) = ((log‘(𝐹𝑃)) / (log‘𝑃)))
7875, 77eqtrid 2786 . . . . . . . . . 10 (𝜑 → -𝑅 = ((log‘(𝐹𝑃)) / (log‘𝑃)))
7974, 78eqtrd 2774 . . . . . . . . 9 (𝜑 → (-1 · 𝑅) = ((log‘(𝐹𝑃)) / (log‘𝑃)))
8079oveq2d 7446 . . . . . . . 8 (𝜑 → (𝑃𝑐(-1 · 𝑅)) = (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))))
818nnrpd 13072 . . . . . . . . 9 (𝜑𝑃 ∈ ℝ+)
82 neg1rr 12378 . . . . . . . . . 10 -1 ∈ ℝ
8382a1i 11 . . . . . . . . 9 (𝜑 → -1 ∈ ℝ)
8481, 83, 73cxpmuld 26793 . . . . . . . 8 (𝜑 → (𝑃𝑐(-1 · 𝑅)) = ((𝑃𝑐-1)↑𝑐𝑅))
8558, 16, 76cxpefd 26768 . . . . . . . . 9 (𝜑 → (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))) = (exp‘(((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃))))
8621recnd 11286 . . . . . . . . . . 11 (𝜑 → (log‘(𝐹𝑃)) ∈ ℂ)
8724rpne0d 13079 . . . . . . . . . . 11 (𝜑 → (log‘𝑃) ≠ 0)
8886, 35, 87divcan1d 12041 . . . . . . . . . 10 (𝜑 → (((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃)) = (log‘(𝐹𝑃)))
8988fveq2d 6910 . . . . . . . . 9 (𝜑 → (exp‘(((log‘(𝐹𝑃)) / (log‘𝑃)) · (log‘𝑃))) = (exp‘(log‘(𝐹𝑃))))
9020reeflogd 26680 . . . . . . . . 9 (𝜑 → (exp‘(log‘(𝐹𝑃))) = (𝐹𝑃))
9185, 89, 903eqtrd 2778 . . . . . . . 8 (𝜑 → (𝑃𝑐((log‘(𝐹𝑃)) / (log‘𝑃))) = (𝐹𝑃))
9280, 84, 913eqtr3d 2782 . . . . . . 7 (𝜑 → ((𝑃𝑐-1)↑𝑐𝑅) = (𝐹𝑃))
9353, 72, 923eqtrrd 2779 . . . . . 6 (𝜑 → (𝐹𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃))
94 fveq2 6906 . . . . . . 7 (𝑃 = 𝑝 → (𝐹𝑃) = (𝐹𝑝))
95 fveq2 6906 . . . . . . 7 (𝑃 = 𝑝 → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
9694, 95eqeq12d 2750 . . . . . 6 (𝑃 = 𝑝 → ((𝐹𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) ↔ (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
9793, 96syl5ibcom 245 . . . . 5 (𝜑 → (𝑃 = 𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
9897adantr 480 . . . 4 ((𝜑𝑝 ∈ ℙ) → (𝑃 = 𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
99 prmnn 16707 . . . . . . . . 9 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
10099ad2antlr 727 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ∈ ℕ)
101 nnq 13001 . . . . . . . 8 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
102100, 101syl 17 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ∈ ℚ)
103 fveq2 6906 . . . . . . . . 9 (𝑦 = 𝑝 → ((𝐽𝑃)‘𝑦) = ((𝐽𝑃)‘𝑝))
104103oveq1d 7445 . . . . . . . 8 (𝑦 = 𝑝 → (((𝐽𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
105 ovex 7463 . . . . . . . 8 (((𝐽𝑃)‘𝑝)↑𝑐𝑅) ∈ V
106104, 50, 105fvmpt 7015 . . . . . . 7 (𝑝 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
107102, 106syl 17 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽𝑃)‘𝑝)↑𝑐𝑅))
10873ad2antrr 726 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑅 ∈ ℂ)
1091081cxpd 26763 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (1↑𝑐𝑅) = 1)
1103ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑃 ∈ ℙ)
11145padicval 27675 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℚ) → ((𝐽𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
112110, 102, 111syl2anc 584 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐽𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
113100nnne0d 12313 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑝 ≠ 0)
114113neneqd 2942 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ 𝑝 = 0)
115114iffalsed 4541 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))) = (𝑃↑-(𝑃 pCnt 𝑝)))
116 pceq0 16904 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℕ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃𝑝))
1173, 99, 116syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃𝑝))
118 dvdsprm 16736 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℤ‘2) ∧ 𝑝 ∈ ℙ) → (𝑃𝑝𝑃 = 𝑝))
1195, 118sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (𝑃𝑝𝑃 = 𝑝))
120119necon3bbid 2975 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑃𝑝𝑃𝑝))
121117, 120bitrd 279 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ 𝑃𝑝))
122121biimpar 477 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃 pCnt 𝑝) = 0)
123122negeqd 11499 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → -(𝑃 pCnt 𝑝) = -0)
124 neg0 11552 . . . . . . . . . . . 12 -0 = 0
125123, 124eqtrdi 2790 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → -(𝑃 pCnt 𝑝) = 0)
126125oveq2d 7446 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = (𝑃↑0))
12758ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝑃 ∈ ℂ)
128127exp0d 14176 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑0) = 1)
129126, 128eqtrd 2774 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = 1)
130112, 115, 1293eqtrd 2778 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐽𝑃)‘𝑝) = 1)
131130oveq1d 7445 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (((𝐽𝑃)‘𝑝)↑𝑐𝑅) = (1↑𝑐𝑅))
132 2re 12337 . . . . . . . . . . . . 13 2 ∈ ℝ
133132a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 2 ∈ ℝ)
134 ostth3.6 . . . . . . . . . . . . . 14 𝑆 = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃))
1352ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 𝐹𝐴)
13611, 13abvcl 20833 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴𝑝 ∈ ℚ) → (𝐹𝑝) ∈ ℝ)
137135, 102, 136syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) ∈ ℝ)
13811, 13, 17abvgt0 20837 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴𝑝 ∈ ℚ ∧ 𝑝 ≠ 0) → 0 < (𝐹𝑝))
139135, 102, 113, 138syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → 0 < (𝐹𝑝))
140137, 139elrpd 13071 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) ∈ ℝ+)
141140adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑝) ∈ ℝ+)
14220ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑃) ∈ ℝ+)
143141, 142ifcld 4576 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) ∈ ℝ+)
144134, 143eqeltrid 2842 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℝ+)
145144rprecred 13085 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (1 / 𝑆) ∈ ℝ)
146 simprr 773 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑝) < 1)
14728ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝐹𝑃) < 1)
148 breq1 5150 . . . . . . . . . . . . . . . 16 ((𝐹𝑝) = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) → ((𝐹𝑝) < 1 ↔ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1))
149 breq1 5150 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) = if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) → ((𝐹𝑃) < 1 ↔ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1))
150148, 149ifboth 4569 . . . . . . . . . . . . . . 15 (((𝐹𝑝) < 1 ∧ (𝐹𝑃) < 1) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1)
151146, 147, 150syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)) < 1)
152134, 151eqbrtrid 5182 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 < 1)
153144reclt1d 13087 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝑆 < 1 ↔ 1 < (1 / 𝑆)))
154152, 153mpbid 232 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 1 < (1 / 𝑆))
155 expnbnd 14267 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (1 / 𝑆) ∈ ℝ ∧ 1 < (1 / 𝑆)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘))
156133, 145, 154, 155syl3anc 1370 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘))
157144rpcnd 13076 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℂ)
158157adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
159144rpne0d 13079 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ≠ 0)
160159adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ≠ 0)
161 nnz 12631 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
162161adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
163158, 160, 162exprecd 14190 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) = (1 / (𝑆𝑘)))
1642ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝐹𝐴)
165 ax-1ne0 11221 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
16612qrng1 27680 . . . . . . . . . . . . . . . . . . 19 1 = (1r𝑄)
16711, 166, 17abv1z 20841 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1)
168164, 165, 167sylancl 586 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) = 1)
1698ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃 ∈ ℕ)
170 nnnn0 12530 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
171 nnexpcl 14111 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑃𝑘) ∈ ℕ)
172169, 170, 171syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃𝑘) ∈ ℕ)
173172nnzd 12637 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃𝑘) ∈ ℤ)
17499ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑝 ∈ ℕ)
175 nnexpcl 14111 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
176174, 170, 175syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
177176nnzd 12637 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℤ)
178 bezout 16576 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑘) ∈ ℤ ∧ (𝑝𝑘) ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)))
179173, 177, 178syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)))
180 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃𝑝)
1813ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑃 ∈ ℙ)
182 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑝 ∈ ℙ)
183 prmrp 16745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃𝑝))
184181, 182, 183syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃𝑝))
185180, 184mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (𝑃 gcd 𝑝) = 1)
186185adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃 gcd 𝑝) = 1)
187169adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℕ)
188174adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
189 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
190 rppwr 16593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃𝑘) gcd (𝑝𝑘)) = 1))
191187, 188, 189, 190syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃𝑘) gcd (𝑝𝑘)) = 1))
192186, 191mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃𝑘) gcd (𝑝𝑘)) = 1)
193192adantrr 717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃𝑘) gcd (𝑝𝑘)) = 1)
194193eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ↔ 1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))))
1952ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝐹𝐴)
196172adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃𝑘) ∈ ℕ)
197 nnq 13001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃𝑘) ∈ ℕ → (𝑃𝑘) ∈ ℚ)
198196, 197syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃𝑘) ∈ ℚ)
199 simprrl 781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℤ)
200 zq 12993 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ℤ → 𝑎 ∈ ℚ)
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℚ)
202 qmulcl 13006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → ((𝑃𝑘) · 𝑎) ∈ ℚ)
203198, 201, 202syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃𝑘) · 𝑎) ∈ ℚ)
204176adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝𝑘) ∈ ℕ)
205 nnq 13001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑝𝑘) ∈ ℕ → (𝑝𝑘) ∈ ℚ)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝𝑘) ∈ ℚ)
207 simprrr 782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℤ)
208 zq 12993 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ℤ → 𝑏 ∈ ℚ)
209207, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℚ)
210 qmulcl 13006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑝𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → ((𝑝𝑘) · 𝑏) ∈ ℚ)
211206, 209, 210syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑝𝑘) · 𝑏) ∈ ℚ)
212 qaddcl 13004 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑃𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ)
213203, 211, 212syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ)
21411, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝐴 ∧ (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) ∈ ℚ) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ∈ ℝ)
215195, 213, 214syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ∈ ℝ)
21611, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝐴 ∧ ((𝑃𝑘) · 𝑎) ∈ ℚ) → (𝐹‘((𝑃𝑘) · 𝑎)) ∈ ℝ)
217195, 203, 216syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) ∈ ℝ)
21811, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝐴 ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (𝐹‘((𝑝𝑘) · 𝑏)) ∈ ℝ)
219195, 211, 218syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) ∈ ℝ)
220217, 219readdcld 11287 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ∈ ℝ)
221 rpexpcl 14117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 ∈ ℝ+𝑘 ∈ ℤ) → (𝑆𝑘) ∈ ℝ+)
222144, 161, 221syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ+)
223222rpred 13074 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
224223adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑆𝑘) ∈ ℝ)
225 remulcl 11237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℝ ∧ (𝑆𝑘) ∈ ℝ) → (2 · (𝑆𝑘)) ∈ ℝ)
226132, 224, 225sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆𝑘)) ∈ ℝ)
227 qex 13000 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℚ ∈ V
228 cnfldadd 21387 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 + = (+g‘ℂfld)
22912, 228ressplusg 17335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℚ ∈ V → + = (+g𝑄))
230227, 229ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 + = (+g𝑄)
23111, 13, 230abvtri 20839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝐴 ∧ ((𝑃𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝𝑘) · 𝑏) ∈ ℚ) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))))
232195, 203, 211, 231syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))))
233 cnfldmul 21389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 · = (.r‘ℂfld)
23412, 233ressmulr 17352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (ℚ ∈ V → · = (.r𝑄))
235227, 234ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 · = (.r𝑄)
23611, 13, 235abvmul 20838 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝐴 ∧ (𝑃𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → (𝐹‘((𝑃𝑘) · 𝑎)) = ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)))
237195, 198, 201, 236syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) = ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)))
23810ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑃 ∈ ℚ)
239170ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℕ0)
24012, 11qabvexp 27684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑃 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑃𝑘)) = ((𝐹𝑃)↑𝑘))
241195, 238, 239, 240syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑃𝑘)) = ((𝐹𝑃)↑𝑘))
242241oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑃𝑘)) · (𝐹𝑎)) = (((𝐹𝑃)↑𝑘) · (𝐹𝑎)))
243237, 242eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) = (((𝐹𝑃)↑𝑘) · (𝐹𝑎)))
244195, 238, 14syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ∈ ℝ)
245244, 239reexpcld 14199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ∈ ℝ)
24611, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑎 ∈ ℚ) → (𝐹𝑎) ∈ ℝ)
247195, 201, 246syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑎) ∈ ℝ)
248245, 247remulcld 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ∈ ℝ)
249 elz 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)))
250249simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑎 ∈ ℤ → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))
251250adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑎 ∈ ℤ) → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))
25211, 17abv0 20840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐹𝐴 → (𝐹‘0) = 0)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (𝐹‘0) = 0)
254 0le1 11783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ≤ 1
255253, 254eqbrtrdi 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (𝐹‘0) ≤ 1)
256255adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑎 ∈ ℤ) → (𝐹‘0) ≤ 1)
257 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 0 → (𝐹𝑎) = (𝐹‘0))
258257breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = 0 → ((𝐹𝑎) ≤ 1 ↔ (𝐹‘0) ≤ 1))
259256, 258syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (𝑎 = 0 → (𝐹𝑎) ≤ 1))
260 ostth3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛))
261 nnq 13001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑛 ∈ ℕ → 𝑛 ∈ ℚ)
26211, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐹𝐴𝑛 ∈ ℚ) → (𝐹𝑛) ∈ ℝ)
2632, 261, 262syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℝ)
264 1re 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 ∈ ℝ
265 lenlt 11336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐹𝑛) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐹𝑛) ≤ 1 ↔ ¬ 1 < (𝐹𝑛)))
266263, 264, 265sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) ≤ 1 ↔ ¬ 1 < (𝐹𝑛)))
267266ralbidva 3173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1 ↔ ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛)))
268260, 267mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1)
269 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = 𝑎 → (𝐹𝑛) = (𝐹𝑎))
270269breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = 𝑎 → ((𝐹𝑛) ≤ 1 ↔ (𝐹𝑎) ≤ 1))
271270rspccv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1 → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
272268, 271syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
273272adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
2742adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝐹𝐴)
275200ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝑎 ∈ ℚ)
276 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (invg𝑄) = (invg𝑄)
27711, 13, 276abvneg 20843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹𝐴𝑎 ∈ ℚ) → (𝐹‘((invg𝑄)‘𝑎)) = (𝐹𝑎))
278274, 275, 277syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg𝑄)‘𝑎)) = (𝐹𝑎))
279 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = ((invg𝑄)‘𝑎) → (𝐹𝑛) = (𝐹‘((invg𝑄)‘𝑎)))
280279breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = ((invg𝑄)‘𝑎) → ((𝐹𝑛) ≤ 1 ↔ (𝐹‘((invg𝑄)‘𝑎)) ≤ 1))
281268adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝐹𝑛) ≤ 1)
28212qrngneg 27681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ ℚ → ((invg𝑄)‘𝑎) = -𝑎)
283275, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ((invg𝑄)‘𝑎) = -𝑎)
284 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → -𝑎 ∈ ℕ)
285283, 284eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ((invg𝑄)‘𝑎) ∈ ℕ)
286280, 281, 285rspcdva 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg𝑄)‘𝑎)) ≤ 1)
287278, 286eqbrtrrd 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹𝑎) ≤ 1)
288287expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ → (𝐹𝑎) ≤ 1))
289259, 273, 2883jaod 1428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑎 ∈ ℤ) → ((𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ) → (𝐹𝑎) ≤ 1))
290251, 289mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑎 ∈ ℤ) → (𝐹𝑎) ≤ 1)
291290ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1)
292291ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1)
293 rsp 3244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎 ∈ ℤ (𝐹𝑎) ≤ 1 → (𝑎 ∈ ℤ → (𝐹𝑎) ≤ 1))
294292, 199, 293sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑎) ≤ 1)
295264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 1 ∈ ℝ)
296161ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℤ)
29719ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹𝑃))
298 expgt0 14132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑃) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹𝑃)) → 0 < ((𝐹𝑃)↑𝑘))
299244, 296, 297, 298syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹𝑃)↑𝑘))
300 lemul2 12117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑎) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝐹𝑃)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹𝑃)↑𝑘))) → ((𝐹𝑎) ≤ 1 ↔ (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1)))
301247, 295, 245, 299, 300syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑎) ≤ 1 ↔ (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1)))
302294, 301mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (((𝐹𝑃)↑𝑘) · 1))
303245recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ∈ ℂ)
304303mulridd 11275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · 1) = ((𝐹𝑃)↑𝑘))
305302, 304breqtrd 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ ((𝐹𝑃)↑𝑘))
306144rpred 13074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → 𝑆 ∈ ℝ)
307306adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑆 ∈ ℝ)
308142adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ∈ ℝ+)
309308rpge0d 13078 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹𝑃))
310174adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℕ)
311310, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℚ)
312195, 311, 136syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ∈ ℝ)
313 max1 13223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑃) ∈ ℝ ∧ (𝐹𝑝) ∈ ℝ) → (𝐹𝑃) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
314244, 312, 313syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
315314, 134breqtrrdi 5189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑃) ≤ 𝑆)
316 leexp1a 14211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹𝑃) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑃) ∧ (𝐹𝑃) ≤ 𝑆)) → ((𝐹𝑃)↑𝑘) ≤ (𝑆𝑘))
317244, 307, 239, 309, 315, 316syl32anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑃)↑𝑘) ≤ (𝑆𝑘))
318248, 245, 224, 305, 317letrd 11415 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑃)↑𝑘) · (𝐹𝑎)) ≤ (𝑆𝑘))
319243, 318eqbrtrd 5169 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃𝑘) · 𝑎)) ≤ (𝑆𝑘))
32011, 13, 235abvmul 20838 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝐴 ∧ (𝑝𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → (𝐹‘((𝑝𝑘) · 𝑏)) = ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)))
321195, 206, 209, 320syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) = ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)))
32212, 11qabvexp 27684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑝 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑝𝑘)) = ((𝐹𝑝)↑𝑘))
323195, 311, 239, 322syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑝𝑘)) = ((𝐹𝑝)↑𝑘))
324323oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑝𝑘)) · (𝐹𝑏)) = (((𝐹𝑝)↑𝑘) · (𝐹𝑏)))
325321, 324eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) = (((𝐹𝑝)↑𝑘) · (𝐹𝑏)))
326312, 239reexpcld 14199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ∈ ℝ)
32711, 13abvcl 20833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝐴𝑏 ∈ ℚ) → (𝐹𝑏) ∈ ℝ)
328195, 209, 327syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑏) ∈ ℝ)
329326, 328remulcld 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ∈ ℝ)
330 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
331330breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑏 → ((𝐹𝑎) ≤ 1 ↔ (𝐹𝑏) ≤ 1))
332331, 292, 207rspcdva 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑏) ≤ 1)
333310nnne0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ≠ 0)
334195, 311, 333, 138syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹𝑝))
335 expgt0 14132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑝) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹𝑝)) → 0 < ((𝐹𝑝)↑𝑘))
336312, 296, 334, 335syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹𝑝)↑𝑘))
337 lemul2 12117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑏) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝐹𝑝)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹𝑝)↑𝑘))) → ((𝐹𝑏) ≤ 1 ↔ (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1)))
338328, 295, 326, 336, 337syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑏) ≤ 1 ↔ (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1)))
339332, 338mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (((𝐹𝑝)↑𝑘) · 1))
340326recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ∈ ℂ)
341340mulridd 11275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · 1) = ((𝐹𝑝)↑𝑘))
342339, 341breqtrd 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ ((𝐹𝑝)↑𝑘))
343141adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ∈ ℝ+)
344343rpge0d 13078 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹𝑝))
345 max2 13225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐹𝑃) ∈ ℝ ∧ (𝐹𝑝) ∈ ℝ) → (𝐹𝑝) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
346244, 312, 345syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ≤ if((𝐹𝑃) ≤ (𝐹𝑝), (𝐹𝑝), (𝐹𝑃)))
347346, 134breqtrrdi 5189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹𝑝) ≤ 𝑆)
348 leexp1a 14211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹𝑝) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑝) ∧ (𝐹𝑝) ≤ 𝑆)) → ((𝐹𝑝)↑𝑘) ≤ (𝑆𝑘))
349312, 307, 239, 344, 347, 348syl32anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹𝑝)↑𝑘) ≤ (𝑆𝑘))
350329, 326, 224, 342, 349letrd 11415 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹𝑝)↑𝑘) · (𝐹𝑏)) ≤ (𝑆𝑘))
351325, 350eqbrtrd 5169 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝𝑘) · 𝑏)) ≤ (𝑆𝑘))
352217, 219, 224, 224, 319, 351le2addd 11879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ≤ ((𝑆𝑘) + (𝑆𝑘)))
353222rpcnd 13076 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
3543532timesd 12506 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 · (𝑆𝑘)) = ((𝑆𝑘) + (𝑆𝑘)))
355354adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆𝑘)) = ((𝑆𝑘) + (𝑆𝑘)))
356352, 355breqtrrd 5175 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃𝑘) · 𝑎)) + (𝐹‘((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘)))
357215, 220, 226, 232, 356letrd 11415 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘)))
358 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) = (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))))
359358breq1d 5157 . . . . . . . . . . . . . . . . . . . . . 22 (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → ((𝐹‘1) ≤ (2 · (𝑆𝑘)) ↔ (𝐹‘(((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏))) ≤ (2 · (𝑆𝑘))))
360357, 359syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (1 = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
361194, 360sylbid 240 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
362361anassrs 467 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
363362rexlimdvva 3210 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃𝑘) gcd (𝑝𝑘)) = (((𝑃𝑘) · 𝑎) + ((𝑝𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆𝑘))))
364179, 363mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) ≤ (2 · (𝑆𝑘)))
365168, 364eqbrtrrd 5171 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 1 ≤ (2 · (𝑆𝑘)))
366222rpregt0d 13080 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑆𝑘) ∈ ℝ ∧ 0 < (𝑆𝑘)))
367 ledivmul2 12144 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ((𝑆𝑘) ∈ ℝ ∧ 0 < (𝑆𝑘))) → ((1 / (𝑆𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆𝑘))))
368264, 132, 366, 367mp3an12i 1464 . . . . . . . . . . . . . . . 16 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑆𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆𝑘))))
369365, 368mpbird 257 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (1 / (𝑆𝑘)) ≤ 2)
370163, 369eqbrtrd 5169 . . . . . . . . . . . . . 14 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ≤ 2)
371 reexpcl 14115 . . . . . . . . . . . . . . . 16 (((1 / 𝑆) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 𝑆)↑𝑘) ∈ ℝ)
372145, 170, 371syl2an 596 . . . . . . . . . . . . . . 15 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ∈ ℝ)
373 lenlt 11336 . . . . . . . . . . . . . . 15 ((((1 / 𝑆)↑𝑘) ∈ ℝ ∧ 2 ∈ ℝ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘)))
374372, 132, 373sylancl 586 . . . . . . . . . . . . . 14 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘)))
375370, 374mpbid 232 . . . . . . . . . . . . 13 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ¬ 2 < ((1 / 𝑆)↑𝑘))
376375pm2.21d 121 . . . . . . . . . . . 12 ((((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹𝑝) < 1))
377376rexlimdva 3152 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → (∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹𝑝) < 1))
378156, 377mpd 15 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝑃𝑝 ∧ (𝐹𝑝) < 1)) → ¬ (𝐹𝑝) < 1)
379378expr 456 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐹𝑝) < 1 → ¬ (𝐹𝑝) < 1))
380379pm2.01d 190 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ (𝐹𝑝) < 1)
381 fveq2 6906 . . . . . . . . . . 11 (𝑛 = 𝑝 → (𝐹𝑛) = (𝐹𝑝))
382381breq2d 5159 . . . . . . . . . 10 (𝑛 = 𝑝 → (1 < (𝐹𝑛) ↔ 1 < (𝐹𝑝)))
383382notbid 318 . . . . . . . . 9 (𝑛 = 𝑝 → (¬ 1 < (𝐹𝑛) ↔ ¬ 1 < (𝐹𝑝)))
384260ad2antrr 726 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹𝑛))
385383, 384, 100rspcdva 3622 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ¬ 1 < (𝐹𝑝))
386 lttri3 11341 . . . . . . . . 9 (((𝐹𝑝) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝐹𝑝) = 1 ↔ (¬ (𝐹𝑝) < 1 ∧ ¬ 1 < (𝐹𝑝))))
387137, 264, 386sylancl 586 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → ((𝐹𝑝) = 1 ↔ (¬ (𝐹𝑝) < 1 ∧ ¬ 1 < (𝐹𝑝))))
388380, 385, 387mpbir2and 713 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) = 1)
389109, 131, 3883eqtr4d 2784 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (((𝐽𝑃)‘𝑝)↑𝑐𝑅) = (𝐹𝑝))
390107, 389eqtr2d 2775 . . . . 5 (((𝜑𝑝 ∈ ℙ) ∧ 𝑃𝑝) → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
391390ex 412 . . . 4 ((𝜑𝑝 ∈ ℙ) → (𝑃𝑝 → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)))
39298, 391pm2.61dne 3025 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝐹𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))
39312, 11, 2, 47, 392ostthlem2 27686 . 2 (𝜑𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)))
394 oveq2 7438 . . . 4 (𝑎 = 𝑅 → (((𝐽𝑃)‘𝑦)↑𝑐𝑎) = (((𝐽𝑃)‘𝑦)↑𝑐𝑅))
395394mpteq2dv 5249 . . 3 (𝑎 = 𝑅 → (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)) = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅)))
396395rspceeqv 3644 . 2 ((𝑅 ∈ ℝ+𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑅))) → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)))
39744, 393, 396syl2anc 584 1 (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽𝑃)‘𝑦)↑𝑐𝑎)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3o 1085   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  ifcif 4530   class class class wbr 5147  cmpt 5230  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  -cneg 11490   / cdiv 11917  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  cq 12987  +crp 13031  cexp 14098  expce 16093  cdvds 16286   gcd cgcd 16527  cprime 16704   pCnt cpc 16869  s cress 17273  +gcplusg 17297  .rcmulr 17298  invgcminusg 18964  AbsValcabv 20825  fldccnfld 21381  logclog 26610  𝑐ccxp 26611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231  ax-mulf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-dvds 16287  df-gcd 16528  df-prm 16705  df-pc 16870  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-grp 18966  df-minusg 18967  df-mulg 19098  df-subg 19153  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-oppr 20350  df-dvdsr 20373  df-unit 20374  df-invr 20404  df-dvr 20417  df-subrng 20562  df-subrg 20586  df-drng 20747  df-abv 20826  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916  df-log 26612  df-cxp 26613
This theorem is referenced by:  ostth  27697
  Copyright terms: Public domain W3C validator