Metamath Proof Explorer

Theorem fourierdlem12

Description: A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem12.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem12.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem12.3 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem12.4 ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑄 )
Assertion fourierdlem12 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem12.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem12.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fourierdlem12.3 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
4 fourierdlem12.4 ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑄 )
5 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
6 2 5 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
7 3 6 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
8 7 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
9 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
10 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) )
11 8 9 10 3syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
12 fvelrnb ⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( 𝑋 ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 ) )
13 11 12 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 ) )
14 4 13 mpbid ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 )
16 8 9 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
18 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
20 17 19 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
22 21 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
23 frn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → ran 𝑄 ⊆ ℝ )
24 16 23 syl ⊢ ( 𝜑 → ran 𝑄 ⊆ ℝ )
25 24 4 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑋 ∈ ℝ )
27 26 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → 𝑋 ∈ ℝ )
28 17 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
29 28 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
31 simpr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
32 elfzoelz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℤ )
33 32 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ℤ )
34 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
35 34 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ℤ )
36 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑖 < 𝑗 ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
37 33 35 36 syl2anc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 < 𝑗 ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
38 31 37 mpbid ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 + 1 ) ≤ 𝑗 )
39 33 peano2zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 + 1 ) ∈ ℤ )
40 eluz ⊢ ( ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
41 39 35 40 syl2anc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
42 38 41 mpbird ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
43 42 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
44 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
45 0red ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 ∈ ℝ )
46 elfzelz ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) → 𝑤 ∈ ℤ )
47 46 zred ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) → 𝑤 ∈ ℝ )
48 47 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ∈ ℝ )
49 32 peano2zd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ℤ )
50 49 zred ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ℝ )
51 50 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
52 32 zred ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℝ )
53 52 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑖 ∈ ℝ )
54 elfzole1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 0 ≤ 𝑖 )
55 54 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 ≤ 𝑖 )
56 53 ltp1d ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑖 < ( 𝑖 + 1 ) )
57 45 53 51 55 56 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 < ( 𝑖 + 1 ) )
58 elfzle1 ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) → ( 𝑖 + 1 ) ≤ 𝑤 )
59 58 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → ( 𝑖 + 1 ) ≤ 𝑤 )
60 45 51 48 57 59 ltletrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 < 𝑤 )
61 45 48 60 ltled ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 ≤ 𝑤 )
62 61 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 ≤ 𝑤 )
63 47 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ∈ ℝ )
64 34 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
65 64 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑗 ∈ ℝ )
66 elfzel2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
67 66 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
68 67 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑀 ∈ ℝ )
69 elfzle2 ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) → 𝑤 ≤ 𝑗 )
70 69 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ≤ 𝑗 )
71 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ≤ 𝑀 )
72 71 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑗 ≤ 𝑀 )
73 63 65 68 70 72 letrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ≤ 𝑀 )
74 73 adantll ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ≤ 𝑀 )
75 46 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ∈ ℤ )
76 0zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 0 ∈ ℤ )
77 66 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑀 ∈ ℤ )
78 elfz ⊢ ( ( 𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑤 ∈ ( 0 ... 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
79 75 76 77 78 syl3anc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → ( 𝑤 ∈ ( 0 ... 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
80 62 74 79 mpbir2and ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
81 80 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
82 44 81 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
83 82 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... 𝑗 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
84 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝜑 )
85 0red ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ∈ ℝ )
86 elfzelz ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) → 𝑤 ∈ ℤ )
87 86 zred ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) → 𝑤 ∈ ℝ )
88 87 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ∈ ℝ )
89 0red ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ∈ ℝ )
90 50 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
91 87 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ∈ ℝ )
92 0red ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 0 ∈ ℝ )
93 52 ltp1d ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 < ( 𝑖 + 1 ) )
94 92 52 50 54 93 lelttrd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 0 < ( 𝑖 + 1 ) )
95 94 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 < ( 𝑖 + 1 ) )
96 elfzle1 ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) → ( 𝑖 + 1 ) ≤ 𝑤 )
97 96 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑤 )
98 89 90 91 95 97 ltletrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 < 𝑤 )
99 98 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 < 𝑤 )
100 85 88 99 ltled ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ≤ 𝑤 )
101 100 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ≤ 𝑤 )
102 101 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ≤ 𝑤 )
103 87 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ∈ ℝ )
104 peano2rem ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − 1 ) ∈ ℝ )
105 64 104 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ∈ ℝ )
106 105 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ ℝ )
107 67 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℝ )
108 elfzle2 ⊢ ( 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) → 𝑤 ≤ ( 𝑗 − 1 ) )
109 108 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ≤ ( 𝑗 − 1 ) )
110 zlem1lt ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑗 ≤ 𝑀 ↔ ( 𝑗 − 1 ) < 𝑀 ) )
111 34 66 110 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 ≤ 𝑀 ↔ ( 𝑗 − 1 ) < 𝑀 ) )
112 71 111 mpbid ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) < 𝑀 )
113 112 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) < 𝑀 )
114 103 106 107 109 113 lelttrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 < 𝑀 )
115 114 adantlr ⊢ ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 < 𝑀 )
116 115 adantlll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 < 𝑀 )
117 86 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ∈ ℤ )
118 0zd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 0 ∈ ℤ )
119 66 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℤ )
120 elfzo ⊢ ( ( 𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑤 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 < 𝑀 ) ) )
121 117 118 119 120 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑤 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 < 𝑀 ) ) )
122 102 116 121 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → 𝑤 ∈ ( 0 ..^ 𝑀 ) )
123 16 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
124 elfzofz ⊢ ( 𝑤 ∈ ( 0 ..^ 𝑀 ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
126 123 125 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
127 fzofzp1 ⊢ ( 𝑤 ∈ ( 0 ..^ 𝑀 ) → ( 𝑤 + 1 ) ∈ ( 0 ... 𝑀 ) )
128 127 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑤 + 1 ) ∈ ( 0 ... 𝑀 ) )
129 123 128 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑤 + 1 ) ) ∈ ℝ )
130 eleq1w ⊢ ( 𝑖 = 𝑤 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) )
131 130 anbi2d ⊢ ( 𝑖 = 𝑤 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) ) )
132 fveq2 ⊢ ( 𝑖 = 𝑤 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑤 ) )
133 oveq1 ⊢ ( 𝑖 = 𝑤 → ( 𝑖 + 1 ) = ( 𝑤 + 1 ) )
134 133 fveq2d ⊢ ( 𝑖 = 𝑤 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
135 132 134 breq12d ⊢ ( 𝑖 = 𝑤 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 𝑤 ) < ( 𝑄 ‘ ( 𝑤 + 1 ) ) ) )
136 131 135 imbi12d ⊢ ( 𝑖 = 𝑤 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑤 ) < ( 𝑄 ‘ ( 𝑤 + 1 ) ) ) ) )
137 7 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
138 137 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
139 136 138 chvarvv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑤 ) < ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
140 126 129 139 ltled ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
141 84 122 140 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝑤 ∈ ( ( 𝑖 + 1 ) ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
142 43 83 141 monoord ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑄 ‘ 𝑗 ) )
143 142 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑄 ‘ 𝑗 ) )
144 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
145 144 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
146 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ( 𝑄 ‘ 𝑗 ) = 𝑋 )
147 145 146 eqled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ( 𝑄 ‘ 𝑗 ) ≤ 𝑋 )
148 147 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ( 𝑄 ‘ 𝑗 ) ≤ 𝑋 )
149 148 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ 𝑗 ) ≤ 𝑋 )
150 22 30 27 143 149 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 𝑋 )
151 22 27 150 lensymd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ¬ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
152 151 intnand ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑖 < 𝑗 ) → ¬ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
153 64 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 ∈ ℝ )
154 52 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑖 ∈ ℝ )
155 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ 𝑖 < 𝑗 )
156 153 154 155 nltled ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 ≤ 𝑖 )
157 156 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ ¬ 𝑖 < 𝑗 ) → 𝑗 ≤ 𝑖 )
158 eqcom ⊢ ( ( 𝑄 ‘ 𝑗 ) = 𝑋 ↔ 𝑋 = ( 𝑄 ‘ 𝑗 ) )
159 158 biimpi ⊢ ( ( 𝑄 ‘ 𝑗 ) = 𝑋 → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
160 159 adantr ⊢ ( ( ( 𝑄 ‘ 𝑗 ) = 𝑋 ∧ 𝑗 ≤ 𝑖 ) → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
161 160 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
162 34 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑗 ∈ ℤ )
163 32 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ℤ )
164 simpr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑗 ≤ 𝑖 )
165 eluz2 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖 ) )
166 162 163 164 165 syl3anbrc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) )
167 166 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) )
168 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
169 0zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ∈ ℤ )
170 66 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑀 ∈ ℤ )
171 elfzelz ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ∈ ℤ )
172 171 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℤ )
173 169 170 172 3jca ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) )
174 0red ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ∈ ℝ )
175 64 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑗 ∈ ℝ )
176 171 zred ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ∈ ℝ )
177 176 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℝ )
178 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑗 )
179 178 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑗 )
180 elfzle1 ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑗 ≤ 𝑤 )
181 180 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑗 ≤ 𝑤 )
182 174 175 177 179 181 letrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑤 )
183 182 adantll ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑤 )
184 176 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℝ )
185 elfzoel2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
186 185 zred ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℝ )
187 186 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑀 ∈ ℝ )
188 52 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑖 ∈ ℝ )
189 elfzle2 ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ≤ 𝑖 )
190 189 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑖 )
191 elfzolt2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 < 𝑀 )
192 191 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑖 < 𝑀 )
193 184 188 187 190 192 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 < 𝑀 )
194 184 187 193 ltled ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑀 )
195 194 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑀 )
196 173 183 195 jca32 ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
197 196 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
198 elfz2 ⊢ ( 𝑤 ∈ ( 0 ... 𝑀 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
199 197 198 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
200 168 199 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
201 200 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
202 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝜑 )
203 0red ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ∈ ℝ )
204 64 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℝ )
205 elfzelz ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ∈ ℤ )
206 205 zred ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ∈ ℝ )
207 206 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℝ )
208 178 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ≤ 𝑗 )
209 elfzle1 ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑗 ≤ 𝑤 )
210 209 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑗 ≤ 𝑤 )
211 203 204 207 208 210 letrd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ≤ 𝑤 )
212 206 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℝ )
213 52 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑖 ∈ ℝ )
214 186 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℝ )
215 peano2rem ⊢ ( 𝑖 ∈ ℝ → ( 𝑖 − 1 ) ∈ ℝ )
216 213 215 syl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) ∈ ℝ )
217 elfzle2 ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ≤ ( 𝑖 − 1 ) )
218 217 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ≤ ( 𝑖 − 1 ) )
219 213 ltm1d ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) < 𝑖 )
220 212 216 213 218 219 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑖 )
221 191 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑖 < 𝑀 )
222 212 213 214 220 221 lttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑀 )
223 222 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑀 )
224 205 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℤ )
225 0zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ∈ ℤ )
226 185 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℤ )
227 224 225 226 120 syl3anc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑤 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 < 𝑀 ) ) )
228 211 223 227 mpbir2and ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ( 0 ..^ 𝑀 ) )
229 228 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ( 0 ..^ 𝑀 ) )
230 202 229 140 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
231 230 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
232 167 201 231 monoord ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ 𝑖 ) )
233 232 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ 𝑖 ) )
234 161 233 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) )
235 25 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
236 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
237 236 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
238 17 237 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
239 235 238 lenltd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
240 239 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
241 240 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
242 234 241 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 )
243 157 242 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 )
244 243 intnanrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
245 152 244 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
246 245 intnand ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
247 elioo3g ⊢ ( 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
248 246 247 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
249 248 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
250 15 249 mpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )