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 ) ) ) ) ยท ( ! โ€˜ ๐‘ ) ) ) )