MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem11 Structured version   Visualization version   GIF version

Theorem 4sqlem11 16988
Description: Lemma for 4sq 16997. Use the pigeonhole principle to show that the sets {𝑚↑2 ∣ 𝑚 ∈ (0...𝑁)} and {-1 − 𝑛↑2 ∣ 𝑛 ∈ (0...𝑁)} have a common element, mod 𝑃. (Contributed by Mario Carneiro, 15-Jul-2014.)
Hypotheses
Ref Expression
4sq.1 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
4sq.2 (𝜑𝑁 ∈ ℕ)
4sq.3 (𝜑𝑃 = ((2 · 𝑁) + 1))
4sq.4 (𝜑𝑃 ∈ ℙ)
4sqlem11.5 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
4sqlem11.6 𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣))
Assertion
Ref Expression
4sqlem11 (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧   𝑣,𝑛,𝐴   𝑛,𝐹   𝑢,𝑛,𝑚,𝑣,𝑁   𝑃,𝑚,𝑛,𝑢,𝑣   𝜑,𝑚,𝑛,𝑢,𝑣   𝑆,𝑚,𝑛,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑢,𝑚)   𝑃(𝑥,𝑦,𝑧,𝑤)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑚)   𝑁(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem 4sqlem11
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 fzfid 14010 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ∈ Fin)
2 4sqlem11.5 . . . . . . . 8 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
3 elfzelz 13560 . . . . . . . . . . . . 13 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
4 zsqcl 14165 . . . . . . . . . . . . 13 (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
53, 4syl 17 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑚↑2) ∈ ℤ)
6 4sq.4 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
7 prmnn 16707 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
9 zmodfz 13929 . . . . . . . . . . . 12 (((𝑚↑2) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
105, 8, 9syl2anr 597 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...𝑁)) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
11 eleq1a 2833 . . . . . . . . . . 11 (((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...𝑁)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1312rexlimdva 3152 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1413abssdv 4077 . . . . . . . 8 (𝜑 → {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ⊆ (0...(𝑃 − 1)))
152, 14eqsstrid 4043 . . . . . . 7 (𝜑𝐴 ⊆ (0...(𝑃 − 1)))
16 prmz 16708 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
176, 16syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℤ)
18 peano2zm 12657 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 − 1) ∈ ℤ)
2019zcnd 12720 . . . . . . . . . . . . 13 (𝜑 → (𝑃 − 1) ∈ ℂ)
2120addlidd 11459 . . . . . . . . . . . 12 (𝜑 → (0 + (𝑃 − 1)) = (𝑃 − 1))
2221oveq1d 7445 . . . . . . . . . . 11 (𝜑 → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2322adantr 480 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2415sselda 3994 . . . . . . . . . . 11 ((𝜑𝑣𝐴) → 𝑣 ∈ (0...(𝑃 − 1)))
25 fzrev3i 13627 . . . . . . . . . . 11 (𝑣 ∈ (0...(𝑃 − 1)) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2624, 25syl 17 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2723, 26eqeltrrd 2839 . . . . . . . . 9 ((𝜑𝑣𝐴) → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1)))
28 4sqlem11.6 . . . . . . . . 9 𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣))
2927, 28fmptd 7133 . . . . . . . 8 (𝜑𝐹:𝐴⟶(0...(𝑃 − 1)))
3029frnd 6744 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ (0...(𝑃 − 1)))
3115, 30unssd 4201 . . . . . 6 (𝜑 → (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)))
321, 31ssfid 9298 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ∈ Fin)
33 hashcl 14391 . . . . 5 ((𝐴 ∪ ran 𝐹) ∈ Fin → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3432, 33syl 17 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3534nn0red 12585 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℝ)
3617zred 12719 . . 3 (𝜑𝑃 ∈ ℝ)
37 ssdomg 9038 . . . . . 6 ((0...(𝑃 − 1)) ∈ Fin → ((𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)) → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
381, 31, 37sylc 65 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))
39 hashdom 14414 . . . . . 6 (((𝐴 ∪ ran 𝐹) ∈ Fin ∧ (0...(𝑃 − 1)) ∈ Fin) → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4032, 1, 39syl2anc 584 . . . . 5 (𝜑 → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4138, 40mpbird 257 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))))
42 fz01en 13588 . . . . . . 7 (𝑃 ∈ ℤ → (0...(𝑃 − 1)) ≈ (1...𝑃))
4317, 42syl 17 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ≈ (1...𝑃))
44 fzfid 14010 . . . . . . 7 (𝜑 → (1...𝑃) ∈ Fin)
45 hashen 14382 . . . . . . 7 (((0...(𝑃 − 1)) ∈ Fin ∧ (1...𝑃) ∈ Fin) → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
461, 44, 45syl2anc 584 . . . . . 6 (𝜑 → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
4743, 46mpbird 257 . . . . 5 (𝜑 → (♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)))
488nnnn0d 12584 . . . . . 6 (𝜑𝑃 ∈ ℕ0)
49 hashfz1 14381 . . . . . 6 (𝑃 ∈ ℕ0 → (♯‘(1...𝑃)) = 𝑃)
5048, 49syl 17 . . . . 5 (𝜑 → (♯‘(1...𝑃)) = 𝑃)
5147, 50eqtrd 2774 . . . 4 (𝜑 → (♯‘(0...(𝑃 − 1))) = 𝑃)
5241, 51breqtrd 5173 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃)
5335, 36, 52lensymd 11409 . 2 (𝜑 → ¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
5436adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 ∈ ℝ)
5554ltp1d 12195 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (𝑃 + 1))
56 4sq.2 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
5756nncnd 12279 . . . . . . . . 9 (𝜑𝑁 ∈ ℂ)
58 1cnd 11253 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
5957, 57, 58, 58add4d 11487 . . . . . . . 8 (𝜑 → ((𝑁 + 𝑁) + (1 + 1)) = ((𝑁 + 1) + (𝑁 + 1)))
60 4sq.3 . . . . . . . . . 10 (𝜑𝑃 = ((2 · 𝑁) + 1))
6160oveq1d 7445 . . . . . . . . 9 (𝜑 → (𝑃 + 1) = (((2 · 𝑁) + 1) + 1))
62 2cn 12338 . . . . . . . . . . 11 2 ∈ ℂ
63 mulcl 11236 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
6462, 57, 63sylancr 587 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
6564, 58, 58addassd 11280 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1)))
66572timesd 12506 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
6766oveq1d 7445 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) + (1 + 1)) = ((𝑁 + 𝑁) + (1 + 1)))
6861, 65, 673eqtrd 2778 . . . . . . . 8 (𝜑 → (𝑃 + 1) = ((𝑁 + 𝑁) + (1 + 1)))
6910ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑚 ∈ (0...𝑁) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))))
708adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℕ)
713ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℤ)
7271, 4syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚↑2) ∈ ℤ)
73 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ (0...𝑁) → 𝑢 ∈ ℤ)
7473ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℤ)
75 zsqcl 14165 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ℤ → (𝑢↑2) ∈ ℤ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢↑2) ∈ ℤ)
77 moddvds 16297 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ (𝑢↑2) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7870, 72, 76, 77syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7971zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℂ)
8074zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℂ)
81 subsq 14245 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8279, 80, 81syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8382breq2d 5159 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚↑2) − (𝑢↑2)) ↔ 𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢))))
846adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℙ)
8571, 74zaddcld 12723 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℤ)
8671, 74zsubcld 12724 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℤ)
87 euclemma 16746 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℙ ∧ (𝑚 + 𝑢) ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8884, 85, 86, 87syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8978, 83, 883bitrd 305 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9085zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℝ)
91 2re 12337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
9256nnred 12278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ)
93 remulcl 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
9491, 92, 93sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℝ)
9594adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) ∈ ℝ)
9684, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℤ)
9796zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℝ)
9871zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℝ)
9974zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℝ)
10092adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℝ)
101 elfzle2 13564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚𝑁)
102101ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚𝑁)
103 elfzle2 13564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (0...𝑁) → 𝑢𝑁)
104103ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢𝑁)
10598, 99, 100, 100, 102, 104le2addd 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (𝑁 + 𝑁))
10657adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℂ)
1071062timesd 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) = (𝑁 + 𝑁))
108105, 107breqtrrd 5175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (2 · 𝑁))
10994ltp1d 12195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (2 · 𝑁) < ((2 · 𝑁) + 1))
110109, 60breqtrrd 5175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) < 𝑃)
111110adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) < 𝑃)
11290, 95, 97, 108, 111lelttrd 11416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) < 𝑃)
11390, 97ltnled 11405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 + 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑚 + 𝑢)))
114112, 113mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
115114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
11617ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
11785adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℤ)
118 1red 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ∈ ℝ)
119 nn0abscl 15347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚𝑢) ∈ ℤ → (abs‘(𝑚𝑢)) ∈ ℕ0)
12086, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℕ0)
121120nn0red 12585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℝ)
122121adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ)
123117zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℝ)
124120adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ0)
125124nn0zd 12636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℤ)
12686zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℂ)
127126adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ∈ ℂ)
12879, 80subeq0ad 11627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) = 0 ↔ 𝑚 = 𝑢))
129128necon3bid 2982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) ≠ 0 ↔ 𝑚𝑢))
130129biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ≠ 0)
131127, 130absrpcld 15483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ+)
132131rpgt0d 13077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 0 < (abs‘(𝑚𝑢)))
133 elnnz 12620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((abs‘(𝑚𝑢)) ∈ ℕ ↔ ((abs‘(𝑚𝑢)) ∈ ℤ ∧ 0 < (abs‘(𝑚𝑢))))
134125, 132, 133sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ)
135134nnge1d 12311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (abs‘(𝑚𝑢)))
136 0cnd 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ∈ ℂ)
13779, 80, 136abs3difd 15495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))))
13879subid1d 11606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 0) = 𝑚)
139138fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = (abs‘𝑚))
140 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
141140ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑚)
14298, 141absidd 15457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑚) = 𝑚)
143139, 142eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = 𝑚)
144 0cn 11250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 ∈ ℂ
145 abssub 15361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
146144, 80, 145sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
14780subid1d 11606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢 − 0) = 𝑢)
148147fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑢 − 0)) = (abs‘𝑢))
149 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (0...𝑁) → 0 ≤ 𝑢)
150149ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑢)
15199, 150absidd 15457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑢) = 𝑢)
152146, 148, 1513eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = 𝑢)
153143, 152oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))) = (𝑚 + 𝑢))
154137, 153breqtrd 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
155154adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
156118, 122, 123, 135, 155letrd 11415 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (𝑚 + 𝑢))
157 elnnz1 12640 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 + 𝑢) ∈ ℕ ↔ ((𝑚 + 𝑢) ∈ ℤ ∧ 1 ≤ (𝑚 + 𝑢)))
158117, 156, 157sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℕ)
159 dvdsle 16343 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℤ ∧ (𝑚 + 𝑢) ∈ ℕ) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
160116, 158, 159syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
161115, 160mtod 198 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (𝑚 + 𝑢))
162161ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (𝑚 + 𝑢)))
163162necon4ad 2956 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑚 = 𝑢))
164 dvdsabsb 16309 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
16596, 86, 164syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
166 letr 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (abs‘(𝑚𝑢)) ∈ ℝ ∧ (𝑚 + 𝑢) ∈ ℝ) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
16797, 121, 90, 166syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
168154, 167mpan2d 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ≤ (abs‘(𝑚𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
169114, 168mtod 198 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
170169adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
17196adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
172 dvdsle 16343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (abs‘(𝑚𝑢)) ∈ ℕ) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
173171, 134, 172syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
174170, 173mtod 198 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (abs‘(𝑚𝑢)))
175174ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (abs‘(𝑚𝑢))))
176175necon4ad 2956 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑚 = 𝑢))
177165, 176sylbid 240 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) → 𝑚 = 𝑢))
178163, 177jaod 859 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢)) → 𝑚 = 𝑢))
17989, 178sylbid 240 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) → 𝑚 = 𝑢))
180 oveq1 7437 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑢 → (𝑚↑2) = (𝑢↑2))
181180oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑢 → ((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃))
182179, 181impbid1 225 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢))
183182ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁)) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢)))
18469, 183dom2lem 9030 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)))
185 f1f1orn 6859 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)) → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
186184, 185syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
187 eqid 2734 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
188187rnmpt 5970 . . . . . . . . . . . . . . . . 17 ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
1892, 188eqtr4i 2765 . . . . . . . . . . . . . . . 16 𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
190 f1oeq3 6838 . . . . . . . . . . . . . . . 16 (𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) → ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))))
191189, 190ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
192186, 191sylibr 234 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴)
193 ovex 7463 . . . . . . . . . . . . . . 15 (0...𝑁) ∈ V
194193f1oen 9011 . . . . . . . . . . . . . 14 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 → (0...𝑁) ≈ 𝐴)
195192, 194syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...𝑁) ≈ 𝐴)
196195ensymd 9043 . . . . . . . . . . . 12 (𝜑𝐴 ≈ (0...𝑁))
197 ax-1cn 11210 . . . . . . . . . . . . . . 15 1 ∈ ℂ
198 pncan 11511 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
19957, 197, 198sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
200199oveq2d 7446 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
20156nnnn0d 12584 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
202 peano2nn0 12563 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
203201, 202syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ0)
204203nn0zd 12636 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℤ)
205 fz01en 13588 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℤ → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
206204, 205syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
207200, 206eqbrtrrd 5171 . . . . . . . . . . . 12 (𝜑 → (0...𝑁) ≈ (1...(𝑁 + 1)))
208 entr 9044 . . . . . . . . . . . 12 ((𝐴 ≈ (0...𝑁) ∧ (0...𝑁) ≈ (1...(𝑁 + 1))) → 𝐴 ≈ (1...(𝑁 + 1)))
209196, 207, 208syl2anc 584 . . . . . . . . . . 11 (𝜑𝐴 ≈ (1...(𝑁 + 1)))
2101, 15ssfid 9298 . . . . . . . . . . . 12 (𝜑𝐴 ∈ Fin)
211 fzfid 14010 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) ∈ Fin)
212 hashen 14382 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
213210, 211, 212syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
214209, 213mpbird 257 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘(1...(𝑁 + 1))))
215 hashfz1 14381 . . . . . . . . . . 11 ((𝑁 + 1) ∈ ℕ0 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
216203, 215syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
217214, 216eqtrd 2774 . . . . . . . . 9 (𝜑 → (♯‘𝐴) = (𝑁 + 1))
21827ex 412 . . . . . . . . . . . . . 14 (𝜑 → (𝑣𝐴 → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1))))
21920adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (𝑃 − 1) ∈ ℂ)
220 fzssuz 13601 . . . . . . . . . . . . . . . . . . . 20 (0...(𝑃 − 1)) ⊆ (ℤ‘0)
221 uzssz 12896 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘0) ⊆ ℤ
222 zsscn 12618 . . . . . . . . . . . . . . . . . . . . 21 ℤ ⊆ ℂ
223221, 222sstri 4004 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘0) ⊆ ℂ
224220, 223sstri 4004 . . . . . . . . . . . . . . . . . . 19 (0...(𝑃 − 1)) ⊆ ℂ
22515, 224sstrdi 4007 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
226225sselda 3994 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝑣 ∈ ℂ)
227226adantrr 717 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑣 ∈ ℂ)
228225sselda 3994 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘 ∈ ℂ)
229228adantrl 716 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑘 ∈ ℂ)
230219, 227, 229subcanad 11660 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘))
231230ex 412 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐴𝑘𝐴) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘)))
232218, 231dom2lem 9030 . . . . . . . . . . . . 13 (𝜑 → (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
233 f1eq1 6799 . . . . . . . . . . . . . 14 (𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)) → (𝐹:𝐴1-1→(0...(𝑃 − 1)) ↔ (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1))))
23428, 233ax-mp 5 . . . . . . . . . . . . 13 (𝐹:𝐴1-1→(0...(𝑃 − 1)) ↔ (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
235232, 234sylibr 234 . . . . . . . . . . . 12 (𝜑𝐹:𝐴1-1→(0...(𝑃 − 1)))
236 f1f1orn 6859 . . . . . . . . . . . 12 (𝐹:𝐴1-1→(0...(𝑃 − 1)) → 𝐹:𝐴1-1-onto→ran 𝐹)
237235, 236syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐴1-1-onto→ran 𝐹)
238210, 237hasheqf1od 14388 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘ran 𝐹))
239238, 217eqtr3d 2776 . . . . . . . . 9 (𝜑 → (♯‘ran 𝐹) = (𝑁 + 1))
240217, 239oveq12d 7448 . . . . . . . 8 (𝜑 → ((♯‘𝐴) + (♯‘ran 𝐹)) = ((𝑁 + 1) + (𝑁 + 1)))
24159, 68, 2403eqtr4d 2784 . . . . . . 7 (𝜑 → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
242241adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
243210adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝐴 ∈ Fin)
2441, 30ssfid 9298 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ Fin)
245244adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → ran 𝐹 ∈ Fin)
246 simpr 484 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝐴 ∩ ran 𝐹) = ∅)
247 hashun 14417 . . . . . . 7 ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
248243, 245, 246, 247syl3anc 1370 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
249242, 248eqtr4d 2777 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = (♯‘(𝐴 ∪ ran 𝐹)))
25055, 249breqtrd 5173 . . . 4 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
251250ex 412 . . 3 (𝜑 → ((𝐴 ∩ ran 𝐹) = ∅ → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹))))
252251necon3bd 2951 . 2 (𝜑 → (¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)) → (𝐴 ∩ ran 𝐹) ≠ ∅))
25353, 252mpd 15 1 (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wrex 3067  cun 3960  cin 3961  wss 3962  c0 4338   class class class wbr 5147  cmpt 5230  ran crn 5689  1-1wf1 6559  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cen 8980  cdom 8981  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543   mod cmo 13905  cexp 14098  chash 14365  abscabs 15269  cdvds 16286  cprime 16704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-dvds 16287  df-gcd 16528  df-prm 16705
This theorem is referenced by:  4sqlem12  16989
  Copyright terms: Public domain W3C validator