Proof of Theorem gausslemma2dlem3
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
2 | | oveq1 5917 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
3 | 2 | breq1d 4039 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
4 | 2 | oveq2d 5926 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
5 | 3, 2, 4 | ifbieq12d 3583 |
. . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
6 | 5 | adantl 277 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
7 | | gausslemma2d.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
8 | 7 | gausslemma2dlem0a 15107 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | | elfz2 10071 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻))) |
10 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
11 | 10 | oveq1i 5920 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 + 1) = ((⌊‘(𝑃 / 4)) + 1) |
12 | 11 | breq1i 4036 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 + 1) ≤ 𝑘 ↔ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) |
13 | | nnz 9326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
14 | | 4nn 9135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℕ |
15 | | znq 9679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
16 | 13, 14, 15 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 4) ∈
ℚ) |
17 | 16 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 4) ∈
ℚ) |
18 | | flqlelt 10335 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 / 4) ∈ ℚ →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
20 | | nnre 8979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
21 | | 4re 9049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 4 ∈
ℝ |
22 | 21 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 4 ∈
ℝ) |
23 | | 4ap0 9071 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 4 #
0 |
24 | 23 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 4 #
0) |
25 | 20, 22, 24 | redivclapd 8844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℕ → (𝑃 / 4) ∈
ℝ) |
26 | 25 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 4) ∈
ℝ) |
27 | 16 | flqcld 10336 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℤ) |
28 | 27 | zred 9429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℝ) |
29 | | peano2re 8145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((⌊‘(𝑃 /
4)) ∈ ℝ → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ) |
30 | 28, 29 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℕ →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
31 | 30 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
32 | | zre 9311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
33 | 32 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → 𝑘 ∈
ℝ) |
34 | | ltleletr 8091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 / 4) ∈ ℝ ∧
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ ∧ 𝑘
∈ ℝ) → (((𝑃
/ 4) < ((⌊‘(𝑃 / 4)) + 1) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘)) |
35 | 26, 31, 33, 34 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) ∧ ((⌊‘(𝑃
/ 4)) + 1) ≤ 𝑘) →
(𝑃 / 4) ≤ 𝑘)) |
36 | 35 | expd 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))) |
37 | 36 | adantld 278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
(((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1)) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))) |
38 | 19, 37 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘)) |
39 | 38 | imp 124 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘) |
40 | 20 | rehalfcld 9219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
41 | 40 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
42 | | 2re 9042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ |
43 | 42 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℤ → 2 ∈
ℝ) |
44 | 32, 43 | remulcld 8040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → (𝑘 · 2) ∈
ℝ) |
45 | 44 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) |
46 | | 2pos 9063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
47 | 42, 46 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
48 | 47 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) |
49 | | lediv1 8878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
50 | 41, 45, 48, 49 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
51 | | nncn 8980 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
52 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 2 ∈
ℂ) |
53 | | 2ap0 9065 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 #
0 |
54 | 53 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 2 #
0) |
55 | 51, 52, 52, 54, 54 | divdivap1d 8831 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2))) |
56 | | 2t2e4 9126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 2) = 4 |
57 | 56 | oveq2i 5921 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 / (2 · 2)) = (𝑃 / 4) |
58 | 55, 57 | eqtrdi 2242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / 4)) |
59 | | zcn 9312 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
60 | | 2cnd 9045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 ∈
ℂ) |
61 | 53 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 #
0) |
62 | 59, 60, 61 | divcanap4d 8805 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) / 2) = 𝑘) |
63 | 58, 62 | breqan12rd 4046 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
64 | 50, 63 | bitrd 188 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
65 | 64 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
66 | 39, 65 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → (𝑃 / 2) ≤ (𝑘 · 2)) |
67 | 66 | exp31 364 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (𝑃 ∈ ℕ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 / 2) ≤ (𝑘 · 2)))) |
68 | 67 | com23 78 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
69 | 12, 68 | biimtrid 152 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
70 | 69 | 3ad2ant3 1022 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
71 | 70 | com12 30 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) ≤ 𝑘 → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
72 | 71 | adantr 276 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻) → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
73 | 72 | impcom 125 |
. . . . . . . . . 10
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻)) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
74 | 9, 73 | sylbi 121 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
75 | 74 | impcom 125 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 / 2) ≤ (𝑘 · 2)) |
76 | | elfzelz 10081 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
77 | 76 | zred 9429 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℝ) |
78 | 42 | a1i 9 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℝ) |
79 | 77, 78 | remulcld 8040 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℝ) |
80 | | lenlt 8085 |
. . . . . . . . 9
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑘 · 2) ↔
¬ (𝑘 · 2) <
(𝑃 / 2))) |
81 | 40, 79, 80 | syl2an 289 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ¬ (𝑘 · 2) < (𝑃 / 2))) |
82 | 75, 81 | mpbid 147 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
83 | 8, 82 | sylan 283 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
84 | 83 | adantr 276 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
85 | 84 | iffalsed 3567 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑃 − (𝑘 · 2))) |
86 | 6, 85 | eqtrd 2226 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑘 · 2))) |
87 | 7, 10 | gausslemma2dlem0d 15110 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
88 | | nn0p1nn 9269 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
89 | | nnuz 9618 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
90 | 88, 89 | eleqtrdi 2286 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
(ℤ≥‘1)) |
91 | 87, 90 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
92 | | fzss1 10119 |
. . . . 5
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
93 | 91, 92 | syl 14 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
94 | 93 | sselda 3179 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ (1...𝐻)) |
95 | 8 | nnzd 9428 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℤ) |
96 | 95 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑃 ∈ ℤ) |
97 | 76 | adantl 277 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ ℤ) |
98 | | 2z 9335 |
. . . . . 6
⊢ 2 ∈
ℤ |
99 | 98 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 2 ∈ ℤ) |
100 | 97, 99 | zmulcld 9435 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℤ) |
101 | 96, 100 | zsubcld 9434 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
102 | 1, 86, 94, 101 | fvmptd2 5631 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
103 | 102 | ralrimiva 2567 |
1
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |