Theorem algcvgb

Description: Two ways of expressing that C is a countdown function for algorithm F . The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Hypotheses	algcvgb.1	⊢ 𝐹 : 𝑆 ⟶ 𝑆
	algcvgb.2	⊢ 𝐶 : 𝑆 ⟶ ℕ0
Assertion	algcvgb	⊢ ( 𝑋 ∈ 𝑆 → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ↔ ( ( ( 𝐶 ‘ 𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ∧ ( ( 𝐶 ‘ 𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) = 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		algcvgb.1	⊢ 𝐹 : 𝑆 ⟶ 𝑆
2		algcvgb.2	⊢ 𝐶 : 𝑆 ⟶ ℕ0
3	2	ffvelcdmi	⊢ ( 𝑋 ∈ 𝑆 → ( 𝐶 ‘ 𝑋 ) ∈ ℕ0 )
4	1	ffvelcdmi	⊢ ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 )
5	2	ffvelcdmi	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ0 )
6	4 5	syl	⊢ ( 𝑋 ∈ 𝑆 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ0 )
7		algcvgblem	⊢ ( ( ( 𝐶 ‘ 𝑋 ) ∈ ℕ0 ∧ ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ0 ) → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ↔ ( ( ( 𝐶 ‘ 𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ∧ ( ( 𝐶 ‘ 𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) = 0 ) ) ) )
8	3 6 7	syl2anc	⊢ ( 𝑋 ∈ 𝑆 → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ↔ ( ( ( 𝐶 ‘ 𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ∧ ( ( 𝐶 ‘ 𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) = 0 ) ) ) )