Metamath Proof Explorer

Theorem faclbnd4lem2

Description: Lemma for faclbnd4 . Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 to antecedents. (Contributed by NM, 23-Dec-2005)

Ref Expression
Assertion faclbnd4lem2 ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 ↑ ( 𝑁 − 1 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) )
2 1 oveq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) )
3 id ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) )
4 oveq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 + 𝐾 ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) )
5 3 4 oveq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) )
6 5 oveq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) = ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) )
7 6 oveq1d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) )
8 2 7 breq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ↔ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) )
9 oveq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 ↑ 𝑁 ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) )
10 9 oveq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) )
11 oveq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 + ( 𝐾 + 1 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) )
12 3 11 oveq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) )
13 12 oveq2d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) = ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) )
14 13 oveq1d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
15 10 14 breq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) )
16 8 15 imbi12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) → ( ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) ↔ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) ) )
17 oveq2 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( 𝑁 − 1 ) ↑ 𝐾 ) = ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) )
18 17 oveq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) )
19 oveq1 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( 𝐾 ↑ 2 ) = ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) )
20 19 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( 2 ↑ ( 𝐾 ↑ 2 ) ) = ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) )
21 oveq2 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) )
22 21 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) )
23 20 22 oveq12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) = ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) )
24 23 oveq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) = ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) )
25 18 24 breq12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ↔ ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) )
26 oveq1 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( 𝐾 + 1 ) = ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) )
27 26 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( 𝑁 ↑ ( 𝐾 + 1 ) ) = ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) )
28 27 oveq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) = ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) )
29 26 oveq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( 𝐾 + 1 ) ↑ 2 ) = ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) )
30 29 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) = ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) )
31 26 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) )
32 31 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) )
33 30 32 oveq12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) = ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) )
34 33 oveq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
35 28 34 breq12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) )
36 25 35 imbi12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) → ( ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) ↔ ( ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) ) )
37 oveq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( 𝑁 − 1 ) = ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) )
38 37 oveq1d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) = ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) )
39 37 oveq2d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) )
40 38 39 oveq12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) = ( ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) )
41 fvoveq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ! ‘ ( 𝑁 − 1 ) ) = ( ! ‘ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) )
42 41 oveq2d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) = ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) )
43 40 42 breq12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ↔ ( ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) ) )
44 oveq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) = ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) )
45 oveq2 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) = ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) )
46 44 45 oveq12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) = ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) )
47 fveq2 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ! ‘ 𝑁 ) = ( ! ‘ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) )
48 47 oveq2d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) )
49 46 48 breq12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) ) )
50 43 49 imbi12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( ( ( ( 𝑁 − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) ↔ ( ( ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) → ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) ) ) )
51 1nn ⊢ 1 ∈ ℕ
52 51 elimel ⊢ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ∈ ℕ
53 1nn0 ⊢ 1 ∈ ℕ0
54 53 elimel ⊢ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ∈ ℕ0
55 53 elimel ⊢ if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ∈ ℕ0
56 52 54 55 faclbnd4lem1 ⊢ ( ( ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ↑ if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) ≤ ( ( ( 2 ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) ) ) ) · ( ! ‘ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) − 1 ) ) ) → ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↑ ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) ≤ ( ( ( 2 ↑ ( ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ↑ 2 ) ) · ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) ↑ ( if ( 𝑀 ∈ ℕ0 , 𝑀 , 1 ) + ( if ( 𝐾 ∈ ℕ0 , 𝐾 , 1 ) + 1 ) ) ) ) · ( ! ‘ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) )
57 16 36 50 56 dedth3h ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ) )