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

Metamath Proof Explorer

Theorem icceuelpartlem

Description: Lemma for icceuelpart . (Contributed by AV, 19-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartiun.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion icceuelpartlem ( 𝜑 → ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑃 ‘ 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpartiun.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartiun.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 fveq2 ⊢ ( ( 𝐼 + 1 ) = 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) )
4 3 olcd ⊢ ( ( 𝐼 + 1 ) = 𝐽 → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) )
5 4 a1d ⊢ ( ( 𝐼 + 1 ) = 𝐽 → ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) ) )
6 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ℤ )
7 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑀 ) → 𝐽 ∈ ℤ )
8 zltp1le ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
9 8 biimpcd ⊢ ( 𝐼 < 𝐽 → ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 + 1 ) ≤ 𝐽 ) )
10 9 adantr ⊢ ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 + 1 ) ≤ 𝐽 ) )
11 10 impcom ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → ( 𝐼 + 1 ) ≤ 𝐽 )
12 df-ne ⊢ ( ( 𝐼 + 1 ) ≠ 𝐽 ↔ ¬ ( 𝐼 + 1 ) = 𝐽 )
13 necom ⊢ ( ( 𝐼 + 1 ) ≠ 𝐽 ↔ 𝐽 ≠ ( 𝐼 + 1 ) )
14 12 13 sylbb1 ⊢ ( ¬ ( 𝐼 + 1 ) = 𝐽 → 𝐽 ≠ ( 𝐼 + 1 ) )
15 14 adantl ⊢ ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → 𝐽 ≠ ( 𝐼 + 1 ) )
16 15 adantl ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → 𝐽 ≠ ( 𝐼 + 1 ) )
17 11 16 jca ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → ( ( 𝐼 + 1 ) ≤ 𝐽 ∧ 𝐽 ≠ ( 𝐼 + 1 ) ) )
18 peano2z ⊢ ( 𝐼 ∈ ℤ → ( 𝐼 + 1 ) ∈ ℤ )
19 18 zred ⊢ ( 𝐼 ∈ ℤ → ( 𝐼 + 1 ) ∈ ℝ )
20 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
21 19 20 anim12i ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( 𝐼 + 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ) )
22 21 adantr ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → ( ( 𝐼 + 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ) )
23 ltlen ⊢ ( ( ( 𝐼 + 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( ( 𝐼 + 1 ) < 𝐽 ↔ ( ( 𝐼 + 1 ) ≤ 𝐽 ∧ 𝐽 ≠ ( 𝐼 + 1 ) ) ) )
24 22 23 syl ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → ( ( 𝐼 + 1 ) < 𝐽 ↔ ( ( 𝐼 + 1 ) ≤ 𝐽 ∧ 𝐽 ≠ ( 𝐼 + 1 ) ) ) )
25 17 24 mpbird ⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) ) → ( 𝐼 + 1 ) < 𝐽 )
26 25 ex ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → ( 𝐼 + 1 ) < 𝐽 ) )
27 6 7 26 syl2an ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → ( 𝐼 + 1 ) < 𝐽 ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → ( 𝐼 + 1 ) < 𝐽 ) )
29 1 2 iccpartgt ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )
30 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
31 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑀 ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
32 breq1 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑖 < 𝑗 ↔ ( 𝐼 + 1 ) < 𝑗 ) )
33 fveq2 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
34 33 breq1d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑗 ) ) )
35 32 34 imbi12d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ↔ ( ( 𝐼 + 1 ) < 𝑗 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑗 ) ) ) )
36 breq2 ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 + 1 ) < 𝑗 ↔ ( 𝐼 + 1 ) < 𝐽 ) )
37 fveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝐽 ) )
38 37 breq2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) )
39 36 38 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐼 + 1 ) < 𝑗 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝑗 ) ) ↔ ( ( 𝐼 + 1 ) < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) ) )
40 35 39 rspc2v ⊢ ( ( ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ∧ 𝐽 ∈ ( 0 ... 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) → ( ( 𝐼 + 1 ) < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) ) )
41 30 31 40 syl2an ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) → ( ( 𝐼 + 1 ) < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) ) )
42 29 41 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝐼 + 1 ) < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) )
43 28 42 syld ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝐼 < 𝐽 ∧ ¬ ( 𝐼 + 1 ) = 𝐽 ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) )
44 43 expdimp ⊢ ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ¬ ( 𝐼 + 1 ) = 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ) )
45 44 impcom ⊢ ( ( ¬ ( 𝐼 + 1 ) = 𝐽 ∧ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) )
46 45 orcd ⊢ ( ( ¬ ( 𝐼 + 1 ) = 𝐽 ∧ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) )
47 46 ex ⊢ ( ¬ ( 𝐼 + 1 ) = 𝐽 → ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) ) )
48 5 47 pm2.61i ⊢ ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) )
49 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑀 ∈ ℕ )
50 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
51 30 adantr ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
53 49 50 52 iccpartxr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
54 31 adantl ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
55 54 adantl ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
56 49 50 55 iccpartxr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ 𝐽 ) ∈ ℝ* )
57 53 56 jca ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐽 ) ∈ ℝ* ) )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐽 ) ∈ ℝ* ) )
59 xrleloe ⊢ ( ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐽 ) ∈ ℝ* ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑃 ‘ 𝐽 ) ↔ ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) ) )
60 58 59 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑃 ‘ 𝐽 ) ↔ ( ( 𝑃 ‘ ( 𝐼 + 1 ) ) < ( 𝑃 ‘ 𝐽 ) ∨ ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 𝐽 ) ) ) )
61 48 60 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝐼 < 𝐽 ) → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑃 ‘ 𝐽 ) )
62 61 exp31 ⊢ ( 𝜑 → ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 < 𝐽 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑃 ‘ 𝐽 ) ) ) )