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

Theorem 4sqlem11 16067
 Description: Lemma for 4sq 16076. 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 13095 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ∈ Fin)
2 4sqlem11.5 . . . . . . . 8 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
3 elfzelz 12663 . . . . . . . . . . . . 13 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
4 zsqcl 13257 . . . . . . . . . . . . 13 (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
53, 4syl 17 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑚↑2) ∈ ℤ)
6 4sq.4 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
7 prmnn 15797 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
9 zmodfz 13015 . . . . . . . . . . . 12 (((𝑚↑2) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
105, 8, 9syl2anr 590 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...𝑁)) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
11 eleq1a 2854 . . . . . . . . . . 11 (((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...𝑁)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1312rexlimdva 3213 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1413abssdv 3897 . . . . . . . 8 (𝜑 → {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ⊆ (0...(𝑃 − 1)))
152, 14syl5eqss 3868 . . . . . . 7 (𝜑𝐴 ⊆ (0...(𝑃 − 1)))
16 prmz 15798 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
176, 16syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℤ)
18 peano2zm 11776 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 − 1) ∈ ℤ)
2019zcnd 11839 . . . . . . . . . . . . 13 (𝜑 → (𝑃 − 1) ∈ ℂ)
2120addid2d 10579 . . . . . . . . . . . 12 (𝜑 → (0 + (𝑃 − 1)) = (𝑃 − 1))
2221oveq1d 6939 . . . . . . . . . . 11 (𝜑 → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2322adantr 474 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2415sselda 3821 . . . . . . . . . . 11 ((𝜑𝑣𝐴) → 𝑣 ∈ (0...(𝑃 − 1)))
25 fzrev3i 12729 . . . . . . . . . . 11 (𝑣 ∈ (0...(𝑃 − 1)) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2624, 25syl 17 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2723, 26eqeltrrd 2860 . . . . . . . . 9 ((𝜑𝑣𝐴) → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1)))
28 4sqlem11.6 . . . . . . . . 9 𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣))
2927, 28fmptd 6650 . . . . . . . 8 (𝜑𝐹:𝐴⟶(0...(𝑃 − 1)))
3029frnd 6300 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ (0...(𝑃 − 1)))
3115, 30unssd 4012 . . . . . 6 (𝜑 → (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)))
321, 31ssfid 8473 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ∈ Fin)
33 hashcl 13466 . . . . 5 ((𝐴 ∪ ran 𝐹) ∈ Fin → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3432, 33syl 17 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3534nn0red 11707 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℝ)
3617zred 11838 . . 3 (𝜑𝑃 ∈ ℝ)
37 ssdomg 8289 . . . . . 6 ((0...(𝑃 − 1)) ∈ Fin → ((𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)) → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
381, 31, 37sylc 65 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))
39 hashdom 13487 . . . . . 6 (((𝐴 ∪ ran 𝐹) ∈ Fin ∧ (0...(𝑃 − 1)) ∈ Fin) → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4032, 1, 39syl2anc 579 . . . . 5 (𝜑 → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4138, 40mpbird 249 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))))
42 fz01en 12690 . . . . . . 7 (𝑃 ∈ ℤ → (0...(𝑃 − 1)) ≈ (1...𝑃))
4317, 42syl 17 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ≈ (1...𝑃))
44 fzfid 13095 . . . . . . 7 (𝜑 → (1...𝑃) ∈ Fin)
45 hashen 13456 . . . . . . 7 (((0...(𝑃 − 1)) ∈ Fin ∧ (1...𝑃) ∈ Fin) → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
461, 44, 45syl2anc 579 . . . . . 6 (𝜑 → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
4743, 46mpbird 249 . . . . 5 (𝜑 → (♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)))
488nnnn0d 11706 . . . . . 6 (𝜑𝑃 ∈ ℕ0)
49 hashfz1 13455 . . . . . 6 (𝑃 ∈ ℕ0 → (♯‘(1...𝑃)) = 𝑃)
5048, 49syl 17 . . . . 5 (𝜑 → (♯‘(1...𝑃)) = 𝑃)
5147, 50eqtrd 2814 . . . 4 (𝜑 → (♯‘(0...(𝑃 − 1))) = 𝑃)
5241, 51breqtrd 4914 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃)
5335, 36, 52lensymd 10529 . 2 (𝜑 → ¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
5436adantr 474 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 ∈ ℝ)
5554ltp1d 11310 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (𝑃 + 1))
56 4sq.2 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
5756nncnd 11396 . . . . . . . . 9 (𝜑𝑁 ∈ ℂ)
58 1cnd 10373 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
5957, 57, 58, 58add4d 10606 . . . . . . . 8 (𝜑 → ((𝑁 + 𝑁) + (1 + 1)) = ((𝑁 + 1) + (𝑁 + 1)))
60 4sq.3 . . . . . . . . . 10 (𝜑𝑃 = ((2 · 𝑁) + 1))
6160oveq1d 6939 . . . . . . . . 9 (𝜑 → (𝑃 + 1) = (((2 · 𝑁) + 1) + 1))
62 2cn 11454 . . . . . . . . . . 11 2 ∈ ℂ
63 mulcl 10358 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
6462, 57, 63sylancr 581 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
6564, 58, 58addassd 10401 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1)))
66572timesd 11629 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
6766oveq1d 6939 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) + (1 + 1)) = ((𝑁 + 𝑁) + (1 + 1)))
6861, 65, 673eqtrd 2818 . . . . . . . 8 (𝜑 → (𝑃 + 1) = ((𝑁 + 𝑁) + (1 + 1)))
6910ex 403 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑚 ∈ (0...𝑁) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))))
708adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℕ)
713ad2antrl 718 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℤ)
7271, 4syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚↑2) ∈ ℤ)
73 elfzelz 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ (0...𝑁) → 𝑢 ∈ ℤ)
7473ad2antll 719 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℤ)
75 zsqcl 13257 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ℤ → (𝑢↑2) ∈ ℤ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢↑2) ∈ ℤ)
77 moddvds 15402 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ (𝑢↑2) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7870, 72, 76, 77syl3anc 1439 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7971zcnd 11839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℂ)
8074zcnd 11839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℂ)
81 subsq 13295 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8279, 80, 81syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8382breq2d 4900 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚↑2) − (𝑢↑2)) ↔ 𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢))))
846adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℙ)
8571, 74zaddcld 11842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℤ)
8671, 74zsubcld 11843 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℤ)
87 euclemma 15833 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℙ ∧ (𝑚 + 𝑢) ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8884, 85, 86, 87syl3anc 1439 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8978, 83, 883bitrd 297 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9085zred 11838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℝ)
91 2re 11453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
9256nnred 11395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ)
93 remulcl 10359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
9491, 92, 93sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℝ)
9594adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) ∈ ℝ)
9684, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℤ)
9796zred 11838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℝ)
9871zred 11838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℝ)
9974zred 11838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℝ)
10092adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℝ)
101 elfzle2 12666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚𝑁)
102101ad2antrl 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚𝑁)
103 elfzle2 12666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (0...𝑁) → 𝑢𝑁)
104103ad2antll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢𝑁)
10598, 99, 100, 100, 102, 104le2addd 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (𝑁 + 𝑁))
10657adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℂ)
1071062timesd 11629 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) = (𝑁 + 𝑁))
108105, 107breqtrrd 4916 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (2 · 𝑁))
10994ltp1d 11310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (2 · 𝑁) < ((2 · 𝑁) + 1))
110109, 60breqtrrd 4916 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) < 𝑃)
111110adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) < 𝑃)
11290, 95, 97, 108, 111lelttrd 10536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) < 𝑃)
11390, 97ltnled 10525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 + 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑚 + 𝑢)))
114112, 113mpbid 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
115114adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
11617ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
11785adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℤ)
118 1red 10379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ∈ ℝ)
119 nn0abscl 14463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚𝑢) ∈ ℤ → (abs‘(𝑚𝑢)) ∈ ℕ0)
12086, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℕ0)
121120nn0red 11707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℝ)
122121adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ)
123117zred 11838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℝ)
124120adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ0)
125124nn0zd 11836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℤ)
12686zcnd 11839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℂ)
127126adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ∈ ℂ)
12879, 80subeq0ad 10746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) = 0 ↔ 𝑚 = 𝑢))
129128necon3bid 3013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) ≠ 0 ↔ 𝑚𝑢))
130129biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ≠ 0)
131127, 130absrpcld 14599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ+)
132131rpgt0d 12188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 0 < (abs‘(𝑚𝑢)))
133 elnnz 11742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((abs‘(𝑚𝑢)) ∈ ℕ ↔ ((abs‘(𝑚𝑢)) ∈ ℤ ∧ 0 < (abs‘(𝑚𝑢))))
134125, 132, 133sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ)
135134nnge1d 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (abs‘(𝑚𝑢)))
136 0cnd 10371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ∈ ℂ)
13779, 80, 136abs3difd 14611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))))
13879subid1d 10725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 0) = 𝑚)
139138fveq2d 6452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = (abs‘𝑚))
140 elfzle1 12665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
141140ad2antrl 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑚)
14298, 141absidd 14573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑚) = 𝑚)
143139, 142eqtrd 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = 𝑚)
144 0cn 10370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 ∈ ℂ
145 abssub 14477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
146144, 80, 145sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
14780subid1d 10725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢 − 0) = 𝑢)
148147fveq2d 6452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑢 − 0)) = (abs‘𝑢))
149 elfzle1 12665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (0...𝑁) → 0 ≤ 𝑢)
150149ad2antll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑢)
15199, 150absidd 14573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑢) = 𝑢)
152146, 148, 1513eqtrd 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = 𝑢)
153143, 152oveq12d 6942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))) = (𝑚 + 𝑢))
154137, 153breqtrd 4914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
155154adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
156118, 122, 123, 135, 155letrd 10535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (𝑚 + 𝑢))
157 elnnz1 11759 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 + 𝑢) ∈ ℕ ↔ ((𝑚 + 𝑢) ∈ ℤ ∧ 1 ≤ (𝑚 + 𝑢)))
158117, 156, 157sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℕ)
159 dvdsle 15443 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℤ ∧ (𝑚 + 𝑢) ∈ ℕ) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
160116, 158, 159syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
161115, 160mtod 190 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (𝑚 + 𝑢))
162161ex 403 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (𝑚 + 𝑢)))
163162necon4ad 2988 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑚 = 𝑢))
164 dvdsabsb 15412 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
16596, 86, 164syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
166 letr 10472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (abs‘(𝑚𝑢)) ∈ ℝ ∧ (𝑚 + 𝑢) ∈ ℝ) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
16797, 121, 90, 166syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
168154, 167mpan2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ≤ (abs‘(𝑚𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
169114, 168mtod 190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
170169adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
17196adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
172 dvdsle 15443 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (abs‘(𝑚𝑢)) ∈ ℕ) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
173171, 134, 172syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
174170, 173mtod 190 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (abs‘(𝑚𝑢)))
175174ex 403 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (abs‘(𝑚𝑢))))
176175necon4ad 2988 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑚 = 𝑢))
177165, 176sylbid 232 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) → 𝑚 = 𝑢))
178163, 177jaod 848 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢)) → 𝑚 = 𝑢))
17989, 178sylbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) → 𝑚 = 𝑢))
180 oveq1 6931 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑢 → (𝑚↑2) = (𝑢↑2))
181180oveq1d 6939 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑢 → ((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃))
182179, 181impbid1 217 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢))
183182ex 403 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁)) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢)))
18469, 183dom2lem 8283 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)))
185 f1f1orn 6404 . . . . . . . . . . . . . . . 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 2778 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
188187rnmpt 5619 . . . . . . . . . . . . . . . . 17 ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
1892, 188eqtr4i 2805 . . . . . . . . . . . . . . . 16 𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
190 f1oeq3 6384 . . . . . . . . . . . . . . . 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 226 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴)
193 ovex 6956 . . . . . . . . . . . . . . 15 (0...𝑁) ∈ V
194193f1oen 8264 . . . . . . . . . . . . . 14 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 → (0...𝑁) ≈ 𝐴)
195192, 194syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...𝑁) ≈ 𝐴)
196195ensymd 8294 . . . . . . . . . . . 12 (𝜑𝐴 ≈ (0...𝑁))
197 ax-1cn 10332 . . . . . . . . . . . . . . 15 1 ∈ ℂ
198 pncan 10630 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
19957, 197, 198sylancl 580 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
200199oveq2d 6940 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
20156nnnn0d 11706 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
202 peano2nn0 11688 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
203201, 202syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ0)
204203nn0zd 11836 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℤ)
205 fz01en 12690 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℤ → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
206204, 205syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
207200, 206eqbrtrrd 4912 . . . . . . . . . . . 12 (𝜑 → (0...𝑁) ≈ (1...(𝑁 + 1)))
208 entr 8295 . . . . . . . . . . . 12 ((𝐴 ≈ (0...𝑁) ∧ (0...𝑁) ≈ (1...(𝑁 + 1))) → 𝐴 ≈ (1...(𝑁 + 1)))
209196, 207, 208syl2anc 579 . . . . . . . . . . 11 (𝜑𝐴 ≈ (1...(𝑁 + 1)))
2101, 15ssfid 8473 . . . . . . . . . . . 12 (𝜑𝐴 ∈ Fin)
211 fzfid 13095 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) ∈ Fin)
212 hashen 13456 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
213210, 211, 212syl2anc 579 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
214209, 213mpbird 249 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘(1...(𝑁 + 1))))
215 hashfz1 13455 . . . . . . . . . . 11 ((𝑁 + 1) ∈ ℕ0 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
216203, 215syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
217214, 216eqtrd 2814 . . . . . . . . 9 (𝜑 → (♯‘𝐴) = (𝑁 + 1))
21827ex 403 . . . . . . . . . . . . . 14 (𝜑 → (𝑣𝐴 → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1))))
21920adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (𝑃 − 1) ∈ ℂ)
220 fzssuz 12703 . . . . . . . . . . . . . . . . . . . 20 (0...(𝑃 − 1)) ⊆ (ℤ‘0)
221 uzssz 12016 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘0) ⊆ ℤ
222 zsscn 11740 . . . . . . . . . . . . . . . . . . . . 21 ℤ ⊆ ℂ
223221, 222sstri 3830 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘0) ⊆ ℂ
224220, 223sstri 3830 . . . . . . . . . . . . . . . . . . 19 (0...(𝑃 − 1)) ⊆ ℂ
22515, 224syl6ss 3833 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
226225sselda 3821 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝑣 ∈ ℂ)
227226adantrr 707 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑣 ∈ ℂ)
228225sselda 3821 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘 ∈ ℂ)
229228adantrl 706 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑘 ∈ ℂ)
230219, 227, 229subcanad 10779 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘))
231230ex 403 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐴𝑘𝐴) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘)))
232218, 231dom2lem 8283 . . . . . . . . . . . . 13 (𝜑 → (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
233 f1eq1 6348 . . . . . . . . . . . . . 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 226 . . . . . . . . . . . 12 (𝜑𝐹:𝐴1-1→(0...(𝑃 − 1)))
236 f1f1orn 6404 . . . . . . . . . . . 12 (𝐹:𝐴1-1→(0...(𝑃 − 1)) → 𝐹:𝐴1-1-onto→ran 𝐹)
237235, 236syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐴1-1-onto→ran 𝐹)
238210, 237hasheqf1od 13463 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘ran 𝐹))
239238, 217eqtr3d 2816 . . . . . . . . 9 (𝜑 → (♯‘ran 𝐹) = (𝑁 + 1))
240217, 239oveq12d 6942 . . . . . . . 8 (𝜑 → ((♯‘𝐴) + (♯‘ran 𝐹)) = ((𝑁 + 1) + (𝑁 + 1)))
24159, 68, 2403eqtr4d 2824 . . . . . . 7 (𝜑 → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
242241adantr 474 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
243210adantr 474 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝐴 ∈ Fin)
2441, 30ssfid 8473 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ Fin)
245244adantr 474 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → ran 𝐹 ∈ Fin)
246 simpr 479 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝐴 ∩ ran 𝐹) = ∅)
247 hashun 13490 . . . . . . 7 ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
248243, 245, 246, 247syl3anc 1439 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
249242, 248eqtr4d 2817 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = (♯‘(𝐴 ∪ ran 𝐹)))
25055, 249breqtrd 4914 . . . 4 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
251250ex 403 . . 3 (𝜑 → ((𝐴 ∩ ran 𝐹) = ∅ → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹))))
252251necon3bd 2983 . 2 (𝜑 → (¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)) → (𝐴 ∩ ran 𝐹) ≠ ∅))
25353, 252mpd 15 1 (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2107  {cab 2763   ≠ wne 2969  ∃wrex 3091   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141   class class class wbr 4888   ↦ cmpt 4967  ran crn 5358  –1-1→wf1 6134  –1-1-onto→wf1o 6136  ‘cfv 6137  (class class class)co 6924   ≈ cen 8240   ≼ cdom 8241  Fincfn 8243  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279   < clt 10413   ≤ cle 10414   − cmin 10608  ℕcn 11378  2c2 11434  ℕ0cn0 11646  ℤcz 11732  ℤ≥cuz 11996  ...cfz 12647   mod cmo 12991  ↑cexp 13182  ♯chash 13439  abscabs 14385   ∥ cdvds 15391  ℙcprime 15794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-n0 11647  df-xnn0 11719  df-z 11733  df-uz 11997  df-rp 12142  df-fz 12648  df-fl 12916  df-mod 12992  df-seq 13124  df-exp 13183  df-hash 13440  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-dvds 15392  df-gcd 15627  df-prm 15795 This theorem is referenced by:  4sqlem12  16068
 Copyright terms: Public domain W3C validator