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 ... 𝐻 ) )