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	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
	lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
	lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
Assertion	lpadmax	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
2		lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3		lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4		eqeq2	⊢ ( ( ♯ ‘ 𝑊 ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) → ( ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = ( ♯ ‘ 𝑊 ) ↔ ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) ) )
5		eqeq2	⊢ ( 𝐿 = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) → ( ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = 𝐿 ↔ ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ0 )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑆 )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐶 ∈ 𝑆 )
9		simpr	⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ≤ ( ♯ ‘ 𝑊 ) )
10	6 7 8 9	lpadlen1	⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = ( ♯ ‘ 𝑊 ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ0 )
12	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑆 )
13	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐶 ∈ 𝑆 )
14		lencl	⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
15	2 14	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
16	15	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
17	16	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
18	11	nn0red	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℝ )
19	1	nn0red	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
20	16 19	ltnled	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
21	20	biimpar	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) < 𝐿 )
22	17 18 21	ltled	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
23	11 12 13 22	lpadlen2	⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = 𝐿 )
24	4 5 10 23	ifbothda	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , ( ♯ ‘ 𝑊 ) , 𝐿 ) )