# Metamath Proof Explorer

## 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 ffvelrni ( 𝑋𝑆 → ( 𝐶𝑋 ) ∈ ℕ0 )
4 1 ffvelrni ( 𝑋𝑆 → ( 𝐹𝑋 ) ∈ 𝑆 )
5 2 ffvelrni ( ( 𝐹𝑋 ) ∈ 𝑆 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) ∈ ℕ0 )
6 4 5 syl ( 𝑋𝑆 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) ∈ ℕ0 )
7 algcvgblem ( ( ( 𝐶𝑋 ) ∈ ℕ0 ∧ ( 𝐶 ‘ ( 𝐹𝑋 ) ) ∈ ℕ0 ) → ( ( ( 𝐶 ‘ ( 𝐹𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) < ( 𝐶𝑋 ) ) ↔ ( ( ( 𝐶𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) < ( 𝐶𝑋 ) ) ∧ ( ( 𝐶𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) = 0 ) ) ) )
8 3 6 7 syl2anc ( 𝑋𝑆 → ( ( ( 𝐶 ‘ ( 𝐹𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) < ( 𝐶𝑋 ) ) ↔ ( ( ( 𝐶𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) < ( 𝐶𝑋 ) ) ∧ ( ( 𝐶𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹𝑋 ) ) = 0 ) ) ) )