Metamath Proof Explorer

Theorem crctcshwlkn0lem3

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊢ ( 𝜑 → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
crctcshwlkn0lem.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion crctcshwlkn0lem3 ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ 𝐽 ) = ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ⊢ ( 𝜑 → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
2 crctcshwlkn0lem.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
3 breq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑥 ≤ ( 𝑁 − 𝑆 ) ↔ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
4 fvoveq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) = ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) )
5 oveq1 ⊢ ( 𝑥 = 𝐽 → ( 𝑥 + 𝑆 ) = ( 𝐽 + 𝑆 ) )
6 5 fvoveq1d ⊢ ( 𝑥 = 𝐽 → ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) = ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) )
7 3 4 6 ifbieq12d ⊢ ( 𝑥 = 𝐽 → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) = if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) )
8 0zd ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 0 ∈ ℤ )
9 elfzoel2 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
10 elfzoelz ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
11 9 10 zsubcld ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
12 11 peano2zd ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ )
13 elfzo1 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) )
14 nnre ⊢ ( 𝑆 ∈ ℕ → 𝑆 ∈ ℝ )
15 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
16 posdif ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 ↔ 0 < ( 𝑁 − 𝑆 ) ) )
17 0red ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 0 ∈ ℝ )
18 resubcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
19 18 ancoms ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
20 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 − 𝑆 ) ∈ ℝ ) → ( 0 < ( 𝑁 − 𝑆 ) → 0 ≤ ( 𝑁 − 𝑆 ) ) )
21 17 19 20 syl2anc ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < ( 𝑁 − 𝑆 ) → 0 ≤ ( 𝑁 − 𝑆 ) ) )
22 19 lep1d ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑁 − 𝑆 ) ≤ ( ( 𝑁 − 𝑆 ) + 1 ) )
23 1red ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 1 ∈ ℝ )
24 19 23 readdcld ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℝ )
25 letr ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 − 𝑆 ) ∈ ℝ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℝ ) → ( ( 0 ≤ ( 𝑁 − 𝑆 ) ∧ ( 𝑁 − 𝑆 ) ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
26 17 19 24 25 syl3anc ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ ( 𝑁 − 𝑆 ) ∧ ( 𝑁 − 𝑆 ) ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
27 22 26 mpan2d ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 𝑆 ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
28 21 27 syld ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < ( 𝑁 − 𝑆 ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
29 16 28 sylbid ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
30 14 15 29 syl2an ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑆 < 𝑁 → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
31 30 3impia ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) )
32 13 31 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) )
33 eluz2 ⊢ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
34 8 12 32 33 syl3anbrc ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
35 1 34 syl ⊢ ( 𝜑 → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
36 fzss1 ⊢ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
37 35 36 syl ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
38 37 sselda ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
39 fvex ⊢ ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) ∈ V
40 fvex ⊢ ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ∈ V
41 39 40 ifex ⊢ if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) ∈ V
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) ∈ V )
43 2 7 38 42 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) )
44 elfz2 ⊢ ( 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ↔ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
45 zre ⊢ ( 𝑆 ∈ ℤ → 𝑆 ∈ ℝ )
46 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
47 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
48 46 47 anim12i ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
49 simprr ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 𝑁 ∈ ℝ )
50 simpl ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 𝑆 ∈ ℝ )
51 49 50 resubcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
52 51 ltp1d ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( 𝑁 − 𝑆 ) < ( ( 𝑁 − 𝑆 ) + 1 ) )
53 1red ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 1 ∈ ℝ )
54 51 53 readdcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℝ )
55 simprl ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → 𝐽 ∈ ℝ )
56 ltletr ⊢ ( ( ( 𝑁 − 𝑆 ) ∈ ℝ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( ( ( 𝑁 − 𝑆 ) < ( ( 𝑁 − 𝑆 ) + 1 ) ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ) → ( 𝑁 − 𝑆 ) < 𝐽 ) )
57 51 54 55 56 syl3anc ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( ( 𝑁 − 𝑆 ) < ( ( 𝑁 − 𝑆 ) + 1 ) ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ) → ( 𝑁 − 𝑆 ) < 𝐽 ) )
58 52 57 mpand ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ( 𝑁 − 𝑆 ) < 𝐽 ) )
59 51 55 ltnled ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( 𝑁 − 𝑆 ) < 𝐽 ↔ ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
60 58 59 sylibd ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
61 45 48 60 syl2an ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
62 61 expcom ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑆 ∈ ℤ → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
63 62 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑆 ∈ ℤ → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
64 63 3adant1 ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑆 ∈ ℤ → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
65 10 64 syl5com ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
66 65 com13 ⊢ ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
67 66 adantr ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) ) )
68 67 impcom ⊢ ( ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) → ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
69 68 com12 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
70 44 69 syl5bi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
71 1 70 syl ⊢ ( 𝜑 → ( 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) ) )
72 71 imp ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → ¬ 𝐽 ≤ ( 𝑁 − 𝑆 ) )
73 72 iffalsed ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → if ( 𝐽 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝐽 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) ) = ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) )
74 43 73 eqtrd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ 𝐽 ) = ( 𝑃 ‘ ( ( 𝐽 + 𝑆 ) − 𝑁 ) ) )