Metamath Proof Explorer

Theorem iccpartnel

Description: A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 8-Jul-2020)

Ref Expression
Hypotheses iccpartnel.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartnel.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
iccpartnel.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑃 )
Assertion iccpartnel ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpartnel.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartnel.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 iccpartnel.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑃 )
4 elioo3g ⊢ ( 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
5 iccpart ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
6 1 5 syl ⊢ ( 𝜑 → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
7 elmapfn ⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
8 7 adantr ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
9 6 8 biimtrdi ⊢ ( 𝜑 → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → 𝑃 Fn ( 0 ... 𝑀 ) ) )
10 2 9 mpd ⊢ ( 𝜑 → 𝑃 Fn ( 0 ... 𝑀 ) )
11 fvelrnb ⊢ ( 𝑃 Fn ( 0 ... 𝑀 ) → ( 𝑋 ∈ ran 𝑃 ↔ ∃ 𝑥 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑥 ) = 𝑋 ) )
12 10 11 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ran 𝑃 ↔ ∃ 𝑥 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑥 ) = 𝑋 ) )
13 3 12 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑥 ) = 𝑋 )
14 elfzelz ⊢ ( 𝑥 ∈ ( 0 ... 𝑀 ) → 𝑥 ∈ ℤ )
15 14 zred ⊢ ( 𝑥 ∈ ( 0 ... 𝑀 ) → 𝑥 ∈ ℝ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℝ )
17 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ℤ )
18 17 zred ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ℝ )
19 lelttric ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐼 ∈ ℝ ) → ( 𝑥 ≤ 𝐼 ∨ 𝐼 < 𝑥 ) )
20 16 18 19 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ≤ 𝐼 ∨ 𝐼 < 𝑥 ) )
21 breq2 ⊢ ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑃 ‘ 𝐼 ) < 𝑋 ) )
22 breq1 ⊢ ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ↔ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
23 21 22 anbi12d ⊢ ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
24 leloe ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐼 ∈ ℝ ) → ( 𝑥 ≤ 𝐼 ↔ ( 𝑥 < 𝐼 ∨ 𝑥 = 𝐼 ) ) )
25 16 18 24 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ≤ 𝐼 ↔ ( 𝑥 < 𝐼 ∨ 𝑥 = 𝐼 ) ) )
26 1 2 iccpartgt ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ( 0 ... 𝑀 ) )
30 elfzofz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ( 0 ... 𝑀 ) )
31 breq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 < 𝑘 ↔ 𝑥 < 𝑘 ) )
32 fveq2 ⊢ ( 𝑖 = 𝑥 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑥 ) )
33 32 breq1d ⊢ ( 𝑖 = 𝑥 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝑘 ) ) )
34 31 33 imbi12d ⊢ ( 𝑖 = 𝑥 → ( ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) ↔ ( 𝑥 < 𝑘 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝑘 ) ) ) )
35 breq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑥 < 𝑘 ↔ 𝑥 < 𝐼 ) )
36 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝐼 ) )
37 36 breq2d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) )
38 35 37 imbi12d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑥 < 𝑘 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝑘 ) ) ↔ ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) ) )
39 34 38 rspc2v ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑀 ) ∧ 𝐼 ∈ ( 0 ... 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) → ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) ) )
40 29 30 39 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) → ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) ) )
41 28 40 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) )
42 pm3.35 ⊢ ( ( 𝑥 < 𝐼 ∧ ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) ) → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) )
43 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
44 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
45 43 44 29 iccpartxr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑥 ) ∈ ℝ* )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑥 ) ∈ ℝ* )
47 simp1 ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑃 ‘ 𝐼 ) ∈ ℝ* )
48 xrltle ⊢ ( ( ( 𝑃 ‘ 𝑥 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ( 𝑃 ‘ 𝑥 ) ≤ ( 𝑃 ‘ 𝐼 ) ) )
49 46 47 48 syl2anr ⊢ ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ( 𝑃 ‘ 𝑥 ) ≤ ( 𝑃 ‘ 𝐼 ) ) )
50 xrlenlt ⊢ ( ( ( 𝑃 ‘ 𝑥 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑥 ) ≤ ( 𝑃 ‘ 𝐼 ) ↔ ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) )
51 46 47 50 syl2anr ⊢ ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) ≤ ( 𝑃 ‘ 𝐼 ) ↔ ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) )
52 49 51 sylibd ⊢ ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) )
53 52 ex ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) ) )
54 53 com13 ⊢ ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) ) )
55 54 imp ⊢ ( ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) )
56 55 imp ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) )
57 56 pm2.21d ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
58 57 ex ⊢ ( ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ∧ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
59 58 ex ⊢ ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
60 42 59 syl ⊢ ( ( 𝑥 < 𝐼 ∧ ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
61 60 ex ⊢ ( 𝑥 < 𝐼 → ( ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
62 61 com13 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑥 < 𝐼 → ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ 𝐼 ) ) → ( 𝑥 < 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
63 41 62 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 < 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
64 63 com12 ⊢ ( 𝑥 < 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
65 fveq2 ⊢ ( 𝑥 = 𝐼 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝐼 ) )
66 65 breq2d ⊢ ( 𝑥 = 𝐼 → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) ) )
67 66 adantr ⊢ ( ( 𝑥 = 𝐼 ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) ) )
68 xrltnr ⊢ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) )
69 68 3ad2ant1 ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) )
70 69 adantl ⊢ ( ( 𝑥 = 𝐼 ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ¬ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) )
71 70 pm2.21d ⊢ ( ( 𝑥 = 𝐼 ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝐼 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
72 67 71 sylbid ⊢ ( ( 𝑥 = 𝐼 ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
73 72 ex ⊢ ( 𝑥 = 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
74 73 a1d ⊢ ( 𝑥 = 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
75 64 74 jaoi ⊢ ( ( 𝑥 < 𝐼 ∨ 𝑥 = 𝐼 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
76 75 com12 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑥 < 𝐼 ∨ 𝑥 = 𝐼 ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
77 25 76 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ≤ 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
78 77 com23 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑥 ≤ 𝐼 → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
79 78 com14 ⊢ ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑥 ≤ 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
80 79 adantr ⊢ ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑥 ≤ 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
81 23 80 biimtrrdi ⊢ ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑥 ≤ 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
82 81 com14 ⊢ ( 𝑥 ≤ 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
83 82 com23 ⊢ ( 𝑥 ≤ 𝐼 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
84 83 impd ⊢ ( 𝑥 ≤ 𝐼 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
85 84 com24 ⊢ ( 𝑥 ≤ 𝐼 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
86 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℤ )
87 zltp1le ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝐼 < 𝑥 ↔ ( 𝐼 + 1 ) ≤ 𝑥 ) )
88 17 86 87 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 < 𝑥 ↔ ( 𝐼 + 1 ) ≤ 𝑥 ) )
89 17 peano2zd ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ℤ )
90 89 zred ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ℝ )
91 leloe ⊢ ( ( ( 𝐼 + 1 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐼 + 1 ) ≤ 𝑥 ↔ ( ( 𝐼 + 1 ) < 𝑥 ∨ ( 𝐼 + 1 ) = 𝑥 ) ) )
92 90 16 91 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 + 1 ) ≤ 𝑥 ↔ ( ( 𝐼 + 1 ) < 𝑥 ∨ ( 𝐼 + 1 ) = 𝑥 ) ) )
93 88 92 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 < 𝑥 ↔ ( ( 𝐼 + 1 ) < 𝑥 ∨ ( 𝐼 + 1 ) = 𝑥 ) ) )
94 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
95 breq1 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑖 < 𝑘 ↔ ( 𝐼 + 1 ) < 𝑘 ) )
96 fveq2 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
97 96 breq1d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑘 ) ) )
98 95 97 imbi12d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) ↔ ( ( 𝐼 + 1 ) < 𝑘 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑘 ) ) ) )
99 breq2 ⊢ ( 𝑘 = 𝑥 → ( ( 𝐼 + 1 ) < 𝑘 ↔ ( 𝐼 + 1 ) < 𝑥 ) )
100 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑥 ) )
101 100 breq2d ⊢ ( 𝑘 = 𝑥 → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) )
102 99 101 imbi12d ⊢ ( 𝑘 = 𝑥 → ( ( ( 𝐼 + 1 ) < 𝑘 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑘 ) ) ↔ ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) ) )
103 98 102 rspc2v ⊢ ( ( ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) → ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) ) )
104 94 29 103 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑘 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑘 ) ) → ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) ) )
105 28 104 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) )
106 pm3.35 ⊢ ( ( ( 𝐼 + 1 ) < 𝑥 ∧ ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) )
107 simp2 ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
108 xrltnsym ⊢ ( ( ( 𝑃 ‘ 𝑥 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ¬ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) )
109 46 107 108 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ¬ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) )
110 109 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) )
111 110 pm2.21d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
112 111 expcom ⊢ ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
113 112 expd ⊢ ( ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
114 113 adantl ⊢ ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
115 114 com14 ⊢ ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
116 106 115 syl ⊢ ( ( ( 𝐼 + 1 ) < 𝑥 ∧ ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
117 116 ex ⊢ ( ( 𝐼 + 1 ) < 𝑥 → ( ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
118 117 com13 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐼 + 1 ) < 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑥 ) ) → ( ( 𝐼 + 1 ) < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
119 105 118 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 + 1 ) < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
120 119 com12 ⊢ ( ( 𝐼 + 1 ) < 𝑥 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
121 fveq2 ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝑥 ) )
122 121 breq2d ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ↔ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ) )
123 121 breq1d ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ↔ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
124 122 123 anbi12d ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
125 xrltnr ⊢ ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* → ¬ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
126 125 3ad2ant2 ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
127 126 pm2.21d ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
128 127 com12 ⊢ ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
129 128 adantl ⊢ ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
130 124 129 biimtrrdi ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
131 130 com23 ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
132 131 a1d ⊢ ( ( 𝐼 + 1 ) = 𝑥 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
133 120 132 jaoi ⊢ ( ( ( 𝐼 + 1 ) < 𝑥 ∨ ( 𝐼 + 1 ) = 𝑥 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
134 133 com12 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐼 + 1 ) < 𝑥 ∨ ( 𝐼 + 1 ) = 𝑥 ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
135 93 134 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
136 135 com23 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝐼 < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
137 136 com14 ⊢ ( ( ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ 𝑥 ) ∧ ( 𝑃 ‘ 𝑥 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝐼 < 𝑥 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
138 23 137 biimtrrdi ⊢ ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝐼 < 𝑥 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
139 138 com14 ⊢ ( 𝐼 < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
140 139 com23 ⊢ ( 𝐼 < 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) ) )
141 140 impd ⊢ ( 𝐼 < 𝑥 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
142 141 com24 ⊢ ( 𝐼 < 𝑥 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
143 85 142 jaoi ⊢ ( ( 𝑥 ≤ 𝐼 ∨ 𝐼 < 𝑥 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
144 143 com12 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑥 ≤ 𝐼 ∨ 𝐼 < 𝑥 ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
145 20 144 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
146 145 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
147 146 com23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
148 147 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑥 ) = 𝑋 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) )
149 13 148 mpd ⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
150 149 imp ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
151 150 com12 ⊢ ( ( ( ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝐼 ) < 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
152 4 151 sylbi ⊢ ( 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
153 ax-1 ⊢ ( ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
154 152 153 pm2.61i ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑃 ‘ 𝐼 ) (,) ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )