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 syl6bi ( ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ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 ) } ) )