Metamath Proof Explorer

Theorem iccpartlt

Description: If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 in GS's mathbox. (Contributed by AV, 12-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartlt ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑀 ∈ ℕ )
4 1 3 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
5 iccpartimp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
6 1 2 4 5 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) )
8 7 adantl ⊢ ( ( 𝑀 = 1 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) )
9 fveq2 ⊢ ( 𝑀 = 1 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 1 ) )
10 1e0p1 ⊢ 1 = ( 0 + 1 )
11 10 fveq2i ⊢ ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ ( 0 + 1 ) )
12 9 11 eqtrdi ⊢ ( 𝑀 = 1 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ ( 0 + 1 ) ) )
13 12 adantr ⊢ ( ( 𝑀 = 1 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ ( 0 + 1 ) ) )
14 8 13 breqtrrd ⊢ ( ( 𝑀 = 1 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
15 14 ex ⊢ ( 𝑀 = 1 → ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
16 1 2 iccpartiltu ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
17 1 2 iccpartigtl ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) )
18 1nn ⊢ 1 ∈ ℕ
19 18 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 ∈ ℕ )
20 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑀 ∈ ℕ )
21 df-ne ⊢ ( 𝑀 ≠ 1 ↔ ¬ 𝑀 = 1 )
22 1 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
23 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
24 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
25 23 24 ltlend ⊢ ( 𝜑 → ( 1 < 𝑀 ↔ ( 1 ≤ 𝑀 ∧ 𝑀 ≠ 1 ) ) )
26 25 biimprd ⊢ ( 𝜑 → ( ( 1 ≤ 𝑀 ∧ 𝑀 ≠ 1 ) → 1 < 𝑀 ) )
27 22 26 mpand ⊢ ( 𝜑 → ( 𝑀 ≠ 1 → 1 < 𝑀 ) )
28 21 27 syl5bir ⊢ ( 𝜑 → ( ¬ 𝑀 = 1 → 1 < 𝑀 ) )
29 28 imp ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 < 𝑀 )
30 elfzo1 ⊢ ( 1 ∈ ( 1 ..^ 𝑀 ) ↔ ( 1 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 1 < 𝑀 ) )
31 19 20 29 30 syl3anbrc ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 ∈ ( 1 ..^ 𝑀 ) )
32 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 1 ) )
33 32 breq2d ⊢ ( 𝑖 = 1 → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) ) )
34 33 rspcv ⊢ ( 1 ∈ ( 1 ..^ 𝑀 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) ) )
35 31 34 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) ) )
36 32 breq1d ⊢ ( 𝑖 = 1 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) ) )
37 36 rspcv ⊢ ( 1 ∈ ( 1 ..^ 𝑀 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) ) )
38 31 37 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) ) )
39 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
40 0elfz ⊢ ( 𝑀 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑀 ) )
41 1 39 40 3syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
42 1 2 41 iccpartxr ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ ℝ* )
43 42 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( 𝑃 ‘ 0 ) ∈ ℝ* )
44 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
45 1nn0 ⊢ 1 ∈ ℕ0
46 45 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 ∈ ℕ0 )
47 1 39 syl ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
48 47 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑀 ∈ ℕ0 )
49 22 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 ≤ 𝑀 )
50 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 𝑀 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 1 ≤ 𝑀 ) )
51 46 48 49 50 syl3anbrc ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 1 ∈ ( 0 ... 𝑀 ) )
52 20 44 51 iccpartxr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( 𝑃 ‘ 1 ) ∈ ℝ* )
53 nn0fz0 ⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( 0 ... 𝑀 ) )
54 39 53 sylib ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( 0 ... 𝑀 ) )
55 1 54 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
56 1 2 55 iccpartxr ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
57 56 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
58 xrlttr ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ℝ* ∧ ( 𝑃 ‘ 1 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ) → ( ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
59 43 52 57 58 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
60 59 expcomd ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ( 𝑃 ‘ 1 ) < ( 𝑃 ‘ 𝑀 ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
61 38 60 syld ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
62 61 com23 ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 1 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
63 35 62 syld ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
64 63 ex ⊢ ( 𝜑 → ( ¬ 𝑀 = 1 → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) ) )
65 64 com24 ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) → ( ¬ 𝑀 = 1 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) ) ) )
66 16 17 65 mp2d ⊢ ( 𝜑 → ( ¬ 𝑀 = 1 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
67 66 com12 ⊢ ( ¬ 𝑀 = 1 → ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
68 15 67 pm2.61i ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )