Metamath Proof Explorer

Theorem 4sqlem11

Description: Lemma for 4sq . Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P . (Contributed by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
4sq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4sq.3 ⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4sq.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4sqlem11.5 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) }
4sqlem11.6 ⊢ 𝐹 = ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) )
Assertion 4sqlem11 ( 𝜑 → ( 𝐴 ∩ ran 𝐹 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 4sq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 4sq.3 ⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4 4sq.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 4sqlem11.5 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) }
6 4sqlem11.6 ⊢ 𝐹 = ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) )
7 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑃 − 1 ) ) ∈ Fin )
8 elfzelz ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℤ )
9 zsqcl ⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ↑ 2 ) ∈ ℤ )
10 8 9 syl ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑚 ↑ 2 ) ∈ ℤ )
11 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
12 4 11 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
13 zmodfz ⊢ ( ( ( 𝑚 ↑ 2 ) ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
14 10 12 13 syl2anr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
15 eleq1a ⊢ ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) → 𝑢 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) → 𝑢 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
17 16 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) → 𝑢 ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
18 17 abssdv ⊢ ( 𝜑 → { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) } ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
19 5 18 eqsstrid ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
20 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
21 4 20 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
22 peano2zm ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
23 21 22 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
24 23 zcnd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
25 24 addid2d ⊢ ( 𝜑 → ( 0 + ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) )
26 25 oveq1d ⊢ ( 𝜑 → ( ( 0 + ( 𝑃 − 1 ) ) − 𝑣 ) = ( ( 𝑃 − 1 ) − 𝑣 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 0 + ( 𝑃 − 1 ) ) − 𝑣 ) = ( ( 𝑃 − 1 ) − 𝑣 ) )
28 19 sselda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
29 fzrev3i ⊢ ( 𝑣 ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( ( 0 + ( 𝑃 − 1 ) ) − 𝑣 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 0 + ( 𝑃 − 1 ) ) − 𝑣 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
31 27 30 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑃 − 1 ) − 𝑣 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
32 31 6 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
33 32 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
34 19 33 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ ran 𝐹 ) ⊆ ( 0 ... ( 𝑃 − 1 ) ) )
35 7 34 ssfid ⊢ ( 𝜑 → ( 𝐴 ∪ ran 𝐹 ) ∈ Fin )
36 hashcl ⊢ ( ( 𝐴 ∪ ran 𝐹 ) ∈ Fin → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ∈ ℕ0 )
37 35 36 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ∈ ℕ0 )
38 37 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ∈ ℝ )
39 21 zred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
40 ssdomg ⊢ ( ( 0 ... ( 𝑃 − 1 ) ) ∈ Fin → ( ( 𝐴 ∪ ran 𝐹 ) ⊆ ( 0 ... ( 𝑃 − 1 ) ) → ( 𝐴 ∪ ran 𝐹 ) ≼ ( 0 ... ( 𝑃 − 1 ) ) ) )
41 7 34 40 sylc ⊢ ( 𝜑 → ( 𝐴 ∪ ran 𝐹 ) ≼ ( 0 ... ( 𝑃 − 1 ) ) )
42 hashdom ⊢ ( ( ( 𝐴 ∪ ran 𝐹 ) ∈ Fin ∧ ( 0 ... ( 𝑃 − 1 ) ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ≤ ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) ↔ ( 𝐴 ∪ ran 𝐹 ) ≼ ( 0 ... ( 𝑃 − 1 ) ) ) )
43 35 7 42 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ≤ ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) ↔ ( 𝐴 ∪ ran 𝐹 ) ≼ ( 0 ... ( 𝑃 − 1 ) ) ) )
44 41 43 mpbird ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ≤ ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) )
45 fz01en ⊢ ( 𝑃 ∈ ℤ → ( 0 ... ( 𝑃 − 1 ) ) ≈ ( 1 ... 𝑃 ) )
46 21 45 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑃 − 1 ) ) ≈ ( 1 ... 𝑃 ) )
47 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑃 ) ∈ Fin )
48 hashen ⊢ ( ( ( 0 ... ( 𝑃 − 1 ) ) ∈ Fin ∧ ( 1 ... 𝑃 ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑃 ) ) ↔ ( 0 ... ( 𝑃 − 1 ) ) ≈ ( 1 ... 𝑃 ) ) )
49 7 47 48 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑃 ) ) ↔ ( 0 ... ( 𝑃 − 1 ) ) ≈ ( 1 ... 𝑃 ) ) )
50 46 49 mpbird ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑃 ) ) )
51 12 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
52 hashfz1 ⊢ ( 𝑃 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑃 ) ) = 𝑃 )
53 51 52 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑃 ) ) = 𝑃 )
54 50 53 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑃 − 1 ) ) ) = 𝑃 )
55 44 54 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ≤ 𝑃 )
56 38 39 55 lensymd ⊢ ( 𝜑 → ¬ 𝑃 < ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) )
57 39 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → 𝑃 ∈ ℝ )
58 57 ltp1d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → 𝑃 < ( 𝑃 + 1 ) )
59 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
60 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
61 59 59 60 60 add4d ⊢ ( 𝜑 → ( ( 𝑁 + 𝑁 ) + ( 1 + 1 ) ) = ( ( 𝑁 + 1 ) + ( 𝑁 + 1 ) ) )
62 3 oveq1d ⊢ ( 𝜑 → ( 𝑃 + 1 ) = ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) )
63 2cn ⊢ 2 ∈ ℂ
64 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 2 · 𝑁 ) ∈ ℂ )
65 63 59 64 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
66 65 60 60 addassd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) + 1 ) = ( ( 2 · 𝑁 ) + ( 1 + 1 ) ) )
67 59 2timesd ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
68 67 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + ( 1 + 1 ) ) = ( ( 𝑁 + 𝑁 ) + ( 1 + 1 ) ) )
69 62 66 68 3eqtrd ⊢ ( 𝜑 → ( 𝑃 + 1 ) = ( ( 𝑁 + 𝑁 ) + ( 1 + 1 ) ) )
70 14 ex ⊢ ( 𝜑 → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
71 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑃 ∈ ℕ )
72 8 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ℤ )
73 72 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 ↑ 2 ) ∈ ℤ )
74 elfzelz ⊢ ( 𝑢 ∈ ( 0 ... 𝑁 ) → 𝑢 ∈ ℤ )
75 74 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑢 ∈ ℤ )
76 zsqcl ⊢ ( 𝑢 ∈ ℤ → ( 𝑢 ↑ 2 ) ∈ ℤ )
77 75 76 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑢 ↑ 2 ) ∈ ℤ )
78 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑚 ↑ 2 ) ∈ ℤ ∧ ( 𝑢 ↑ 2 ) ∈ ℤ ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) )
79 71 73 77 78 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ) )
80 72 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ℂ )
81 75 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑢 ∈ ℂ )
82 subsq ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) = ( ( 𝑚 + 𝑢 ) · ( 𝑚 − 𝑢 ) ) )
83 80 81 82 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑚 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) = ( ( 𝑚 + 𝑢 ) · ( 𝑚 − 𝑢 ) ) )
84 83 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( ( 𝑚 ↑ 2 ) − ( 𝑢 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑚 + 𝑢 ) · ( 𝑚 − 𝑢 ) ) ) )
85 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑃 ∈ ℙ )
86 72 75 zaddcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 𝑢 ) ∈ ℤ )
87 72 75 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 − 𝑢 ) ∈ ℤ )
88 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑚 + 𝑢 ) ∈ ℤ ∧ ( 𝑚 − 𝑢 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑚 + 𝑢 ) · ( 𝑚 − 𝑢 ) ) ↔ ( 𝑃 ∥ ( 𝑚 + 𝑢 ) ∨ 𝑃 ∥ ( 𝑚 − 𝑢 ) ) ) )
89 85 86 87 88 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( ( 𝑚 + 𝑢 ) · ( 𝑚 − 𝑢 ) ) ↔ ( 𝑃 ∥ ( 𝑚 + 𝑢 ) ∨ 𝑃 ∥ ( 𝑚 − 𝑢 ) ) ) )
90 79 84 89 3bitrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) ↔ ( 𝑃 ∥ ( 𝑚 + 𝑢 ) ∨ 𝑃 ∥ ( 𝑚 − 𝑢 ) ) ) )
91 86 zred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 𝑢 ) ∈ ℝ )
92 2re ⊢ 2 ∈ ℝ
93 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
94 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 · 𝑁 ) ∈ ℝ )
95 92 93 94 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 2 · 𝑁 ) ∈ ℝ )
97 85 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑃 ∈ ℤ )
98 97 zred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑃 ∈ ℝ )
99 72 zred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ∈ ℝ )
100 75 zred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑢 ∈ ℝ )
101 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℝ )
102 elfzle2 ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ≤ 𝑁 )
103 102 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑚 ≤ 𝑁 )
104 elfzle2 ⊢ ( 𝑢 ∈ ( 0 ... 𝑁 ) → 𝑢 ≤ 𝑁 )
105 104 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑢 ≤ 𝑁 )
106 99 100 101 101 103 105 le2addd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 𝑢 ) ≤ ( 𝑁 + 𝑁 ) )
107 59 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 𝑁 ∈ ℂ )
108 107 2timesd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
109 106 108 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 𝑢 ) ≤ ( 2 · 𝑁 ) )
110 95 ltp1d ⊢ ( 𝜑 → ( 2 · 𝑁 ) < ( ( 2 · 𝑁 ) + 1 ) )
111 110 3 breqtrrd ⊢ ( 𝜑 → ( 2 · 𝑁 ) < 𝑃 )
112 111 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 2 · 𝑁 ) < 𝑃 )
113 91 96 98 109 112 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 + 𝑢 ) < 𝑃 )
114 91 98 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑚 + 𝑢 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
115 113 114 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ¬ 𝑃 ≤ ( 𝑚 + 𝑢 ) )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ¬ 𝑃 ≤ ( 𝑚 + 𝑢 ) )
117 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 𝑃 ∈ ℤ )
118 86 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑚 + 𝑢 ) ∈ ℤ )
119 1red ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 1 ∈ ℝ )
120 nn0abscl ⊢ ( ( 𝑚 − 𝑢 ) ∈ ℤ → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ0 )
121 87 120 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ0 )
122 121 nn0red ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℝ )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℝ )
124 118 zred ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑚 + 𝑢 ) ∈ ℝ )
125 121 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ0 )
126 125 nn0zd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℤ )
127 87 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 − 𝑢 ) ∈ ℂ )
128 127 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑚 − 𝑢 ) ∈ ℂ )
129 80 81 subeq0ad ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑚 − 𝑢 ) = 0 ↔ 𝑚 = 𝑢 ) )
130 129 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑚 − 𝑢 ) ≠ 0 ↔ 𝑚 ≠ 𝑢 ) )
131 130 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑚 − 𝑢 ) ≠ 0 )
132 128 131 absrpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℝ+ )
133 132 rpgt0d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 0 < ( abs ‘ ( 𝑚 − 𝑢 ) ) )
134 elnnz ⊢ ( ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ ↔ ( ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℤ ∧ 0 < ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
135 126 133 134 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ )
136 135 nnge1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 1 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) )
137 0cnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 0 ∈ ℂ )
138 80 81 137 abs3difd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ≤ ( ( abs ‘ ( 𝑚 − 0 ) ) + ( abs ‘ ( 0 − 𝑢 ) ) ) )
139 80 subid1d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 − 0 ) = 𝑚 )
140 139 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 0 ) ) = ( abs ‘ 𝑚 ) )
141 elfzle1 ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑚 )
142 141 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 0 ≤ 𝑚 )
143 99 142 absidd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ 𝑚 ) = 𝑚 )
144 140 143 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 0 ) ) = 𝑚 )
145 0cn ⊢ 0 ∈ ℂ
146 abssub ⊢ ( ( 0 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 0 ) ) )
147 145 81 146 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 0 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 0 ) ) )
148 81 subid1d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑢 − 0 ) = 𝑢 )
149 148 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑢 − 0 ) ) = ( abs ‘ 𝑢 ) )
150 elfzle1 ⊢ ( 𝑢 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑢 )
151 150 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → 0 ≤ 𝑢 )
152 100 151 absidd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ 𝑢 ) = 𝑢 )
153 147 149 152 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 0 − 𝑢 ) ) = 𝑢 )
154 144 153 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( abs ‘ ( 𝑚 − 0 ) ) + ( abs ‘ ( 0 − 𝑢 ) ) ) = ( 𝑚 + 𝑢 ) )
155 138 154 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ≤ ( 𝑚 + 𝑢 ) )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( abs ‘ ( 𝑚 − 𝑢 ) ) ≤ ( 𝑚 + 𝑢 ) )
157 119 123 124 136 156 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 1 ≤ ( 𝑚 + 𝑢 ) )
158 elnnz1 ⊢ ( ( 𝑚 + 𝑢 ) ∈ ℕ ↔ ( ( 𝑚 + 𝑢 ) ∈ ℤ ∧ 1 ≤ ( 𝑚 + 𝑢 ) ) )
159 118 157 158 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑚 + 𝑢 ) ∈ ℕ )
160 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑚 + 𝑢 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝑚 + 𝑢 ) → 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
161 117 159 160 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑃 ∥ ( 𝑚 + 𝑢 ) → 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
162 116 161 mtod ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ¬ 𝑃 ∥ ( 𝑚 + 𝑢 ) )
163 162 ex ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 ≠ 𝑢 → ¬ 𝑃 ∥ ( 𝑚 + 𝑢 ) ) )
164 163 necon4ad ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( 𝑚 + 𝑢 ) → 𝑚 = 𝑢 ) )
165 dvdsabsb ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑚 − 𝑢 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝑚 − 𝑢 ) ↔ 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
166 97 87 165 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( 𝑚 − 𝑢 ) ↔ 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
167 letr ⊢ ( ( 𝑃 ∈ ℝ ∧ ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℝ ∧ ( 𝑚 + 𝑢 ) ∈ ℝ ) → ( ( 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) ∧ ( abs ‘ ( 𝑚 − 𝑢 ) ) ≤ ( 𝑚 + 𝑢 ) ) → 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
168 98 122 91 167 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) ∧ ( abs ‘ ( 𝑚 − 𝑢 ) ) ≤ ( 𝑚 + 𝑢 ) ) → 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
169 155 168 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) → 𝑃 ≤ ( 𝑚 + 𝑢 ) ) )
170 115 169 mtod ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ¬ 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) )
171 170 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ¬ 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) )
172 97 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → 𝑃 ∈ ℤ )
173 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( abs ‘ ( 𝑚 − 𝑢 ) ) ∈ ℕ ) → ( 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) → 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
174 172 135 173 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ( 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) → 𝑃 ≤ ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
175 171 174 mtod ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑚 ≠ 𝑢 ) → ¬ 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) )
176 175 ex ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑚 ≠ 𝑢 → ¬ 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) ) )
177 176 necon4ad ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( abs ‘ ( 𝑚 − 𝑢 ) ) → 𝑚 = 𝑢 ) )
178 166 177 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑃 ∥ ( 𝑚 − 𝑢 ) → 𝑚 = 𝑢 ) )
179 164 178 jaod ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑃 ∥ ( 𝑚 + 𝑢 ) ∨ 𝑃 ∥ ( 𝑚 − 𝑢 ) ) → 𝑚 = 𝑢 ) )
180 90 179 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) → 𝑚 = 𝑢 ) )
181 oveq1 ⊢ ( 𝑚 = 𝑢 → ( 𝑚 ↑ 2 ) = ( 𝑢 ↑ 2 ) )
182 181 oveq1d ⊢ ( 𝑚 = 𝑢 → ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) )
183 180 182 impbid1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) ↔ 𝑚 = 𝑢 ) )
184 183 ex ⊢ ( 𝜑 → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑢 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑚 ↑ 2 ) mod 𝑃 ) = ( ( 𝑢 ↑ 2 ) mod 𝑃 ) ↔ 𝑚 = 𝑢 ) ) )
185 70 184 dom2lem ⊢ ( 𝜑 → ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1→ ( 0 ... ( 𝑃 − 1 ) ) )
186 f1f1orn ⊢ ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1→ ( 0 ... ( 𝑃 − 1 ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) )
187 185 186 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) )
188 eqid ⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) = ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) )
189 188 rnmpt ⊢ ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) = { 𝑢 ∣ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑢 = ( ( 𝑚 ↑ 2 ) mod 𝑃 ) }
190 5 189 eqtr4i ⊢ 𝐴 = ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) )
191 f1oeq3 ⊢ ( 𝐴 = ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ 𝐴 ↔ ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) ) )
192 190 191 ax-mp ⊢ ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ 𝐴 ↔ ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) )
193 187 192 sylibr ⊢ ( 𝜑 → ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ 𝐴 )
194 ovex ⊢ ( 0 ... 𝑁 ) ∈ V
195 194 f1oen ⊢ ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑚 ↑ 2 ) mod 𝑃 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ 𝐴 → ( 0 ... 𝑁 ) ≈ 𝐴 )
196 193 195 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ≈ 𝐴 )
197 196 ensymd ⊢ ( 𝜑 → 𝐴 ≈ ( 0 ... 𝑁 ) )
198 ax-1cn ⊢ 1 ∈ ℂ
199 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
200 59 198 199 sylancl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
201 200 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
202 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
203 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
204 202 203 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
205 204 nn0zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
206 fz01en ⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ≈ ( 1 ... ( 𝑁 + 1 ) ) )
207 205 206 syl ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ≈ ( 1 ... ( 𝑁 + 1 ) ) )
208 201 207 eqbrtrrd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ≈ ( 1 ... ( 𝑁 + 1 ) ) )
209 entr ⊢ ( ( 𝐴 ≈ ( 0 ... 𝑁 ) ∧ ( 0 ... 𝑁 ) ≈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐴 ≈ ( 1 ... ( 𝑁 + 1 ) ) )
210 197 208 209 syl2anc ⊢ ( 𝜑 → 𝐴 ≈ ( 1 ... ( 𝑁 + 1 ) ) )
211 7 19 ssfid ⊢ ( 𝜑 → 𝐴 ∈ Fin )
212 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
213 hashen ⊢ ( ( 𝐴 ∈ Fin ∧ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ↔ 𝐴 ≈ ( 1 ... ( 𝑁 + 1 ) ) ) )
214 211 212 213 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ↔ 𝐴 ≈ ( 1 ... ( 𝑁 + 1 ) ) ) )
215 210 214 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
216 hashfz1 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
217 204 216 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
218 215 217 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( 𝑁 + 1 ) )
219 31 ex ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐴 → ( ( 𝑃 − 1 ) − 𝑣 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ) )
220 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝑃 − 1 ) ∈ ℂ )
221 fzssuz ⊢ ( 0 ... ( 𝑃 − 1 ) ) ⊆ ( ℤ≥ ‘ 0 )
222 uzssz ⊢ ( ℤ≥ ‘ 0 ) ⊆ ℤ
223 zsscn ⊢ ℤ ⊆ ℂ
224 222 223 sstri ⊢ ( ℤ≥ ‘ 0 ) ⊆ ℂ
225 221 224 sstri ⊢ ( 0 ... ( 𝑃 − 1 ) ) ⊆ ℂ
226 19 225 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
227 226 sselda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ℂ )
228 227 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) ) → 𝑣 ∈ ℂ )
229 226 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℂ )
230 229 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) ) → 𝑘 ∈ ℂ )
231 220 228 230 subcanad ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ( 𝑃 − 1 ) − 𝑣 ) = ( ( 𝑃 − 1 ) − 𝑘 ) ↔ 𝑣 = 𝑘 ) )
232 231 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝑃 − 1 ) − 𝑣 ) = ( ( 𝑃 − 1 ) − 𝑘 ) ↔ 𝑣 = 𝑘 ) ) )
233 219 232 dom2lem ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) ) : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) )
234 f1eq1 ⊢ ( 𝐹 = ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) ) → ( 𝐹 : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) ) : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) ) )
235 6 234 ax-mp ⊢ ( 𝐹 : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( 𝑣 ∈ 𝐴 ↦ ( ( 𝑃 − 1 ) − 𝑣 ) ) : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) )
236 233 235 sylibr ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) )
237 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ ( 0 ... ( 𝑃 − 1 ) ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
238 236 237 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
239 211 238 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ran 𝐹 ) )
240 239 218 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ran 𝐹 ) = ( 𝑁 + 1 ) )
241 218 240 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ran 𝐹 ) ) = ( ( 𝑁 + 1 ) + ( 𝑁 + 1 ) ) )
242 61 69 241 3eqtr4d ⊢ ( 𝜑 → ( 𝑃 + 1 ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ran 𝐹 ) ) )
243 242 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ( 𝑃 + 1 ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ran 𝐹 ) ) )
244 211 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → 𝐴 ∈ Fin )
245 7 33 ssfid ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
246 245 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ran 𝐹 ∈ Fin )
247 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ( 𝐴 ∩ ran 𝐹 ) = ∅ )
248 hashun ⊢ ( ( 𝐴 ∈ Fin ∧ ran 𝐹 ∈ Fin ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ran 𝐹 ) ) )
249 244 246 247 248 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ran 𝐹 ) ) )
250 243 249 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → ( 𝑃 + 1 ) = ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) )
251 58 250 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ ran 𝐹 ) = ∅ ) → 𝑃 < ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) )
252 251 ex ⊢ ( 𝜑 → ( ( 𝐴 ∩ ran 𝐹 ) = ∅ → 𝑃 < ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) ) )
253 252 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑃 < ( ♯ ‘ ( 𝐴 ∪ ran 𝐹 ) ) → ( 𝐴 ∩ ran 𝐹 ) ≠ ∅ ) )
254 56 253 mpd ⊢ ( 𝜑 → ( 𝐴 ∩ ran 𝐹 ) ≠ ∅ )