Metamath Proof Explorer

Theorem gausslemma2dlem1a

Description: Lemma for gausslemma2dlem1 . (Contributed by AV, 1-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
Assertion gausslemma2dlem1a ( 𝜑 → ran 𝑅 = ( 1 ... 𝐻 ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3 gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4 3 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝑅 ↔ ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) )
5 4 elv ⊢ ( 𝑦 ∈ ran 𝑅 ↔ ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
6 iftrue ⊢ ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑥 · 2 ) )
7 6 eqeq2d ⊢ ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑥 · 2 ) ) )
8 7 adantr ⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑥 · 2 ) ) )
9 elfz1b ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) )
10 id ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ )
11 2nn ⊢ 2 ∈ ℕ
12 11 a1i ⊢ ( 𝑥 ∈ ℕ → 2 ∈ ℕ )
13 10 12 nnmulcld ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℕ )
14 13 3ad2ant1 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑥 · 2 ) ∈ ℕ )
15 14 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑥 · 2 ) ∈ ℕ )
16 2 eleq1i ⊢ ( 𝐻 ∈ ℕ ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
17 16 biimpi ⊢ ( 𝐻 ∈ ℕ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
18 17 3ad2ant2 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
19 18 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
20 nnoddn2prm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
21 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
22 21 anim1i ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
23 20 22 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
24 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
25 2z ⊢ 2 ∈ ℤ
26 25 a1i ⊢ ( 𝑥 ∈ ℕ → 2 ∈ ℤ )
27 24 26 zmulcld ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℤ )
28 27 3ad2ant1 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑥 · 2 ) ∈ ℤ )
29 23 28 anim12i ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
30 df-3an ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ↔ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
31 29 30 sylibr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
32 31 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ) )
33 1 32 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ) )
34 33 impcom ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
35 ltoddhalfle ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
36 34 35 syl ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
37 36 biimp3a ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
38 15 19 37 3jca ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
39 38 3exp ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝜑 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) ) )
40 9 39 sylbi ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝜑 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) ) )
41 40 impcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
42 41 impcom ⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
43 2 oveq2i ⊢ ( 1 ... 𝐻 ) = ( 1 ... ( ( 𝑃 − 1 ) / 2 ) )
44 43 eleq2i ⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 · 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
45 elfz1b ⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
46 44 45 bitri ⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
47 42 46 sylibr ⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) )
48 eleq1 ⊢ ( 𝑦 = ( 𝑥 · 2 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ) )
49 47 48 syl5ibrcom ⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = ( 𝑥 · 2 ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
50 8 49 sylbid ⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
51 iffalse ⊢ ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑃 − ( 𝑥 · 2 ) ) )
52 51 eqeq2d ⊢ ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) ) )
53 52 adantr ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) ) )
54 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
55 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
56 1 54 55 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
57 56 ad2antrl ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 𝑃 ∈ ℤ )
58 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 𝑥 ∈ ℤ )
59 25 a1i ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 2 ∈ ℤ )
60 58 59 zmulcld ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑥 · 2 ) ∈ ℤ )
61 60 ad2antll ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑥 · 2 ) ∈ ℤ )
62 57 61 zsubcld ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ )
63 55 zred ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
64 2 breq2i ⊢ ( 𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
65 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
66 65 adantr ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → 𝑥 ∈ ℝ )
67 peano2rem ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
68 67 adantl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − 1 ) ∈ ℝ )
69 2re ⊢ 2 ∈ ℝ
70 2pos ⊢ 0 < 2
71 69 70 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
72 71 a1i ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
73 lemuldiv ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
74 66 68 72 73 syl3anc ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
75 64 74 bitr4id ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 ≤ 𝐻 ↔ ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ) )
76 13 nnred ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℝ )
77 76 adantr ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 · 2 ) ∈ ℝ )
78 simpr ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℝ )
79 77 68 78 lesub2d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
80 recn ⊢ ( 𝑃 ∈ ℝ → 𝑃 ∈ ℂ )
81 1cnd ⊢ ( 𝑃 ∈ ℝ → 1 ∈ ℂ )
82 80 81 nncand ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 − 1 ) ) = 1 )
83 82 adantl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − ( 𝑃 − 1 ) ) = 1 )
84 83 breq1d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ↔ 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
85 84 biimpd ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
86 79 85 sylbid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
87 75 86 sylbid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 ≤ 𝐻 → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
88 87 impancom ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
89 88 3adant2 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
90 9 89 sylbi ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
91 90 com12 ⊢ ( 𝑃 ∈ ℝ → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
92 63 91 syl ⊢ ( 𝑃 ∈ ℙ → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
93 1 54 92 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
94 93 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) )
95 94 adantl ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) )
96 elnnz1 ⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ ↔ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ∧ 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
97 62 95 96 sylanbrc ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ )
98 9 simp2bi ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 𝐻 ∈ ℕ )
99 98 ad2antll ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 𝐻 ∈ ℕ )
100 nnre ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
101 100 rehalfcld ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ∈ ℝ )
102 101 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 / 2 ) ∈ ℝ )
103 60 zred ⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑥 · 2 ) ∈ ℝ )
104 lenlt ⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) )
105 102 103 104 syl2an ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) )
106 22 60 anim12i ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
107 106 30 sylibr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
108 halfleoddlt ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
109 107 108 syl ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
110 109 biimpa ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 / 2 ) < ( 𝑥 · 2 ) )
111 nncn ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℂ )
112 subhalfhalf ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
113 111 112 syl ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
114 113 breq1d ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
115 114 ad3antrrr ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
116 110 115 mpbird ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) )
117 100 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℝ )
118 101 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 / 2 ) ∈ ℝ )
119 103 adantl ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑥 · 2 ) ∈ ℝ )
120 117 118 119 3jca ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) )
121 120 adantr ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) )
122 ltsub23 ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ) )
123 121 122 syl ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ) )
124 116 123 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) )
125 21 ad2antrr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℤ )
126 simplr ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ¬ 2 ∥ 𝑃 )
127 60 adantl ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑥 · 2 ) ∈ ℤ )
128 125 127 zsubcld ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ )
129 125 126 128 3jca ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) )
130 129 adantr ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) )
131 ltoddhalfle ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) → ( ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
132 130 131 syl ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
133 124 132 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
134 133 ex ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
135 2 breq2i ⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
136 134 135 imbitrrdi ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
137 105 136 sylbird ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
138 137 ex ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) ) )
139 1 20 138 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) ) )
140 139 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
141 140 impcom ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 )
142 elfz1b ⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
143 97 99 141 142 syl3anbrc ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) )
144 eleq1 ⊢ ( 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) ) )
145 143 144 syl5ibrcom ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
146 53 145 sylbid ⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
147 50 146 pm2.61ian ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
148 147 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
149 elfz1b ⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) )
150 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℕ )
151 simpl ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 2 ∥ 𝑦 )
152 nnehalf ⊢ ( ( 𝑦 ∈ ℕ ∧ 2 ∥ 𝑦 ) → ( 𝑦 / 2 ) ∈ ℕ )
153 150 151 152 syl2anr ⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 / 2 ) ∈ ℕ )
154 simpr2 ⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝐻 ∈ ℕ )
155 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
156 155 ad2antrr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → 𝑦 ∈ ℝ )
157 nnrp ⊢ ( 𝐻 ∈ ℕ → 𝐻 ∈ ℝ+ )
158 157 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → 𝐻 ∈ ℝ+ )
159 158 adantr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → 𝐻 ∈ ℝ+ )
160 2rp ⊢ 2 ∈ ℝ+
161 1le2 ⊢ 1 ≤ 2
162 160 161 pm3.2i ⊢ ( 2 ∈ ℝ+ ∧ 1 ≤ 2 )
163 162 a1i ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 2 ∈ ℝ+ ∧ 1 ≤ 2 ) )
164 ledivge1le ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 ≤ 2 ) ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) )
165 156 159 163 164 syl3anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) )
166 165 ex ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
167 166 com23 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
168 167 3impia ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 / 2 ) ≤ 𝐻 ) )
169 168 impcom ⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 / 2 ) ≤ 𝐻 )
170 153 154 169 3jca ⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
171 170 ex ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
172 149 171 biimtrid ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
173 172 3impia ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
174 elfz1b ⊢ ( ( 𝑦 / 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
175 173 174 sylibr ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑦 / 2 ) ∈ ( 1 ... 𝐻 ) )
176 oveq1 ⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑥 · 2 ) = ( ( 𝑦 / 2 ) · 2 ) )
177 176 breq1d ⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) ) )
178 176 oveq2d ⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) )
179 177 176 178 ifbieq12d ⊢ ( 𝑥 = ( 𝑦 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) )
180 179 eqeq2d ⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) ) )
181 180 adantl ⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) ∧ 𝑥 = ( 𝑦 / 2 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) ) )
182 elfzelz ⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 ∈ ℤ )
183 182 zcnd ⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 ∈ ℂ )
184 183 3ad2ant3 ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 ∈ ℂ )
185 2cnd ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
186 2ne0 ⊢ 2 ≠ 0
187 186 a1i ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ≠ 0 )
188 184 185 187 divcan1d ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) · 2 ) = 𝑦 )
189 2 breq2i ⊢ ( 𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
190 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
191 1 20 22 3syl ⊢ ( 𝜑 → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
192 191 adantl ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
193 190 192 anim12ci ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑦 ∈ ℤ ) )
194 df-3an ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) ↔ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑦 ∈ ℤ ) )
195 193 194 sylibr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) )
196 ltoddhalfle ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) → ( 𝑦 < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
197 195 196 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑦 < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
198 197 exbiri ⊢ ( 𝑦 ∈ ℕ → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
199 198 com23 ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
200 189 199 biimtrid ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
201 200 a1d ⊢ ( 𝑦 ∈ ℕ → ( 𝐻 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) ) )
202 201 3imp ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) )
203 149 202 sylbi ⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) )
204 203 com12 ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 < ( 𝑃 / 2 ) ) )
205 204 3impia ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 < ( 𝑃 / 2 ) )
206 188 205 eqbrtrd ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) )
207 206 iftrued ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) = ( ( 𝑦 / 2 ) · 2 ) )
208 207 188 eqtr2d ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) )
209 175 181 208 rspcedvd ⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
210 209 3exp ⊢ ( 2 ∥ 𝑦 → ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) ) )
211 54 55 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
212 211 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑃 ∈ ℤ )
213 190 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℤ )
214 213 adantl ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑦 ∈ ℤ )
215 212 214 zsubcld ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℤ )
216 155 ad2antrl ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → 𝑦 ∈ ℝ )
217 67 rehalfcld ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
218 217 adantr ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
219 simpl ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → 𝑃 ∈ ℝ )
220 216 218 219 3jca ⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) )
221 220 ex ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
222 54 63 221 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
223 222 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
224 223 impcom ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) )
225 lesub2 ⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
226 224 225 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
227 55 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
228 1cnd ⊢ ( 𝑃 ∈ ℂ → 1 ∈ ℂ )
229 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
230 229 a1i ⊢ ( 𝑃 ∈ ℂ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
231 divsubdir ⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
232 228 230 231 mpd3an23 ⊢ ( 𝑃 ∈ ℂ → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
233 232 oveq2d ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) )
234 id ⊢ ( 𝑃 ∈ ℂ → 𝑃 ∈ ℂ )
235 halfcl ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 / 2 ) ∈ ℂ )
236 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
237 236 a1i ⊢ ( 𝑃 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
238 234 235 237 subsubd ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) = ( ( 𝑃 − ( 𝑃 / 2 ) ) + ( 1 / 2 ) ) )
239 112 oveq1d ⊢ ( 𝑃 ∈ ℂ → ( ( 𝑃 − ( 𝑃 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
240 233 238 239 3eqtrd ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
241 54 227 240 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
242 241 ad2antrl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
243 242 breq1d ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ↔ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
244 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
245 halfre ⊢ ( 1 / 2 ) ∈ ℝ
246 245 a1i ⊢ ( 𝑃 ∈ ℕ → ( 1 / 2 ) ∈ ℝ )
247 nngt0 ⊢ ( 𝑃 ∈ ℕ → 0 < 𝑃 )
248 71 a1i ⊢ ( 𝑃 ∈ ℕ → ( 2 ∈ ℝ ∧ 0 < 2 ) )
249 divgt0 ⊢ ( ( ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 < ( 𝑃 / 2 ) )
250 100 247 248 249 syl21anc ⊢ ( 𝑃 ∈ ℕ → 0 < ( 𝑃 / 2 ) )
251 halfgt0 ⊢ 0 < ( 1 / 2 )
252 251 a1i ⊢ ( 𝑃 ∈ ℕ → 0 < ( 1 / 2 ) )
253 101 246 250 252 addgt0d ⊢ ( 𝑃 ∈ ℕ → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
254 54 244 253 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
255 254 ad2antrl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
256 0red ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 0 ∈ ℝ )
257 simpr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℝ )
258 257 rehalfcld ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 / 2 ) ∈ ℝ )
259 245 a1i ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 1 / 2 ) ∈ ℝ )
260 258 259 readdcld ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ )
261 resubcl ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
262 261 ancoms ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
263 256 260 262 3jca ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) )
264 263 ex ⊢ ( 𝑦 ∈ ℝ → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
265 155 264 syl ⊢ ( 𝑦 ∈ ℕ → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
266 265 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
267 266 com12 ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
268 54 63 267 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
269 268 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
270 269 impcom ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) )
271 ltletr ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) → ( ( 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) → 0 < ( 𝑃 − 𝑦 ) ) )
272 270 271 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) → 0 < ( 𝑃 − 𝑦 ) ) )
273 255 272 mpand ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
274 243 273 sylbid ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
275 226 274 sylbid ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 0 < ( 𝑃 − 𝑦 ) ) )
276 275 ex ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
277 276 com23 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
278 189 277 biimtrid ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ 𝐻 → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
279 278 3impia ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
280 279 impcom ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 0 < ( 𝑃 − 𝑦 ) )
281 elnnz ⊢ ( ( 𝑃 − 𝑦 ) ∈ ℕ ↔ ( ( 𝑃 − 𝑦 ) ∈ ℤ ∧ 0 < ( 𝑃 − 𝑦 ) ) )
282 215 280 281 sylanbrc ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℕ )
283 23 adantr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
284 simpr ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ¬ 2 ∥ 𝑦 )
285 284 213 anim12ci ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦 ) )
286 omoe ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦 ) ) → 2 ∥ ( 𝑃 − 𝑦 ) )
287 283 285 286 syl2an2r ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 2 ∥ ( 𝑃 − 𝑦 ) )
288 nnehalf ⊢ ( ( ( 𝑃 − 𝑦 ) ∈ ℕ ∧ 2 ∥ ( 𝑃 − 𝑦 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ )
289 282 287 288 syl2anc ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ )
290 simpr2 ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝐻 ∈ ℕ )
291 1red ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 1 ∈ ℝ )
292 155 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℝ )
293 292 adantl ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑦 ∈ ℝ )
294 54 63 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℝ )
295 294 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑃 ∈ ℝ )
296 nnge1 ⊢ ( 𝑦 ∈ ℕ → 1 ≤ 𝑦 )
297 296 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 1 ≤ 𝑦 )
298 297 adantl ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 1 ≤ 𝑦 )
299 291 293 295 298 lesub2dd ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) )
300 295 293 resubcld ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
301 54 63 67 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − 1 ) ∈ ℝ )
302 301 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
303 71 a1i ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
304 lediv1 ⊢ ( ( ( 𝑃 − 𝑦 ) ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
305 300 302 303 304 syl3anc ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
306 299 305 mpbid ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
307 2 breq2i ⊢ ( ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
308 306 307 sylibr ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 )
309 289 290 308 3jca ⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) )
310 309 ex ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) ) )
311 elfz1b ⊢ ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) )
312 310 149 311 3imtr4g ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) )
313 312 ex ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ¬ 2 ∥ 𝑦 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) ) )
314 1 313 syl ⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑦 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) ) )
315 314 3imp21 ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) )
316 oveq1 ⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑥 · 2 ) = ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) )
317 316 breq1d ⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) ) )
318 316 oveq2d ⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) )
319 317 316 318 ifbieq12d ⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) )
320 319 eqeq2d ⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) ) )
321 320 adantl ⊢ ( ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) ∧ 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) ) )
322 1 54 227 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
323 322 3ad2ant2 ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℂ )
324 183 3ad2ant3 ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 ∈ ℂ )
325 323 324 subcld ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℂ )
326 2cnd ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
327 186 a1i ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ≠ 0 )
328 325 326 327 divcan1d ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) = ( 𝑃 − 𝑦 ) )
329 zre ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ℝ )
330 halfge0 ⊢ 0 ≤ ( 1 / 2 )
331 rehalfcl ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 / 2 ) ∈ ℝ )
332 331 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 / 2 ) ∈ ℝ )
333 332 259 subge02d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 0 ≤ ( 1 / 2 ) ↔ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) )
334 330 333 mpbii ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) )
335 simpl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑦 ∈ ℝ )
336 245 a1i ⊢ ( 𝑃 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
337 331 336 resubcld ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ )
338 337 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ )
339 letr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ) → ( ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
340 335 338 332 339 syl3anc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
341 334 340 mpan2d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
342 80 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℂ )
343 1cnd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 1 ∈ ℂ )
344 229 a1i ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
345 342 343 344 231 syl3anc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
346 345 breq2d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) )
347 lesub ⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ) )
348 332 257 335 347 syl3anc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ) )
349 258 262 lenltd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
350 2cnd ⊢ ( 𝑃 ∈ ℝ → 2 ∈ ℂ )
351 186 a1i ⊢ ( 𝑃 ∈ ℝ → 2 ≠ 0 )
352 80 350 351 divcan1d ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) · 2 ) = 𝑃 )
353 352 eqcomd ⊢ ( 𝑃 ∈ ℝ → 𝑃 = ( ( 𝑃 / 2 ) · 2 ) )
354 353 oveq1d ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( ( ( 𝑃 / 2 ) · 2 ) − ( 𝑃 / 2 ) ) )
355 331 recnd ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 / 2 ) ∈ ℂ )
356 355 350 mulcomd ⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) · 2 ) = ( 2 · ( 𝑃 / 2 ) ) )
357 356 oveq1d ⊢ ( 𝑃 ∈ ℝ → ( ( ( 𝑃 / 2 ) · 2 ) − ( 𝑃 / 2 ) ) = ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) )
358 350 355 mulsubfacd ⊢ ( 𝑃 ∈ ℝ → ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) = ( ( 2 − 1 ) · ( 𝑃 / 2 ) ) )
359 2m1e1 ⊢ ( 2 − 1 ) = 1
360 359 a1i ⊢ ( 𝑃 ∈ ℝ → ( 2 − 1 ) = 1 )
361 360 oveq1d ⊢ ( 𝑃 ∈ ℝ → ( ( 2 − 1 ) · ( 𝑃 / 2 ) ) = ( 1 · ( 𝑃 / 2 ) ) )
362 355 mullidd ⊢ ( 𝑃 ∈ ℝ → ( 1 · ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
363 358 361 362 3eqtrd ⊢ ( 𝑃 ∈ ℝ → ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
364 354 357 363 3eqtrd ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
365 364 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
366 365 breq2d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ↔ 𝑦 ≤ ( 𝑃 / 2 ) ) )
367 348 349 366 3bitr3d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( 𝑃 / 2 ) ) )
368 341 346 367 3imtr4d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
369 368 ex ⊢ ( 𝑦 ∈ ℝ → ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
370 155 369 syl ⊢ ( 𝑦 ∈ ℕ → ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
371 370 com3l ⊢ ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
372 329 371 syl ⊢ ( 𝑃 ∈ ℤ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
373 54 55 372 3syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
374 1 373 syl ⊢ ( 𝜑 → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
375 374 adantl ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
376 375 com13 ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
377 189 376 biimtrid ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
378 377 a1d ⊢ ( 𝑦 ∈ ℕ → ( 𝐻 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) ) )
379 378 3imp ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
380 379 com12 ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
381 149 380 biimtrid ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
382 381 3impia ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) )
383 328 382 eqnbrtrd ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ¬ ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) )
384 383 iffalsed ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) = ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) )
385 328 oveq2d ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) = ( 𝑃 − ( 𝑃 − 𝑦 ) ) )
386 322 183 anim12i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
387 386 3adant1 ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
388 nncan ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑃 − ( 𝑃 − 𝑦 ) ) = 𝑦 )
389 387 388 syl ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( 𝑃 − 𝑦 ) ) = 𝑦 )
390 384 385 389 3eqtrrd ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) )
391 315 321 390 rspcedvd ⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
392 391 3exp ⊢ ( ¬ 2 ∥ 𝑦 → ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) ) )
393 210 392 pm2.61i ⊢ ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) )
394 148 393 impbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 ∈ ( 1 ... 𝐻 ) ) )
395 5 394 bitrid ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ ( 1 ... 𝐻 ) ) )
396 395 eqrdv ⊢ ( 𝜑 → ran 𝑅 = ( 1 ... 𝐻 ) )