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

Theorem 4sqlem11 16915
Description: Lemma for 4sq 16924. 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 13962 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ∈ Fin)
2 4sqlem11.5 . . . . . . . 8 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
3 elfzelz 13525 . . . . . . . . . . . . 13 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
4 zsqcl 14117 . . . . . . . . . . . . 13 (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
53, 4syl 17 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑚↑2) ∈ ℤ)
6 4sq.4 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
7 prmnn 16636 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
9 zmodfz 13882 . . . . . . . . . . . 12 (((𝑚↑2) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
105, 8, 9syl2anr 596 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...𝑁)) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
11 eleq1a 2823 . . . . . . . . . . 11 (((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...𝑁)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1312rexlimdva 3150 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1413abssdv 4061 . . . . . . . 8 (𝜑 → {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ⊆ (0...(𝑃 − 1)))
152, 14eqsstrid 4026 . . . . . . 7 (𝜑𝐴 ⊆ (0...(𝑃 − 1)))
16 prmz 16637 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
176, 16syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℤ)
18 peano2zm 12627 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 − 1) ∈ ℤ)
2019zcnd 12689 . . . . . . . . . . . . 13 (𝜑 → (𝑃 − 1) ∈ ℂ)
2120addlidd 11437 . . . . . . . . . . . 12 (𝜑 → (0 + (𝑃 − 1)) = (𝑃 − 1))
2221oveq1d 7429 . . . . . . . . . . 11 (𝜑 → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2322adantr 480 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2415sselda 3978 . . . . . . . . . . 11 ((𝜑𝑣𝐴) → 𝑣 ∈ (0...(𝑃 − 1)))
25 fzrev3i 13592 . . . . . . . . . . 11 (𝑣 ∈ (0...(𝑃 − 1)) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2624, 25syl 17 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2723, 26eqeltrrd 2829 . . . . . . . . 9 ((𝜑𝑣𝐴) → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1)))
28 4sqlem11.6 . . . . . . . . 9 𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣))
2927, 28fmptd 7118 . . . . . . . 8 (𝜑𝐹:𝐴⟶(0...(𝑃 − 1)))
3029frnd 6724 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ (0...(𝑃 − 1)))
3115, 30unssd 4182 . . . . . 6 (𝜑 → (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)))
321, 31ssfid 9283 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ∈ Fin)
33 hashcl 14339 . . . . 5 ((𝐴 ∪ ran 𝐹) ∈ Fin → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3432, 33syl 17 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
3534nn0red 12555 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ∈ ℝ)
3617zred 12688 . . 3 (𝜑𝑃 ∈ ℝ)
37 ssdomg 9012 . . . . . 6 ((0...(𝑃 − 1)) ∈ Fin → ((𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)) → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
381, 31, 37sylc 65 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))
39 hashdom 14362 . . . . . 6 (((𝐴 ∪ ran 𝐹) ∈ Fin ∧ (0...(𝑃 − 1)) ∈ Fin) → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4032, 1, 39syl2anc 583 . . . . 5 (𝜑 → ((♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
4138, 40mpbird 257 . . . 4 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ (♯‘(0...(𝑃 − 1))))
42 fz01en 13553 . . . . . . 7 (𝑃 ∈ ℤ → (0...(𝑃 − 1)) ≈ (1...𝑃))
4317, 42syl 17 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ≈ (1...𝑃))
44 fzfid 13962 . . . . . . 7 (𝜑 → (1...𝑃) ∈ Fin)
45 hashen 14330 . . . . . . 7 (((0...(𝑃 − 1)) ∈ Fin ∧ (1...𝑃) ∈ Fin) → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
461, 44, 45syl2anc 583 . . . . . 6 (𝜑 → ((♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
4743, 46mpbird 257 . . . . 5 (𝜑 → (♯‘(0...(𝑃 − 1))) = (♯‘(1...𝑃)))
488nnnn0d 12554 . . . . . 6 (𝜑𝑃 ∈ ℕ0)
49 hashfz1 14329 . . . . . 6 (𝑃 ∈ ℕ0 → (♯‘(1...𝑃)) = 𝑃)
5048, 49syl 17 . . . . 5 (𝜑 → (♯‘(1...𝑃)) = 𝑃)
5147, 50eqtrd 2767 . . . 4 (𝜑 → (♯‘(0...(𝑃 − 1))) = 𝑃)
5241, 51breqtrd 5168 . . 3 (𝜑 → (♯‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃)
5335, 36, 52lensymd 11387 . 2 (𝜑 → ¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
5436adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 ∈ ℝ)
5554ltp1d 12166 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (𝑃 + 1))
56 4sq.2 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
5756nncnd 12250 . . . . . . . . 9 (𝜑𝑁 ∈ ℂ)
58 1cnd 11231 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
5957, 57, 58, 58add4d 11464 . . . . . . . 8 (𝜑 → ((𝑁 + 𝑁) + (1 + 1)) = ((𝑁 + 1) + (𝑁 + 1)))
60 4sq.3 . . . . . . . . . 10 (𝜑𝑃 = ((2 · 𝑁) + 1))
6160oveq1d 7429 . . . . . . . . 9 (𝜑 → (𝑃 + 1) = (((2 · 𝑁) + 1) + 1))
62 2cn 12309 . . . . . . . . . . 11 2 ∈ ℂ
63 mulcl 11214 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
6462, 57, 63sylancr 586 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
6564, 58, 58addassd 11258 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1)))
66572timesd 12477 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
6766oveq1d 7429 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) + (1 + 1)) = ((𝑁 + 𝑁) + (1 + 1)))
6861, 65, 673eqtrd 2771 . . . . . . . 8 (𝜑 → (𝑃 + 1) = ((𝑁 + 𝑁) + (1 + 1)))
6910ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑚 ∈ (0...𝑁) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))))
708adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℕ)
713ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℤ)
7271, 4syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚↑2) ∈ ℤ)
73 elfzelz 13525 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ (0...𝑁) → 𝑢 ∈ ℤ)
7473ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℤ)
75 zsqcl 14117 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ℤ → (𝑢↑2) ∈ ℤ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢↑2) ∈ ℤ)
77 moddvds 16233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ (𝑢↑2) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7870, 72, 76, 77syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
7971zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℂ)
8074zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℂ)
81 subsq 14197 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8279, 80, 81syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8382breq2d 5154 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚↑2) − (𝑢↑2)) ↔ 𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢))))
846adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℙ)
8571, 74zaddcld 12692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℤ)
8671, 74zsubcld 12693 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℤ)
87 euclemma 16675 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℙ ∧ (𝑚 + 𝑢) ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8884, 85, 86, 87syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
8978, 83, 883bitrd 305 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9085zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℝ)
91 2re 12308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
9256nnred 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ)
93 remulcl 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
9491, 92, 93sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℝ)
9594adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) ∈ ℝ)
9684, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℤ)
9796zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℝ)
9871zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℝ)
9974zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℝ)
10092adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℝ)
101 elfzle2 13529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚𝑁)
102101ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚𝑁)
103 elfzle2 13529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (0...𝑁) → 𝑢𝑁)
104103ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢𝑁)
10598, 99, 100, 100, 102, 104le2addd 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (𝑁 + 𝑁))
10657adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℂ)
1071062timesd 12477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) = (𝑁 + 𝑁))
108105, 107breqtrrd 5170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (2 · 𝑁))
10994ltp1d 12166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (2 · 𝑁) < ((2 · 𝑁) + 1))
110109, 60breqtrrd 5170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) < 𝑃)
111110adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) < 𝑃)
11290, 95, 97, 108, 111lelttrd 11394 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) < 𝑃)
11390, 97ltnled 11383 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 + 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑚 + 𝑢)))
114112, 113mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
115114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
11617ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
11785adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℤ)
118 1red 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ∈ ℝ)
119 nn0abscl 15283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚𝑢) ∈ ℤ → (abs‘(𝑚𝑢)) ∈ ℕ0)
12086, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℕ0)
121120nn0red 12555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℝ)
122121adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ)
123117zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℝ)
124120adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ0)
125124nn0zd 12606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℤ)
12686zcnd 12689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℂ)
127126adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ∈ ℂ)
12879, 80subeq0ad 11603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) = 0 ↔ 𝑚 = 𝑢))
129128necon3bid 2980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) ≠ 0 ↔ 𝑚𝑢))
130129biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ≠ 0)
131127, 130absrpcld 15419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ+)
132131rpgt0d 13043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 0 < (abs‘(𝑚𝑢)))
133 elnnz 12590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((abs‘(𝑚𝑢)) ∈ ℕ ↔ ((abs‘(𝑚𝑢)) ∈ ℤ ∧ 0 < (abs‘(𝑚𝑢))))
134125, 132, 133sylanbrc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ)
135134nnge1d 12282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (abs‘(𝑚𝑢)))
136 0cnd 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ∈ ℂ)
13779, 80, 136abs3difd 15431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))))
13879subid1d 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 0) = 𝑚)
139138fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = (abs‘𝑚))
140 elfzle1 13528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
141140ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑚)
14298, 141absidd 15393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑚) = 𝑚)
143139, 142eqtrd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = 𝑚)
144 0cn 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 ∈ ℂ
145 abssub 15297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
146144, 80, 145sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
14780subid1d 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢 − 0) = 𝑢)
148147fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑢 − 0)) = (abs‘𝑢))
149 elfzle1 13528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (0...𝑁) → 0 ≤ 𝑢)
150149ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑢)
15199, 150absidd 15393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑢) = 𝑢)
152146, 148, 1513eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = 𝑢)
153143, 152oveq12d 7432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))) = (𝑚 + 𝑢))
154137, 153breqtrd 5168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
155154adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
156118, 122, 123, 135, 155letrd 11393 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (𝑚 + 𝑢))
157 elnnz1 12610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 + 𝑢) ∈ ℕ ↔ ((𝑚 + 𝑢) ∈ ℤ ∧ 1 ≤ (𝑚 + 𝑢)))
158117, 156, 157sylanbrc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℕ)
159 dvdsle 16278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℤ ∧ (𝑚 + 𝑢) ∈ ℕ) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
160116, 158, 159syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
161115, 160mtod 197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (𝑚 + 𝑢))
162161ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (𝑚 + 𝑢)))
163162necon4ad 2954 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑚 = 𝑢))
164 dvdsabsb 16244 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
16596, 86, 164syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
166 letr 11330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (abs‘(𝑚𝑢)) ∈ ℝ ∧ (𝑚 + 𝑢) ∈ ℝ) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
16797, 121, 90, 166syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
168154, 167mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ≤ (abs‘(𝑚𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
169114, 168mtod 197 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
170169adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
17196adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
172 dvdsle 16278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (abs‘(𝑚𝑢)) ∈ ℕ) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
173171, 134, 172syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
174170, 173mtod 197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (abs‘(𝑚𝑢)))
175174ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (abs‘(𝑚𝑢))))
176175necon4ad 2954 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑚 = 𝑢))
177165, 176sylbid 239 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) → 𝑚 = 𝑢))
178163, 177jaod 858 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢)) → 𝑚 = 𝑢))
17989, 178sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) → 𝑚 = 𝑢))
180 oveq1 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑢 → (𝑚↑2) = (𝑢↑2))
181180oveq1d 7429 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑢 → ((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃))
182179, 181impbid1 224 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢))
183182ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁)) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢)))
18469, 183dom2lem 9004 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)))
185 f1f1orn 6844 . . . . . . . . . . . . . . . 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 2727 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
188187rnmpt 5951 . . . . . . . . . . . . . . . . 17 ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
1892, 188eqtr4i 2758 . . . . . . . . . . . . . . . 16 𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
190 f1oeq3 6823 . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴)
193 ovex 7447 . . . . . . . . . . . . . . 15 (0...𝑁) ∈ V
194193f1oen 8985 . . . . . . . . . . . . . 14 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 → (0...𝑁) ≈ 𝐴)
195192, 194syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...𝑁) ≈ 𝐴)
196195ensymd 9017 . . . . . . . . . . . 12 (𝜑𝐴 ≈ (0...𝑁))
197 ax-1cn 11188 . . . . . . . . . . . . . . 15 1 ∈ ℂ
198 pncan 11488 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
19957, 197, 198sylancl 585 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
200199oveq2d 7430 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
20156nnnn0d 12554 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
202 peano2nn0 12534 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
203201, 202syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ0)
204203nn0zd 12606 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℤ)
205 fz01en 13553 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℤ → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
206204, 205syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
207200, 206eqbrtrrd 5166 . . . . . . . . . . . 12 (𝜑 → (0...𝑁) ≈ (1...(𝑁 + 1)))
208 entr 9018 . . . . . . . . . . . 12 ((𝐴 ≈ (0...𝑁) ∧ (0...𝑁) ≈ (1...(𝑁 + 1))) → 𝐴 ≈ (1...(𝑁 + 1)))
209196, 207, 208syl2anc 583 . . . . . . . . . . 11 (𝜑𝐴 ≈ (1...(𝑁 + 1)))
2101, 15ssfid 9283 . . . . . . . . . . . 12 (𝜑𝐴 ∈ Fin)
211 fzfid 13962 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) ∈ Fin)
212 hashen 14330 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
213210, 211, 212syl2anc 583 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) = (♯‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
214209, 213mpbird 257 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘(1...(𝑁 + 1))))
215 hashfz1 14329 . . . . . . . . . . 11 ((𝑁 + 1) ∈ ℕ0 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
216203, 215syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
217214, 216eqtrd 2767 . . . . . . . . 9 (𝜑 → (♯‘𝐴) = (𝑁 + 1))
21827ex 412 . . . . . . . . . . . . . 14 (𝜑 → (𝑣𝐴 → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1))))
21920adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (𝑃 − 1) ∈ ℂ)
220 fzssuz 13566 . . . . . . . . . . . . . . . . . . . 20 (0...(𝑃 − 1)) ⊆ (ℤ‘0)
221 uzssz 12865 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘0) ⊆ ℤ
222 zsscn 12588 . . . . . . . . . . . . . . . . . . . . 21 ℤ ⊆ ℂ
223221, 222sstri 3987 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘0) ⊆ ℂ
224220, 223sstri 3987 . . . . . . . . . . . . . . . . . . 19 (0...(𝑃 − 1)) ⊆ ℂ
22515, 224sstrdi 3990 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
226225sselda 3978 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐴) → 𝑣 ∈ ℂ)
227226adantrr 716 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑣 ∈ ℂ)
228225sselda 3978 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘 ∈ ℂ)
229228adantrl 715 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑘 ∈ ℂ)
230219, 227, 229subcanad 11636 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘))
231230ex 412 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐴𝑘𝐴) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘)))
232218, 231dom2lem 9004 . . . . . . . . . . . . 13 (𝜑 → (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
233 f1eq1 6782 . . . . . . . . . . . . . 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 233 . . . . . . . . . . . 12 (𝜑𝐹:𝐴1-1→(0...(𝑃 − 1)))
236 f1f1orn 6844 . . . . . . . . . . . 12 (𝐹:𝐴1-1→(0...(𝑃 − 1)) → 𝐹:𝐴1-1-onto→ran 𝐹)
237235, 236syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐴1-1-onto→ran 𝐹)
238210, 237hasheqf1od 14336 . . . . . . . . . 10 (𝜑 → (♯‘𝐴) = (♯‘ran 𝐹))
239238, 217eqtr3d 2769 . . . . . . . . 9 (𝜑 → (♯‘ran 𝐹) = (𝑁 + 1))
240217, 239oveq12d 7432 . . . . . . . 8 (𝜑 → ((♯‘𝐴) + (♯‘ran 𝐹)) = ((𝑁 + 1) + (𝑁 + 1)))
24159, 68, 2403eqtr4d 2777 . . . . . . 7 (𝜑 → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
242241adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = ((♯‘𝐴) + (♯‘ran 𝐹)))
243210adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝐴 ∈ Fin)
2441, 30ssfid 9283 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ Fin)
245244adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → ran 𝐹 ∈ Fin)
246 simpr 484 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝐴 ∩ ran 𝐹) = ∅)
247 hashun 14365 . . . . . . 7 ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
248243, 245, 246, 247syl3anc 1369 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (♯‘(𝐴 ∪ ran 𝐹)) = ((♯‘𝐴) + (♯‘ran 𝐹)))
249242, 248eqtr4d 2770 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = (♯‘(𝐴 ∪ ran 𝐹)))
25055, 249breqtrd 5168 . . . 4 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)))
251250ex 412 . . 3 (𝜑 → ((𝐴 ∩ ran 𝐹) = ∅ → 𝑃 < (♯‘(𝐴 ∪ ran 𝐹))))
252251necon3bd 2949 . 2 (𝜑 → (¬ 𝑃 < (♯‘(𝐴 ∪ ran 𝐹)) → (𝐴 ∩ ran 𝐹) ≠ ∅))
25353, 252mpd 15 1 (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 846   = wceq 1534  wcel 2099  {cab 2704  wne 2935  wrex 3065  cun 3942  cin 3943  wss 3944  c0 4318   class class class wbr 5142  cmpt 5225  ran crn 5673  1-1wf1 6539  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7414  cen 8952  cdom 8953  Fincfn 8955  cc 11128  cr 11129  0cc0 11130  1c1 11131   + caddc 11133   · cmul 11135   < clt 11270  cle 11271  cmin 11466  cn 12234  2c2 12289  0cn0 12494  cz 12580  cuz 12844  ...cfz 13508   mod cmo 13858  cexp 14050  chash 14313  abscabs 15205  cdvds 16222  cprime 16633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-xnn0 12567  df-z 12581  df-uz 12845  df-rp 12999  df-fz 13509  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-dvds 16223  df-gcd 16461  df-prm 16634
This theorem is referenced by:  4sqlem12  16916
  Copyright terms: Public domain W3C validator