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