Step | Hyp | Ref
| Expression |
1 | | ostth3.5 |
. . . 4
⊢ 𝑅 = -((log‘(𝐹‘𝑃)) / (log‘𝑃)) |
2 | | ostth.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
3 | | ostth3.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
4 | | prmuz2 16149 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
6 | | eluz2b2 12415 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
7 | 5, 6 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
8 | 7 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | | nnq 12456 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℚ) |
11 | | qabsabv.a |
. . . . . . . . . 10
⊢ 𝐴 = (AbsVal‘𝑄) |
12 | | qrng.q |
. . . . . . . . . . 11
⊢ 𝑄 = (ℂfld
↾s ℚ) |
13 | 12 | qrngbas 26367 |
. . . . . . . . . 10
⊢ ℚ =
(Base‘𝑄) |
14 | 11, 13 | abvcl 19726 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ) → (𝐹‘𝑃) ∈ ℝ) |
15 | 2, 10, 14 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑃) ∈ ℝ) |
16 | 8 | nnne0d 11778 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ≠ 0) |
17 | 12 | qrng0 26369 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑄) |
18 | 11, 13, 17 | abvgt0 19730 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0) → 0 < (𝐹‘𝑃)) |
19 | 2, 10, 16, 18 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝐹‘𝑃)) |
20 | 15, 19 | elrpd 12523 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑃) ∈
ℝ+) |
21 | 20 | relogcld 25378 |
. . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑃)) ∈ ℝ) |
22 | 8 | nnred 11743 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℝ) |
23 | 7 | simprd 499 |
. . . . . . 7
⊢ (𝜑 → 1 < 𝑃) |
24 | 22, 23 | rplogcld 25384 |
. . . . . 6
⊢ (𝜑 → (log‘𝑃) ∈
ℝ+) |
25 | 21, 24 | rerpdivcld 12557 |
. . . . 5
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℝ) |
26 | 25 | renegcld 11157 |
. . . 4
⊢ (𝜑 → -((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℝ) |
27 | 1, 26 | eqeltrid 2838 |
. . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) |
28 | | ostth3.4 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) < 1) |
29 | | 1rp 12488 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
30 | | logltb 25355 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑃) ∈ ℝ+ ∧ 1 ∈
ℝ+) → ((𝐹‘𝑃) < 1 ↔ (log‘(𝐹‘𝑃)) < (log‘1))) |
31 | 20, 29, 30 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑃) < 1 ↔ (log‘(𝐹‘𝑃)) < (log‘1))) |
32 | 28, 31 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < (log‘1)) |
33 | | log1 25341 |
. . . . . . . 8
⊢
(log‘1) = 0 |
34 | 32, 33 | breqtrdi 5081 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < 0) |
35 | 24 | rpcnd 12528 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑃) ∈
ℂ) |
36 | 35 | mul01d 10929 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝑃) · 0) =
0) |
37 | 34, 36 | breqtrrd 5068 |
. . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < ((log‘𝑃) · 0)) |
38 | | 0red 10734 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
39 | 21, 38, 24 | ltdivmuld 12577 |
. . . . . 6
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0 ↔ (log‘(𝐹‘𝑃)) < ((log‘𝑃) · 0))) |
40 | 37, 39 | mpbird 260 |
. . . . 5
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0) |
41 | 25 | lt0neg1d 11299 |
. . . . 5
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0 ↔ 0 < -((log‘(𝐹‘𝑃)) / (log‘𝑃)))) |
42 | 40, 41 | mpbid 235 |
. . . 4
⊢ (𝜑 → 0 < -((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
43 | 42, 1 | breqtrrdi 5082 |
. . 3
⊢ (𝜑 → 0 < 𝑅) |
44 | 27, 43 | elrpd 12523 |
. 2
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
45 | | padic.j |
. . . . 5
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) |
46 | 12, 11, 45 | padicabvcxp 26380 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |
47 | 3, 44, 46 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |
48 | | fveq2 6686 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑃 → ((𝐽‘𝑃)‘𝑦) = ((𝐽‘𝑃)‘𝑃)) |
49 | 48 | oveq1d 7197 |
. . . . . . . . 9
⊢ (𝑦 = 𝑃 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
50 | | eqid 2739 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) |
51 | | ovex 7215 |
. . . . . . . . 9
⊢ (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅) ∈ V |
52 | 49, 50, 51 | fvmpt 6787 |
. . . . . . . 8
⊢ (𝑃 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
53 | 10, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
54 | 45 | padicval 26365 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ ℚ) → ((𝐽‘𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃)))) |
55 | 3, 10, 54 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐽‘𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃)))) |
56 | 16 | neneqd 2940 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑃 = 0) |
57 | 56 | iffalsed 4435 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))) = (𝑃↑-(𝑃 pCnt 𝑃))) |
58 | 8 | nncnd 11744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℂ) |
59 | 58 | exp1d 13609 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃↑1) = 𝑃) |
60 | 59 | oveq2d 7198 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃)) |
61 | | 1z 12105 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
62 | | pcid 16321 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 1 ∈
ℤ) → (𝑃 pCnt
(𝑃↑1)) =
1) |
63 | 3, 61, 62 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = 1) |
64 | 60, 63 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝑃) = 1) |
65 | 64 | negeqd 10970 |
. . . . . . . . . . 11
⊢ (𝜑 → -(𝑃 pCnt 𝑃) = -1) |
66 | 65 | oveq2d 7198 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑-1)) |
67 | | neg1z 12111 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → -1 ∈
ℤ) |
69 | 58, 16, 68 | cxpexpzd 25466 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑𝑐-1) = (𝑃↑-1)) |
70 | 66, 69 | eqtr4d 2777 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑𝑐-1)) |
71 | 55, 57, 70 | 3eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → ((𝐽‘𝑃)‘𝑃) = (𝑃↑𝑐-1)) |
72 | 71 | oveq1d 7197 |
. . . . . . 7
⊢ (𝜑 → (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅) = ((𝑃↑𝑐-1)↑𝑐𝑅)) |
73 | 27 | recnd 10759 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
74 | 73 | mulm1d 11182 |
. . . . . . . . . 10
⊢ (𝜑 → (-1 · 𝑅) = -𝑅) |
75 | 1 | negeqi 10969 |
. . . . . . . . . . 11
⊢ -𝑅 = --((log‘(𝐹‘𝑃)) / (log‘𝑃)) |
76 | 25 | recnd 10759 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℂ) |
77 | 76 | negnegd 11078 |
. . . . . . . . . . 11
⊢ (𝜑 → --((log‘(𝐹‘𝑃)) / (log‘𝑃)) = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
78 | 75, 77 | syl5eq 2786 |
. . . . . . . . . 10
⊢ (𝜑 → -𝑅 = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
79 | 74, 78 | eqtrd 2774 |
. . . . . . . . 9
⊢ (𝜑 → (-1 · 𝑅) = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
80 | 79 | oveq2d 7198 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐(-1 · 𝑅)) = (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃)))) |
81 | 8 | nnrpd 12524 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
82 | | neg1rr 11843 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℝ) |
84 | 81, 83, 73 | cxpmuld 25491 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐(-1 · 𝑅)) = ((𝑃↑𝑐-1)↑𝑐𝑅)) |
85 | 58, 16, 76 | cxpefd 25467 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃))) = (exp‘(((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃)))) |
86 | 21 | recnd 10759 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐹‘𝑃)) ∈ ℂ) |
87 | 24 | rpne0d 12531 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑃) ≠ 0) |
88 | 86, 35, 87 | divcan1d 11507 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃)) = (log‘(𝐹‘𝑃))) |
89 | 88 | fveq2d 6690 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃))) = (exp‘(log‘(𝐹‘𝑃)))) |
90 | 20 | reeflogd 25379 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(log‘(𝐹‘𝑃))) = (𝐹‘𝑃)) |
91 | 85, 89, 90 | 3eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃))) = (𝐹‘𝑃)) |
92 | 80, 84, 91 | 3eqtr3d 2782 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑐-1)↑𝑐𝑅) = (𝐹‘𝑃)) |
93 | 53, 72, 92 | 3eqtrrd 2779 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃)) |
94 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑃 = 𝑝 → (𝐹‘𝑃) = (𝐹‘𝑝)) |
95 | | fveq2 6686 |
. . . . . . 7
⊢ (𝑃 = 𝑝 → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
96 | 94, 95 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑃 = 𝑝 → ((𝐹‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) ↔ (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
97 | 93, 96 | syl5ibcom 248 |
. . . . 5
⊢ (𝜑 → (𝑃 = 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
98 | 97 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 = 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
99 | | prmnn 16127 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
100 | 99 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ∈ ℕ) |
101 | | nnq 12456 |
. . . . . . . 8
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℚ) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ∈ ℚ) |
103 | | fveq2 6686 |
. . . . . . . . 9
⊢ (𝑦 = 𝑝 → ((𝐽‘𝑃)‘𝑦) = ((𝐽‘𝑃)‘𝑝)) |
104 | 103 | oveq1d 7197 |
. . . . . . . 8
⊢ (𝑦 = 𝑝 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
105 | | ovex 7215 |
. . . . . . . 8
⊢ (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) ∈ V |
106 | 104, 50, 105 | fvmpt 6787 |
. . . . . . 7
⊢ (𝑝 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
107 | 102, 106 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
108 | 73 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑅 ∈ ℂ) |
109 | 108 | 1cxpd 25462 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (1↑𝑐𝑅) = 1) |
110 | 3 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑃 ∈ ℙ) |
111 | 45 | padicval 26365 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℚ) → ((𝐽‘𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝)))) |
112 | 110, 102,
111 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐽‘𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝)))) |
113 | 100 | nnne0d 11778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ≠ 0) |
114 | 113 | neneqd 2940 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ 𝑝 = 0) |
115 | 114 | iffalsed 4435 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))) = (𝑃↑-(𝑃 pCnt 𝑝))) |
116 | | pceq0 16319 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℕ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃 ∥ 𝑝)) |
117 | 3, 99, 116 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃 ∥ 𝑝)) |
118 | | dvdsprm 16156 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑝 ∈ ℙ) → (𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝)) |
119 | 5, 118 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝)) |
120 | 119 | necon3bbid 2972 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑃 ∥ 𝑝 ↔ 𝑃 ≠ 𝑝)) |
121 | 117, 120 | bitrd 282 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ 𝑃 ≠ 𝑝)) |
122 | 121 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃 pCnt 𝑝) = 0) |
123 | 122 | negeqd 10970 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → -(𝑃 pCnt 𝑝) = -0) |
124 | | neg0 11022 |
. . . . . . . . . . . 12
⊢ -0 =
0 |
125 | 123, 124 | eqtrdi 2790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → -(𝑃 pCnt 𝑝) = 0) |
126 | 125 | oveq2d 7198 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = (𝑃↑0)) |
127 | 58 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑃 ∈ ℂ) |
128 | 127 | exp0d 13608 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑0) = 1) |
129 | 126, 128 | eqtrd 2774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = 1) |
130 | 112, 115,
129 | 3eqtrd 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐽‘𝑃)‘𝑝) = 1) |
131 | 130 | oveq1d 7197 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) = (1↑𝑐𝑅)) |
132 | | 2re 11802 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
133 | 132 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 2 ∈
ℝ) |
134 | | ostth3.6 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) |
135 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝐹 ∈ 𝐴) |
136 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) ∈ ℝ) |
137 | 135, 102,
136 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) ∈ ℝ) |
138 | 11, 13, 17 | abvgt0 19730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑝 ≠ 0) → 0 < (𝐹‘𝑝)) |
139 | 135, 102,
113, 138 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 0 < (𝐹‘𝑝)) |
140 | 137, 139 | elrpd 12523 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) ∈
ℝ+) |
141 | 140 | adantrr 717 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑝) ∈
ℝ+) |
142 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑃) ∈
ℝ+) |
143 | 141, 142 | ifcld 4470 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) ∈
ℝ+) |
144 | 134, 143 | eqeltrid 2838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈
ℝ+) |
145 | 144 | rprecred 12537 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (1 / 𝑆) ∈ ℝ) |
146 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑝) < 1) |
147 | 28 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑃) < 1) |
148 | | breq1 5043 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑝) = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) → ((𝐹‘𝑝) < 1 ↔ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1)) |
149 | | breq1 5043 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑃) = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) → ((𝐹‘𝑃) < 1 ↔ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1)) |
150 | 148, 149 | ifboth 4463 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑝) < 1 ∧ (𝐹‘𝑃) < 1) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1) |
151 | 146, 147,
150 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1) |
152 | 134, 151 | eqbrtrid 5075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 < 1) |
153 | 144 | reclt1d 12539 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝑆 < 1 ↔ 1 < (1 / 𝑆))) |
154 | 152, 153 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 1 < (1 / 𝑆)) |
155 | | expnbnd 13697 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (1 / 𝑆) ∈ ℝ ∧ 1 < (1 / 𝑆)) → ∃𝑘 ∈ ℕ 2 < ((1 /
𝑆)↑𝑘)) |
156 | 133, 145,
154, 155 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘)) |
157 | 144 | rpcnd 12528 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈ ℂ) |
158 | 157 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ) |
159 | 144 | rpne0d 12531 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ≠ 0) |
160 | 159 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ≠ 0) |
161 | | nnz 12097 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
162 | 161 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
163 | 158, 160,
162 | exprecd 13622 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) = (1 / (𝑆↑𝑘))) |
164 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ 𝐴) |
165 | | ax-1ne0 10696 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
0 |
166 | 12 | qrng1 26370 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 =
(1r‘𝑄) |
167 | 11, 166, 17 | abv1z 19734 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) |
168 | 164, 165,
167 | sylancl 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) = 1) |
169 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ∈ ℕ) |
170 | | nnnn0 11995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
171 | | nnexpcl 13546 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑃↑𝑘) ∈
ℕ) |
172 | 169, 170,
171 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃↑𝑘) ∈ ℕ) |
173 | 172 | nnzd 12179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃↑𝑘) ∈ ℤ) |
174 | 99 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑝 ∈ ℕ) |
175 | | nnexpcl 13546 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
176 | 174, 170,
175 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
177 | 176 | nnzd 12179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℤ) |
178 | | bezout 15999 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃↑𝑘) ∈ ℤ ∧ (𝑝↑𝑘) ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) |
179 | 173, 177,
178 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) |
180 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ≠ 𝑝) |
181 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ∈ ℙ) |
182 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑝 ∈ ℙ) |
183 | | prmrp 16165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 ≠ 𝑝)) |
184 | 181, 182,
183 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 ≠ 𝑝)) |
185 | 180, 184 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝑃 gcd 𝑝) = 1) |
186 | 185 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃 gcd 𝑝) = 1) |
187 | 169 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℕ) |
188 | 174 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ) |
189 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
190 | | rppwr 16017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1)) |
191 | 187, 188,
189, 190 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1)) |
192 | 186, 191 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1) |
193 | 192 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1) |
194 | 193 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ↔ 1 = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)))) |
195 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝐹 ∈ 𝐴) |
196 | 172 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃↑𝑘) ∈ ℕ) |
197 | | nnq 12456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃↑𝑘) ∈ ℕ → (𝑃↑𝑘) ∈ ℚ) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃↑𝑘) ∈ ℚ) |
199 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℤ) |
200 | | zq 12448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℚ) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℚ) |
202 | | qmulcl 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃↑𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → ((𝑃↑𝑘) · 𝑎) ∈ ℚ) |
203 | 198, 201,
202 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃↑𝑘) · 𝑎) ∈ ℚ) |
204 | 176 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝↑𝑘) ∈ ℕ) |
205 | | nnq 12456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝↑𝑘) ∈ ℕ → (𝑝↑𝑘) ∈ ℚ) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝↑𝑘) ∈ ℚ) |
207 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℤ) |
208 | | zq 12448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℚ) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℚ) |
210 | | qmulcl 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑝↑𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → ((𝑝↑𝑘) · 𝑏) ∈ ℚ) |
211 | 206, 209,
210 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑝↑𝑘) · 𝑏) ∈ ℚ) |
212 | | qaddcl 12459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃↑𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) |
213 | 203, 211,
212 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) |
214 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ 𝐴 ∧ (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
215 | 195, 213,
214 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
216 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑃↑𝑘) · 𝑎) ∈ ℚ) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ∈ ℝ) |
217 | 195, 203,
216 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ∈ ℝ) |
218 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ∈ ℝ) |
219 | 195, 211,
218 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ∈ ℝ) |
220 | 217, 219 | readdcld 10760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
221 | | rpexpcl 13552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝑆↑𝑘) ∈
ℝ+) |
222 | 144, 161,
221 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈
ℝ+) |
223 | 222 | rpred 12526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈ ℝ) |
224 | 223 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑆↑𝑘) ∈ ℝ) |
225 | | remulcl 10712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℝ ∧ (𝑆↑𝑘) ∈ ℝ) → (2 · (𝑆↑𝑘)) ∈ ℝ) |
226 | 132, 224,
225 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆↑𝑘)) ∈ ℝ) |
227 | | qex 12455 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℚ
∈ V |
228 | | cnfldadd 20234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ + =
(+g‘ℂfld) |
229 | 12, 228 | ressplusg 16727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℚ
∈ V → + = (+g‘𝑄)) |
230 | 227, 229 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ + =
(+g‘𝑄) |
231 | 11, 13, 230 | abvtri 19732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑃↑𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏)))) |
232 | 195, 203,
211, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏)))) |
233 | | cnfldmul 20235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ·
= (.r‘ℂfld) |
234 | 12, 233 | ressmulr 16740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (ℚ
∈ V → · = (.r‘𝑄)) |
235 | 227, 234 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ·
= (.r‘𝑄) |
236 | 11, 13, 235 | abvmul 19731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑃↑𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎))) |
237 | 195, 198,
201, 236 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎))) |
238 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑃 ∈ ℚ) |
239 | 170 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℕ0) |
240 | 12, 11 | qabvexp 26374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑃↑𝑘)) = ((𝐹‘𝑃)↑𝑘)) |
241 | 195, 238,
239, 240 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑃↑𝑘)) = ((𝐹‘𝑃)↑𝑘)) |
242 | 241 | oveq1d 7197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎)) = (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎))) |
243 | 237, 242 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎))) |
244 | 195, 238,
14 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ∈ ℝ) |
245 | 244, 239 | reexpcld 13631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ∈ ℝ) |
246 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ) → (𝐹‘𝑎) ∈ ℝ) |
247 | 195, 201,
246 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑎) ∈ ℝ) |
248 | 245, 247 | remulcld 10761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ∈ ℝ) |
249 | | elz 12076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))) |
250 | 249 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 ∈ ℤ → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)) |
251 | 250 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)) |
252 | 11, 17 | abv0 19733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0) |
253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (𝐹‘0) = 0) |
254 | | 0le1 11253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 0 ≤
1 |
255 | 253, 254 | eqbrtrdi 5079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (𝐹‘0) ≤ 1) |
256 | 255 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝐹‘0) ≤ 1) |
257 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = 0 → (𝐹‘𝑎) = (𝐹‘0)) |
258 | 257 | breq1d 5050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = 0 → ((𝐹‘𝑎) ≤ 1 ↔ (𝐹‘0) ≤ 1)) |
259 | 256, 258 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 = 0 → (𝐹‘𝑎) ≤ 1)) |
260 | | ostth3.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) |
261 | | nnq 12456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℚ) |
262 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ) → (𝐹‘𝑛) ∈ ℝ) |
263 | 2, 261, 262 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ) |
264 | | 1re 10731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 1 ∈
ℝ |
265 | | lenlt 10809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐹‘𝑛) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐹‘𝑛) ≤ 1 ↔ ¬ 1 <
(𝐹‘𝑛))) |
266 | 263, 264,
265 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ≤ 1 ↔ ¬ 1 < (𝐹‘𝑛))) |
267 | 266 | ralbidva 3109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1 ↔ ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))) |
268 | 260, 267 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1) |
269 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑛 = 𝑎 → (𝐹‘𝑛) = (𝐹‘𝑎)) |
270 | 269 | breq1d 5050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) ≤ 1 ↔ (𝐹‘𝑎) ≤ 1)) |
271 | 270 | rspccv 3526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) ≤ 1 → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
272 | 268, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
273 | 272 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
274 | 2 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝐹 ∈ 𝐴) |
275 | 200 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝑎 ∈ ℚ) |
276 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(invg‘𝑄) = (invg‘𝑄) |
277 | 11, 13, 276 | abvneg 19736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ) → (𝐹‘((invg‘𝑄)‘𝑎)) = (𝐹‘𝑎)) |
278 | 274, 275,
277 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg‘𝑄)‘𝑎)) = (𝐹‘𝑎)) |
279 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑛 = ((invg‘𝑄)‘𝑎) → (𝐹‘𝑛) = (𝐹‘((invg‘𝑄)‘𝑎))) |
280 | 279 | breq1d 5050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑛 = ((invg‘𝑄)‘𝑎) → ((𝐹‘𝑛) ≤ 1 ↔ (𝐹‘((invg‘𝑄)‘𝑎)) ≤ 1)) |
281 | 268 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1) |
282 | 12 | qrngneg 26371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∈ ℚ →
((invg‘𝑄)‘𝑎) = -𝑎) |
283 | 275, 282 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) →
((invg‘𝑄)‘𝑎) = -𝑎) |
284 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → -𝑎 ∈ ℕ) |
285 | 283, 284 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) →
((invg‘𝑄)‘𝑎) ∈ ℕ) |
286 | 280, 281,
285 | rspcdva 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg‘𝑄)‘𝑎)) ≤ 1) |
287 | 278, 286 | eqbrtrrd 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘𝑎) ≤ 1) |
288 | 287 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
289 | 259, 273,
288 | 3jaod 1429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ) → (𝐹‘𝑎) ≤ 1)) |
290 | 251, 289 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝐹‘𝑎) ≤ 1) |
291 | 290 | ralrimiva 3097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ∀𝑎 ∈ ℤ (𝐹‘𝑎) ≤ 1) |
292 | 291 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ∀𝑎 ∈ ℤ (𝐹‘𝑎) ≤ 1) |
293 | | rsp 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑎 ∈
ℤ (𝐹‘𝑎) ≤ 1 → (𝑎 ∈ ℤ → (𝐹‘𝑎) ≤ 1)) |
294 | 292, 199,
293 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑎) ≤ 1) |
295 | 264 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 1 ∈
ℝ) |
296 | 161 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℤ) |
297 | 19 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹‘𝑃)) |
298 | | expgt0 13566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹‘𝑃)) → 0 < ((𝐹‘𝑃)↑𝑘)) |
299 | 244, 296,
297, 298 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹‘𝑃)↑𝑘)) |
300 | | lemul2 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑎) ∈ ℝ ∧ 1 ∈ ℝ ∧
(((𝐹‘𝑃)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹‘𝑃)↑𝑘))) → ((𝐹‘𝑎) ≤ 1 ↔ (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1))) |
301 | 247, 295,
245, 299, 300 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑎) ≤ 1 ↔ (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1))) |
302 | 294, 301 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1)) |
303 | 245 | recnd 10759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ∈ ℂ) |
304 | 303 | mulid1d 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · 1) = ((𝐹‘𝑃)↑𝑘)) |
305 | 302, 304 | breqtrd 5066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ ((𝐹‘𝑃)↑𝑘)) |
306 | 144 | rpred 12526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈ ℝ) |
307 | 306 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑆 ∈ ℝ) |
308 | 142 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ∈
ℝ+) |
309 | 308 | rpge0d 12530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹‘𝑃)) |
310 | 174 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℕ) |
311 | 310, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℚ) |
312 | 195, 311,
136 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ∈ ℝ) |
313 | | max1 12673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ (𝐹‘𝑝) ∈ ℝ) → (𝐹‘𝑃) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
314 | 244, 312,
313 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
315 | 314, 134 | breqtrrdi 5082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ≤ 𝑆) |
316 | | leexp1a 13643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹‘𝑃) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤
(𝐹‘𝑃) ∧ (𝐹‘𝑃) ≤ 𝑆)) → ((𝐹‘𝑃)↑𝑘) ≤ (𝑆↑𝑘)) |
317 | 244, 307,
239, 309, 315, 316 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ≤ (𝑆↑𝑘)) |
318 | 248, 245,
224, 305, 317 | letrd 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (𝑆↑𝑘)) |
319 | 243, 318 | eqbrtrd 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ≤ (𝑆↑𝑘)) |
320 | 11, 13, 235 | abvmul 19731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑝↑𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏))) |
321 | 195, 206,
209, 320 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏))) |
322 | 12, 11 | qabvexp 26374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑝↑𝑘)) = ((𝐹‘𝑝)↑𝑘)) |
323 | 195, 311,
239, 322 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑝↑𝑘)) = ((𝐹‘𝑝)↑𝑘)) |
324 | 323 | oveq1d 7197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏)) = (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏))) |
325 | 321, 324 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏))) |
326 | 312, 239 | reexpcld 13631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ∈ ℝ) |
327 | 11, 13 | abvcl 19726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑏 ∈ ℚ) → (𝐹‘𝑏) ∈ ℝ) |
328 | 195, 209,
327 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑏) ∈ ℝ) |
329 | 326, 328 | remulcld 10761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ∈ ℝ) |
330 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
331 | 330 | breq1d 5050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) ≤ 1 ↔ (𝐹‘𝑏) ≤ 1)) |
332 | 331, 292,
207 | rspcdva 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑏) ≤ 1) |
333 | 310 | nnne0d 11778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ≠ 0) |
334 | 195, 311,
333, 138 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹‘𝑝)) |
335 | | expgt0 13566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹‘𝑝) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹‘𝑝)) → 0 < ((𝐹‘𝑝)↑𝑘)) |
336 | 312, 296,
334, 335 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹‘𝑝)↑𝑘)) |
337 | | lemul2 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑏) ∈ ℝ ∧ 1 ∈ ℝ ∧
(((𝐹‘𝑝)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹‘𝑝)↑𝑘))) → ((𝐹‘𝑏) ≤ 1 ↔ (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1))) |
338 | 328, 295,
326, 336, 337 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑏) ≤ 1 ↔ (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1))) |
339 | 332, 338 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1)) |
340 | 326 | recnd 10759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ∈ ℂ) |
341 | 340 | mulid1d 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · 1) = ((𝐹‘𝑝)↑𝑘)) |
342 | 339, 341 | breqtrd 5066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ ((𝐹‘𝑝)↑𝑘)) |
343 | 141 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ∈
ℝ+) |
344 | 343 | rpge0d 12530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹‘𝑝)) |
345 | | max2 12675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ (𝐹‘𝑝) ∈ ℝ) → (𝐹‘𝑝) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
346 | 244, 312,
345 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
347 | 346, 134 | breqtrrdi 5082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ≤ 𝑆) |
348 | | leexp1a 13643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹‘𝑝) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤
(𝐹‘𝑝) ∧ (𝐹‘𝑝) ≤ 𝑆)) → ((𝐹‘𝑝)↑𝑘) ≤ (𝑆↑𝑘)) |
349 | 312, 307,
239, 344, 347, 348 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ≤ (𝑆↑𝑘)) |
350 | 329, 326,
224, 342, 349 | letrd 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (𝑆↑𝑘)) |
351 | 325, 350 | eqbrtrd 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ≤ (𝑆↑𝑘)) |
352 | 217, 219,
224, 224, 319, 351 | le2addd 11349 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ≤ ((𝑆↑𝑘) + (𝑆↑𝑘))) |
353 | 222 | rpcnd 12528 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈ ℂ) |
354 | 353 | 2timesd 11971 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 · (𝑆↑𝑘)) = ((𝑆↑𝑘) + (𝑆↑𝑘))) |
355 | 354 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆↑𝑘)) = ((𝑆↑𝑘) + (𝑆↑𝑘))) |
356 | 352, 355 | breqtrrd 5068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘))) |
357 | 215, 220,
226, 232, 356 | letrd 10887 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘))) |
358 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 =
(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) = (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)))) |
359 | 358 | breq1d 5050 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 =
(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → ((𝐹‘1) ≤ (2 · (𝑆↑𝑘)) ↔ (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘)))) |
360 | 357, 359 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (1 = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
361 | 194, 360 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
362 | 361 | anassrs 471 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
363 | 362 | rexlimdvva 3205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
364 | 179, 363 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘))) |
365 | 168, 364 | eqbrtrrd 5064 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 1 ≤ (2 ·
(𝑆↑𝑘))) |
366 | 222 | rpregt0d 12532 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑆↑𝑘) ∈ ℝ ∧ 0 < (𝑆↑𝑘))) |
367 | | ledivmul2 11609 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ ((𝑆↑𝑘) ∈ ℝ ∧ 0 < (𝑆↑𝑘))) → ((1 / (𝑆↑𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆↑𝑘)))) |
368 | 264, 132,
366, 367 | mp3an12i 1466 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑆↑𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆↑𝑘)))) |
369 | 365, 368 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (1 / (𝑆↑𝑘)) ≤ 2) |
370 | 163, 369 | eqbrtrd 5062 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ≤ 2) |
371 | | reexpcl 13550 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑆) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((1 / 𝑆)↑𝑘) ∈ ℝ) |
372 | 145, 170,
371 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ∈ ℝ) |
373 | | lenlt 10809 |
. . . . . . . . . . . . . . 15
⊢ ((((1 /
𝑆)↑𝑘) ∈ ℝ ∧ 2 ∈ ℝ)
→ (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1
/ 𝑆)↑𝑘))) |
374 | 372, 132,
373 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘))) |
375 | 370, 374 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ¬ 2 < ((1 /
𝑆)↑𝑘)) |
376 | 375 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹‘𝑝) < 1)) |
377 | 376 | rexlimdva 3195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹‘𝑝) < 1)) |
378 | 156, 377 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ¬ (𝐹‘𝑝) < 1) |
379 | 378 | expr 460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐹‘𝑝) < 1 → ¬ (𝐹‘𝑝) < 1)) |
380 | 379 | pm2.01d 193 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ (𝐹‘𝑝) < 1) |
381 | | fveq2 6686 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → (𝐹‘𝑛) = (𝐹‘𝑝)) |
382 | 381 | breq2d 5052 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑝 → (1 < (𝐹‘𝑛) ↔ 1 < (𝐹‘𝑝))) |
383 | 382 | notbid 321 |
. . . . . . . . 9
⊢ (𝑛 = 𝑝 → (¬ 1 < (𝐹‘𝑛) ↔ ¬ 1 < (𝐹‘𝑝))) |
384 | 260 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) |
385 | 383, 384,
100 | rspcdva 3531 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ 1 < (𝐹‘𝑝)) |
386 | | lttri3 10814 |
. . . . . . . . 9
⊢ (((𝐹‘𝑝) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐹‘𝑝) = 1 ↔ (¬ (𝐹‘𝑝) < 1 ∧ ¬ 1 < (𝐹‘𝑝)))) |
387 | 137, 264,
386 | sylancl 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐹‘𝑝) = 1 ↔ (¬ (𝐹‘𝑝) < 1 ∧ ¬ 1 < (𝐹‘𝑝)))) |
388 | 380, 385,
387 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) = 1) |
389 | 109, 131,
388 | 3eqtr4d 2784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) = (𝐹‘𝑝)) |
390 | 107, 389 | eqtr2d 2775 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
391 | 390 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 ≠ 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
392 | 98, 391 | pm2.61dne 3021 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
393 | 12, 11, 2, 47, 392 | ostthlem2 26376 |
. 2
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) |
394 | | oveq2 7190 |
. . . 4
⊢ (𝑎 = 𝑅 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎) = (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) |
395 | 394 | mpteq2dv 5136 |
. . 3
⊢ (𝑎 = 𝑅 → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎)) = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) |
396 | 395 | rspceeqv 3544 |
. 2
⊢ ((𝑅 ∈ ℝ+
∧ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎))) |
397 | 44, 393, 396 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎))) |