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