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 ∈ Word S
lpadlen.3 ⊢ φ → C ∈ S
Assertion lpadmax ⊢ φ → C leftpad W ⁡ L = if L ≤ W W L

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢ φ → L ∈ ℕ 0
2 lpadlen.2 ⊢ φ → W ∈ Word S
3 lpadlen.3 ⊢ φ → C ∈ S
4 eqeq2 ⊢ W = if L ≤ W W L → C leftpad W ⁡ L = W ↔ C leftpad W ⁡ L = if L ≤ W W L
5 eqeq2 ⊢ L = if L ≤ W W L → C leftpad W ⁡ L = L ↔ C leftpad W ⁡ L = if L ≤ W W L
6 1 adantr ⊢ φ ∧ L ≤ W → L ∈ ℕ 0
7 2 adantr ⊢ φ ∧ L ≤ W → W ∈ Word S
8 3 adantr ⊢ φ ∧ L ≤ W → C ∈ S
9 simpr ⊢ φ ∧ L ≤ W → L ≤ W
10 6 7 8 9 lpadlen1 ⊢ φ ∧ L ≤ W → C leftpad W ⁡ L = W
11 1 adantr ⊢ φ ∧ ¬ L ≤ W → L ∈ ℕ 0
12 2 adantr ⊢ φ ∧ ¬ L ≤ W → W ∈ Word S
13 3 adantr ⊢ φ ∧ ¬ L ≤ W → C ∈ S
14 lencl ⊢ W ∈ Word S → 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 → C leftpad W ⁡ L = L
24 4 5 10 23 ifbothda ⊢ φ → C leftpad W ⁡ L = if L ≤ W W L