Step | Hyp | Ref
| Expression |
1 | | ostth3.5 |
. . . 4
⊢ 𝑅 = -((log‘(𝐹‘𝑃)) / (log‘𝑃)) |
2 | | ostth.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
3 | | ostth3.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
4 | | prmuz2 15408 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
6 | | eluz2b2 11761 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
7 | 5, 6 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃)) |
8 | 7 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | | nnq 11801 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℚ) |
11 | | qabsabv.a |
. . . . . . . . . 10
⊢ 𝐴 = (AbsVal‘𝑄) |
12 | | qrng.q |
. . . . . . . . . . 11
⊢ 𝑄 = (ℂfld
↾s ℚ) |
13 | 12 | qrngbas 25308 |
. . . . . . . . . 10
⊢ ℚ =
(Base‘𝑄) |
14 | 11, 13 | abvcl 18824 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ) → (𝐹‘𝑃) ∈ ℝ) |
15 | 2, 10, 14 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑃) ∈ ℝ) |
16 | 8 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ≠ 0) |
17 | 12 | qrng0 25310 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑄) |
18 | 11, 13, 17 | abvgt0 18828 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0) → 0 < (𝐹‘𝑃)) |
19 | 2, 10, 16, 18 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝐹‘𝑃)) |
20 | 15, 19 | elrpd 11869 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑃) ∈
ℝ+) |
21 | 20 | relogcld 24369 |
. . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑃)) ∈ ℝ) |
22 | 8 | nnred 11035 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℝ) |
23 | 7 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → 1 < 𝑃) |
24 | 22, 23 | rplogcld 24375 |
. . . . . 6
⊢ (𝜑 → (log‘𝑃) ∈
ℝ+) |
25 | 21, 24 | rerpdivcld 11903 |
. . . . 5
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℝ) |
26 | 25 | renegcld 10457 |
. . . 4
⊢ (𝜑 → -((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℝ) |
27 | 1, 26 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) |
28 | | ostth3.4 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) < 1) |
29 | | 1rp 11836 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
30 | | logltb 24346 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑃) ∈ ℝ+ ∧ 1 ∈
ℝ+) → ((𝐹‘𝑃) < 1 ↔ (log‘(𝐹‘𝑃)) < (log‘1))) |
31 | 20, 29, 30 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑃) < 1 ↔ (log‘(𝐹‘𝑃)) < (log‘1))) |
32 | 28, 31 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < (log‘1)) |
33 | | log1 24332 |
. . . . . . . 8
⊢
(log‘1) = 0 |
34 | 32, 33 | syl6breq 4694 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < 0) |
35 | 24 | rpcnd 11874 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑃) ∈
ℂ) |
36 | 35 | mul01d 10235 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝑃) · 0) =
0) |
37 | 34, 36 | breqtrrd 4681 |
. . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑃)) < ((log‘𝑃) · 0)) |
38 | | 0red 10041 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
39 | 21, 38, 24 | ltdivmuld 11923 |
. . . . . 6
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0 ↔ (log‘(𝐹‘𝑃)) < ((log‘𝑃) · 0))) |
40 | 37, 39 | mpbird 247 |
. . . . 5
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0) |
41 | 25 | lt0neg1d 10597 |
. . . . 5
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) < 0 ↔ 0 < -((log‘(𝐹‘𝑃)) / (log‘𝑃)))) |
42 | 40, 41 | mpbid 222 |
. . . 4
⊢ (𝜑 → 0 < -((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
43 | 42, 1 | syl6breqr 4695 |
. . 3
⊢ (𝜑 → 0 < 𝑅) |
44 | 27, 43 | elrpd 11869 |
. 2
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
45 | | padic.j |
. . . . 5
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) |
46 | 12, 11, 45 | padicabvcxp 25321 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+)
→ (𝑦 ∈ ℚ
↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |
47 | 3, 44, 46 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴) |
48 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑃 → ((𝐽‘𝑃)‘𝑦) = ((𝐽‘𝑃)‘𝑃)) |
49 | 48 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 = 𝑃 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
50 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) |
51 | | ovex 6678 |
. . . . . . . . 9
⊢ (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅) ∈ V |
52 | 49, 50, 51 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑃 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
53 | 10, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅)) |
54 | 45 | padicval 25306 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ ℚ) → ((𝐽‘𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃)))) |
55 | 3, 10, 54 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐽‘𝑃)‘𝑃) = if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃)))) |
56 | 16 | neneqd 2799 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑃 = 0) |
57 | 56 | iffalsed 4097 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑃 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑃))) = (𝑃↑-(𝑃 pCnt 𝑃))) |
58 | 8 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℂ) |
59 | 58 | exp1d 13003 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃↑1) = 𝑃) |
60 | 59 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃)) |
61 | | 1z 11407 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
62 | | pcid 15577 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 1 ∈
ℤ) → (𝑃 pCnt
(𝑃↑1)) =
1) |
63 | 3, 61, 62 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = 1) |
64 | 60, 63 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 pCnt 𝑃) = 1) |
65 | 64 | negeqd 10275 |
. . . . . . . . . . 11
⊢ (𝜑 → -(𝑃 pCnt 𝑃) = -1) |
66 | 65 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑-1)) |
67 | | neg1z 11413 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℤ |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → -1 ∈
ℤ) |
69 | 58, 16, 68 | cxpexpzd 24457 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃↑𝑐-1) = (𝑃↑-1)) |
70 | 66, 69 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃↑-(𝑃 pCnt 𝑃)) = (𝑃↑𝑐-1)) |
71 | 55, 57, 70 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → ((𝐽‘𝑃)‘𝑃) = (𝑃↑𝑐-1)) |
72 | 71 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((𝐽‘𝑃)‘𝑃)↑𝑐𝑅) = ((𝑃↑𝑐-1)↑𝑐𝑅)) |
73 | 27 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
74 | 73 | mulm1d 10482 |
. . . . . . . . . 10
⊢ (𝜑 → (-1 · 𝑅) = -𝑅) |
75 | 1 | negeqi 10274 |
. . . . . . . . . . 11
⊢ -𝑅 = --((log‘(𝐹‘𝑃)) / (log‘𝑃)) |
76 | 25 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘(𝐹‘𝑃)) / (log‘𝑃)) ∈ ℂ) |
77 | 76 | negnegd 10383 |
. . . . . . . . . . 11
⊢ (𝜑 → --((log‘(𝐹‘𝑃)) / (log‘𝑃)) = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
78 | 75, 77 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → -𝑅 = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
79 | 74, 78 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (-1 · 𝑅) = ((log‘(𝐹‘𝑃)) / (log‘𝑃))) |
80 | 79 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐(-1 · 𝑅)) = (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃)))) |
81 | 8 | nnrpd 11870 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
82 | | neg1rr 11125 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℝ) |
84 | 81, 83, 73 | cxpmuld 24480 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐(-1 · 𝑅)) = ((𝑃↑𝑐-1)↑𝑐𝑅)) |
85 | 58, 16, 76 | cxpefd 24458 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃))) = (exp‘(((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃)))) |
86 | 21 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐹‘𝑃)) ∈ ℂ) |
87 | 24 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝑃) ≠ 0) |
88 | 86, 35, 87 | divcan1d 10802 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃)) = (log‘(𝐹‘𝑃))) |
89 | 88 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(((log‘(𝐹‘𝑃)) / (log‘𝑃)) · (log‘𝑃))) = (exp‘(log‘(𝐹‘𝑃)))) |
90 | 20 | reeflogd 24370 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(log‘(𝐹‘𝑃))) = (𝐹‘𝑃)) |
91 | 85, 89, 90 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑐((log‘(𝐹‘𝑃)) / (log‘𝑃))) = (𝐹‘𝑃)) |
92 | 80, 84, 91 | 3eqtr3d 2664 |
. . . . . . 7
⊢ (𝜑 → ((𝑃↑𝑐-1)↑𝑐𝑅) = (𝐹‘𝑃)) |
93 | 53, 72, 92 | 3eqtrrd 2661 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃)) |
94 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑃 = 𝑝 → (𝐹‘𝑃) = (𝐹‘𝑝)) |
95 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑃 = 𝑝 → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
96 | 94, 95 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑃 = 𝑝 → ((𝐹‘𝑃) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑃) ↔ (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
97 | 93, 96 | syl5ibcom 235 |
. . . . 5
⊢ (𝜑 → (𝑃 = 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
98 | 97 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 = 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
99 | | prmnn 15388 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
100 | 99 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ∈ ℕ) |
101 | | nnq 11801 |
. . . . . . . 8
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℚ) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ∈ ℚ) |
103 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = 𝑝 → ((𝐽‘𝑃)‘𝑦) = ((𝐽‘𝑃)‘𝑝)) |
104 | 103 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑦 = 𝑝 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
105 | | ovex 6678 |
. . . . . . . 8
⊢ (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) ∈ V |
106 | 104, 50, 105 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑝 ∈ ℚ → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
107 | 102, 106 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝) = (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅)) |
108 | 73 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑅 ∈ ℂ) |
109 | 108 | 1cxpd 24453 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (1↑𝑐𝑅) = 1) |
110 | 3 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑃 ∈ ℙ) |
111 | 45 | padicval 25306 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℚ) → ((𝐽‘𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝)))) |
112 | 110, 102,
111 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐽‘𝑃)‘𝑝) = if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝)))) |
113 | 100 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑝 ≠ 0) |
114 | 113 | neneqd 2799 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ 𝑝 = 0) |
115 | 114 | iffalsed 4097 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → if(𝑝 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑝))) = (𝑃↑-(𝑃 pCnt 𝑝))) |
116 | | pceq0 15575 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℕ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃 ∥ 𝑝)) |
117 | 3, 99, 116 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ ¬ 𝑃 ∥ 𝑝)) |
118 | | dvdsprm 15415 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑝 ∈ ℙ) → (𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝)) |
119 | 5, 118 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 ∥ 𝑝 ↔ 𝑃 = 𝑝)) |
120 | 119 | necon3bbid 2831 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑃 ∥ 𝑝 ↔ 𝑃 ≠ 𝑝)) |
121 | 117, 120 | bitrd 268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑃 pCnt 𝑝) = 0 ↔ 𝑃 ≠ 𝑝)) |
122 | 121 | biimpar 502 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃 pCnt 𝑝) = 0) |
123 | 122 | negeqd 10275 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → -(𝑃 pCnt 𝑝) = -0) |
124 | | neg0 10327 |
. . . . . . . . . . . 12
⊢ -0 =
0 |
125 | 123, 124 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → -(𝑃 pCnt 𝑝) = 0) |
126 | 125 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = (𝑃↑0)) |
127 | 58 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝑃 ∈ ℂ) |
128 | 127 | exp0d 13002 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑0) = 1) |
129 | 126, 128 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝑃↑-(𝑃 pCnt 𝑝)) = 1) |
130 | 112, 115,
129 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐽‘𝑃)‘𝑝) = 1) |
131 | 130 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) = (1↑𝑐𝑅)) |
132 | | 2re 11090 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
133 | 132 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 2 ∈
ℝ) |
134 | | ostth3.6 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) |
135 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 𝐹 ∈ 𝐴) |
136 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) ∈ ℝ) |
137 | 135, 102,
136 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) ∈ ℝ) |
138 | 11, 13, 17 | abvgt0 18828 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑝 ≠ 0) → 0 < (𝐹‘𝑝)) |
139 | 135, 102,
113, 138 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → 0 < (𝐹‘𝑝)) |
140 | 137, 139 | elrpd 11869 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) ∈
ℝ+) |
141 | 140 | adantrr 753 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑝) ∈
ℝ+) |
142 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑃) ∈
ℝ+) |
143 | 141, 142 | ifcld 4131 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) ∈
ℝ+) |
144 | 134, 143 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈
ℝ+) |
145 | 144 | rprecred 11883 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (1 / 𝑆) ∈ ℝ) |
146 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑝) < 1) |
147 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝐹‘𝑃) < 1) |
148 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑝) = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) → ((𝐹‘𝑝) < 1 ↔ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1)) |
149 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑃) = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) → ((𝐹‘𝑃) < 1 ↔ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1)) |
150 | 148, 149 | ifboth 4124 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑝) < 1 ∧ (𝐹‘𝑃) < 1) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1) |
151 | 146, 147,
150 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃)) < 1) |
152 | 134, 151 | syl5eqbr 4688 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 < 1) |
153 | 144 | reclt1d 11885 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝑆 < 1 ↔ 1 < (1 / 𝑆))) |
154 | 152, 153 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 1 < (1 / 𝑆)) |
155 | | expnbnd 12993 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (1 / 𝑆) ∈ ℝ ∧ 1 < (1 / 𝑆)) → ∃𝑘 ∈ ℕ 2 < ((1 /
𝑆)↑𝑘)) |
156 | 133, 145,
154, 155 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘)) |
157 | 144 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈ ℂ) |
158 | 157 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ) |
159 | 144 | rpne0d 11877 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ≠ 0) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑆 ≠ 0) |
161 | | nnz 11399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
162 | 161 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
163 | 158, 160,
162 | exprecd 13016 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) = (1 / (𝑆↑𝑘))) |
164 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ 𝐴) |
165 | | ax-1ne0 10005 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
0 |
166 | 12 | qrng1 25311 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 =
(1r‘𝑄) |
167 | 11, 166, 17 | abv1z 18832 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) |
168 | 164, 165,
167 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) = 1) |
169 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ∈ ℕ) |
170 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
171 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑃↑𝑘) ∈
ℕ) |
172 | 169, 170,
171 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃↑𝑘) ∈ ℕ) |
173 | 172 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃↑𝑘) ∈ ℤ) |
174 | 99 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑝 ∈ ℕ) |
175 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
176 | 174, 170,
175 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
177 | 176 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℤ) |
178 | | bezout 15260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃↑𝑘) ∈ ℤ ∧ (𝑝↑𝑘) ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) |
179 | 173, 177,
178 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) |
180 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ≠ 𝑝) |
181 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑃 ∈ ℙ) |
182 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑝 ∈ ℙ) |
183 | | prmrp 15424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 ≠ 𝑝)) |
184 | 181, 182,
183 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ((𝑃 gcd 𝑝) = 1 ↔ 𝑃 ≠ 𝑝)) |
185 | 180, 184 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (𝑃 gcd 𝑝) = 1) |
186 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑃 gcd 𝑝) = 1) |
187 | 169 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℕ) |
188 | 174 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ) |
189 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
190 | | rppwr 15277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1)) |
191 | 187, 188,
189, 190 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃 gcd 𝑝) = 1 → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1)) |
192 | 186, 191 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1) |
193 | 192 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = 1) |
194 | 193 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ↔ 1 = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)))) |
195 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝐹 ∈ 𝐴) |
196 | 172 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃↑𝑘) ∈ ℕ) |
197 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃↑𝑘) ∈ ℕ → (𝑃↑𝑘) ∈ ℚ) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑃↑𝑘) ∈ ℚ) |
199 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℤ) |
200 | | zq 11794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℚ) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑎 ∈ ℚ) |
202 | | qmulcl 11806 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃↑𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → ((𝑃↑𝑘) · 𝑎) ∈ ℚ) |
203 | 198, 201,
202 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑃↑𝑘) · 𝑎) ∈ ℚ) |
204 | 176 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝↑𝑘) ∈ ℕ) |
205 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝↑𝑘) ∈ ℕ → (𝑝↑𝑘) ∈ ℚ) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑝↑𝑘) ∈ ℚ) |
207 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℤ) |
208 | | zq 11794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℚ) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑏 ∈ ℚ) |
210 | | qmulcl 11806 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑝↑𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → ((𝑝↑𝑘) · 𝑏) ∈ ℚ) |
211 | 206, 209,
210 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝑝↑𝑘) · 𝑏) ∈ ℚ) |
212 | | qaddcl 11804 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑃↑𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) |
213 | 203, 211,
212 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) |
214 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ 𝐴 ∧ (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) ∈ ℚ) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
215 | 195, 213,
214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
216 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑃↑𝑘) · 𝑎) ∈ ℚ) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ∈ ℝ) |
217 | 195, 203,
216 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ∈ ℝ) |
218 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ∈ ℝ) |
219 | 195, 211,
218 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ∈ ℝ) |
220 | 217, 219 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ∈ ℝ) |
221 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝑆↑𝑘) ∈
ℝ+) |
222 | 144, 161,
221 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈
ℝ+) |
223 | 222 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈ ℝ) |
224 | 223 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝑆↑𝑘) ∈ ℝ) |
225 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℝ ∧ (𝑆↑𝑘) ∈ ℝ) → (2 · (𝑆↑𝑘)) ∈ ℝ) |
226 | 132, 224,
225 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆↑𝑘)) ∈ ℝ) |
227 | | qex 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℚ
∈ V |
228 | | cnfldadd 19751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ + =
(+g‘ℂfld) |
229 | 12, 228 | ressplusg 15993 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℚ
∈ V → + = (+g‘𝑄)) |
230 | 227, 229 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ + =
(+g‘𝑄) |
231 | 11, 13, 230 | abvtri 18830 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ 𝐴 ∧ ((𝑃↑𝑘) · 𝑎) ∈ ℚ ∧ ((𝑝↑𝑘) · 𝑏) ∈ ℚ) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏)))) |
232 | 195, 203,
211, 231 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏)))) |
233 | | cnfldmul 19752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ·
= (.r‘ℂfld) |
234 | 12, 233 | ressmulr 16006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (ℚ
∈ V → · = (.r‘𝑄)) |
235 | 227, 234 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ·
= (.r‘𝑄) |
236 | 11, 13, 235 | abvmul 18829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑃↑𝑘) ∈ ℚ ∧ 𝑎 ∈ ℚ) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎))) |
237 | 195, 198,
201, 236 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎))) |
238 | 10 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑃 ∈ ℚ) |
239 | 170 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℕ0) |
240 | 12, 11 | qabvexp 25315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑃↑𝑘)) = ((𝐹‘𝑃)↑𝑘)) |
241 | 195, 238,
239, 240 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑃↑𝑘)) = ((𝐹‘𝑃)↑𝑘)) |
242 | 241 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑃↑𝑘)) · (𝐹‘𝑎)) = (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎))) |
243 | 237, 242 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) = (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎))) |
244 | 195, 238,
14 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ∈ ℝ) |
245 | 244, 239 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ∈ ℝ) |
246 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ) → (𝐹‘𝑎) ∈ ℝ) |
247 | 195, 201,
246 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑎) ∈ ℝ) |
248 | 245, 247 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ∈ ℝ) |
249 | | elz 11379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ))) |
250 | 249 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 ∈ ℤ → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)) |
251 | 250 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ)) |
252 | 11, 17 | abv0 18831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0) |
253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (𝐹‘0) = 0) |
254 | | 0le1 10551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 0 ≤
1 |
255 | 253, 254 | syl6eqbr 4692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (𝐹‘0) ≤ 1) |
256 | 255 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝐹‘0) ≤ 1) |
257 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = 0 → (𝐹‘𝑎) = (𝐹‘0)) |
258 | 257 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = 0 → ((𝐹‘𝑎) ≤ 1 ↔ (𝐹‘0) ≤ 1)) |
259 | 256, 258 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 = 0 → (𝐹‘𝑎) ≤ 1)) |
260 | | ostth3.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) |
261 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℚ) |
262 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ) → (𝐹‘𝑛) ∈ ℝ) |
263 | 2, 261, 262 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ) |
264 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 1 ∈
ℝ |
265 | | lenlt 10116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐹‘𝑛) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐹‘𝑛) ≤ 1 ↔ ¬ 1 <
(𝐹‘𝑛))) |
266 | 263, 264,
265 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ≤ 1 ↔ ¬ 1 < (𝐹‘𝑛))) |
267 | 266 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1 ↔ ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))) |
268 | 260, 267 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1) |
269 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑛 = 𝑎 → (𝐹‘𝑛) = (𝐹‘𝑎)) |
270 | 269 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑛 = 𝑎 → ((𝐹‘𝑛) ≤ 1 ↔ (𝐹‘𝑎) ≤ 1)) |
271 | 270 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) ≤ 1 → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
272 | 268, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
273 | 272 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
274 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝐹 ∈ 𝐴) |
275 | 200 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → 𝑎 ∈ ℚ) |
276 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(invg‘𝑄) = (invg‘𝑄) |
277 | 11, 13, 276 | abvneg 18834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑎 ∈ ℚ) → (𝐹‘((invg‘𝑄)‘𝑎)) = (𝐹‘𝑎)) |
278 | 274, 275,
277 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg‘𝑄)‘𝑎)) = (𝐹‘𝑎)) |
279 | 12 | qrngneg 25312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∈ ℚ →
((invg‘𝑄)‘𝑎) = -𝑎) |
280 | 275, 279 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) →
((invg‘𝑄)‘𝑎) = -𝑎) |
281 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → -𝑎 ∈ ℕ) |
282 | 280, 281 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) →
((invg‘𝑄)‘𝑎) ∈ ℕ) |
283 | 268 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1) |
284 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑛 = ((invg‘𝑄)‘𝑎) → (𝐹‘𝑛) = (𝐹‘((invg‘𝑄)‘𝑎))) |
285 | 284 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑛 = ((invg‘𝑄)‘𝑎) → ((𝐹‘𝑛) ≤ 1 ↔ (𝐹‘((invg‘𝑄)‘𝑎)) ≤ 1)) |
286 | 285 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((invg‘𝑄)‘𝑎) ∈ ℕ → (∀𝑛 ∈ ℕ (𝐹‘𝑛) ≤ 1 → (𝐹‘((invg‘𝑄)‘𝑎)) ≤ 1)) |
287 | 282, 283,
286 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘((invg‘𝑄)‘𝑎)) ≤ 1) |
288 | 278, 287 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ (𝑎 ∈ ℤ ∧ -𝑎 ∈ ℕ)) → (𝐹‘𝑎) ≤ 1) |
289 | 288 | expr 643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ → (𝐹‘𝑎) ≤ 1)) |
290 | 259, 273,
289 | 3jaod 1392 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → ((𝑎 = 0 ∨ 𝑎 ∈ ℕ ∨ -𝑎 ∈ ℕ) → (𝐹‘𝑎) ≤ 1)) |
291 | 251, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ) → (𝐹‘𝑎) ≤ 1) |
292 | 291 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ∀𝑎 ∈ ℤ (𝐹‘𝑎) ≤ 1) |
293 | 292 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ∀𝑎 ∈ ℤ (𝐹‘𝑎) ≤ 1) |
294 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑎 ∈
ℤ (𝐹‘𝑎) ≤ 1 → (𝑎 ∈ ℤ → (𝐹‘𝑎) ≤ 1)) |
295 | 293, 199,
294 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑎) ≤ 1) |
296 | 264 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 1 ∈
ℝ) |
297 | 161 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑘 ∈ ℤ) |
298 | 19 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹‘𝑃)) |
299 | | expgt0 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹‘𝑃)) → 0 < ((𝐹‘𝑃)↑𝑘)) |
300 | 244, 297,
298, 299 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹‘𝑃)↑𝑘)) |
301 | | lemul2 10876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑎) ∈ ℝ ∧ 1 ∈ ℝ ∧
(((𝐹‘𝑃)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹‘𝑃)↑𝑘))) → ((𝐹‘𝑎) ≤ 1 ↔ (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1))) |
302 | 247, 296,
245, 300, 301 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑎) ≤ 1 ↔ (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1))) |
303 | 295, 302 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (((𝐹‘𝑃)↑𝑘) · 1)) |
304 | 245 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ∈ ℂ) |
305 | 304 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · 1) = ((𝐹‘𝑃)↑𝑘)) |
306 | 303, 305 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ ((𝐹‘𝑃)↑𝑘)) |
307 | 144 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → 𝑆 ∈ ℝ) |
308 | 307 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑆 ∈ ℝ) |
309 | 142 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ∈
ℝ+) |
310 | 309 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹‘𝑃)) |
311 | 174 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℕ) |
312 | 311, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ∈ ℚ) |
313 | 195, 312,
136 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ∈ ℝ) |
314 | | max1 12016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ (𝐹‘𝑝) ∈ ℝ) → (𝐹‘𝑃) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
315 | 244, 313,
314 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
316 | 315, 134 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑃) ≤ 𝑆) |
317 | | leexp1a 12919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹‘𝑃) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤
(𝐹‘𝑃) ∧ (𝐹‘𝑃) ≤ 𝑆)) → ((𝐹‘𝑃)↑𝑘) ≤ (𝑆↑𝑘)) |
318 | 244, 308,
239, 310, 316, 317 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑃)↑𝑘) ≤ (𝑆↑𝑘)) |
319 | 248, 245,
224, 306, 318 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑃)↑𝑘) · (𝐹‘𝑎)) ≤ (𝑆↑𝑘)) |
320 | 243, 319 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑃↑𝑘) · 𝑎)) ≤ (𝑆↑𝑘)) |
321 | 11, 13, 235 | abvmul 18829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑝↑𝑘) ∈ ℚ ∧ 𝑏 ∈ ℚ) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏))) |
322 | 195, 206,
209, 321 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏))) |
323 | 12, 11 | qabvexp 25315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑝 ∈ ℚ ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑝↑𝑘)) = ((𝐹‘𝑝)↑𝑘)) |
324 | 195, 312,
239, 323 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(𝑝↑𝑘)) = ((𝐹‘𝑝)↑𝑘)) |
325 | 324 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘(𝑝↑𝑘)) · (𝐹‘𝑏)) = (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏))) |
326 | 322, 325 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) = (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏))) |
327 | 313, 239 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ∈ ℝ) |
328 | 11, 13 | abvcl 18824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑏 ∈ ℚ) → (𝐹‘𝑏) ∈ ℝ) |
329 | 195, 209,
328 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑏) ∈ ℝ) |
330 | 327, 329 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ∈ ℝ) |
331 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
332 | 331 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) ≤ 1 ↔ (𝐹‘𝑏) ≤ 1)) |
333 | 332 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 ∈ ℤ →
(∀𝑎 ∈ ℤ
(𝐹‘𝑎) ≤ 1 → (𝐹‘𝑏) ≤ 1)) |
334 | 207, 293,
333 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑏) ≤ 1) |
335 | 311 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 𝑝 ≠ 0) |
336 | 195, 312,
335, 138 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < (𝐹‘𝑝)) |
337 | | expgt0 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹‘𝑝) ∈ ℝ ∧ 𝑘 ∈ ℤ ∧ 0 < (𝐹‘𝑝)) → 0 < ((𝐹‘𝑝)↑𝑘)) |
338 | 313, 297,
336, 337 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 < ((𝐹‘𝑝)↑𝑘)) |
339 | | lemul2 10876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑏) ∈ ℝ ∧ 1 ∈ ℝ ∧
(((𝐹‘𝑝)↑𝑘) ∈ ℝ ∧ 0 < ((𝐹‘𝑝)↑𝑘))) → ((𝐹‘𝑏) ≤ 1 ↔ (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1))) |
340 | 329, 296,
327, 338, 339 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑏) ≤ 1 ↔ (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1))) |
341 | 334, 340 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (((𝐹‘𝑝)↑𝑘) · 1)) |
342 | 327 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ∈ ℂ) |
343 | 342 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · 1) = ((𝐹‘𝑝)↑𝑘)) |
344 | 341, 343 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ ((𝐹‘𝑝)↑𝑘)) |
345 | 141 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ∈
ℝ+) |
346 | 345 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → 0 ≤ (𝐹‘𝑝)) |
347 | | max2 12018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹‘𝑃) ∈ ℝ ∧ (𝐹‘𝑝) ∈ ℝ) → (𝐹‘𝑝) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
348 | 244, 313,
347 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ≤ if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))) |
349 | 348, 134 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘𝑝) ≤ 𝑆) |
350 | | leexp1a 12919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹‘𝑝) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤
(𝐹‘𝑝) ∧ (𝐹‘𝑝) ≤ 𝑆)) → ((𝐹‘𝑝)↑𝑘) ≤ (𝑆↑𝑘)) |
351 | 313, 308,
239, 346, 349, 350 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘𝑝)↑𝑘) ≤ (𝑆↑𝑘)) |
352 | 330, 327,
224, 344, 351 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝐹‘𝑝)↑𝑘) · (𝐹‘𝑏)) ≤ (𝑆↑𝑘)) |
353 | 326, 352 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘((𝑝↑𝑘) · 𝑏)) ≤ (𝑆↑𝑘)) |
354 | 217, 219,
224, 224, 320, 353 | le2addd 10646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ≤ ((𝑆↑𝑘) + (𝑆↑𝑘))) |
355 | 222 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝑆↑𝑘) ∈ ℂ) |
356 | 355 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 · (𝑆↑𝑘)) = ((𝑆↑𝑘) + (𝑆↑𝑘))) |
357 | 356 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (2 · (𝑆↑𝑘)) = ((𝑆↑𝑘) + (𝑆↑𝑘))) |
358 | 354, 357 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → ((𝐹‘((𝑃↑𝑘) · 𝑎)) + (𝐹‘((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘))) |
359 | 215, 220,
226, 232, 358 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘))) |
360 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 =
(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) = (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)))) |
361 | 360 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 =
(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → ((𝐹‘1) ≤ (2 · (𝑆↑𝑘)) ↔ (𝐹‘(((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏))) ≤ (2 · (𝑆↑𝑘)))) |
362 | 359, 361 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (1 = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
363 | 194, 362 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ (𝑘 ∈ ℕ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ))) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
364 | 363 | anassrs 680 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
365 | 364 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ((𝑃↑𝑘) gcd (𝑝↑𝑘)) = (((𝑃↑𝑘) · 𝑎) + ((𝑝↑𝑘) · 𝑏)) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘)))) |
366 | 179, 365 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (𝐹‘1) ≤ (2 · (𝑆↑𝑘))) |
367 | 168, 366 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → 1 ≤ (2 ·
(𝑆↑𝑘))) |
368 | 222 | rpregt0d 11878 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((𝑆↑𝑘) ∈ ℝ ∧ 0 < (𝑆↑𝑘))) |
369 | | ledivmul2 10902 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ ((𝑆↑𝑘) ∈ ℝ ∧ 0 < (𝑆↑𝑘))) → ((1 / (𝑆↑𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆↑𝑘)))) |
370 | 264, 132,
369 | mp3an12 1414 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆↑𝑘) ∈ ℝ ∧ 0 < (𝑆↑𝑘)) → ((1 / (𝑆↑𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆↑𝑘)))) |
371 | 368, 370 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑆↑𝑘)) ≤ 2 ↔ 1 ≤ (2 · (𝑆↑𝑘)))) |
372 | 367, 371 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (1 / (𝑆↑𝑘)) ≤ 2) |
373 | 163, 372 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ≤ 2) |
374 | | reexpcl 12877 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑆) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((1 / 𝑆)↑𝑘) ∈ ℝ) |
375 | 145, 170,
374 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑆)↑𝑘) ∈ ℝ) |
376 | | lenlt 10116 |
. . . . . . . . . . . . . . 15
⊢ ((((1 /
𝑆)↑𝑘) ∈ ℝ ∧ 2 ∈ ℝ)
→ (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1
/ 𝑆)↑𝑘))) |
377 | 375, 132,
376 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (((1 / 𝑆)↑𝑘) ≤ 2 ↔ ¬ 2 < ((1 / 𝑆)↑𝑘))) |
378 | 373, 377 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → ¬ 2 < ((1 /
𝑆)↑𝑘)) |
379 | 378 | pm2.21d 118 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) ∧ 𝑘 ∈ ℕ) → (2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹‘𝑝) < 1)) |
380 | 379 | rexlimdva 3031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → (∃𝑘 ∈ ℕ 2 < ((1 / 𝑆)↑𝑘) → ¬ (𝐹‘𝑝) < 1)) |
381 | 156, 380 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑃 ≠ 𝑝 ∧ (𝐹‘𝑝) < 1)) → ¬ (𝐹‘𝑝) < 1) |
382 | 381 | expr 643 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐹‘𝑝) < 1 → ¬ (𝐹‘𝑝) < 1)) |
383 | 382 | pm2.01d 181 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ (𝐹‘𝑝) < 1) |
384 | 260 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛)) |
385 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → (𝐹‘𝑛) = (𝐹‘𝑝)) |
386 | 385 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → (1 < (𝐹‘𝑛) ↔ 1 < (𝐹‘𝑝))) |
387 | 386 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑝 → (¬ 1 < (𝐹‘𝑛) ↔ ¬ 1 < (𝐹‘𝑝))) |
388 | 387 | rspcv 3305 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℕ →
(∀𝑛 ∈ ℕ
¬ 1 < (𝐹‘𝑛) → ¬ 1 < (𝐹‘𝑝))) |
389 | 100, 384,
388 | sylc 65 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ¬ 1 < (𝐹‘𝑝)) |
390 | | lttri3 10121 |
. . . . . . . . 9
⊢ (((𝐹‘𝑝) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝐹‘𝑝) = 1 ↔ (¬ (𝐹‘𝑝) < 1 ∧ ¬ 1 < (𝐹‘𝑝)))) |
391 | 137, 264,
390 | sylancl 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → ((𝐹‘𝑝) = 1 ↔ (¬ (𝐹‘𝑝) < 1 ∧ ¬ 1 < (𝐹‘𝑝)))) |
392 | 383, 389,
391 | mpbir2and 957 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) = 1) |
393 | 109, 131,
392 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (((𝐽‘𝑃)‘𝑝)↑𝑐𝑅) = (𝐹‘𝑝)) |
394 | 107, 393 | eqtr2d 2657 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑃 ≠ 𝑝) → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
395 | 394 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑃 ≠ 𝑝 → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝))) |
396 | 98, 395 | pm2.61dne 2880 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = ((𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))‘𝑝)) |
397 | 12, 11, 2, 47, 396 | ostthlem2 25317 |
. 2
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) |
398 | | oveq2 6658 |
. . . . 5
⊢ (𝑎 = 𝑅 → (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎) = (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) |
399 | 398 | mpteq2dv 4745 |
. . . 4
⊢ (𝑎 = 𝑅 → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎)) = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) |
400 | 399 | eqeq2d 2632 |
. . 3
⊢ (𝑎 = 𝑅 → (𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎)) ↔ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)))) |
401 | 400 | rspcev 3309 |
. 2
⊢ ((𝑅 ∈ ℝ+
∧ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅))) → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎))) |
402 | 44, 397, 401 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎))) |