Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | 1 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ (ℙ ∖
{2})) |
3 | | gausslemma2d.h |
. . . . . . . . 9
⊢ 𝐻 = ((𝑃 − 1) / 2) |
4 | | gausslemma2d.r |
. . . . . . . . 9
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
5 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 𝑥 ∈ (1...𝐻)) |
6 | 2, 3, 4, 5 | gausslemma2dlem1cl 15117 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ∈
ℤ) |
7 | 6 | ralrimiva 2567 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐻)if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ∈
ℤ) |
8 | 4 | fnmpt 5372 |
. . . . . . 7
⊢
(∀𝑥 ∈
(1...𝐻)if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ∈ ℤ → 𝑅 Fn (1...𝐻)) |
9 | 7, 8 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn (1...𝐻)) |
10 | | dffn4 5474 |
. . . . . 6
⊢ (𝑅 Fn (1...𝐻) ↔ 𝑅:(1...𝐻)–onto→ran 𝑅) |
11 | 9, 10 | sylib 122 |
. . . . 5
⊢ (𝜑 → 𝑅:(1...𝐻)–onto→ran 𝑅) |
12 | 1, 3, 4 | gausslemma2dlem1a 15116 |
. . . . . 6
⊢ (𝜑 → ran 𝑅 = (1...𝐻)) |
13 | | foeq3 5466 |
. . . . . 6
⊢ (ran
𝑅 = (1...𝐻) → (𝑅:(1...𝐻)–onto→ran 𝑅 ↔ 𝑅:(1...𝐻)–onto→(1...𝐻))) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑅:(1...𝐻)–onto→ran 𝑅 ↔ 𝑅:(1...𝐻)–onto→(1...𝐻))) |
15 | 11, 14 | mpbid 147 |
. . . 4
⊢ (𝜑 → 𝑅:(1...𝐻)–onto→(1...𝐻)) |
16 | | fof 5468 |
. . . 4
⊢ (𝑅:(1...𝐻)–onto→(1...𝐻) → 𝑅:(1...𝐻)⟶(1...𝐻)) |
17 | 15, 16 | syl 14 |
. . 3
⊢ (𝜑 → 𝑅:(1...𝐻)⟶(1...𝐻)) |
18 | | simprl 529 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑦 ∈ (1...𝐻)) |
19 | 18 | elfzelzd 10082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑦 ∈ ℤ) |
20 | 19 | adantr 276 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → 𝑦 ∈ ℤ) |
21 | 20 | adantr 276 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 𝑦 ∈ ℤ) |
22 | 21 | zcnd 9430 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 𝑦 ∈ ℂ) |
23 | | simprr 531 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑧 ∈ (1...𝐻)) |
24 | 23 | elfzelzd 10082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑧 ∈ ℤ) |
25 | 24 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 𝑧 ∈ ℤ) |
26 | 25 | zcnd 9430 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 𝑧 ∈ ℂ) |
27 | | 2cnd 9045 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 2 ∈
ℂ) |
28 | | 2ap0 9065 |
. . . . . . . 8
⊢ 2 #
0 |
29 | 28 | a1i 9 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 2 # 0) |
30 | | simplr 528 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = (𝑅‘𝑧)) |
31 | | oveq1 5917 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 · 2) = (𝑦 · 2)) |
32 | 31 | breq1d 4039 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑦 · 2) < (𝑃 / 2))) |
33 | 31 | oveq2d 5926 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑦 · 2))) |
34 | 32, 31, 33 | ifbieq12d 3583 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) |
35 | 1 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑃 ∈ (ℙ ∖
{2})) |
36 | 35, 3, 4, 18 | gausslemma2dlem1cl 15117 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2))) ∈
ℤ) |
37 | 4, 34, 18, 36 | fvmptd3 5643 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑅‘𝑦) = if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) |
38 | 37 | ad2antrr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) |
39 | | simpr 110 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑦 · 2) < (𝑃 / 2)) |
40 | 39 | iftrued 3564 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2))) = (𝑦 · 2)) |
41 | 38, 40 | eqtrd 2226 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = (𝑦 · 2)) |
42 | | oveq1 5917 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 · 2) = (𝑧 · 2)) |
43 | 42 | breq1d 4039 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑧 · 2) < (𝑃 / 2))) |
44 | 42 | oveq2d 5926 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑧 · 2))) |
45 | 43, 42, 44 | ifbieq12d 3583 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
46 | 35, 3, 4, 23 | gausslemma2dlem1cl 15117 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2))) ∈
ℤ) |
47 | 4, 45, 23, 46 | fvmptd3 5643 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑅‘𝑧) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
48 | 47 | ad2antrr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
49 | | 2z 9335 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
50 | | dvdsmul2 11944 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ 2 ∈
ℤ) → 2 ∥ (𝑦 · 2)) |
51 | 19, 49, 50 | sylancl 413 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 2 ∥ (𝑦 · 2)) |
52 | 51 | ad2antrr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 2 ∥ (𝑦 · 2)) |
53 | 52, 41 | breqtrrd 4057 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 2 ∥ (𝑅‘𝑦)) |
54 | 53 | adantr 276 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → 2 ∥ (𝑅‘𝑦)) |
55 | | eldifi 3281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
56 | | prmz 12236 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
57 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
58 | 35, 57 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑃 ∈ ℤ) |
59 | | oddn2prm 12386 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 2 ∥ 𝑃) |
60 | 1, 59 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ 2 ∥ 𝑃) |
61 | 60 | adantr 276 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → ¬ 2 ∥ 𝑃) |
62 | 49 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 2 ∈
ℤ) |
63 | 24, 62 | zmulcld 9435 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑧 · 2) ∈ ℤ) |
64 | | dvdsmul2 11944 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 2 ∈
ℤ) → 2 ∥ (𝑧 · 2)) |
65 | 24, 49, 64 | sylancl 413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 2 ∥ (𝑧 · 2)) |
66 | | omeo 12026 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ ((𝑧 · 2) ∈ ℤ
∧ 2 ∥ (𝑧 ·
2))) → ¬ 2 ∥ (𝑃 − (𝑧 · 2))) |
67 | 58, 61, 63, 65, 66 | syl22anc 1250 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → ¬ 2 ∥ (𝑃 − (𝑧 · 2))) |
68 | 67 | adantr 276 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑃 − (𝑧 · 2))) |
69 | 47 | adantr 276 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
70 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → ¬ (𝑧 · 2) < (𝑃 / 2)) |
71 | 70 | iffalsed 3567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2))) = (𝑃 − (𝑧 · 2))) |
72 | 69, 71 | eqtrd 2226 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = (𝑃 − (𝑧 · 2))) |
73 | 72 | breq2d 4041 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → (2 ∥ (𝑅‘𝑧) ↔ 2 ∥ (𝑃 − (𝑧 · 2)))) |
74 | 68, 73 | mtbird 674 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑅‘𝑧)) |
75 | 74 | ad4ant14 514 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑅‘𝑧)) |
76 | | simpr 110 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → (𝑅‘𝑦) = (𝑅‘𝑧)) |
77 | 76 | breq2d 4041 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → (2 ∥ (𝑅‘𝑦) ↔ 2 ∥ (𝑅‘𝑧))) |
78 | 77 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → (2 ∥ (𝑅‘𝑦) ↔ 2 ∥ (𝑅‘𝑧))) |
79 | 75, 78 | mtbird 674 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) ∧ ¬ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑅‘𝑦)) |
80 | 54, 79 | pm2.65da 662 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → ¬ ¬ (𝑧 · 2) < (𝑃 / 2)) |
81 | | zq 9681 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 · 2) ∈ ℤ
→ (𝑧 · 2)
∈ ℚ) |
82 | 63, 81 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑧 · 2) ∈ ℚ) |
83 | 1, 57 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
84 | | 2nn 9133 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
85 | | znq 9679 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 / 2)
∈ ℚ) |
86 | 83, 84, 85 | sylancl 413 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 / 2) ∈ ℚ) |
87 | 86 | adantr 276 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑃 / 2) ∈ ℚ) |
88 | | qdclt 10305 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 · 2) ∈ ℚ
∧ (𝑃 / 2) ∈
ℚ) → DECID (𝑧 · 2) < (𝑃 / 2)) |
89 | 82, 87, 88 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → DECID (𝑧 · 2) < (𝑃 / 2)) |
90 | | exmiddc 837 |
. . . . . . . . . . . . 13
⊢
(DECID (𝑧 · 2) < (𝑃 / 2) → ((𝑧 · 2) < (𝑃 / 2) ∨ ¬ (𝑧 · 2) < (𝑃 / 2))) |
91 | 89, 90 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → ((𝑧 · 2) < (𝑃 / 2) ∨ ¬ (𝑧 · 2) < (𝑃 / 2))) |
92 | 91 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → ((𝑧 · 2) < (𝑃 / 2) ∨ ¬ (𝑧 · 2) < (𝑃 / 2))) |
93 | 80, 92 | ecased 1360 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑧 · 2) < (𝑃 / 2)) |
94 | 93 | iftrued 3564 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2))) = (𝑧 · 2)) |
95 | 48, 94 | eqtrd 2226 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = (𝑧 · 2)) |
96 | 30, 41, 95 | 3eqtr3d 2234 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → (𝑦 · 2) = (𝑧 · 2)) |
97 | 22, 26, 27, 29, 96 | mulcanap2ad 8673 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ (𝑦 · 2) < (𝑃 / 2)) → 𝑦 = 𝑧) |
98 | 19 | zcnd 9430 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑦 ∈ ℂ) |
99 | 98 | ad2antrr 488 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 𝑦 ∈ ℂ) |
100 | 24 | zcnd 9430 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → 𝑧 ∈ ℂ) |
101 | 100 | ad2antrr 488 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 𝑧 ∈ ℂ) |
102 | | 2cnd 9045 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 2 ∈
ℂ) |
103 | 28 | a1i 9 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 2 # 0) |
104 | 83 | zcnd 9430 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℂ) |
105 | 104 | ad3antrrr 492 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 𝑃 ∈ ℂ) |
106 | 19, 62 | zmulcld 9435 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑦 · 2) ∈ ℤ) |
107 | 106 | zcnd 9430 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑦 · 2) ∈ ℂ) |
108 | 107 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑦 · 2) ∈ ℂ) |
109 | 63 | zcnd 9430 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → (𝑧 · 2) ∈ ℂ) |
110 | 109 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑧 · 2) ∈ ℂ) |
111 | | simplr 528 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = (𝑅‘𝑧)) |
112 | 37 | ad2antrr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) |
113 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → ¬ (𝑦 · 2) < (𝑃 / 2)) |
114 | 113 | iffalsed 3567 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2))) = (𝑃 − (𝑦 · 2))) |
115 | 112, 114 | eqtrd 2226 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = (𝑃 − (𝑦 · 2))) |
116 | 47 | ad2antrr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
117 | 65 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → 2 ∥ (𝑧 · 2)) |
118 | 47 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2)))) |
119 | | simpr 110 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (𝑧 · 2) < (𝑃 / 2)) |
120 | 119 | iftrued 3564 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2))) = (𝑧 · 2)) |
121 | 118, 120 | eqtrd 2226 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = (𝑧 · 2)) |
122 | 117, 121 | breqtrrd 4057 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → 2 ∥ (𝑅‘𝑧)) |
123 | 77 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (2 ∥ (𝑅‘𝑦) ↔ 2 ∥ (𝑅‘𝑧))) |
124 | 122, 123 | mpbird 167 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → 2 ∥ (𝑅‘𝑦)) |
125 | | omeo 12026 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ ((𝑦 · 2) ∈ ℤ
∧ 2 ∥ (𝑦 ·
2))) → ¬ 2 ∥ (𝑃 − (𝑦 · 2))) |
126 | 58, 61, 106, 51, 125 | syl22anc 1250 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → ¬ 2 ∥ (𝑃 − (𝑦 · 2))) |
127 | 126 | ad3antrrr 492 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑃 − (𝑦 · 2))) |
128 | 37 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) |
129 | | simplr 528 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → ¬ (𝑦 · 2) < (𝑃 / 2)) |
130 | 129 | iffalsed 3567 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2))) = (𝑃 − (𝑦 · 2))) |
131 | 128, 130 | eqtrd 2226 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (𝑅‘𝑦) = (𝑃 − (𝑦 · 2))) |
132 | 131 | breq2d 4041 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → (2 ∥ (𝑅‘𝑦) ↔ 2 ∥ (𝑃 − (𝑦 · 2)))) |
133 | 127, 132 | mtbird 674 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) ∧ (𝑧 · 2) < (𝑃 / 2)) → ¬ 2 ∥ (𝑅‘𝑦)) |
134 | 124, 133 | pm2.65da 662 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → ¬ (𝑧 · 2) < (𝑃 / 2)) |
135 | 134 | iffalsed 3567 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → if((𝑧 · 2) < (𝑃 / 2), (𝑧 · 2), (𝑃 − (𝑧 · 2))) = (𝑃 − (𝑧 · 2))) |
136 | 116, 135 | eqtrd 2226 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑅‘𝑧) = (𝑃 − (𝑧 · 2))) |
137 | 111, 115,
136 | 3eqtr3d 2234 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑃 − (𝑦 · 2)) = (𝑃 − (𝑧 · 2))) |
138 | 105, 108,
110, 137 | subcand 8361 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → (𝑦 · 2) = (𝑧 · 2)) |
139 | 99, 101, 102, 103, 138 | mulcanap2ad 8673 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) ∧ ¬ (𝑦 · 2) < (𝑃 / 2)) → 𝑦 = 𝑧) |
140 | 49 | a1i 9 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → 2 ∈ ℤ) |
141 | 20, 140 | zmulcld 9435 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → (𝑦 · 2) ∈ ℤ) |
142 | | zq 9681 |
. . . . . . . . 9
⊢ ((𝑦 · 2) ∈ ℤ
→ (𝑦 · 2)
∈ ℚ) |
143 | 141, 142 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → (𝑦 · 2) ∈ ℚ) |
144 | 86 | ad2antrr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → (𝑃 / 2) ∈ ℚ) |
145 | | qdclt 10305 |
. . . . . . . 8
⊢ (((𝑦 · 2) ∈ ℚ
∧ (𝑃 / 2) ∈
ℚ) → DECID (𝑦 · 2) < (𝑃 / 2)) |
146 | 143, 144,
145 | syl2anc 411 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → DECID (𝑦 · 2) < (𝑃 / 2)) |
147 | | exmiddc 837 |
. . . . . . 7
⊢
(DECID (𝑦 · 2) < (𝑃 / 2) → ((𝑦 · 2) < (𝑃 / 2) ∨ ¬ (𝑦 · 2) < (𝑃 / 2))) |
148 | 146, 147 | syl 14 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → ((𝑦 · 2) < (𝑃 / 2) ∨ ¬ (𝑦 · 2) < (𝑃 / 2))) |
149 | 97, 139, 148 | mpjaodan 799 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) ∧ (𝑅‘𝑦) = (𝑅‘𝑧)) → 𝑦 = 𝑧) |
150 | 149 | ex 115 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (1...𝐻) ∧ 𝑧 ∈ (1...𝐻))) → ((𝑅‘𝑦) = (𝑅‘𝑧) → 𝑦 = 𝑧)) |
151 | 150 | ralrimivva 2576 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (1...𝐻)∀𝑧 ∈ (1...𝐻)((𝑅‘𝑦) = (𝑅‘𝑧) → 𝑦 = 𝑧)) |
152 | | dff13 5803 |
. . 3
⊢ (𝑅:(1...𝐻)–1-1→(1...𝐻) ↔ (𝑅:(1...𝐻)⟶(1...𝐻) ∧ ∀𝑦 ∈ (1...𝐻)∀𝑧 ∈ (1...𝐻)((𝑅‘𝑦) = (𝑅‘𝑧) → 𝑦 = 𝑧))) |
153 | 17, 151, 152 | sylanbrc 417 |
. 2
⊢ (𝜑 → 𝑅:(1...𝐻)–1-1→(1...𝐻)) |
154 | | df-f1o 5253 |
. 2
⊢ (𝑅:(1...𝐻)–1-1-onto→(1...𝐻) ↔ (𝑅:(1...𝐻)–1-1→(1...𝐻) ∧ 𝑅:(1...𝐻)–onto→(1...𝐻))) |
155 | 153, 15, 154 | sylanbrc 417 |
1
⊢ (𝜑 → 𝑅:(1...𝐻)–1-1-onto→(1...𝐻)) |