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

Theorem ostth3 27002
Description: - Lemma for ostth 27003: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
qrng.q 𝑄 = (β„‚fld β†Ύs β„š)
qabsabv.a 𝐴 = (AbsValβ€˜π‘„)
padic.j 𝐽 = (π‘ž ∈ β„™ ↦ (π‘₯ ∈ β„š ↦ if(π‘₯ = 0, 0, (π‘žβ†‘-(π‘ž pCnt π‘₯)))))
ostth.k 𝐾 = (π‘₯ ∈ β„š ↦ if(π‘₯ = 0, 0, 1))
ostth.1 (πœ‘ β†’ 𝐹 ∈ 𝐴)
ostth3.2 (πœ‘ β†’ βˆ€π‘› ∈ β„• Β¬ 1 < (πΉβ€˜π‘›))
ostth3.3 (πœ‘ β†’ 𝑃 ∈ β„™)
ostth3.4 (πœ‘ β†’ (πΉβ€˜π‘ƒ) < 1)
ostth3.5 𝑅 = -((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))
ostth3.6 𝑆 = if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ))
Assertion
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 16577 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
53, 4syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
6 eluz2b2 12851 . . . . . . . . . . . 12 (𝑃 ∈ (β„€β‰₯β€˜2) ↔ (𝑃 ∈ β„• ∧ 1 < 𝑃))
75, 6sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ (𝑃 ∈ β„• ∧ 1 < 𝑃))
87simpld 496 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„•)
9 nnq 12892 . . . . . . . . . 10 (𝑃 ∈ β„• β†’ 𝑃 ∈ β„š)
108, 9syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ β„š)
11 qabsabv.a . . . . . . . . . 10 𝐴 = (AbsValβ€˜π‘„)
12 qrng.q . . . . . . . . . . 11 𝑄 = (β„‚fld β†Ύs β„š)
1312qrngbas 26983 . . . . . . . . . 10 β„š = (Baseβ€˜π‘„)
1411, 13abvcl 20297 . . . . . . . . 9 ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ β„š) β†’ (πΉβ€˜π‘ƒ) ∈ ℝ)
152, 10, 14syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ∈ ℝ)
168nnne0d 12208 . . . . . . . . 9 (πœ‘ β†’ 𝑃 β‰  0)
1712qrng0 26985 . . . . . . . . . 10 0 = (0gβ€˜π‘„)
1811, 13, 17abvgt0 20301 . . . . . . . . 9 ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ β„š ∧ 𝑃 β‰  0) β†’ 0 < (πΉβ€˜π‘ƒ))
192, 10, 16, 18syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ 0 < (πΉβ€˜π‘ƒ))
2015, 19elrpd 12959 . . . . . . 7 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ∈ ℝ+)
2120relogcld 25994 . . . . . 6 (πœ‘ β†’ (logβ€˜(πΉβ€˜π‘ƒ)) ∈ ℝ)
228nnred 12173 . . . . . . 7 (πœ‘ β†’ 𝑃 ∈ ℝ)
237simprd 497 . . . . . . 7 (πœ‘ β†’ 1 < 𝑃)
2422, 23rplogcld 26000 . . . . . 6 (πœ‘ β†’ (logβ€˜π‘ƒ) ∈ ℝ+)
2521, 24rerpdivcld 12993 . . . . 5 (πœ‘ β†’ ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) ∈ ℝ)
2625renegcld 11587 . . . 4 (πœ‘ β†’ -((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) ∈ ℝ)
271, 26eqeltrid 2838 . . 3 (πœ‘ β†’ 𝑅 ∈ ℝ)
28 ostth3.4 . . . . . . . . 9 (πœ‘ β†’ (πΉβ€˜π‘ƒ) < 1)
29 1rp 12924 . . . . . . . . . 10 1 ∈ ℝ+
30 logltb 25971 . . . . . . . . . 10 (((πΉβ€˜π‘ƒ) ∈ ℝ+ ∧ 1 ∈ ℝ+) β†’ ((πΉβ€˜π‘ƒ) < 1 ↔ (logβ€˜(πΉβ€˜π‘ƒ)) < (logβ€˜1)))
3120, 29, 30sylancl 587 . . . . . . . . 9 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) < 1 ↔ (logβ€˜(πΉβ€˜π‘ƒ)) < (logβ€˜1)))
3228, 31mpbid 231 . . . . . . . 8 (πœ‘ β†’ (logβ€˜(πΉβ€˜π‘ƒ)) < (logβ€˜1))
33 log1 25957 . . . . . . . 8 (logβ€˜1) = 0
3432, 33breqtrdi 5147 . . . . . . 7 (πœ‘ β†’ (logβ€˜(πΉβ€˜π‘ƒ)) < 0)
3524rpcnd 12964 . . . . . . . 8 (πœ‘ β†’ (logβ€˜π‘ƒ) ∈ β„‚)
3635mul01d 11359 . . . . . . 7 (πœ‘ β†’ ((logβ€˜π‘ƒ) Β· 0) = 0)
3734, 36breqtrrd 5134 . . . . . 6 (πœ‘ β†’ (logβ€˜(πΉβ€˜π‘ƒ)) < ((logβ€˜π‘ƒ) Β· 0))
38 0red 11163 . . . . . . 7 (πœ‘ β†’ 0 ∈ ℝ)
3921, 38, 24ltdivmuld 13013 . . . . . 6 (πœ‘ β†’ (((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) < 0 ↔ (logβ€˜(πΉβ€˜π‘ƒ)) < ((logβ€˜π‘ƒ) Β· 0)))
4037, 39mpbird 257 . . . . 5 (πœ‘ β†’ ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) < 0)
4125lt0neg1d 11729 . . . . 5 (πœ‘ β†’ (((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) < 0 ↔ 0 < -((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))))
4240, 41mpbid 231 . . . 4 (πœ‘ β†’ 0 < -((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)))
4342, 1breqtrrdi 5148 . . 3 (πœ‘ β†’ 0 < 𝑅)
4427, 43elrpd 12959 . 2 (πœ‘ β†’ 𝑅 ∈ ℝ+)
45 padic.j . . . . 5 𝐽 = (π‘ž ∈ β„™ ↦ (π‘₯ ∈ β„š ↦ if(π‘₯ = 0, 0, (π‘žβ†‘-(π‘ž pCnt π‘₯)))))
4612, 11, 45padicabvcxp 26996 . . . 4 ((𝑃 ∈ β„™ ∧ 𝑅 ∈ ℝ+) β†’ (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅)) ∈ 𝐴)
473, 44, 46syl2anc 585 . . 3 (πœ‘ β†’ (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅)) ∈ 𝐴)
48 fveq2 6843 . . . . . . . . . 10 (𝑦 = 𝑃 β†’ ((π½β€˜π‘ƒ)β€˜π‘¦) = ((π½β€˜π‘ƒ)β€˜π‘ƒ))
4948oveq1d 7373 . . . . . . . . 9 (𝑦 = 𝑃 β†’ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅) = (((π½β€˜π‘ƒ)β€˜π‘ƒ)↑𝑐𝑅))
50 eqid 2733 . . . . . . . . 9 (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅)) = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))
51 ovex 7391 . . . . . . . . 9 (((π½β€˜π‘ƒ)β€˜π‘ƒ)↑𝑐𝑅) ∈ V
5249, 50, 51fvmpt 6949 . . . . . . . 8 (𝑃 ∈ β„š β†’ ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘ƒ) = (((π½β€˜π‘ƒ)β€˜π‘ƒ)↑𝑐𝑅))
5310, 52syl 17 . . . . . . 7 (πœ‘ β†’ ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘ƒ) = (((π½β€˜π‘ƒ)β€˜π‘ƒ)↑𝑐𝑅))
5445padicval 26981 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ 𝑃 ∈ β„š) β†’ ((π½β€˜π‘ƒ)β€˜π‘ƒ) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
553, 10, 54syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ ((π½β€˜π‘ƒ)β€˜π‘ƒ) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))))
5616neneqd 2945 . . . . . . . . . 10 (πœ‘ β†’ Β¬ 𝑃 = 0)
5756iffalsed 4498 . . . . . . . . 9 (πœ‘ β†’ if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))) = (𝑃↑-(𝑃 pCnt 𝑃)))
588nncnd 12174 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ β„‚)
5958exp1d 14052 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑃↑1) = 𝑃)
6059oveq2d 7374 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃))
61 1z 12538 . . . . . . . . . . . . . 14 1 ∈ β„€
62 pcid 16750 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ 1 ∈ β„€) β†’ (𝑃 pCnt (𝑃↑1)) = 1)
633, 61, 62sylancl 587 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃 pCnt (𝑃↑1)) = 1)
6460, 63eqtr3d 2775 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑃 pCnt 𝑃) = 1)
6564negeqd 11400 . . . . . . . . . . 11 (πœ‘ β†’ -(𝑃 pCnt 𝑃) = -1)
6665oveq2d 7374 . . . . . . . . . 10 (πœ‘ β†’ (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑-1))
67 neg1z 12544 . . . . . . . . . . . 12 -1 ∈ β„€
6867a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ -1 ∈ β„€)
6958, 16, 68cxpexpzd 26082 . . . . . . . . . 10 (πœ‘ β†’ (𝑃↑𝑐-1) = (𝑃↑-1))
7066, 69eqtr4d 2776 . . . . . . . . 9 (πœ‘ β†’ (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑𝑐-1))
7155, 57, 703eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ ((π½β€˜π‘ƒ)β€˜π‘ƒ) = (𝑃↑𝑐-1))
7271oveq1d 7373 . . . . . . 7 (πœ‘ β†’ (((π½β€˜π‘ƒ)β€˜π‘ƒ)↑𝑐𝑅) = ((𝑃↑𝑐-1)↑𝑐𝑅))
7327recnd 11188 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ β„‚)
7473mulm1d 11612 . . . . . . . . . 10 (πœ‘ β†’ (-1 Β· 𝑅) = -𝑅)
751negeqi 11399 . . . . . . . . . . 11 -𝑅 = --((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))
7625recnd 11188 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) ∈ β„‚)
7776negnegd 11508 . . . . . . . . . . 11 (πœ‘ β†’ --((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) = ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)))
7875, 77eqtrid 2785 . . . . . . . . . 10 (πœ‘ β†’ -𝑅 = ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)))
7974, 78eqtrd 2773 . . . . . . . . 9 (πœ‘ β†’ (-1 Β· 𝑅) = ((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)))
8079oveq2d 7374 . . . . . . . 8 (πœ‘ β†’ (𝑃↑𝑐(-1 Β· 𝑅)) = (𝑃↑𝑐((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))))
818nnrpd 12960 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ ℝ+)
82 neg1rr 12273 . . . . . . . . . 10 -1 ∈ ℝ
8382a1i 11 . . . . . . . . 9 (πœ‘ β†’ -1 ∈ ℝ)
8481, 83, 73cxpmuld 26107 . . . . . . . 8 (πœ‘ β†’ (𝑃↑𝑐(-1 Β· 𝑅)) = ((𝑃↑𝑐-1)↑𝑐𝑅))
8558, 16, 76cxpefd 26083 . . . . . . . . 9 (πœ‘ β†’ (𝑃↑𝑐((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))) = (expβ€˜(((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) Β· (logβ€˜π‘ƒ))))
8621recnd 11188 . . . . . . . . . . 11 (πœ‘ β†’ (logβ€˜(πΉβ€˜π‘ƒ)) ∈ β„‚)
8724rpne0d 12967 . . . . . . . . . . 11 (πœ‘ β†’ (logβ€˜π‘ƒ) β‰  0)
8886, 35, 87divcan1d 11937 . . . . . . . . . 10 (πœ‘ β†’ (((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) Β· (logβ€˜π‘ƒ)) = (logβ€˜(πΉβ€˜π‘ƒ)))
8988fveq2d 6847 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ)) Β· (logβ€˜π‘ƒ))) = (expβ€˜(logβ€˜(πΉβ€˜π‘ƒ))))
9020reeflogd 25995 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(logβ€˜(πΉβ€˜π‘ƒ))) = (πΉβ€˜π‘ƒ))
9185, 89, 903eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ (𝑃↑𝑐((logβ€˜(πΉβ€˜π‘ƒ)) / (logβ€˜π‘ƒ))) = (πΉβ€˜π‘ƒ))
9280, 84, 913eqtr3d 2781 . . . . . . 7 (πœ‘ β†’ ((𝑃↑𝑐-1)↑𝑐𝑅) = (πΉβ€˜π‘ƒ))
9353, 72, 923eqtrrd 2778 . . . . . 6 (πœ‘ β†’ (πΉβ€˜π‘ƒ) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘ƒ))
94 fveq2 6843 . . . . . . 7 (𝑃 = 𝑝 β†’ (πΉβ€˜π‘ƒ) = (πΉβ€˜π‘))
95 fveq2 6843 . . . . . . 7 (𝑃 = 𝑝 β†’ ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘ƒ) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘))
9694, 95eqeq12d 2749 . . . . . 6 (𝑃 = 𝑝 β†’ ((πΉβ€˜π‘ƒ) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘ƒ) ↔ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘)))
9793, 96syl5ibcom 244 . . . . 5 (πœ‘ β†’ (𝑃 = 𝑝 β†’ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘)))
9897adantr 482 . . . 4 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑃 = 𝑝 β†’ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘)))
99 prmnn 16555 . . . . . . . . 9 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„•)
10099ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑝 ∈ β„•)
101 nnq 12892 . . . . . . . 8 (𝑝 ∈ β„• β†’ 𝑝 ∈ β„š)
102100, 101syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑝 ∈ β„š)
103 fveq2 6843 . . . . . . . . 9 (𝑦 = 𝑝 β†’ ((π½β€˜π‘ƒ)β€˜π‘¦) = ((π½β€˜π‘ƒ)β€˜π‘))
104103oveq1d 7373 . . . . . . . 8 (𝑦 = 𝑝 β†’ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅) = (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅))
105 ovex 7391 . . . . . . . 8 (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅) ∈ V
106104, 50, 105fvmpt 6949 . . . . . . 7 (𝑝 ∈ β„š β†’ ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘) = (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅))
107102, 106syl 17 . . . . . 6 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘) = (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅))
10873ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑅 ∈ β„‚)
1091081cxpd 26078 . . . . . . 7 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (1↑𝑐𝑅) = 1)
1103ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑃 ∈ β„™)
11145padicval 26981 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ 𝑝 ∈ β„š) β†’ ((π½β€˜π‘ƒ)β€˜π‘) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
112110, 102, 111syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ ((π½β€˜π‘ƒ)β€˜π‘) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))))
113100nnne0d 12208 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑝 β‰  0)
114113neneqd 2945 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ Β¬ 𝑝 = 0)
115114iffalsed 4498 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))) = (𝑃↑-(𝑃 pCnt 𝑝)))
116 pceq0 16748 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ β„™ ∧ 𝑝 ∈ β„•) β†’ ((𝑃 pCnt 𝑝) = 0 ↔ Β¬ 𝑃 βˆ₯ 𝑝))
1173, 99, 116syl2an 597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑃 pCnt 𝑝) = 0 ↔ Β¬ 𝑃 βˆ₯ 𝑝))
118 dvdsprm 16584 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (β„€β‰₯β€˜2) ∧ 𝑝 ∈ β„™) β†’ (𝑃 βˆ₯ 𝑝 ↔ 𝑃 = 𝑝))
1195, 118sylan 581 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑃 βˆ₯ 𝑝 ↔ 𝑃 = 𝑝))
120119necon3bbid 2978 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (Β¬ 𝑃 βˆ₯ 𝑝 ↔ 𝑃 β‰  𝑝))
121117, 120bitrd 279 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑃 pCnt 𝑝) = 0 ↔ 𝑃 β‰  𝑝))
122121biimpar 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (𝑃 pCnt 𝑝) = 0)
123122negeqd 11400 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ -(𝑃 pCnt 𝑝) = -0)
124 neg0 11452 . . . . . . . . . . . 12 -0 = 0
125123, 124eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ -(𝑃 pCnt 𝑝) = 0)
126125oveq2d 7374 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (𝑃↑-(𝑃 pCnt 𝑝)) = (𝑃↑0))
12758ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝑃 ∈ β„‚)
128127exp0d 14051 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (𝑃↑0) = 1)
129126, 128eqtrd 2773 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (𝑃↑-(𝑃 pCnt 𝑝)) = 1)
130112, 115, 1293eqtrd 2777 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ ((π½β€˜π‘ƒ)β€˜π‘) = 1)
131130oveq1d 7373 . . . . . . 7 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅) = (1↑𝑐𝑅))
132 2re 12232 . . . . . . . . . . . . 13 2 ∈ ℝ
133132a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 2 ∈ ℝ)
134 ostth3.6 . . . . . . . . . . . . . 14 𝑆 = if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ))
1352ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 𝐹 ∈ 𝐴)
13611, 13abvcl 20297 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ β„š) β†’ (πΉβ€˜π‘) ∈ ℝ)
137135, 102, 136syl2anc 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (πΉβ€˜π‘) ∈ ℝ)
13811, 13, 17abvgt0 20301 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ β„š ∧ 𝑝 β‰  0) β†’ 0 < (πΉβ€˜π‘))
139135, 102, 113, 138syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ 0 < (πΉβ€˜π‘))
140137, 139elrpd 12959 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (πΉβ€˜π‘) ∈ ℝ+)
141140adantrr 716 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (πΉβ€˜π‘) ∈ ℝ+)
14220ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (πΉβ€˜π‘ƒ) ∈ ℝ+)
143141, 142ifcld 4533 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) ∈ ℝ+)
144134, 143eqeltrid 2838 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑆 ∈ ℝ+)
145144rprecred 12973 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (1 / 𝑆) ∈ ℝ)
146 simprr 772 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (πΉβ€˜π‘) < 1)
14728ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (πΉβ€˜π‘ƒ) < 1)
148 breq1 5109 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘) = if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) β†’ ((πΉβ€˜π‘) < 1 ↔ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) < 1))
149 breq1 5109 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘ƒ) = if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) β†’ ((πΉβ€˜π‘ƒ) < 1 ↔ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) < 1))
150148, 149ifboth 4526 . . . . . . . . . . . . . . 15 (((πΉβ€˜π‘) < 1 ∧ (πΉβ€˜π‘ƒ) < 1) β†’ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) < 1)
151146, 147, 150syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)) < 1)
152134, 151eqbrtrid 5141 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑆 < 1)
153144reclt1d 12975 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (𝑆 < 1 ↔ 1 < (1 / 𝑆)))
154152, 153mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 1 < (1 / 𝑆))
155 expnbnd 14141 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (1 / 𝑆) ∈ ℝ ∧ 1 < (1 / 𝑆)) β†’ βˆƒπ‘˜ ∈ β„• 2 < ((1 / 𝑆)β†‘π‘˜))
156133, 145, 154, 155syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ βˆƒπ‘˜ ∈ β„• 2 < ((1 / 𝑆)β†‘π‘˜))
157144rpcnd 12964 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑆 ∈ β„‚)
158157adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 𝑆 ∈ β„‚)
159144rpne0d 12967 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑆 β‰  0)
160159adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 𝑆 β‰  0)
161 nnz 12525 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„€)
162161adantl 483 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„€)
163158, 160, 162exprecd 14065 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((1 / 𝑆)β†‘π‘˜) = (1 / (π‘†β†‘π‘˜)))
1642ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 𝐹 ∈ 𝐴)
165 ax-1ne0 11125 . . . . . . . . . . . . . . . . . 18 1 β‰  0
16612qrng1 26986 . . . . . . . . . . . . . . . . . . 19 1 = (1rβ€˜π‘„)
16711, 166, 17abv1z 20305 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ 𝐴 ∧ 1 β‰  0) β†’ (πΉβ€˜1) = 1)
168164, 165, 167sylancl 587 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜1) = 1)
1698ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑃 ∈ β„•)
170 nnnn0 12425 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
171 nnexpcl 13986 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (π‘ƒβ†‘π‘˜) ∈ β„•)
172169, 170, 171syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘ƒβ†‘π‘˜) ∈ β„•)
173172nnzd 12531 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘ƒβ†‘π‘˜) ∈ β„€)
17499ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑝 ∈ β„•)
175 nnexpcl 13986 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (π‘β†‘π‘˜) ∈ β„•)
176174, 170, 175syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘β†‘π‘˜) ∈ β„•)
177176nnzd 12531 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘β†‘π‘˜) ∈ β„€)
178 bezout 16429 . . . . . . . . . . . . . . . . . . 19 (((π‘ƒβ†‘π‘˜) ∈ β„€ ∧ (π‘β†‘π‘˜) ∈ β„€) β†’ βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)))
179173, 177, 178syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)))
180 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑃 β‰  𝑝)
1813ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑃 ∈ β„™)
182 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑝 ∈ β„™)
183 prmrp 16593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ β„™ ∧ 𝑝 ∈ β„™) β†’ ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 β‰  𝑝))
184181, 182, 183syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 β‰  𝑝))
185180, 184mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (𝑃 gcd 𝑝) = 1)
186185adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (𝑃 gcd 𝑝) = 1)
187169adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ β„•)
188174adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 𝑝 ∈ β„•)
189 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
190 rppwr 16445 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ β„• ∧ 𝑝 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ ((𝑃 gcd 𝑝) = 1 β†’ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = 1))
191187, 188, 189, 190syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((𝑃 gcd 𝑝) = 1 β†’ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = 1))
192186, 191mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = 1)
193192adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = 1)
194193eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) ↔ 1 = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))))
1952ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝐹 ∈ 𝐴)
196172adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (π‘ƒβ†‘π‘˜) ∈ β„•)
197 nnq 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘ƒβ†‘π‘˜) ∈ β„• β†’ (π‘ƒβ†‘π‘˜) ∈ β„š)
198196, 197syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (π‘ƒβ†‘π‘˜) ∈ β„š)
199 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ π‘Ž ∈ β„€)
200 zq 12884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘Ž ∈ β„€ β†’ π‘Ž ∈ β„š)
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ π‘Ž ∈ β„š)
202 qmulcl 12897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘ƒβ†‘π‘˜) ∈ β„š ∧ π‘Ž ∈ β„š) β†’ ((π‘ƒβ†‘π‘˜) Β· π‘Ž) ∈ β„š)
203198, 201, 202syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((π‘ƒβ†‘π‘˜) Β· π‘Ž) ∈ β„š)
204176adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (π‘β†‘π‘˜) ∈ β„•)
205 nnq 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘β†‘π‘˜) ∈ β„• β†’ (π‘β†‘π‘˜) ∈ β„š)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (π‘β†‘π‘˜) ∈ β„š)
207 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑏 ∈ β„€)
208 zq 12884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ β„€ β†’ 𝑏 ∈ β„š)
209207, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑏 ∈ β„š)
210 qmulcl 12897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘β†‘π‘˜) ∈ β„š ∧ 𝑏 ∈ β„š) β†’ ((π‘β†‘π‘˜) Β· 𝑏) ∈ β„š)
211206, 209, 210syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((π‘β†‘π‘˜) Β· 𝑏) ∈ β„š)
212 qaddcl 12895 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((π‘ƒβ†‘π‘˜) Β· π‘Ž) ∈ β„š ∧ ((π‘β†‘π‘˜) Β· 𝑏) ∈ β„š) β†’ (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) ∈ β„š)
213203, 211, 212syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) ∈ β„š)
21411, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ 𝐴 ∧ (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) ∈ β„š) β†’ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ∈ ℝ)
215195, 213, 214syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ∈ ℝ)
21611, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ 𝐴 ∧ ((π‘ƒβ†‘π‘˜) Β· π‘Ž) ∈ β„š) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) ∈ ℝ)
217195, 203, 216syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) ∈ ℝ)
21811, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ 𝐴 ∧ ((π‘β†‘π‘˜) Β· 𝑏) ∈ β„š) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) ∈ ℝ)
219195, 211, 218syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) ∈ ℝ)
220217, 219readdcld 11189 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) + (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏))) ∈ ℝ)
221 rpexpcl 13992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 ∈ ℝ+ ∧ π‘˜ ∈ β„€) β†’ (π‘†β†‘π‘˜) ∈ ℝ+)
222144, 161, 221syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘†β†‘π‘˜) ∈ ℝ+)
223222rpred 12962 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘†β†‘π‘˜) ∈ ℝ)
224223adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (π‘†β†‘π‘˜) ∈ ℝ)
225 remulcl 11141 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ ℝ ∧ (π‘†β†‘π‘˜) ∈ ℝ) β†’ (2 Β· (π‘†β†‘π‘˜)) ∈ ℝ)
226132, 224, 225sylancr 588 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (2 Β· (π‘†β†‘π‘˜)) ∈ ℝ)
227 qex 12891 . . . . . . . . . . . . . . . . . . . . . . . . . 26 β„š ∈ V
228 cnfldadd 20817 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 + = (+gβ€˜β„‚fld)
22912, 228ressplusg 17176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (β„š ∈ V β†’ + = (+gβ€˜π‘„))
230227, 229ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 + = (+gβ€˜π‘„)
23111, 13, 230abvtri 20303 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ 𝐴 ∧ ((π‘ƒβ†‘π‘˜) Β· π‘Ž) ∈ β„š ∧ ((π‘β†‘π‘˜) Β· 𝑏) ∈ β„š) β†’ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ≀ ((πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) + (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏))))
232195, 203, 211, 231syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ≀ ((πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) + (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏))))
233 cnfldmul 20818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Β· = (.rβ€˜β„‚fld)
23412, 233ressmulr 17193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (β„š ∈ V β†’ Β· = (.rβ€˜π‘„))
235227, 234ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Β· = (.rβ€˜π‘„)
23611, 13, 235abvmul 20302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 ∈ 𝐴 ∧ (π‘ƒβ†‘π‘˜) ∈ β„š ∧ π‘Ž ∈ β„š) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) = ((πΉβ€˜(π‘ƒβ†‘π‘˜)) Β· (πΉβ€˜π‘Ž)))
237195, 198, 201, 236syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) = ((πΉβ€˜(π‘ƒβ†‘π‘˜)) Β· (πΉβ€˜π‘Ž)))
23810ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑃 ∈ β„š)
239170ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ π‘˜ ∈ β„•0)
24012, 11qabvexp 26990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ β„š ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(π‘ƒβ†‘π‘˜)) = ((πΉβ€˜π‘ƒ)β†‘π‘˜))
241195, 238, 239, 240syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜(π‘ƒβ†‘π‘˜)) = ((πΉβ€˜π‘ƒ)β†‘π‘˜))
242241oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜(π‘ƒβ†‘π‘˜)) Β· (πΉβ€˜π‘Ž)) = (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)))
243237, 242eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) = (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)))
244195, 238, 14syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘ƒ) ∈ ℝ)
245244, 239reexpcld 14074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘ƒ)β†‘π‘˜) ∈ ℝ)
24611, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 ∈ 𝐴 ∧ π‘Ž ∈ β„š) β†’ (πΉβ€˜π‘Ž) ∈ ℝ)
247195, 201, 246syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘Ž) ∈ ℝ)
248245, 247remulcld 11190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ∈ ℝ)
249 elz 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (π‘Ž ∈ β„€ ↔ (π‘Ž ∈ ℝ ∧ (π‘Ž = 0 ∨ π‘Ž ∈ β„• ∨ -π‘Ž ∈ β„•)))
250249simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (π‘Ž ∈ β„€ β†’ (π‘Ž = 0 ∨ π‘Ž ∈ β„• ∨ -π‘Ž ∈ β„•))
251250adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (π‘Ž = 0 ∨ π‘Ž ∈ β„• ∨ -π‘Ž ∈ β„•))
25211, 17abv0 20304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐹 ∈ 𝐴 β†’ (πΉβ€˜0) = 0)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πœ‘ β†’ (πΉβ€˜0) = 0)
254 0le1 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ≀ 1
255253, 254eqbrtrdi 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (πœ‘ β†’ (πΉβ€˜0) ≀ 1)
256255adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (πΉβ€˜0) ≀ 1)
257 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (π‘Ž = 0 β†’ (πΉβ€˜π‘Ž) = (πΉβ€˜0))
258257breq1d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (π‘Ž = 0 β†’ ((πΉβ€˜π‘Ž) ≀ 1 ↔ (πΉβ€˜0) ≀ 1))
259256, 258syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (π‘Ž = 0 β†’ (πΉβ€˜π‘Ž) ≀ 1))
260 ostth3.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πœ‘ β†’ βˆ€π‘› ∈ β„• Β¬ 1 < (πΉβ€˜π‘›))
261 nnq 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„š)
26211, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ β„š) β†’ (πΉβ€˜π‘›) ∈ ℝ)
2632, 261, 262syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ ℝ)
264 1re 11160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 ∈ ℝ
265 lenlt 11238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((πΉβ€˜π‘›) ∈ ℝ ∧ 1 ∈ ℝ) β†’ ((πΉβ€˜π‘›) ≀ 1 ↔ Β¬ 1 < (πΉβ€˜π‘›)))
266263, 264, 265sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΉβ€˜π‘›) ≀ 1 ↔ Β¬ 1 < (πΉβ€˜π‘›)))
267266ralbidva 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πœ‘ β†’ (βˆ€π‘› ∈ β„• (πΉβ€˜π‘›) ≀ 1 ↔ βˆ€π‘› ∈ β„• Β¬ 1 < (πΉβ€˜π‘›)))
268260, 267mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (πœ‘ β†’ βˆ€π‘› ∈ β„• (πΉβ€˜π‘›) ≀ 1)
269 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = π‘Ž β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘Ž))
270269breq1d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = π‘Ž β†’ ((πΉβ€˜π‘›) ≀ 1 ↔ (πΉβ€˜π‘Ž) ≀ 1))
271270rspccv 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (βˆ€π‘› ∈ β„• (πΉβ€˜π‘›) ≀ 1 β†’ (π‘Ž ∈ β„• β†’ (πΉβ€˜π‘Ž) ≀ 1))
272268, 271syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (πœ‘ β†’ (π‘Ž ∈ β„• β†’ (πΉβ€˜π‘Ž) ≀ 1))
273272adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (π‘Ž ∈ β„• β†’ (πΉβ€˜π‘Ž) ≀ 1))
2742adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ 𝐹 ∈ 𝐴)
275200ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ π‘Ž ∈ β„š)
276 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (invgβ€˜π‘„) = (invgβ€˜π‘„)
27711, 13, 276abvneg 20307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹 ∈ 𝐴 ∧ π‘Ž ∈ β„š) β†’ (πΉβ€˜((invgβ€˜π‘„)β€˜π‘Ž)) = (πΉβ€˜π‘Ž))
278274, 275, 277syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ (πΉβ€˜((invgβ€˜π‘„)β€˜π‘Ž)) = (πΉβ€˜π‘Ž))
279 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑛 = ((invgβ€˜π‘„)β€˜π‘Ž) β†’ (πΉβ€˜π‘›) = (πΉβ€˜((invgβ€˜π‘„)β€˜π‘Ž)))
280279breq1d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑛 = ((invgβ€˜π‘„)β€˜π‘Ž) β†’ ((πΉβ€˜π‘›) ≀ 1 ↔ (πΉβ€˜((invgβ€˜π‘„)β€˜π‘Ž)) ≀ 1))
281268adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ βˆ€π‘› ∈ β„• (πΉβ€˜π‘›) ≀ 1)
28212qrngneg 26987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (π‘Ž ∈ β„š β†’ ((invgβ€˜π‘„)β€˜π‘Ž) = -π‘Ž)
283275, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ ((invgβ€˜π‘„)β€˜π‘Ž) = -π‘Ž)
284 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ -π‘Ž ∈ β„•)
285283, 284eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ ((invgβ€˜π‘„)β€˜π‘Ž) ∈ β„•)
286280, 281, 285rspcdva 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ (πΉβ€˜((invgβ€˜π‘„)β€˜π‘Ž)) ≀ 1)
287278, 286eqbrtrrd 5130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ (π‘Ž ∈ β„€ ∧ -π‘Ž ∈ β„•)) β†’ (πΉβ€˜π‘Ž) ≀ 1)
288287expr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (-π‘Ž ∈ β„• β†’ (πΉβ€˜π‘Ž) ≀ 1))
289259, 273, 2883jaod 1429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ ((π‘Ž = 0 ∨ π‘Ž ∈ β„• ∨ -π‘Ž ∈ β„•) β†’ (πΉβ€˜π‘Ž) ≀ 1))
290251, 289mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ π‘Ž ∈ β„€) β†’ (πΉβ€˜π‘Ž) ≀ 1)
291290ralrimiva 3140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ βˆ€π‘Ž ∈ β„€ (πΉβ€˜π‘Ž) ≀ 1)
292291ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ βˆ€π‘Ž ∈ β„€ (πΉβ€˜π‘Ž) ≀ 1)
293 rsp 3229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘Ž ∈ β„€ (πΉβ€˜π‘Ž) ≀ 1 β†’ (π‘Ž ∈ β„€ β†’ (πΉβ€˜π‘Ž) ≀ 1))
294292, 199, 293sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘Ž) ≀ 1)
295264a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 1 ∈ ℝ)
296161ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ π‘˜ ∈ β„€)
29719ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 < (πΉβ€˜π‘ƒ))
298 expgt0 14007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πΉβ€˜π‘ƒ) ∈ ℝ ∧ π‘˜ ∈ β„€ ∧ 0 < (πΉβ€˜π‘ƒ)) β†’ 0 < ((πΉβ€˜π‘ƒ)β†‘π‘˜))
299244, 296, 297, 298syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 < ((πΉβ€˜π‘ƒ)β†‘π‘˜))
300 lemul2 12013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πΉβ€˜π‘Ž) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((πΉβ€˜π‘ƒ)β†‘π‘˜) ∈ ℝ ∧ 0 < ((πΉβ€˜π‘ƒ)β†‘π‘˜))) β†’ ((πΉβ€˜π‘Ž) ≀ 1 ↔ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ≀ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· 1)))
301247, 295, 245, 299, 300syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘Ž) ≀ 1 ↔ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ≀ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· 1)))
302294, 301mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ≀ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· 1))
303245recnd 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘ƒ)β†‘π‘˜) ∈ β„‚)
304303mulid1d 11177 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· 1) = ((πΉβ€˜π‘ƒ)β†‘π‘˜))
305302, 304breqtrd 5132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ≀ ((πΉβ€˜π‘ƒ)β†‘π‘˜))
306144rpred 12962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ 𝑆 ∈ ℝ)
307306adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑆 ∈ ℝ)
308142adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘ƒ) ∈ ℝ+)
309308rpge0d 12966 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 ≀ (πΉβ€˜π‘ƒ))
310174adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑝 ∈ β„•)
311310, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑝 ∈ β„š)
312195, 311, 136syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ∈ ℝ)
313 max1 13110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πΉβ€˜π‘ƒ) ∈ ℝ ∧ (πΉβ€˜π‘) ∈ ℝ) β†’ (πΉβ€˜π‘ƒ) ≀ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)))
314244, 312, 313syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘ƒ) ≀ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)))
315314, 134breqtrrdi 5148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘ƒ) ≀ 𝑆)
316 leexp1a 14086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πΉβ€˜π‘ƒ) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ π‘˜ ∈ β„•0) ∧ (0 ≀ (πΉβ€˜π‘ƒ) ∧ (πΉβ€˜π‘ƒ) ≀ 𝑆)) β†’ ((πΉβ€˜π‘ƒ)β†‘π‘˜) ≀ (π‘†β†‘π‘˜))
317244, 307, 239, 309, 315, 316syl32anc 1379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘ƒ)β†‘π‘˜) ≀ (π‘†β†‘π‘˜))
318248, 245, 224, 305, 317letrd 11317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘ƒ)β†‘π‘˜) Β· (πΉβ€˜π‘Ž)) ≀ (π‘†β†‘π‘˜))
319243, 318eqbrtrd 5128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) ≀ (π‘†β†‘π‘˜))
32011, 13, 235abvmul 20302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹 ∈ 𝐴 ∧ (π‘β†‘π‘˜) ∈ β„š ∧ 𝑏 ∈ β„š) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) = ((πΉβ€˜(π‘β†‘π‘˜)) Β· (πΉβ€˜π‘)))
321195, 206, 209, 320syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) = ((πΉβ€˜(π‘β†‘π‘˜)) Β· (πΉβ€˜π‘)))
32212, 11qabvexp 26990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ β„š ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(π‘β†‘π‘˜)) = ((πΉβ€˜π‘)β†‘π‘˜))
323195, 311, 239, 322syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜(π‘β†‘π‘˜)) = ((πΉβ€˜π‘)β†‘π‘˜))
324323oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜(π‘β†‘π‘˜)) Β· (πΉβ€˜π‘)) = (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)))
325321, 324eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) = (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)))
326312, 239reexpcld 14074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘)β†‘π‘˜) ∈ ℝ)
32711, 13abvcl 20297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 ∈ 𝐴 ∧ 𝑏 ∈ β„š) β†’ (πΉβ€˜π‘) ∈ ℝ)
328195, 209, 327syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ∈ ℝ)
329326, 328remulcld 11190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ∈ ℝ)
330 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ž = 𝑏 β†’ (πΉβ€˜π‘Ž) = (πΉβ€˜π‘))
331330breq1d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘Ž = 𝑏 β†’ ((πΉβ€˜π‘Ž) ≀ 1 ↔ (πΉβ€˜π‘) ≀ 1))
332331, 292, 207rspcdva 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ≀ 1)
333310nnne0d 12208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 𝑝 β‰  0)
334195, 311, 333, 138syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 < (πΉβ€˜π‘))
335 expgt0 14007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πΉβ€˜π‘) ∈ ℝ ∧ π‘˜ ∈ β„€ ∧ 0 < (πΉβ€˜π‘)) β†’ 0 < ((πΉβ€˜π‘)β†‘π‘˜))
336312, 296, 334, 335syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 < ((πΉβ€˜π‘)β†‘π‘˜))
337 lemul2 12013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πΉβ€˜π‘) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((πΉβ€˜π‘)β†‘π‘˜) ∈ ℝ ∧ 0 < ((πΉβ€˜π‘)β†‘π‘˜))) β†’ ((πΉβ€˜π‘) ≀ 1 ↔ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ≀ (((πΉβ€˜π‘)β†‘π‘˜) Β· 1)))
338328, 295, 326, 336, 337syl112anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘) ≀ 1 ↔ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ≀ (((πΉβ€˜π‘)β†‘π‘˜) Β· 1)))
339332, 338mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ≀ (((πΉβ€˜π‘)β†‘π‘˜) Β· 1))
340326recnd 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘)β†‘π‘˜) ∈ β„‚)
341340mulid1d 11177 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘)β†‘π‘˜) Β· 1) = ((πΉβ€˜π‘)β†‘π‘˜))
342339, 341breqtrd 5132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ≀ ((πΉβ€˜π‘)β†‘π‘˜))
343141adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ∈ ℝ+)
344343rpge0d 12966 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ 0 ≀ (πΉβ€˜π‘))
345 max2 13112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πΉβ€˜π‘ƒ) ∈ ℝ ∧ (πΉβ€˜π‘) ∈ ℝ) β†’ (πΉβ€˜π‘) ≀ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)))
346244, 312, 345syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ≀ if((πΉβ€˜π‘ƒ) ≀ (πΉβ€˜π‘), (πΉβ€˜π‘), (πΉβ€˜π‘ƒ)))
347346, 134breqtrrdi 5148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜π‘) ≀ 𝑆)
348 leexp1a 14086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πΉβ€˜π‘) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ π‘˜ ∈ β„•0) ∧ (0 ≀ (πΉβ€˜π‘) ∧ (πΉβ€˜π‘) ≀ 𝑆)) β†’ ((πΉβ€˜π‘)β†‘π‘˜) ≀ (π‘†β†‘π‘˜))
349312, 307, 239, 344, 347, 348syl32anc 1379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜π‘)β†‘π‘˜) ≀ (π‘†β†‘π‘˜))
350329, 326, 224, 342, 349letrd 11317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((πΉβ€˜π‘)β†‘π‘˜) Β· (πΉβ€˜π‘)) ≀ (π‘†β†‘π‘˜))
351325, 350eqbrtrd 5128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏)) ≀ (π‘†β†‘π‘˜))
352217, 219, 224, 224, 319, 351le2addd 11779 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) + (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏))) ≀ ((π‘†β†‘π‘˜) + (π‘†β†‘π‘˜)))
353222rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (π‘†β†‘π‘˜) ∈ β„‚)
3543532timesd 12401 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘†β†‘π‘˜)) = ((π‘†β†‘π‘˜) + (π‘†β†‘π‘˜)))
355354adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (2 Β· (π‘†β†‘π‘˜)) = ((π‘†β†‘π‘˜) + (π‘†β†‘π‘˜)))
356352, 355breqtrrd 5134 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ ((πΉβ€˜((π‘ƒβ†‘π‘˜) Β· π‘Ž)) + (πΉβ€˜((π‘β†‘π‘˜) Β· 𝑏))) ≀ (2 Β· (π‘†β†‘π‘˜)))
357215, 220, 226, 232, 356letrd 11317 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ≀ (2 Β· (π‘†β†‘π‘˜)))
358 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . 23 (1 = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ (πΉβ€˜1) = (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))))
359358breq1d 5116 . . . . . . . . . . . . . . . . . . . . . 22 (1 = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ ((πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜)) ↔ (πΉβ€˜(((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏))) ≀ (2 Β· (π‘†β†‘π‘˜))))
360357, 359syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (1 = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ (πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜))))
361194, 360sylbid 239 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ (π‘˜ ∈ β„• ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€))) β†’ (((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ (πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜))))
362361anassrs 469 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ (((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ (πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜))))
363362rexlimdvva 3202 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ ((π‘ƒβ†‘π‘˜) gcd (π‘β†‘π‘˜)) = (((π‘ƒβ†‘π‘˜) Β· π‘Ž) + ((π‘β†‘π‘˜) Β· 𝑏)) β†’ (πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜))))
364179, 363mpd 15 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜1) ≀ (2 Β· (π‘†β†‘π‘˜)))
365168, 364eqbrtrrd 5130 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ 1 ≀ (2 Β· (π‘†β†‘π‘˜)))
366222rpregt0d 12968 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((π‘†β†‘π‘˜) ∈ ℝ ∧ 0 < (π‘†β†‘π‘˜)))
367 ledivmul2 12039 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ((π‘†β†‘π‘˜) ∈ ℝ ∧ 0 < (π‘†β†‘π‘˜))) β†’ ((1 / (π‘†β†‘π‘˜)) ≀ 2 ↔ 1 ≀ (2 Β· (π‘†β†‘π‘˜))))
368264, 132, 366, 367mp3an12i 1466 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((1 / (π‘†β†‘π‘˜)) ≀ 2 ↔ 1 ≀ (2 Β· (π‘†β†‘π‘˜))))
369365, 368mpbird 257 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘†β†‘π‘˜)) ≀ 2)
370163, 369eqbrtrd 5128 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((1 / 𝑆)β†‘π‘˜) ≀ 2)
371 reexpcl 13990 . . . . . . . . . . . . . . . 16 (((1 / 𝑆) ∈ ℝ ∧ π‘˜ ∈ β„•0) β†’ ((1 / 𝑆)β†‘π‘˜) ∈ ℝ)
372145, 170, 371syl2an 597 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ ((1 / 𝑆)β†‘π‘˜) ∈ ℝ)
373 lenlt 11238 . . . . . . . . . . . . . . 15 ((((1 / 𝑆)β†‘π‘˜) ∈ ℝ ∧ 2 ∈ ℝ) β†’ (((1 / 𝑆)β†‘π‘˜) ≀ 2 ↔ Β¬ 2 < ((1 / 𝑆)β†‘π‘˜)))
374372, 132, 373sylancl 587 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (((1 / 𝑆)β†‘π‘˜) ≀ 2 ↔ Β¬ 2 < ((1 / 𝑆)β†‘π‘˜)))
375370, 374mpbid 231 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ Β¬ 2 < ((1 / 𝑆)β†‘π‘˜))
376375pm2.21d 121 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) ∧ π‘˜ ∈ β„•) β†’ (2 < ((1 / 𝑆)β†‘π‘˜) β†’ Β¬ (πΉβ€˜π‘) < 1))
377376rexlimdva 3149 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ (βˆƒπ‘˜ ∈ β„• 2 < ((1 / 𝑆)β†‘π‘˜) β†’ Β¬ (πΉβ€˜π‘) < 1))
378156, 377mpd 15 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑃 β‰  𝑝 ∧ (πΉβ€˜π‘) < 1)) β†’ Β¬ (πΉβ€˜π‘) < 1)
379378expr 458 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ ((πΉβ€˜π‘) < 1 β†’ Β¬ (πΉβ€˜π‘) < 1))
380379pm2.01d 189 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ Β¬ (πΉβ€˜π‘) < 1)
381 fveq2 6843 . . . . . . . . . . 11 (𝑛 = 𝑝 β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘))
382381breq2d 5118 . . . . . . . . . 10 (𝑛 = 𝑝 β†’ (1 < (πΉβ€˜π‘›) ↔ 1 < (πΉβ€˜π‘)))
383382notbid 318 . . . . . . . . 9 (𝑛 = 𝑝 β†’ (Β¬ 1 < (πΉβ€˜π‘›) ↔ Β¬ 1 < (πΉβ€˜π‘)))
384260ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ βˆ€π‘› ∈ β„• Β¬ 1 < (πΉβ€˜π‘›))
385383, 384, 100rspcdva 3581 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ Β¬ 1 < (πΉβ€˜π‘))
386 lttri3 11243 . . . . . . . . 9 (((πΉβ€˜π‘) ∈ ℝ ∧ 1 ∈ ℝ) β†’ ((πΉβ€˜π‘) = 1 ↔ (Β¬ (πΉβ€˜π‘) < 1 ∧ Β¬ 1 < (πΉβ€˜π‘))))
387137, 264, 386sylancl 587 . . . . . . . 8 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ ((πΉβ€˜π‘) = 1 ↔ (Β¬ (πΉβ€˜π‘) < 1 ∧ Β¬ 1 < (πΉβ€˜π‘))))
388380, 385, 387mpbir2and 712 . . . . . . 7 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (πΉβ€˜π‘) = 1)
389109, 131, 3883eqtr4d 2783 . . . . . 6 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (((π½β€˜π‘ƒ)β€˜π‘)↑𝑐𝑅) = (πΉβ€˜π‘))
390107, 389eqtr2d 2774 . . . . 5 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ 𝑃 β‰  𝑝) β†’ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘))
391390ex 414 . . . 4 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑃 β‰  𝑝 β†’ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘)))
39298, 391pm2.61dne 3028 . . 3 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (πΉβ€˜π‘) = ((𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))β€˜π‘))
39312, 11, 2, 47, 392ostthlem2 26992 . 2 (πœ‘ β†’ 𝐹 = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅)))
394 oveq2 7366 . . . 4 (π‘Ž = 𝑅 β†’ (((π½β€˜π‘ƒ)β€˜π‘¦)β†‘π‘π‘Ž) = (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))
395394mpteq2dv 5208 . . 3 (π‘Ž = 𝑅 β†’ (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)β†‘π‘π‘Ž)) = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅)))
396395rspceeqv 3596 . 2 ((𝑅 ∈ ℝ+ ∧ 𝐹 = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)↑𝑐𝑅))) β†’ βˆƒπ‘Ž ∈ ℝ+ 𝐹 = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)β†‘π‘π‘Ž)))
39744, 393, 396syl2anc 585 1 (πœ‘ β†’ βˆƒπ‘Ž ∈ ℝ+ 𝐹 = (𝑦 ∈ β„š ↦ (((π½β€˜π‘ƒ)β€˜π‘¦)β†‘π‘π‘Ž)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444  ifcif 4487   class class class wbr 5106   ↦ cmpt 5189  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   < clt 11194   ≀ cle 11195  -cneg 11391   / cdiv 11817  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„šcq 12878  β„+crp 12920  β†‘cexp 13973  expce 15949   βˆ₯ cdvds 16141   gcd cgcd 16379  β„™cprime 16552   pCnt cpc 16713   β†Ύs cress 17117  +gcplusg 17138  .rcmulr 17139  invgcminusg 18754  AbsValcabv 20289  β„‚fldccnfld 20812  logclog 25926  β†‘𝑐ccxp 25927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-sin 15957  df-cos 15958  df-pi 15960  df-dvds 16142  df-gcd 16380  df-prm 16553  df-pc 16714  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-grp 18756  df-minusg 18757  df-mulg 18878  df-subg 18930  df-cntz 19102  df-cmn 19569  df-mgp 19902  df-ur 19919  df-ring 19971  df-cring 19972  df-oppr 20054  df-dvdsr 20075  df-unit 20076  df-invr 20106  df-dvr 20117  df-drng 20199  df-subrg 20234  df-abv 20290  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-cxp 25929
This theorem is referenced by:  ostth  27003
  Copyright terms: Public domain W3C validator