This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimpi ⊢ ( ( 𝑄 ‘ 𝑗 ) = 𝑋 → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
157 156 adantr ⊢ ( ( ( 𝑄 ‘ 𝑗 ) = 𝑋 ∧ 𝑗 ≤ 𝑖 ) → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
158 157 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → 𝑋 = ( 𝑄 ‘ 𝑗 ) )
159 33 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑗 ∈ ℤ )
160 31 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ℤ )
161 simpr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑗 ≤ 𝑖 )
162 eluz2 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖 ) )
163 159 160 161 162 syl3anbrc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) )
164 163 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) )
165 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
166 0zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ∈ ℤ )
167 45 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑀 ∈ ℤ )
168 elfzelz ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ∈ ℤ )
169 168 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℤ )
170 166 167 169 3jca ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) )
171 0red ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ∈ ℝ )
172 67 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑗 ∈ ℝ )
173 168 zred ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ∈ ℝ )
174 173 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℝ )
175 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑗 )
176 175 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑗 )
177 elfzle1 ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑗 ≤ 𝑤 )
178 177 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑗 ≤ 𝑤 )
179 171 172 174 176 178 letrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑤 )
180 179 adantll ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 0 ≤ 𝑤 )
181 173 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ℝ )
182 elfzoel2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
183 182 zred ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℝ )
184 183 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑀 ∈ ℝ )
185 55 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑖 ∈ ℝ )
186 elfzle2 ⊢ ( 𝑤 ∈ ( 𝑗 ... 𝑖 ) → 𝑤 ≤ 𝑖 )
187 186 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑖 )
188 elfzolt2 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 < 𝑀 )
189 188 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑖 < 𝑀 )
190 181 185 184 187 189 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 < 𝑀 )
191 181 184 190 ltled ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑀 )
192 191 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ≤ 𝑀 )
193 170 180 192 jca32 ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
194 193 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
195 elfz2 ⊢ ( 𝑤 ∈ ( 0 ... 𝑀 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( 0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀 ) ) )
196 194 195 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → 𝑤 ∈ ( 0 ... 𝑀 ) )
197 165 196 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
198 197 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) ∧ 𝑤 ∈ ( 𝑗 ... 𝑖 ) ) → ( 𝑄 ‘ 𝑤 ) ∈ ℝ )
199 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝜑 )
200 0red ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ∈ ℝ )
201 67 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℝ )
202 elfzelz ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ∈ ℤ )
203 202 zred ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ∈ ℝ )
204 203 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℝ )
205 175 ad2antlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ≤ 𝑗 )
206 elfzle1 ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑗 ≤ 𝑤 )
207 206 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑗 ≤ 𝑤 )
208 200 201 204 205 207 letrd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ≤ 𝑤 )
209 203 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℝ )
210 55 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑖 ∈ ℝ )
211 183 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℝ )
212 peano2rem ⊢ ( 𝑖 ∈ ℝ → ( 𝑖 − 1 ) ∈ ℝ )
213 210 212 syl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) ∈ ℝ )
214 elfzle2 ⊢ ( 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) → 𝑤 ≤ ( 𝑖 − 1 ) )
215 214 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ≤ ( 𝑖 − 1 ) )
216 210 ltm1d ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) < 𝑖 )
217 209 213 210 215 216 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑖 )
218 188 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑖 < 𝑀 )
219 209 210 211 217 218 lttrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑀 )
220 219 adantlr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 < 𝑀 )
221 202 adantl ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ℤ )
222 0zd ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 0 ∈ ℤ )
223 182 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℤ )
224 221 222 223 117 syl3anc ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑤 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑤 ∧ 𝑤 < 𝑀 ) ) )
225 208 220 224 mpbir2and ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ( 0 ..^ 𝑀 ) )
226 225 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → 𝑤 ∈ ( 0 ..^ 𝑀 ) )
227 199 226 137 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
228 227 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) ∧ 𝑤 ∈ ( 𝑗 ... ( 𝑖 − 1 ) ) ) → ( 𝑄 ‘ 𝑤 ) ≤ ( 𝑄 ‘ ( 𝑤 + 1 ) ) )
229 164 198 228 monoord ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ 𝑖 ) )
230 229 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ 𝑖 ) )
231 158 230 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) )
232 24 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
233 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
234 233 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
235 16 234 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
236 232 235 lenltd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
237 236 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
238 237 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ( 𝑋 ≤ ( 𝑄 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 ) )
239 231 238 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ 𝑗 ≤ 𝑖 ) → ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 )
240 154 239 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ ( 𝑄 ‘ 𝑖 ) < 𝑋 )
241 240 intnanrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) ∧ ¬ 𝑖 < 𝑗 ) → ¬ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
242 149 241 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
243 242 intnand ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
244 elioo3g ⊢ ( 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑋 ∧ 𝑋 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
245 243 244 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝑋 ) → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
246 245 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑗 ) = 𝑋 → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
247 14 246 mpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )