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