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

Theorem 4sqlem11 15706
Description: Lemma for 4sq 15715. 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 12812 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ∈ Fin)
2 4sqlem11.5 . . . . . . . 8 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
3 elfzelz 12380 . . . . . . . . . . . . 13 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
4 zsqcl 12974 . . . . . . . . . . . . 13 (𝑚 ∈ ℤ → (𝑚↑2) ∈ ℤ)
53, 4syl 17 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑚↑2) ∈ ℤ)
6 4sq.4 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
7 prmnn 15435 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℕ)
9 zmodfz 12732 . . . . . . . . . . . 12 (((𝑚↑2) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
105, 8, 9syl2anr 494 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...𝑁)) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)))
11 eleq1a 2725 . . . . . . . . . . 11 (((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1210, 11syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...𝑁)) → (𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1312rexlimdva 3060 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃) → 𝑢 ∈ (0...(𝑃 − 1))))
1413abssdv 3709 . . . . . . . 8 (𝜑 → {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} ⊆ (0...(𝑃 − 1)))
152, 14syl5eqss 3682 . . . . . . 7 (𝜑𝐴 ⊆ (0...(𝑃 − 1)))
16 prmz 15436 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
176, 16syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℤ)
18 peano2zm 11458 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
1917, 18syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 − 1) ∈ ℤ)
2019zcnd 11521 . . . . . . . . . . . . 13 (𝜑 → (𝑃 − 1) ∈ ℂ)
2120addid2d 10275 . . . . . . . . . . . 12 (𝜑 → (0 + (𝑃 − 1)) = (𝑃 − 1))
2221oveq1d 6705 . . . . . . . . . . 11 (𝜑 → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2322adantr 480 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) = ((𝑃 − 1) − 𝑣))
2415sselda 3636 . . . . . . . . . . 11 ((𝜑𝑣𝐴) → 𝑣 ∈ (0...(𝑃 − 1)))
25 fzrev3i 12445 . . . . . . . . . . 11 (𝑣 ∈ (0...(𝑃 − 1)) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2624, 25syl 17 . . . . . . . . . 10 ((𝜑𝑣𝐴) → ((0 + (𝑃 − 1)) − 𝑣) ∈ (0...(𝑃 − 1)))
2723, 26eqeltrrd 2731 . . . . . . . . 9 ((𝜑𝑣𝐴) → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1)))
28 4sqlem11.6 . . . . . . . . 9 𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣))
2927, 28fmptd 6425 . . . . . . . 8 (𝜑𝐹:𝐴⟶(0...(𝑃 − 1)))
30 frn 6091 . . . . . . . 8 (𝐹:𝐴⟶(0...(𝑃 − 1)) → ran 𝐹 ⊆ (0...(𝑃 − 1)))
3129, 30syl 17 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ (0...(𝑃 − 1)))
3215, 31unssd 3822 . . . . . 6 (𝜑 → (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)))
33 ssdomg 8043 . . . . . 6 ((0...(𝑃 − 1)) ∈ Fin → ((𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1)) → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
341, 32, 33sylc 65 . . . . 5 (𝜑 → (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1)))
35 ssfi 8221 . . . . . . 7 (((0...(𝑃 − 1)) ∈ Fin ∧ (𝐴 ∪ ran 𝐹) ⊆ (0...(𝑃 − 1))) → (𝐴 ∪ ran 𝐹) ∈ Fin)
361, 32, 35syl2anc 694 . . . . . 6 (𝜑 → (𝐴 ∪ ran 𝐹) ∈ Fin)
37 hashdom 13206 . . . . . 6 (((𝐴 ∪ ran 𝐹) ∈ Fin ∧ (0...(𝑃 − 1)) ∈ Fin) → ((#‘(𝐴 ∪ ran 𝐹)) ≤ (#‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
3836, 1, 37syl2anc 694 . . . . 5 (𝜑 → ((#‘(𝐴 ∪ ran 𝐹)) ≤ (#‘(0...(𝑃 − 1))) ↔ (𝐴 ∪ ran 𝐹) ≼ (0...(𝑃 − 1))))
3934, 38mpbird 247 . . . 4 (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ≤ (#‘(0...(𝑃 − 1))))
40 fz01en 12407 . . . . . . 7 (𝑃 ∈ ℤ → (0...(𝑃 − 1)) ≈ (1...𝑃))
4117, 40syl 17 . . . . . 6 (𝜑 → (0...(𝑃 − 1)) ≈ (1...𝑃))
42 fzfid 12812 . . . . . . 7 (𝜑 → (1...𝑃) ∈ Fin)
43 hashen 13175 . . . . . . 7 (((0...(𝑃 − 1)) ∈ Fin ∧ (1...𝑃) ∈ Fin) → ((#‘(0...(𝑃 − 1))) = (#‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
441, 42, 43syl2anc 694 . . . . . 6 (𝜑 → ((#‘(0...(𝑃 − 1))) = (#‘(1...𝑃)) ↔ (0...(𝑃 − 1)) ≈ (1...𝑃)))
4541, 44mpbird 247 . . . . 5 (𝜑 → (#‘(0...(𝑃 − 1))) = (#‘(1...𝑃)))
468nnnn0d 11389 . . . . . 6 (𝜑𝑃 ∈ ℕ0)
47 hashfz1 13174 . . . . . 6 (𝑃 ∈ ℕ0 → (#‘(1...𝑃)) = 𝑃)
4846, 47syl 17 . . . . 5 (𝜑 → (#‘(1...𝑃)) = 𝑃)
4945, 48eqtrd 2685 . . . 4 (𝜑 → (#‘(0...(𝑃 − 1))) = 𝑃)
5039, 49breqtrd 4711 . . 3 (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃)
51 hashcl 13185 . . . . . 6 ((𝐴 ∪ ran 𝐹) ∈ Fin → (#‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
5236, 51syl 17 . . . . 5 (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ∈ ℕ0)
5352nn0red 11390 . . . 4 (𝜑 → (#‘(𝐴 ∪ ran 𝐹)) ∈ ℝ)
5417zred 11520 . . . 4 (𝜑𝑃 ∈ ℝ)
5553, 54lenltd 10221 . . 3 (𝜑 → ((#‘(𝐴 ∪ ran 𝐹)) ≤ 𝑃 ↔ ¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹))))
5650, 55mpbid 222 . 2 (𝜑 → ¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹)))
5754adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 ∈ ℝ)
5857ltp1d 10992 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (𝑃 + 1))
59 4sq.2 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
6059nncnd 11074 . . . . . . . . 9 (𝜑𝑁 ∈ ℂ)
61 1cnd 10094 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
6260, 60, 61, 61add4d 10302 . . . . . . . 8 (𝜑 → ((𝑁 + 𝑁) + (1 + 1)) = ((𝑁 + 1) + (𝑁 + 1)))
63 4sq.3 . . . . . . . . . 10 (𝜑𝑃 = ((2 · 𝑁) + 1))
6463oveq1d 6705 . . . . . . . . 9 (𝜑 → (𝑃 + 1) = (((2 · 𝑁) + 1) + 1))
65 2cn 11129 . . . . . . . . . . 11 2 ∈ ℂ
66 mulcl 10058 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
6765, 60, 66sylancr 696 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
6867, 61, 61addassd 10100 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1)))
69602timesd 11313 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
7069oveq1d 6705 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) + (1 + 1)) = ((𝑁 + 𝑁) + (1 + 1)))
7164, 68, 703eqtrd 2689 . . . . . . . 8 (𝜑 → (𝑃 + 1) = ((𝑁 + 𝑁) + (1 + 1)))
7210ex 449 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑚 ∈ (0...𝑁) → ((𝑚↑2) mod 𝑃) ∈ (0...(𝑃 − 1))))
738adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℕ)
743ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℤ)
7574, 4syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚↑2) ∈ ℤ)
76 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 ∈ (0...𝑁) → 𝑢 ∈ ℤ)
7776ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℤ)
78 zsqcl 12974 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ℤ → (𝑢↑2) ∈ ℤ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢↑2) ∈ ℤ)
80 moddvds 15038 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ (𝑚↑2) ∈ ℤ ∧ (𝑢↑2) ∈ ℤ) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
8173, 75, 79, 80syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑃 ∥ ((𝑚↑2) − (𝑢↑2))))
8274zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℂ)
8377zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℂ)
84 subsq 13012 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8582, 83, 84syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚↑2) − (𝑢↑2)) = ((𝑚 + 𝑢) · (𝑚𝑢)))
8685breq2d 4697 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚↑2) − (𝑢↑2)) ↔ 𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢))))
876adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℙ)
8874, 77zaddcld 11524 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℤ)
8974, 77zsubcld 11525 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℤ)
90 euclemma 15472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℙ ∧ (𝑚 + 𝑢) ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9187, 88, 89, 90syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ ((𝑚 + 𝑢) · (𝑚𝑢)) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9281, 86, 913bitrd 294 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ (𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢))))
9388zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ∈ ℝ)
94 2re 11128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℝ
9559nnred 11073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℝ)
96 remulcl 10059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
9794, 95, 96sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℝ)
9897adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) ∈ ℝ)
9987, 16syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℤ)
10099zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑃 ∈ ℝ)
10174zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚 ∈ ℝ)
10277zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢 ∈ ℝ)
10395adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℝ)
104 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → 𝑚𝑁)
105104ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑚𝑁)
106 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (0...𝑁) → 𝑢𝑁)
107106ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑢𝑁)
108101, 102, 103, 103, 105, 107le2addd 10684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (𝑁 + 𝑁))
10960adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 𝑁 ∈ ℂ)
1101092timesd 11313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) = (𝑁 + 𝑁))
111108, 110breqtrrd 4713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) ≤ (2 · 𝑁))
11297ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (2 · 𝑁) < ((2 · 𝑁) + 1))
113112, 63breqtrrd 4713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) < 𝑃)
114113adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (2 · 𝑁) < 𝑃)
11593, 98, 100, 111, 114lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 + 𝑢) < 𝑃)
11693, 100ltnled 10222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚 + 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑚 + 𝑢)))
117115, 116mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
118117adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (𝑚 + 𝑢))
11917ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
12088adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℤ)
121 1red 10093 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ∈ ℝ)
122 nn0abscl 14096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚𝑢) ∈ ℤ → (abs‘(𝑚𝑢)) ∈ ℕ0)
12389, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℕ0)
124123nn0red 11390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ∈ ℝ)
125124adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ)
126120zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℝ)
127123adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ0)
128127nn0zd 11518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℤ)
12989zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢) ∈ ℂ)
130129adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ∈ ℂ)
13182, 83subeq0ad 10440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) = 0 ↔ 𝑚 = 𝑢))
132131necon3bid 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑚𝑢) ≠ 0 ↔ 𝑚𝑢))
133132biimpar 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚𝑢) ≠ 0)
134130, 133absrpcld 14231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℝ+)
135134rpgt0d 11913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 0 < (abs‘(𝑚𝑢)))
136 elnnz 11425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((abs‘(𝑚𝑢)) ∈ ℕ ↔ ((abs‘(𝑚𝑢)) ∈ ℤ ∧ 0 < (abs‘(𝑚𝑢))))
137128, 135, 136sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ∈ ℕ)
138137nnge1d 11101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (abs‘(𝑚𝑢)))
139 0cnd 10071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ∈ ℂ)
14082, 83, 139abs3difd 14243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))))
14182subid1d 10419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚 − 0) = 𝑚)
142141fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = (abs‘𝑚))
143 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (0...𝑁) → 0 ≤ 𝑚)
144143ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑚)
145101, 144absidd 14205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑚) = 𝑚)
146142, 145eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚 − 0)) = 𝑚)
147 0cn 10070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 ∈ ℂ
148 abssub 14110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
149147, 83, 148sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = (abs‘(𝑢 − 0)))
15083subid1d 10419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑢 − 0) = 𝑢)
151150fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑢 − 0)) = (abs‘𝑢))
152 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (0...𝑁) → 0 ≤ 𝑢)
153152ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → 0 ≤ 𝑢)
154102, 153absidd 14205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘𝑢) = 𝑢)
155149, 151, 1543eqtrd 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(0 − 𝑢)) = 𝑢)
156146, 155oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((abs‘(𝑚 − 0)) + (abs‘(0 − 𝑢))) = (𝑚 + 𝑢))
157140, 156breqtrd 4711 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
158157adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢))
159121, 125, 126, 138, 158letrd 10232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 1 ≤ (𝑚 + 𝑢))
160 elnnz1 11441 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 + 𝑢) ∈ ℕ ↔ ((𝑚 + 𝑢) ∈ ℤ ∧ 1 ≤ (𝑚 + 𝑢)))
161120, 159, 160sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑚 + 𝑢) ∈ ℕ)
162 dvdsle 15079 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ ℤ ∧ (𝑚 + 𝑢) ∈ ℕ) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
163119, 161, 162syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑃 ≤ (𝑚 + 𝑢)))
164118, 163mtod 189 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (𝑚 + 𝑢))
165164ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (𝑚 + 𝑢)))
166165necon4ad 2842 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚 + 𝑢) → 𝑚 = 𝑢))
167 dvdsabsb 15048 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℤ ∧ (𝑚𝑢) ∈ ℤ) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
16899, 89, 167syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) ↔ 𝑃 ∥ (abs‘(𝑚𝑢))))
169 letr 10169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (abs‘(𝑚𝑢)) ∈ ℝ ∧ (𝑚 + 𝑢) ∈ ℝ) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
170100, 124, 93, 169syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ≤ (abs‘(𝑚𝑢)) ∧ (abs‘(𝑚𝑢)) ≤ (𝑚 + 𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
171157, 170mpan2d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ≤ (abs‘(𝑚𝑢)) → 𝑃 ≤ (𝑚 + 𝑢)))
172117, 171mtod 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
173172adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ≤ (abs‘(𝑚𝑢)))
17499adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → 𝑃 ∈ ℤ)
175 dvdsle 15079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (abs‘(𝑚𝑢)) ∈ ℕ) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
176174, 137, 175syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑃 ≤ (abs‘(𝑚𝑢))))
177173, 176mtod 189 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) ∧ 𝑚𝑢) → ¬ 𝑃 ∥ (abs‘(𝑚𝑢)))
178177ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑚𝑢 → ¬ 𝑃 ∥ (abs‘(𝑚𝑢))))
179178necon4ad 2842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (abs‘(𝑚𝑢)) → 𝑚 = 𝑢))
180168, 179sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (𝑃 ∥ (𝑚𝑢) → 𝑚 = 𝑢))
181166, 180jaod 394 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → ((𝑃 ∥ (𝑚 + 𝑢) ∨ 𝑃 ∥ (𝑚𝑢)) → 𝑚 = 𝑢))
18292, 181sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) → 𝑚 = 𝑢))
183 oveq1 6697 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑢 → (𝑚↑2) = (𝑢↑2))
184183oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑢 → ((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃))
185182, 184impbid1 215 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁))) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢))
186185ex 449 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑚 ∈ (0...𝑁) ∧ 𝑢 ∈ (0...𝑁)) → (((𝑚↑2) mod 𝑃) = ((𝑢↑2) mod 𝑃) ↔ 𝑚 = 𝑢)))
18772, 186dom2lem 8037 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)))
188 f1f1orn 6186 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1→(0...(𝑃 − 1)) → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
189187, 188syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
190 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
191190rnmpt 5403 . . . . . . . . . . . . . . . . 17 ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}
1922, 191eqtr4i 2676 . . . . . . . . . . . . . . . 16 𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))
193 f1oeq3 6167 . . . . . . . . . . . . . . . 16 (𝐴 = ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)) → ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃))))
194192, 193ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 ↔ (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto→ran (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)))
195189, 194sylibr 224 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴)
196 ovex 6718 . . . . . . . . . . . . . . 15 (0...𝑁) ∈ V
197196f1oen 8018 . . . . . . . . . . . . . 14 ((𝑚 ∈ (0...𝑁) ↦ ((𝑚↑2) mod 𝑃)):(0...𝑁)–1-1-onto𝐴 → (0...𝑁) ≈ 𝐴)
198195, 197syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...𝑁) ≈ 𝐴)
199198ensymd 8048 . . . . . . . . . . . 12 (𝜑𝐴 ≈ (0...𝑁))
200 ax-1cn 10032 . . . . . . . . . . . . . . 15 1 ∈ ℂ
201 pncan 10325 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
20260, 200, 201sylancl 695 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
203202oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
20459nnnn0d 11389 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ0)
205 peano2nn0 11371 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
206204, 205syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ ℕ0)
207206nn0zd 11518 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℤ)
208 fz01en 12407 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℤ → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
209207, 208syl 17 . . . . . . . . . . . . 13 (𝜑 → (0...((𝑁 + 1) − 1)) ≈ (1...(𝑁 + 1)))
210203, 209eqbrtrrd 4709 . . . . . . . . . . . 12 (𝜑 → (0...𝑁) ≈ (1...(𝑁 + 1)))
211 entr 8049 . . . . . . . . . . . 12 ((𝐴 ≈ (0...𝑁) ∧ (0...𝑁) ≈ (1...(𝑁 + 1))) → 𝐴 ≈ (1...(𝑁 + 1)))
212199, 210, 211syl2anc 694 . . . . . . . . . . 11 (𝜑𝐴 ≈ (1...(𝑁 + 1)))
213 ssfi 8221 . . . . . . . . . . . . 13 (((0...(𝑃 − 1)) ∈ Fin ∧ 𝐴 ⊆ (0...(𝑃 − 1))) → 𝐴 ∈ Fin)
2141, 15, 213syl2anc 694 . . . . . . . . . . . 12 (𝜑𝐴 ∈ Fin)
215 fzfid 12812 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) ∈ Fin)
216 hashen 13175 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) → ((#‘𝐴) = (#‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
217214, 215, 216syl2anc 694 . . . . . . . . . . 11 (𝜑 → ((#‘𝐴) = (#‘(1...(𝑁 + 1))) ↔ 𝐴 ≈ (1...(𝑁 + 1))))
218212, 217mpbird 247 . . . . . . . . . 10 (𝜑 → (#‘𝐴) = (#‘(1...(𝑁 + 1))))
219 hashfz1 13174 . . . . . . . . . . 11 ((𝑁 + 1) ∈ ℕ0 → (#‘(1...(𝑁 + 1))) = (𝑁 + 1))
220206, 219syl 17 . . . . . . . . . 10 (𝜑 → (#‘(1...(𝑁 + 1))) = (𝑁 + 1))
221218, 220eqtrd 2685 . . . . . . . . 9 (𝜑 → (#‘𝐴) = (𝑁 + 1))
22227ex 449 . . . . . . . . . . . . . . 15 (𝜑 → (𝑣𝐴 → ((𝑃 − 1) − 𝑣) ∈ (0...(𝑃 − 1))))
22320adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (𝑃 − 1) ∈ ℂ)
224 fzssuz 12420 . . . . . . . . . . . . . . . . . . . . 21 (0...(𝑃 − 1)) ⊆ (ℤ‘0)
225 uzssz 11745 . . . . . . . . . . . . . . . . . . . . . 22 (ℤ‘0) ⊆ ℤ
226 zsscn 11423 . . . . . . . . . . . . . . . . . . . . . 22 ℤ ⊆ ℂ
227225, 226sstri 3645 . . . . . . . . . . . . . . . . . . . . 21 (ℤ‘0) ⊆ ℂ
228224, 227sstri 3645 . . . . . . . . . . . . . . . . . . . 20 (0...(𝑃 − 1)) ⊆ ℂ
22915, 228syl6ss 3648 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ⊆ ℂ)
230229sselda 3636 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝐴) → 𝑣 ∈ ℂ)
231230adantrr 753 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑣 ∈ ℂ)
232229sselda 3636 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → 𝑘 ∈ ℂ)
233232adantrl 752 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → 𝑘 ∈ ℂ)
234223, 231, 233subcanad 10473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑣𝐴𝑘𝐴)) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘))
235234ex 449 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑣𝐴𝑘𝐴) → (((𝑃 − 1) − 𝑣) = ((𝑃 − 1) − 𝑘) ↔ 𝑣 = 𝑘)))
236222, 235dom2lem 8037 . . . . . . . . . . . . . 14 (𝜑 → (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
237 f1eq1 6134 . . . . . . . . . . . . . . 15 (𝐹 = (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)) → (𝐹:𝐴1-1→(0...(𝑃 − 1)) ↔ (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1))))
23828, 237ax-mp 5 . . . . . . . . . . . . . 14 (𝐹:𝐴1-1→(0...(𝑃 − 1)) ↔ (𝑣𝐴 ↦ ((𝑃 − 1) − 𝑣)):𝐴1-1→(0...(𝑃 − 1)))
239236, 238sylibr 224 . . . . . . . . . . . . 13 (𝜑𝐹:𝐴1-1→(0...(𝑃 − 1)))
240 f1f1orn 6186 . . . . . . . . . . . . 13 (𝐹:𝐴1-1→(0...(𝑃 − 1)) → 𝐹:𝐴1-1-onto→ran 𝐹)
241239, 240syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝐴1-1-onto→ran 𝐹)
242 f1oeng 8016 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ 𝐹:𝐴1-1-onto→ran 𝐹) → 𝐴 ≈ ran 𝐹)
243214, 241, 242syl2anc 694 . . . . . . . . . . 11 (𝜑𝐴 ≈ ran 𝐹)
244 ssfi 8221 . . . . . . . . . . . . 13 (((0...(𝑃 − 1)) ∈ Fin ∧ ran 𝐹 ⊆ (0...(𝑃 − 1))) → ran 𝐹 ∈ Fin)
2451, 31, 244syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 ∈ Fin)
246 hashen 13175 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin) → ((#‘𝐴) = (#‘ran 𝐹) ↔ 𝐴 ≈ ran 𝐹))
247214, 245, 246syl2anc 694 . . . . . . . . . . 11 (𝜑 → ((#‘𝐴) = (#‘ran 𝐹) ↔ 𝐴 ≈ ran 𝐹))
248243, 247mpbird 247 . . . . . . . . . 10 (𝜑 → (#‘𝐴) = (#‘ran 𝐹))
249248, 221eqtr3d 2687 . . . . . . . . 9 (𝜑 → (#‘ran 𝐹) = (𝑁 + 1))
250221, 249oveq12d 6708 . . . . . . . 8 (𝜑 → ((#‘𝐴) + (#‘ran 𝐹)) = ((𝑁 + 1) + (𝑁 + 1)))
25162, 71, 2503eqtr4d 2695 . . . . . . 7 (𝜑 → (𝑃 + 1) = ((#‘𝐴) + (#‘ran 𝐹)))
252251adantr 480 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = ((#‘𝐴) + (#‘ran 𝐹)))
253214adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝐴 ∈ Fin)
254245adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → ran 𝐹 ∈ Fin)
255 simpr 476 . . . . . . 7 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝐴 ∩ ran 𝐹) = ∅)
256 hashun 13209 . . . . . . 7 ((𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) = ∅) → (#‘(𝐴 ∪ ran 𝐹)) = ((#‘𝐴) + (#‘ran 𝐹)))
257253, 254, 255, 256syl3anc 1366 . . . . . 6 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (#‘(𝐴 ∪ ran 𝐹)) = ((#‘𝐴) + (#‘ran 𝐹)))
258252, 257eqtr4d 2688 . . . . 5 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → (𝑃 + 1) = (#‘(𝐴 ∪ ran 𝐹)))
25958, 258breqtrd 4711 . . . 4 ((𝜑 ∧ (𝐴 ∩ ran 𝐹) = ∅) → 𝑃 < (#‘(𝐴 ∪ ran 𝐹)))
260259ex 449 . . 3 (𝜑 → ((𝐴 ∩ ran 𝐹) = ∅ → 𝑃 < (#‘(𝐴 ∪ ran 𝐹))))
261260necon3bd 2837 . 2 (𝜑 → (¬ 𝑃 < (#‘(𝐴 ∪ ran 𝐹)) → (𝐴 ∩ ran 𝐹) ≠ ∅))
26256, 261mpd 15 1 (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wrex 2942  cun 3605  cin 3606  wss 3607  c0 3948   class class class wbr 4685  cmpt 4762  ran crn 5144  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  cen 7994  cdom 7995  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364   mod cmo 12708  cexp 12900  #chash 13157  abscabs 14018  cdvds 15027  cprime 15432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433
This theorem is referenced by:  4sqlem12  15707
  Copyright terms: Public domain W3C validator