Metamath Proof Explorer

Theorem lpadmax

Description: Length of a left-padded word, in the general case, expressed with an if statement. (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 ⊢φ→L∈ℕ0
lpadlen.2 ⊢φ→W∈WordS
lpadlen.3 ⊢φ→C∈S
Assertion lpadmax ⊢φ→CleftpadW⁡L=ifL≤WWL

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢φ→L∈ℕ0
2 lpadlen.2 ⊢φ→W∈WordS
3 lpadlen.3 ⊢φ→C∈S
4 eqeq2 ⊢W=ifL≤WWL→CleftpadW⁡L=W↔CleftpadW⁡L=ifL≤WWL
5 eqeq2 ⊢L=ifL≤WWL→CleftpadW⁡L=L↔CleftpadW⁡L=ifL≤WWL
6 1 adantr ⊢φ∧L≤W→L∈ℕ0
7 2 adantr ⊢φ∧L≤W→W∈WordS
8 3 adantr ⊢φ∧L≤W→C∈S
9 simpr ⊢φ∧L≤W→L≤W
10 6 7 8 9 lpadlen1 ⊢φ∧L≤W→CleftpadW⁡L=W
11 1 adantr ⊢φ∧¬L≤W→L∈ℕ0
12 2 adantr ⊢φ∧¬L≤W→W∈WordS
13 3 adantr ⊢φ∧¬L≤W→C∈S
14 lencl ⊢W∈WordS→W∈ℕ0
15 2 14 syl ⊢φ→W∈ℕ0
16 15 nn0red ⊢φ→W∈ℝ
17 16 adantr ⊢φ∧¬L≤W→W∈ℝ
18 11 nn0red ⊢φ∧¬L≤W→L∈ℝ
19 1 nn0red ⊢φ→L∈ℝ
20 16 19 ltnled ⊢φ→W<L↔¬L≤W
21 20 biimpar ⊢φ∧¬L≤W→W<L
22 17 18 21 ltled ⊢φ∧¬L≤W→W≤L
23 11 12 13 22 lpadlen2 ⊢φ∧¬L≤W→CleftpadW⁡L=L
24 4 5 10 23 ifbothda ⊢φ→CleftpadW⁡L=ifL≤WWL