Metamath Proof Explorer

Theorem smuval2

Description: The partial sum sequence stabilizes at N after the N + 1 -th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a 
|- ( ph -> A C_ NN0 )
smuval.b 
|- ( ph -> B C_ NN0 )
smuval.p 
|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
smuval.n 
|- ( ph -> N e. NN0 )
smuval2.m 
|- ( ph -> M e. ( ZZ>= ` ( N + 1 ) ) )
Assertion smuval2 
|- ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` M ) ) )

Proof

Step Hyp Ref Expression
1 smuval.a 
 |-  ( ph -> A C_ NN0 )
2 smuval.b 
 |-  ( ph -> B C_ NN0 )
3 smuval.p 
 |-  P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 smuval.n 
 |-  ( ph -> N e. NN0 )
5 smuval2.m 
 |-  ( ph -> M e. ( ZZ>= ` ( N + 1 ) ) )
6 fveq2 
 |-  ( x = ( N + 1 ) -> ( P ` x ) = ( P ` ( N + 1 ) ) )
7 6 eleq2d 
 |-  ( x = ( N + 1 ) -> ( N e. ( P ` x ) <-> N e. ( P ` ( N + 1 ) ) ) )
8 7 bibi2d 
 |-  ( x = ( N + 1 ) -> ( ( N e. ( A smul B ) <-> N e. ( P ` x ) ) <-> ( N e. ( A smul B ) <-> N e. ( P ` ( N + 1 ) ) ) ) )
9 8 imbi2d 
 |-  ( x = ( N + 1 ) -> ( ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` x ) ) ) <-> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( N + 1 ) ) ) ) ) )
10 fveq2 
 |-  ( x = k -> ( P ` x ) = ( P ` k ) )
11 10 eleq2d 
 |-  ( x = k -> ( N e. ( P ` x ) <-> N e. ( P ` k ) ) )
12 11 bibi2d 
 |-  ( x = k -> ( ( N e. ( A smul B ) <-> N e. ( P ` x ) ) <-> ( N e. ( A smul B ) <-> N e. ( P ` k ) ) ) )
13 12 imbi2d 
 |-  ( x = k -> ( ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` x ) ) ) <-> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` k ) ) ) ) )
14 fveq2 
 |-  ( x = ( k + 1 ) -> ( P ` x ) = ( P ` ( k + 1 ) ) )
15 14 eleq2d 
 |-  ( x = ( k + 1 ) -> ( N e. ( P ` x ) <-> N e. ( P ` ( k + 1 ) ) ) )
16 15 bibi2d 
 |-  ( x = ( k + 1 ) -> ( ( N e. ( A smul B ) <-> N e. ( P ` x ) ) <-> ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) ) )
17 16 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` x ) ) ) <-> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) ) ) )
18 fveq2 
 |-  ( x = M -> ( P ` x ) = ( P ` M ) )
19 18 eleq2d 
 |-  ( x = M -> ( N e. ( P ` x ) <-> N e. ( P ` M ) ) )
20 19 bibi2d 
 |-  ( x = M -> ( ( N e. ( A smul B ) <-> N e. ( P ` x ) ) <-> ( N e. ( A smul B ) <-> N e. ( P ` M ) ) ) )
21 20 imbi2d 
 |-  ( x = M -> ( ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` x ) ) ) <-> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` M ) ) ) ) )
22 1 2 3 4 smuval 
 |-  ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( N + 1 ) ) ) )
23 1 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> A C_ NN0 )
24 2 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> B C_ NN0 )
25 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
26 4 25 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
27 eluznn0 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. NN0 )
28 26 27 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. NN0 )
29 23 24 3 28 smupp1 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( P ` ( k + 1 ) ) = ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
30 29 eleq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( P ` ( k + 1 ) ) <-> N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) ) )
31 23 24 3 smupf 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> P : NN0 --> ~P NN0 )
32 31 28 ffvelrnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( P ` k ) e. ~P NN0 )
33 32 elpwid 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( P ` k ) C_ NN0 )
34 ssrab2 
 |-  { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } C_ NN0
35 34 a1i 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } C_ NN0 )
36 26 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N + 1 ) e. NN0 )
37 33 35 36 sadeq 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) )
38 inrab2 
 |-  ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) = { n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) | ( k e. A /\ ( n - k ) e. B ) }
39 simpr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) )
40 39 elin1d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n e. NN0 )
41 40 nn0red 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n e. RR )
42 4 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. NN0 )
43 42 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> N e. NN0 )
44 43 nn0red 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> N e. RR )
45 1red 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> 1 e. RR )
46 44 45 readdcld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( N + 1 ) e. RR )
47 28 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> k e. NN0 )
48 47 nn0red 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> k e. RR )
49 39 elin2d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n e. ( 0 ..^ ( N + 1 ) ) )
50 elfzolt2 
 |-  ( n e. ( 0 ..^ ( N + 1 ) ) -> n < ( N + 1 ) )
51 49 50 syl 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n < ( N + 1 ) )
52 eluzle 
 |-  ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( N + 1 ) <_ k )
53 52 ad2antlr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( N + 1 ) <_ k )
54 41 46 48 51 53 ltletrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> n < k )
55 41 48 ltnled 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( n < k <-> -. k <_ n ) )
56 54 55 mpbid 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> -. k <_ n )
57 24 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> B C_ NN0 )
58 57 sseld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( n - k ) e. B -> ( n - k ) e. NN0 ) )
59 nn0ge0 
 |-  ( ( n - k ) e. NN0 -> 0 <_ ( n - k ) )
60 58 59 syl6 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( n - k ) e. B -> 0 <_ ( n - k ) ) )
61 41 48 subge0d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( 0 <_ ( n - k ) <-> k <_ n ) )
62 60 61 sylibd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( n - k ) e. B -> k <_ n ) )
63 62 adantld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( k e. A /\ ( n - k ) e. B ) -> k <_ n ) )
64 56 63 mtod 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) /\ n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) ) -> -. ( k e. A /\ ( n - k ) e. B ) )
65 64 ralrimiva 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> A. n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) -. ( k e. A /\ ( n - k ) e. B ) )
66 rabeq0 
 |-  ( { n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) | ( k e. A /\ ( n - k ) e. B ) } = (/) <-> A. n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) -. ( k e. A /\ ( n - k ) e. B ) )
67 65 66 sylibr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> { n e. ( NN0 i^i ( 0 ..^ ( N + 1 ) ) ) | ( k e. A /\ ( n - k ) e. B ) } = (/) )
68 38 67 syl5eq 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) = (/) )
69 68 oveq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd (/) ) )
70 inss1 
 |-  ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) C_ ( P ` k )
71 70 33 sstrid 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) C_ NN0 )
72 sadid1 
 |-  ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) C_ NN0 -> ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd (/) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) )
73 71 72 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd (/) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) )
74 69 73 eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) )
75 74 ineq1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) )
76 inass 
 |-  ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( P ` k ) i^i ( ( 0 ..^ ( N + 1 ) ) i^i ( 0 ..^ ( N + 1 ) ) ) )
77 inidm 
 |-  ( ( 0 ..^ ( N + 1 ) ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( 0 ..^ ( N + 1 ) )
78 77 ineq2i 
 |-  ( ( P ` k ) i^i ( ( 0 ..^ ( N + 1 ) ) i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) )
79 76 78 eqtri 
 |-  ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) )
80 75 79 eqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) sadd ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } i^i ( 0 ..^ ( N + 1 ) ) ) ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) )
81 37 80 eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) )
82 81 eleq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) i^i ( 0 ..^ ( N + 1 ) ) ) <-> N e. ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) ) )
83 elin 
 |-  ( N e. ( ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) i^i ( 0 ..^ ( N + 1 ) ) ) <-> ( N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) )
84 elin 
 |-  ( N e. ( ( P ` k ) i^i ( 0 ..^ ( N + 1 ) ) ) <-> ( N e. ( P ` k ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) )
85 82 83 84 3bitr3g 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) <-> ( N e. ( P ` k ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) ) )
86 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
87 42 86 eleqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( ZZ>= ` 0 ) )
88 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
89 87 88 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( 0 ... N ) )
90 42 nn0zd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ZZ )
91 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
92 90 91 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
93 89 92 eleqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( 0 ..^ ( N + 1 ) ) )
94 93 biantrud 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) <-> ( N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) ) )
95 93 biantrud 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( P ` k ) <-> ( N e. ( P ` k ) /\ N e. ( 0 ..^ ( N + 1 ) ) ) ) )
96 85 94 95 3bitr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) <-> N e. ( P ` k ) ) )
97 30 96 bitrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N e. ( P ` ( k + 1 ) ) <-> N e. ( P ` k ) ) )
98 97 bibi2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) <-> ( N e. ( A smul B ) <-> N e. ( P ` k ) ) ) )
99 98 biimprd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N e. ( A smul B ) <-> N e. ( P ` k ) ) -> ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) ) )
100 99 expcom 
 |-  ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( ph -> ( ( N e. ( A smul B ) <-> N e. ( P ` k ) ) -> ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) ) ) )
101 100 a2d 
 |-  ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` k ) ) ) -> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( k + 1 ) ) ) ) ) )
102 9 13 17 21 22 101 uzind4i 
 |-  ( M e. ( ZZ>= ` ( N + 1 ) ) -> ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` M ) ) ) )
103 5 102 mpcom 
 |-  ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` M ) ) )