Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (0...(𝑃 − 1)) ∈ Fin) |
2 | | 4sqlem11.5 |
. . . . . . . 8
⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} |
3 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ) |
4 | | zsqcl 12934 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℤ → (𝑚↑2) ∈
ℤ) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → (𝑚↑2) ∈ ℤ) |
6 | | 4sq.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
7 | | prmnn 15388 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | | zmodfz 12692 |
. . . . . . . . . . . 12
⊢ (((𝑚↑2) ∈ ℤ ∧
𝑃 ∈ ℕ) →
((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))) |
10 | 5, 8, 9 | syl2anr 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))) |
11 | | eleq1a 2696 |
. . . . . . . . . . 11
⊢ (((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1)))) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1)))) |
13 | 12 | rexlimdva 3031 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1)))) |
14 | 13 | abssdv 3676 |
. . . . . . . 8
⊢ (𝜑 → {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ⊆ (0...(𝑃 − 1))) |
15 | 2, 14 | syl5eqss 3649 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ (0...(𝑃 − 1))) |
16 | | prmz 15389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℤ) |
18 | | peano2zm 11420 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
20 | 19 | zcnd 11483 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
21 | 20 | addid2d 10237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + (𝑃 − 1)) = (𝑃 − 1)) |
22 | 21 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣)) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣)) |
24 | 15 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ (0...(𝑃 − 1))) |
25 | | fzrev3i 12407 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (0...(𝑃 − 1)) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1))) |
27 | 23, 26 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1))) |
28 | | 4sqlem11.6 |
. . . . . . . . 9
⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)) |
29 | 27, 28 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶(0...(𝑃 − 1))) |
30 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(0...(𝑃 − 1)) → ran 𝐹 ⊆ (0...(𝑃 − 1))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ (0...(𝑃 − 1))) |
32 | 15, 31 | unssd 3789 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1))) |
33 | | ssdomg 8001 |
. . . . . 6
⊢
((0...(𝑃 − 1))
∈ Fin → ((𝐴 ∪
ran 𝐹) ⊆ (0...(𝑃 − 1)) → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))) |
34 | 1, 32, 33 | sylc 65 |
. . . . 5
⊢ (𝜑 → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))) |
35 | | ssfi 8180 |
. . . . . . 7
⊢
(((0...(𝑃 −
1)) ∈ Fin ∧ (𝐴
∪ ran 𝐹) ⊆
(0...(𝑃 − 1))) →
(𝐴 ∪ ran 𝐹) ∈ Fin) |
36 | 1, 32, 35 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∪ ran 𝐹) ∈ Fin) |
37 | | hashdom 13168 |
. . . . . 6
⊢ (((𝐴 ∪ ran 𝐹) ∈ Fin ∧ (0...(𝑃 − 1)) ∈ Fin) →
((#‘(𝐴 ∪ ran
𝐹)) ≤
(#‘(0...(𝑃 −
1))) ↔ (𝐴 ∪ ran
𝐹) ≼ (0...(𝑃 − 1)))) |
38 | 36, 1, 37 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((#‘(𝐴 ∪ ran 𝐹)) ≤ (#‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))) |
39 | 34, 38 | mpbird 247 |
. . . 4
⊢ (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ≤ (#‘(0...(𝑃 − 1)))) |
40 | | fz01en 12369 |
. . . . . . 7
⊢ (𝑃 ∈ ℤ →
(0...(𝑃 − 1)) ≈
(1...𝑃)) |
41 | 17, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0...(𝑃 − 1)) ≈ (1...𝑃)) |
42 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (1...𝑃) ∈ Fin) |
43 | | hashen 13135 |
. . . . . . 7
⊢
(((0...(𝑃 −
1)) ∈ Fin ∧ (1...𝑃) ∈ Fin) → ((#‘(0...(𝑃 − 1))) =
(#‘(1...𝑃)) ↔
(0...(𝑃 − 1)) ≈
(1...𝑃))) |
44 | 1, 42, 43 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((#‘(0...(𝑃 − 1))) =
(#‘(1...𝑃)) ↔
(0...(𝑃 − 1)) ≈
(1...𝑃))) |
45 | 41, 44 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (#‘(0...(𝑃 − 1))) =
(#‘(1...𝑃))) |
46 | 8 | nnnn0d 11351 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
47 | | hashfz1 13134 |
. . . . . 6
⊢ (𝑃 ∈ ℕ0
→ (#‘(1...𝑃)) =
𝑃) |
48 | 46, 47 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘(1...𝑃)) = 𝑃) |
49 | 45, 48 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (#‘(0...(𝑃 − 1))) = 𝑃) |
50 | 39, 49 | breqtrd 4679 |
. . 3
⊢ (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃) |
51 | | hashcl 13147 |
. . . . . 6
⊢ ((𝐴 ∪ ran 𝐹) ∈ Fin → (#‘(𝐴 ∪ ran 𝐹)) ∈
ℕ0) |
52 | 36, 51 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ∈
ℕ0) |
53 | 52 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ∈ ℝ) |
54 | 17 | zred 11482 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℝ) |
55 | 53, 54 | lenltd 10183 |
. . 3
⊢ (𝜑 → ((#‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃 ↔ ¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹)))) |
56 | 50, 55 | mpbid 222 |
. 2
⊢ (𝜑 → ¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹))) |
57 | 54 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 ∈ ℝ) |
58 | 57 | ltp1d 10954 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (𝑃 + 1)) |
59 | | 4sq.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
60 | 59 | nncnd 11036 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
61 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
62 | 60, 60, 61, 61 | add4d 10264 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + 𝑁) + (1 + 1)) = ((𝑁 + 1) + (𝑁 + 1))) |
63 | | 4sq.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
64 | 63 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 + 1) = (((2 · 𝑁) + 1) + 1)) |
65 | | 2cn 11091 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
66 | | mulcl 10020 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → (2 · 𝑁) ∈ ℂ) |
67 | 65, 60, 66 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
68 | 67, 61, 61 | addassd 10062 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1))) |
69 | 60 | 2timesd 11275 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁)) |
70 | 69 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁) + (1 + 1)) = ((𝑁 + 𝑁) + (1 + 1))) |
71 | 64, 68, 70 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 + 1) = ((𝑁 + 𝑁) + (1 + 1))) |
72 | 10 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑚 ∈ (0...𝑁) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))) |
73 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℕ) |
74 | 3 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℤ) |
75 | 74, 4 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚↑2) ∈ ℤ) |
76 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 ∈ (0...𝑁) → 𝑢 ∈ ℤ) |
77 | 76 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℤ) |
78 | | zsqcl 12934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ ℤ → (𝑢↑2) ∈
ℤ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢↑2) ∈ ℤ) |
80 | | moddvds 14991 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧
(𝑢↑2) ∈ ℤ)
→ (((𝑚↑2) mod
𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2)))) |
81 | 73, 75, 79, 80 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2)))) |
82 | 74 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℂ) |
83 | 77 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℂ) |
84 | | subsq 12972 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚 − 𝑢))) |
85 | 82, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚 − 𝑢))) |
86 | 85 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚↑2) − (𝑢↑2)) ↔ 𝑃 ∥ ((𝑚 + 𝑢) · (𝑚 − 𝑢)))) |
87 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℙ) |
88 | 74, 77 | zaddcld 11486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℤ) |
89 | 74, 77 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 𝑢) ∈ ℤ) |
90 | | euclemma 15425 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℙ ∧ (𝑚 + 𝑢) ∈ ℤ ∧ (𝑚 − 𝑢) ∈ ℤ) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚 − 𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚 − 𝑢)))) |
91 | 87, 88, 89, 90 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚 − 𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚 − 𝑢)))) |
92 | 81, 86, 91 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚 − 𝑢)))) |
93 | 88 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℝ) |
94 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℝ |
95 | 59 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℝ) |
96 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
97 | 94, 95, 96 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
98 | 97 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) ∈ ℝ) |
99 | 87, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℤ) |
100 | 99 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℝ) |
101 | 74 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℝ) |
102 | 77 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℝ) |
103 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℝ) |
104 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ≤ 𝑁) |
105 | 104 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ≤ 𝑁) |
106 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 ∈ (0...𝑁) → 𝑢 ≤ 𝑁) |
107 | 106 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ≤ 𝑁) |
108 | 101, 102,
103, 103, 105, 107 | le2addd 10646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (𝑁 + 𝑁)) |
109 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℂ) |
110 | 109 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) = (𝑁 + 𝑁)) |
111 | 108, 110 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (2 · 𝑁)) |
112 | 97 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2 · 𝑁) < ((2 · 𝑁) + 1)) |
113 | 112, 63 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (2 · 𝑁) < 𝑃) |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) < 𝑃) |
115 | 93, 98, 100, 111, 114 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) < 𝑃) |
116 | 93, 100 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 + 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑚 + 𝑢))) |
117 | 115, 116 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (𝑚 + 𝑢)) |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → ¬ 𝑃 ≤ (𝑚 + 𝑢)) |
119 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 𝑃 ∈ ℤ) |
120 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑚 + 𝑢) ∈ ℤ) |
121 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 1 ∈ ℝ) |
122 | | nn0abscl 14052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 − 𝑢) ∈ ℤ → (abs‘(𝑚 − 𝑢)) ∈
ℕ0) |
123 | 89, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 𝑢)) ∈
ℕ0) |
124 | 123 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 𝑢)) ∈ ℝ) |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ∈ ℝ) |
126 | 120 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑚 + 𝑢) ∈ ℝ) |
127 | 123 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ∈
ℕ0) |
128 | 127 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ∈ ℤ) |
129 | 89 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 𝑢) ∈ ℂ) |
130 | 129 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑚 − 𝑢) ∈ ℂ) |
131 | 82, 83 | subeq0ad 10402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 − 𝑢) = 0 ↔ 𝑚 = 𝑢)) |
132 | 131 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 − 𝑢) ≠ 0 ↔ 𝑚 ≠ 𝑢)) |
133 | 132 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑚 − 𝑢) ≠ 0) |
134 | 130, 133 | absrpcld 14187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ∈
ℝ+) |
135 | 134 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 0 < (abs‘(𝑚 − 𝑢))) |
136 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((abs‘(𝑚
− 𝑢)) ∈ ℕ
↔ ((abs‘(𝑚
− 𝑢)) ∈ ℤ
∧ 0 < (abs‘(𝑚
− 𝑢)))) |
137 | 128, 135,
136 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ∈ ℕ) |
138 | 137 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 1 ≤ (abs‘(𝑚 − 𝑢))) |
139 | | 0cnd 10033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ∈
ℂ) |
140 | 82, 83, 139 | abs3difd 14199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 𝑢)) ≤ ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢)))) |
141 | 82 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 0) = 𝑚) |
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = (abs‘𝑚)) |
143 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚) |
144 | 143 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑚) |
145 | 101, 144 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑚) = 𝑚) |
146 | 142, 145 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = 𝑚) |
147 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 0 ∈
ℂ |
148 | | abssub 14066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((0
∈ ℂ ∧ 𝑢
∈ ℂ) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0))) |
149 | 147, 83, 148 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0))) |
150 | 83 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢 − 0) = 𝑢) |
151 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑢 − 0)) = (abs‘𝑢)) |
152 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑢 ∈ (0...𝑁) → 0 ≤ 𝑢) |
153 | 152 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑢) |
154 | 102, 153 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑢) = 𝑢) |
155 | 149, 151,
154 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = 𝑢) |
156 | 146, 155 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))) = (𝑚 + 𝑢)) |
157 | 140, 156 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 𝑢)) ≤ (𝑚 + 𝑢)) |
158 | 157 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (abs‘(𝑚 − 𝑢)) ≤ (𝑚 + 𝑢)) |
159 | 121, 125,
126, 138, 158 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 1 ≤ (𝑚 + 𝑢)) |
160 | | elnnz1 11403 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑚 + 𝑢) ∈ ℕ ↔ ((𝑚 + 𝑢) ∈ ℤ ∧ 1 ≤ (𝑚 + 𝑢))) |
161 | 120, 159,
160 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑚 + 𝑢) ∈ ℕ) |
162 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ ℤ ∧ (𝑚 + 𝑢) ∈ ℕ) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢))) |
163 | 119, 161,
162 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢))) |
164 | 118, 163 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → ¬ 𝑃 ∥ (𝑚 + 𝑢)) |
165 | 164 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 ≠ 𝑢 → ¬ 𝑃 ∥ (𝑚 + 𝑢))) |
166 | 165 | necon4ad 2813 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑚 = 𝑢)) |
167 | | dvdsabsb 15001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℤ ∧ (𝑚 − 𝑢) ∈ ℤ) → (𝑃 ∥ (𝑚 − 𝑢) ↔ 𝑃 ∥ (abs‘(𝑚 − 𝑢)))) |
168 | 99, 89, 167 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 − 𝑢) ↔ 𝑃 ∥ (abs‘(𝑚 − 𝑢)))) |
169 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℝ ∧
(abs‘(𝑚 − 𝑢)) ∈ ℝ ∧ (𝑚 + 𝑢) ∈ ℝ) → ((𝑃 ≤ (abs‘(𝑚 − 𝑢)) ∧ (abs‘(𝑚 − 𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢))) |
170 | 100, 124,
93, 169 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ≤ (abs‘(𝑚 − 𝑢)) ∧ (abs‘(𝑚 − 𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢))) |
171 | 157, 170 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ≤ (abs‘(𝑚 − 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢))) |
172 | 117, 171 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (abs‘(𝑚 − 𝑢))) |
173 | 172 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → ¬ 𝑃 ≤ (abs‘(𝑚 − 𝑢))) |
174 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → 𝑃 ∈ ℤ) |
175 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℤ ∧
(abs‘(𝑚 − 𝑢)) ∈ ℕ) → (𝑃 ∥ (abs‘(𝑚 − 𝑢)) → 𝑃 ≤ (abs‘(𝑚 − 𝑢)))) |
176 | 174, 137,
175 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → (𝑃 ∥ (abs‘(𝑚 − 𝑢)) → 𝑃 ≤ (abs‘(𝑚 − 𝑢)))) |
177 | 173, 176 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚 ≠ 𝑢) → ¬ 𝑃 ∥ (abs‘(𝑚 − 𝑢))) |
178 | 177 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 ≠ 𝑢 → ¬ 𝑃 ∥ (abs‘(𝑚 − 𝑢)))) |
179 | 178 | necon4ad 2813 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (abs‘(𝑚 − 𝑢)) → 𝑚 = 𝑢)) |
180 | 168, 179 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 − 𝑢) → 𝑚 = 𝑢)) |
181 | 166, 180 | jaod 395 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚 − 𝑢)) → 𝑚 = 𝑢)) |
182 | 92, 181 | sylbid 230 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) → 𝑚 = 𝑢)) |
183 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑢 → (𝑚↑2) = (𝑢↑2)) |
184 | 183 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑢 → ((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃)) |
185 | 182, 184 | impbid1 215 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢)) |
186 | 185 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁)) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢))) |
187 | 72, 186 | dom2lem 7995 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1))) |
188 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)) → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran
(𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran
(𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))) |
190 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) |
191 | 190 | rnmpt 5371 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} |
192 | 2, 191 | eqtr4i 2647 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) |
193 | | f1oeq3 6129 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) → ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran
(𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))) |
194 | 192, 193 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran
(𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))) |
195 | 189, 194 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→𝐴) |
196 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢
(0...𝑁) ∈
V |
197 | 196 | f1oen 7976 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→𝐴 → (0...𝑁) ≈ 𝐴) |
198 | 195, 197 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...𝑁) ≈ 𝐴) |
199 | 198 | ensymd 8007 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≈ (0...𝑁)) |
200 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
201 | | pncan 10287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
202 | 60, 200, 201 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
203 | 202 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
204 | 59 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
205 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
207 | 206 | nn0zd 11480 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
208 | | fz01en 12369 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + 1) ∈ ℤ →
(0...((𝑁 + 1) − 1))
≈ (1...(𝑁 +
1))) |
209 | 207, 208 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1))) |
210 | 203, 209 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...𝑁) ≈ (1...(𝑁 + 1))) |
211 | | entr 8008 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≈ (0...𝑁) ∧ (0...𝑁) ≈ (1...(𝑁 + 1))) → 𝐴 ≈ (1...(𝑁 + 1))) |
212 | 199, 210,
211 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≈ (1...(𝑁 + 1))) |
213 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢
(((0...(𝑃 −
1)) ∈ Fin ∧ 𝐴
⊆ (0...(𝑃 −
1))) → 𝐴 ∈
Fin) |
214 | 1, 15, 213 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
215 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...(𝑁 + 1)) ∈ Fin) |
216 | | hashen 13135 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) →
((#‘𝐴) =
(#‘(1...(𝑁 + 1)))
↔ 𝐴 ≈
(1...(𝑁 +
1)))) |
217 | 214, 215,
216 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴) = (#‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1)))) |
218 | 212, 217 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐴) = (#‘(1...(𝑁 + 1)))) |
219 | | hashfz1 13134 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℕ0
→ (#‘(1...(𝑁 +
1))) = (𝑁 +
1)) |
220 | 206, 219 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(1...(𝑁 + 1))) = (𝑁 + 1)) |
221 | 218, 220 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐴) = (𝑁 + 1)) |
222 | 27 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑣 ∈ 𝐴 → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1)))) |
223 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴)) → (𝑃 − 1) ∈ ℂ) |
224 | | fzssuz 12382 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0...(𝑃 − 1))
⊆ (ℤ≥‘0) |
225 | | uzssz 11707 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℤ≥‘0) ⊆ ℤ |
226 | | zsscn 11385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℤ
⊆ ℂ |
227 | 225, 226 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘0) ⊆ ℂ |
228 | 224, 227 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0...(𝑃 − 1))
⊆ ℂ |
229 | 15, 228 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
230 | 229 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ ℂ) |
231 | 230 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴)) → 𝑣 ∈ ℂ) |
232 | 229 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ) |
233 | 232 | adantrl 752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℂ) |
234 | 223, 231,
233 | subcanad 10435 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴)) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘)) |
235 | 234 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘))) |
236 | 222, 235 | dom2lem 7995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴–1-1→(0...(𝑃 − 1))) |
237 | | f1eq1 6096 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)) → (𝐹:𝐴–1-1→(0...(𝑃 − 1)) ↔ (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴–1-1→(0...(𝑃 − 1)))) |
238 | 28, 237 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴–1-1→(0...(𝑃 − 1)) ↔ (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴–1-1→(0...(𝑃 − 1))) |
239 | 236, 238 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐴–1-1→(0...(𝑃 − 1))) |
240 | | f1f1orn 6148 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴–1-1→(0...(𝑃 − 1)) → 𝐹:𝐴–1-1-onto→ran
𝐹) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
242 | | f1oeng 7974 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→ran
𝐹) → 𝐴 ≈ ran 𝐹) |
243 | 214, 241,
242 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≈ ran 𝐹) |
244 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢
(((0...(𝑃 −
1)) ∈ Fin ∧ ran 𝐹
⊆ (0...(𝑃 −
1))) → ran 𝐹 ∈
Fin) |
245 | 1, 31, 244 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
246 | | hashen 13135 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin) →
((#‘𝐴) = (#‘ran
𝐹) ↔ 𝐴 ≈ ran 𝐹)) |
247 | 214, 245,
246 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴) = (#‘ran 𝐹) ↔ 𝐴 ≈ ran 𝐹)) |
248 | 243, 247 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐴) = (#‘ran 𝐹)) |
249 | 248, 221 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (𝜑 → (#‘ran 𝐹) = (𝑁 + 1)) |
250 | 221, 249 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) + (#‘ran 𝐹)) = ((𝑁 + 1) + (𝑁 + 1))) |
251 | 62, 71, 250 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (𝜑 → (𝑃 + 1) = ((#‘𝐴) + (#‘ran 𝐹))) |
252 | 251 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = ((#‘𝐴) + (#‘ran 𝐹))) |
253 | 214 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝐴 ∈ Fin) |
254 | 245 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → ran 𝐹 ∈ Fin) |
255 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝐴 ∩ ran 𝐹) = ∅) |
256 | | hashun 13171 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) = ∅) → (#‘(𝐴 ∪ ran 𝐹)) = ((#‘𝐴) + (#‘ran 𝐹))) |
257 | 253, 254,
255, 256 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (#‘(𝐴 ∪ ran 𝐹)) = ((#‘𝐴) + (#‘ran 𝐹))) |
258 | 252, 257 | eqtr4d 2659 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = (#‘(𝐴 ∪ ran 𝐹))) |
259 | 58, 258 | breqtrd 4679 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (#‘(𝐴 ∪ ran 𝐹))) |
260 | 259 | ex 450 |
. . 3
⊢ (𝜑 → ((𝐴 ∩ ran 𝐹) = ∅ → 𝑃 < (#‘(𝐴 ∪ ran 𝐹)))) |
261 | 260 | necon3bd 2808 |
. 2
⊢ (𝜑 → (¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹)) → (𝐴 ∩ ran 𝐹) ≠ ∅)) |
262 | 56, 261 | mpd 15 |
1
⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅) |