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

Metamath Proof Explorer

Theorem clwlkclwwlklem2fv2

Description: Lemma 4b for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 22-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion clwlkclwwlklem2fv2 ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2 simpr ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) )
3 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
4 2z ⊢ 2 ∈ ℤ
5 3 4 jctir ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) )
6 zsubcl ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
7 5 6 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
8 7 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
9 8 adantr ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
10 2 9 eqeltrd ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → 𝑥 ∈ ℤ )
11 10 ex ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → 𝑥 ∈ ℤ ) )
12 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
13 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
14 2re ⊢ 2 ∈ ℝ
15 14 a1i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 2 ∈ ℝ )
16 13 15 resubcld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
17 16 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ )
18 lttri3 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℝ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) ) )
19 12 17 18 syl2anr ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) ) )
20 simpl ⊢ ( ( ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ∧ ¬ ( ( ♯ ‘ 𝑃 ) − 2 ) < 𝑥 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
21 19 20 biimtrdi ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
22 21 ex ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 ∈ ℤ → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
23 11 22 syld ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
24 23 com13 ⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) ) )
25 24 pm2.43i ⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
26 25 impcom ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ¬ 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) )
27 26 iffalsed ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) )
28 fveq2 ⊢ ( 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
29 28 adantl ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
30 29 preq1d ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } )
31 30 fveq2d ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )
32 27 31 eqtrd ⊢ ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 = ( ( ♯ ‘ 𝑃 ) − 2 ) ) → if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )
33 5 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 2 ∈ ℤ ) )
34 33 6 syl ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ )
35 13 15 subge0d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ↔ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
36 35 biimpar ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) )
37 elnn0z ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℤ ∧ 0 ≤ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
38 34 36 37 sylanbrc ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 )
39 nn0ge2m1nn ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ )
40 1red ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 1 ∈ ℝ )
41 14 a1i ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ∈ ℝ )
42 13 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℝ )
43 1lt2 ⊢ 1 < 2
44 43 a1i ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 1 < 2 )
45 40 41 42 44 ltsub2dd ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) < ( ( ♯ ‘ 𝑃 ) − 1 ) )
46 elfzo0 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑃 ) − 2 ) < ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
47 38 39 45 46 syl3anbrc ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 2 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
48 fvexd ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) ∈ V )
49 1 32 47 48 fvmptd2 ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐹 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) = ( ◡ 𝐸 ‘ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ) )