Metamath Proof Explorer

Theorem unitscyglem4

Description: Lemma for unitscyg (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 
|- B = ( Base ` G )
unitscyglem1.2 
|- .^ = ( .g ` G )
unitscyglem1.3 
|- ( ph -> G e. Grp )
unitscyglem1.4 
|- ( ph -> B e. Fin )
unitscyglem1.5 
|- ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
unitscyglem4.1 
|- ( ph -> D e. NN )
unitscyglem4.2 
|- ( ph -> D || ( # ` B ) )
Assertion unitscyglem4 
|- ( ph -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 
 |-  B = ( Base ` G )
2 unitscyglem1.2 
 |-  .^ = ( .g ` G )
3 unitscyglem1.3 
 |-  ( ph -> G e. Grp )
4 unitscyglem1.4 
 |-  ( ph -> B e. Fin )
5 unitscyglem1.5 
 |-  ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
6 unitscyglem4.1 
 |-  ( ph -> D e. NN )
7 unitscyglem4.2 
 |-  ( ph -> D || ( # ` B ) )
8 nfcv 
 |-  F/_ y B
9 nfcv 
 |-  F/_ x B
10 nfv 
 |-  F/ x ( ( od ` G ) ` y ) = D
11 nfv 
 |-  F/ y ( ( od ` G ) ` x ) = D
12 fveqeq2 
 |-  ( y = x -> ( ( ( od ` G ) ` y ) = D <-> ( ( od ` G ) ` x ) = D ) )
13 8 9 10 11 12 cbvrabw 
 |-  { y e. B | ( ( od ` G ) ` y ) = D } = { x e. B | ( ( od ` G ) ` x ) = D }
14 13 fveq2i 
 |-  ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = D } )
15 14 a1i 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) )
16 7 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> D || ( # ` B ) )
17 16 ex 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) -> D || ( # ` B ) ) )
18 17 ancrd 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) -> ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) ) )
19 18 imdistani 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( ph /\ ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) ) )
20 breq1 
 |-  ( m = D -> ( m || ( # ` B ) <-> D || ( # ` B ) ) )
21 eqeq2 
 |-  ( m = D -> ( ( ( od ` G ) ` x ) = m <-> ( ( od ` G ) ` x ) = D ) )
22 21 rabbidv 
 |-  ( m = D -> { x e. B | ( ( od ` G ) ` x ) = m } = { x e. B | ( ( od ` G ) ` x ) = D } )
23 22 neeq1d 
 |-  ( m = D -> ( { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) )
24 20 23 anbi12d 
 |-  ( m = D -> ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) <-> ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) ) )
25 22 fveq2d 
 |-  ( m = D -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) )
26 fveq2 
 |-  ( m = D -> ( phi ` m ) = ( phi ` D ) )
27 25 26 eqeq12d 
 |-  ( m = D -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) ) )
28 24 27 imbi12d 
 |-  ( m = D -> ( ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) ) <-> ( ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) ) ) )
29 1 2 3 4 5 unitscyglem3 
 |-  ( ph -> A. m e. NN ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) ) )
30 28 29 6 rspcdva 
 |-  ( ph -> ( ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) ) )
31 30 imp 
 |-  ( ( ph /\ ( D || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) )
32 19 31 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) )
33 15 32 eqtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )
34 id 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
35 34 necon1bi 
 |-  ( -. { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = D } = (/) )
36 35 adantl 
 |-  ( ( ph /\ -. { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = D } = (/) )
37 3 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> G e. Grp )
38 4 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> B e. Fin )
39 1 37 38 hashfingrpnn 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. NN )
40 1 2 37 38 39 grpods 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( ( # ` B ) .^ x ) = ( 0g ` G ) } ) )
41 simpr 
 |-  ( ( ( ( ph /\ x e. B ) /\ l e. ZZ ) /\ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) -> ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) )
42 41 eqcomd 
 |-  ( ( ( ( ph /\ x e. B ) /\ l e. ZZ ) /\ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) -> ( # ` B ) = ( l x. ( ( od ` G ) ` x ) ) )
43 42 oveq1d 
 |-  ( ( ( ( ph /\ x e. B ) /\ l e. ZZ ) /\ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) -> ( ( # ` B ) .^ x ) = ( ( l x. ( ( od ` G ) ` x ) ) .^ x ) )
44 3 adantr 
 |-  ( ( ph /\ x e. B ) -> G e. Grp )
45 44 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> G e. Grp )
46 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> l e. ZZ )
47 eqid 
 |-  ( od ` G ) = ( od ` G )
48 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
49 1 47 48 odcld 
 |-  ( ( ph /\ x e. B ) -> ( ( od ` G ) ` x ) e. NN0 )
50 49 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( ( od ` G ) ` x ) e. NN0 )
51 50 nn0zd 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( ( od ` G ) ` x ) e. ZZ )
52 simplr 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> x e. B )
53 46 51 52 3jca 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( l e. ZZ /\ ( ( od ` G ) ` x ) e. ZZ /\ x e. B ) )
54 1 2 mulgass 
 |-  ( ( G e. Grp /\ ( l e. ZZ /\ ( ( od ` G ) ` x ) e. ZZ /\ x e. B ) ) -> ( ( l x. ( ( od ` G ) ` x ) ) .^ x ) = ( l .^ ( ( ( od ` G ) ` x ) .^ x ) ) )
55 45 53 54 syl2anc 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( ( l x. ( ( od ` G ) ` x ) ) .^ x ) = ( l .^ ( ( ( od ` G ) ` x ) .^ x ) ) )
56 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
57 1 47 2 56 odid 
 |-  ( x e. B -> ( ( ( od ` G ) ` x ) .^ x ) = ( 0g ` G ) )
58 52 57 syl 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( ( ( od ` G ) ` x ) .^ x ) = ( 0g ` G ) )
59 58 oveq2d 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( l .^ ( ( ( od ` G ) ` x ) .^ x ) ) = ( l .^ ( 0g ` G ) ) )
60 1 2 56 mulgz 
 |-  ( ( G e. Grp /\ l e. ZZ ) -> ( l .^ ( 0g ` G ) ) = ( 0g ` G ) )
61 44 60 sylan 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( l .^ ( 0g ` G ) ) = ( 0g ` G ) )
62 59 61 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( l .^ ( ( ( od ` G ) ` x ) .^ x ) ) = ( 0g ` G ) )
63 55 62 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ l e. ZZ ) -> ( ( l x. ( ( od ` G ) ` x ) ) .^ x ) = ( 0g ` G ) )
64 63 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ l e. ZZ ) /\ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) -> ( ( l x. ( ( od ` G ) ` x ) ) .^ x ) = ( 0g ` G ) )
65 43 64 eqtrd 
 |-  ( ( ( ( ph /\ x e. B ) /\ l e. ZZ ) /\ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) -> ( ( # ` B ) .^ x ) = ( 0g ` G ) )
66 4 adantr 
 |-  ( ( ph /\ x e. B ) -> B e. Fin )
67 1 47 oddvds2 
 |-  ( ( G e. Grp /\ B e. Fin /\ x e. B ) -> ( ( od ` G ) ` x ) || ( # ` B ) )
68 44 66 48 67 syl3anc 
 |-  ( ( ph /\ x e. B ) -> ( ( od ` G ) ` x ) || ( # ` B ) )
69 49 nn0zd 
 |-  ( ( ph /\ x e. B ) -> ( ( od ` G ) ` x ) e. ZZ )
70 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
71 66 70 syl 
 |-  ( ( ph /\ x e. B ) -> ( # ` B ) e. NN0 )
72 71 nn0zd 
 |-  ( ( ph /\ x e. B ) -> ( # ` B ) e. ZZ )
73 divides 
 |-  ( ( ( ( od ` G ) ` x ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( ( od ` G ) ` x ) || ( # ` B ) <-> E. l e. ZZ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) )
74 69 72 73 syl2anc 
 |-  ( ( ph /\ x e. B ) -> ( ( ( od ` G ) ` x ) || ( # ` B ) <-> E. l e. ZZ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) ) )
75 68 74 mpbid 
 |-  ( ( ph /\ x e. B ) -> E. l e. ZZ ( l x. ( ( od ` G ) ` x ) ) = ( # ` B ) )
76 65 75 r19.29a 
 |-  ( ( ph /\ x e. B ) -> ( ( # ` B ) .^ x ) = ( 0g ` G ) )
77 76 rabeqcda 
 |-  ( ph -> { x e. B | ( ( # ` B ) .^ x ) = ( 0g ` G ) } = B )
78 77 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { x e. B | ( ( # ` B ) .^ x ) = ( 0g ` G ) } = B )
79 78 fveq2d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( # ` B ) .^ x ) = ( 0g ` G ) } ) = ( # ` B ) )
80 40 79 eqtr2d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) = sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
81 nfv 
 |-  F/ k ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) )
82 nfcv 
 |-  F/_ k ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } )
83 fzfid 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( 1 ... ( # ` B ) ) e. Fin )
84 ssrab2 
 |-  { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } C_ ( 1 ... ( # ` B ) )
85 84 a1i 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } C_ ( 1 ... ( # ` B ) ) )
86 83 85 ssfid 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } e. Fin )
87 38 adantr 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> B e. Fin )
88 ssrab2 
 |-  { x e. B | ( ( od ` G ) ` x ) = k } C_ B
89 88 a1i 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
90 87 89 ssfid 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
91 hashcl 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = k } e. Fin -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
92 90 91 syl 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
93 92 nn0cnd 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. CC )
94 breq1 
 |-  ( a = ( # ` B ) -> ( a || ( # ` B ) <-> ( # ` B ) || ( # ` B ) ) )
95 1zzd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> 1 e. ZZ )
96 39 nnzd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. ZZ )
97 39 nnge1d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> 1 <_ ( # ` B ) )
98 39 nnred 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. RR )
99 98 leidd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) <_ ( # ` B ) )
100 95 96 96 97 99 elfzd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. ( 1 ... ( # ` B ) ) )
101 iddvds 
 |-  ( ( # ` B ) e. ZZ -> ( # ` B ) || ( # ` B ) )
102 96 101 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) || ( # ` B ) )
103 94 100 102 elrabd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
104 eqeq2 
 |-  ( k = ( # ` B ) -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` x ) = ( # ` B ) ) )
105 104 rabbidv 
 |-  ( k = ( # ` B ) -> { x e. B | ( ( od ` G ) ` x ) = k } = { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } )
106 105 fveq2d 
 |-  ( k = ( # ` B ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) )
107 81 82 86 93 103 106 fsumsplit1 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) + sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) ) )
108 ssrab2 
 |-  { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } C_ B
109 108 a1i 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } C_ B )
110 38 109 ssfid 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } e. Fin )
111 hashcl 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } e. Fin -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) e. NN0 )
112 110 111 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) e. NN0 )
113 112 nn0red 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) e. RR )
114 diffi 
 |-  ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } e. Fin -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) e. Fin )
115 86 114 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) e. Fin )
116 38 adantr 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> B e. Fin )
117 88 a1i 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
118 116 117 ssfid 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
119 118 91 syl 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
120 115 119 fsumnn0cl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
121 120 nn0red 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. RR )
122 39 phicld 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( phi ` ( # ` B ) ) e. NN )
123 122 nnred 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( phi ` ( # ` B ) ) e. RR )
124 eldifi 
 |-  ( k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) -> k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
125 breq1 
 |-  ( a = k -> ( a || ( # ` B ) <-> k || ( # ` B ) ) )
126 125 elrab 
 |-  ( k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } <-> ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) )
127 126 biimpi 
 |-  ( k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } -> ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) )
128 elfzelz 
 |-  ( k e. ( 1 ... ( # ` B ) ) -> k e. ZZ )
129 elfzle1 
 |-  ( k e. ( 1 ... ( # ` B ) ) -> 1 <_ k )
130 128 129 jca 
 |-  ( k e. ( 1 ... ( # ` B ) ) -> ( k e. ZZ /\ 1 <_ k ) )
131 130 adantr 
 |-  ( ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) -> ( k e. ZZ /\ 1 <_ k ) )
132 127 131 syl 
 |-  ( k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } -> ( k e. ZZ /\ 1 <_ k ) )
133 124 132 syl 
 |-  ( k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) -> ( k e. ZZ /\ 1 <_ k ) )
134 133 adantl 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( k e. ZZ /\ 1 <_ k ) )
135 elnnz1 
 |-  ( k e. NN <-> ( k e. ZZ /\ 1 <_ k ) )
136 134 135 sylibr 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> k e. NN )
137 phicl 
 |-  ( k e. NN -> ( phi ` k ) e. NN )
138 136 137 syl 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( phi ` k ) e. NN )
139 138 nnred 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( phi ` k ) e. RR )
140 115 139 fsumrecl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) e. RR )
141 simplll 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ph )
142 simplr 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> z e. B )
143 141 142 jca 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ph /\ z e. B ) )
144 simpr 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` z ) = ( # ` B ) )
145 143 144 jca 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) )
146 fveqeq2 
 |-  ( x = ( ( ( # ` B ) / D ) .^ z ) -> ( ( ( od ` G ) ` x ) = D <-> ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) = D ) )
147 3 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> G e. Grp )
148 7 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D || ( # ` B ) )
149 6 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D e. NN )
150 149 nnzd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D e. ZZ )
151 149 nnne0d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D =/= 0 )
152 4 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> B e. Fin )
153 152 70 syl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) e. NN0 )
154 153 nn0zd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) e. ZZ )
155 dvdsval2 
 |-  ( ( D e. ZZ /\ D =/= 0 /\ ( # ` B ) e. ZZ ) -> ( D || ( # ` B ) <-> ( ( # ` B ) / D ) e. ZZ ) )
156 150 151 154 155 syl3anc 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( D || ( # ` B ) <-> ( ( # ` B ) / D ) e. ZZ ) )
157 148 156 mpbid 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / D ) e. ZZ )
158 simplr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> z e. B )
159 1 2 147 157 158 mulgcld 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) .^ z ) e. B )
160 153 nn0cnd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) e. CC )
161 6 nncnd 
 |-  ( ph -> D e. CC )
162 161 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D e. CC )
163 1 147 152 hashfingrpnn 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) e. NN )
164 163 nnne0d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) =/= 0 )
165 160 160 162 164 151 divdiv2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / ( ( # ` B ) / D ) ) = ( ( ( # ` B ) x. D ) / ( # ` B ) ) )
166 162 160 164 divcan3d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) x. D ) / ( # ` B ) ) = D )
167 165 166 eqtr2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D = ( ( # ` B ) / ( ( # ` B ) / D ) ) )
168 simpr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` z ) = ( # ` B ) )
169 168 oveq2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) = ( ( ( # ` B ) / D ) gcd ( # ` B ) ) )
170 4 70 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
171 170 nn0cnd 
 |-  ( ph -> ( # ` B ) e. CC )
172 6 nnne0d 
 |-  ( ph -> D =/= 0 )
173 171 161 172 divcan2d 
 |-  ( ph -> ( D x. ( ( # ` B ) / D ) ) = ( # ` B ) )
174 173 eqcomd 
 |-  ( ph -> ( # ` B ) = ( D x. ( ( # ` B ) / D ) ) )
175 174 adantr 
 |-  ( ( ph /\ z e. B ) -> ( # ` B ) = ( D x. ( ( # ` B ) / D ) ) )
176 175 adantr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) = ( D x. ( ( # ` B ) / D ) ) )
177 176 oveq2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( # ` B ) ) = ( ( ( # ` B ) / D ) gcd ( D x. ( ( # ` B ) / D ) ) ) )
178 nndivdvds 
 |-  ( ( ( # ` B ) e. NN /\ D e. NN ) -> ( D || ( # ` B ) <-> ( ( # ` B ) / D ) e. NN ) )
179 163 149 178 syl2anc 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( D || ( # ` B ) <-> ( ( # ` B ) / D ) e. NN ) )
180 148 179 mpbid 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / D ) e. NN )
181 180 nnnn0d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / D ) e. NN0 )
182 181 150 gcdmultipled 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( D x. ( ( # ` B ) / D ) ) ) = ( ( # ` B ) / D ) )
183 177 182 eqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( # ` B ) ) = ( ( # ` B ) / D ) )
184 169 183 eqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) = ( ( # ` B ) / D ) )
185 184 eqcomd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / D ) = ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) )
186 185 oveq2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / ( ( # ` B ) / D ) ) = ( ( # ` B ) / ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) ) )
187 167 186 eqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> D = ( ( # ` B ) / ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) ) )
188 168 eqcomd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) = ( ( od ` G ) ` z ) )
189 1 47 2 odmulg 
 |-  ( ( G e. Grp /\ z e. B /\ ( ( # ` B ) / D ) e. ZZ ) -> ( ( od ` G ) ` z ) = ( ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) x. ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) ) )
190 147 158 157 189 syl3anc 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` z ) = ( ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) x. ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) ) )
191 188 190 eqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( # ` B ) = ( ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) x. ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) ) )
192 191 eqcomd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) x. ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) ) = ( # ` B ) )
193 157 zcnd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / D ) e. CC )
194 184 193 eqeltrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) e. CC )
195 1 47 159 odcld 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) e. NN0 )
196 195 nn0cnd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) e. CC )
197 168 154 eqeltrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` z ) e. ZZ )
198 168 164 eqnetrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` z ) =/= 0 )
199 157 197 198 3jca 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) e. ZZ /\ ( ( od ` G ) ` z ) e. ZZ /\ ( ( od ` G ) ` z ) =/= 0 ) )
200 gcd2n0cl 
 |-  ( ( ( ( # ` B ) / D ) e. ZZ /\ ( ( od ` G ) ` z ) e. ZZ /\ ( ( od ` G ) ` z ) =/= 0 ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) e. NN )
201 199 200 syl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) e. NN )
202 201 nnne0d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) =/= 0 )
203 160 194 196 202 divmuld 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) ) = ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) <-> ( ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) x. ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) ) = ( # ` B ) ) )
204 192 203 mpbird 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( # ` B ) / ( ( ( # ` B ) / D ) gcd ( ( od ` G ) ` z ) ) ) = ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) )
205 187 204 eqtr2d 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( od ` G ) ` ( ( ( # ` B ) / D ) .^ z ) ) = D )
206 146 159 205 elrabd 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> ( ( ( # ` B ) / D ) .^ z ) e. { x e. B | ( ( od ` G ) ` x ) = D } )
207 ne0i 
 |-  ( ( ( ( # ` B ) / D ) .^ z ) e. { x e. B | ( ( od ` G ) ` x ) = D } -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
208 206 207 syl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
209 145 208 syl 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) /\ z e. B ) /\ ( ( od ` G ) ` z ) = ( # ` B ) ) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
210 rabn0 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) <-> E. x e. B ( ( od ` G ) ` x ) = ( # ` B ) )
211 nfv 
 |-  F/ z ( ( od ` G ) ` x ) = ( # ` B )
212 nfv 
 |-  F/ x ( ( od ` G ) ` z ) = ( # ` B )
213 fveqeq2 
 |-  ( x = z -> ( ( ( od ` G ) ` x ) = ( # ` B ) <-> ( ( od ` G ) ` z ) = ( # ` B ) ) )
214 211 212 213 cbvrexw 
 |-  ( E. x e. B ( ( od ` G ) ` x ) = ( # ` B ) <-> E. z e. B ( ( od ` G ) ` z ) = ( # ` B ) )
215 210 214 bitri 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) <-> E. z e. B ( ( od ` G ) ` z ) = ( # ` B ) )
216 215 biimpi 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) -> E. z e. B ( ( od ` G ) ` z ) = ( # ` B ) )
217 216 adantl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) -> E. z e. B ( ( od ` G ) ` z ) = ( # ` B ) )
218 209 217 r19.29a 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
219 218 ex 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) )
220 219 necon4d 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } = (/) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } = (/) ) )
221 220 imp 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } = (/) )
222 221 fveq2d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) = ( # ` (/) ) )
223 hash0 
 |-  ( # ` (/) ) = 0
224 223 a1i 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` (/) ) = 0 )
225 222 224 eqtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) = 0 )
226 122 nngt0d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> 0 < ( phi ` ( # ` B ) ) )
227 225 226 eqbrtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) < ( phi ` ( # ` B ) ) )
228 eldif 
 |-  ( z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) <-> ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) )
229 228 biimpi 
 |-  ( z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) -> ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) )
230 229 adantl 
 |-  ( ( ph /\ z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) )
231 breq1 
 |-  ( a = z -> ( a || ( # ` B ) <-> z || ( # ` B ) ) )
232 231 elrab 
 |-  ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } <-> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
233 232 biimpi 
 |-  ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } -> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
234 233 adantr 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
235 velsn 
 |-  ( z e. { ( # ` B ) } <-> z = ( # ` B ) )
236 235 bicomi 
 |-  ( z = ( # ` B ) <-> z e. { ( # ` B ) } )
237 236 biimpi 
 |-  ( z = ( # ` B ) -> z e. { ( # ` B ) } )
238 237 necon3bi 
 |-  ( -. z e. { ( # ` B ) } -> z =/= ( # ` B ) )
239 238 adantl 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> z =/= ( # ` B ) )
240 234 239 jca 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) )
241 240 adantl 
 |-  ( ( ph /\ ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) ) -> ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) )
242 1zzd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> 1 e. ZZ )
243 4 adantr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> B e. Fin )
244 243 70 syl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. NN0 )
245 244 nn0zd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. ZZ )
246 245 242 zsubcld 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( ( # ` B ) - 1 ) e. ZZ )
247 elfzelz 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> z e. ZZ )
248 247 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> z e. ZZ )
249 248 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z e. ZZ )
250 249 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. ZZ )
251 elfzle1 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> 1 <_ z )
252 251 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> 1 <_ z )
253 252 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> 1 <_ z )
254 253 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> 1 <_ z )
255 elfzle2 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> z <_ ( # ` B ) )
256 255 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> z <_ ( # ` B ) )
257 256 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z <_ ( # ` B ) )
258 257 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z <_ ( # ` B ) )
259 simprr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z =/= ( # ` B ) )
260 259 necomd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) =/= z )
261 258 260 jca 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z <_ ( # ` B ) /\ ( # ` B ) =/= z ) )
262 250 zred 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. RR )
263 244 nn0red 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. RR )
264 262 263 ltlend 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z < ( # ` B ) <-> ( z <_ ( # ` B ) /\ ( # ` B ) =/= z ) ) )
265 261 264 mpbird 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z < ( # ` B ) )
266 250 245 zltlem1d 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z < ( # ` B ) <-> z <_ ( ( # ` B ) - 1 ) ) )
267 265 266 mpbid 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
268 242 246 250 254 267 elfzd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. ( 1 ... ( ( # ` B ) - 1 ) ) )
269 simprlr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z || ( # ` B ) )
270 231 268 269 elrabd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
271 270 ex 
 |-  ( ph -> ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
272 271 adantr 
 |-  ( ( ph /\ ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) ) -> ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
273 241 272 mpd 
 |-  ( ( ph /\ ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
274 273 ex 
 |-  ( ph -> ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
275 274 adantr 
 |-  ( ( ph /\ z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
276 230 275 mpd 
 |-  ( ( ph /\ z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
277 276 ex 
 |-  ( ph -> ( z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
278 277 ssrdv 
 |-  ( ph -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) C_ { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
279 1zzd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 e. ZZ )
280 170 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
281 280 adantr 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( # ` B ) e. ZZ )
282 elfzelz 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z e. ZZ )
283 282 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. ZZ )
284 elfzle1 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> 1 <_ z )
285 284 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 <_ z )
286 283 zred 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. RR )
287 281 zred 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( # ` B ) e. RR )
288 1red 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 e. RR )
289 287 288 resubcld 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( ( # ` B ) - 1 ) e. RR )
290 elfzle2 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z <_ ( ( # ` B ) - 1 ) )
291 290 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
292 287 lem1d 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( ( # ` B ) - 1 ) <_ ( # ` B ) )
293 286 289 287 291 292 letrd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z <_ ( # ` B ) )
294 279 281 283 285 293 elfzd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. ( 1 ... ( # ` B ) ) )
295 294 ex 
 |-  ( ph -> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z e. ( 1 ... ( # ` B ) ) ) )
296 295 ssrdv 
 |-  ( ph -> ( 1 ... ( ( # ` B ) - 1 ) ) C_ ( 1 ... ( # ` B ) ) )
297 rabss2 
 |-  ( ( 1 ... ( ( # ` B ) - 1 ) ) C_ ( 1 ... ( # ` B ) ) -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
298 296 297 syl 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
299 298 sseld 
 |-  ( ph -> ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) )
300 299 imp 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
301 170 ad2antrr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) e. NN0 )
302 301 nn0red 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) e. RR )
303 302 leidd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) <_ ( # ` B ) )
304 simpr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z = ( # ` B ) )
305 304 eqcomd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) = z )
306 231 elrab 
 |-  ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } <-> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) )
307 306 biimpi 
 |-  ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) )
308 307 adantl 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) )
309 291 adantrr 
 |-  ( ( ph /\ ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
310 309 ex 
 |-  ( ph -> ( ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) -> z <_ ( ( # ` B ) - 1 ) ) )
311 310 adantr 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) -> z <_ ( ( # ` B ) - 1 ) ) )
312 308 311 mpd 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z <_ ( ( # ` B ) - 1 ) )
313 300 233 248 3syl 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. ZZ )
314 280 adantr 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` B ) e. ZZ )
315 313 314 zltlem1d 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( z < ( # ` B ) <-> z <_ ( ( # ` B ) - 1 ) ) )
316 312 315 mpbird 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z < ( # ` B ) )
317 316 adantr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z < ( # ` B ) )
318 305 317 eqbrtrd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) < ( # ` B ) )
319 302 302 ltnled 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( ( # ` B ) < ( # ` B ) <-> -. ( # ` B ) <_ ( # ` B ) ) )
320 318 319 mpbid 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> -. ( # ` B ) <_ ( # ` B ) )
321 303 320 pm2.21dd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z =/= ( # ` B ) )
322 simpr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z =/= ( # ` B ) ) -> z =/= ( # ` B ) )
323 321 322 pm2.61dane 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z =/= ( # ` B ) )
324 300 323 eldifsnd 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) )
325 324 ex 
 |-  ( ph -> ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) )
326 325 ssrdv 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) )
327 278 326 eqssd 
 |-  ( ph -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) = { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
328 327 sumeq1d 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
329 fzfid 
 |-  ( ph -> ( 1 ... ( ( # ` B ) - 1 ) ) e. Fin )
330 ssrab2 
 |-  { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( 1 ... ( ( # ` B ) - 1 ) )
331 330 a1i 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( 1 ... ( ( # ` B ) - 1 ) ) )
332 329 331 ssfid 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } e. Fin )
333 4 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> B e. Fin )
334 88 a1i 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
335 333 334 ssfid 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
336 335 91 syl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
337 336 nn0red 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. RR )
338 125 elrab 
 |-  ( k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } <-> ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) )
339 338 biimpi 
 |-  ( k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) )
340 339 adantl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) )
341 elfzelz 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> k e. ZZ )
342 elfzle1 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> 1 <_ k )
343 341 342 jca 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> ( k e. ZZ /\ 1 <_ k ) )
344 343 adantr 
 |-  ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> ( k e. ZZ /\ 1 <_ k ) )
345 344 adantl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
346 345 135 sylibr 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> k e. NN )
347 346 ex 
 |-  ( ph -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> k e. NN ) )
348 347 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> k e. NN ) )
349 340 348 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> k e. NN )
350 349 phicld 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. NN )
351 350 nnred 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. RR )
352 simpll 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ph )
353 338 biimpri 
 |-  ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
354 353 adantl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
355 354 adantr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
356 352 355 jca 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
357 356 337 syl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. RR )
358 simpr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
359 356 358 jca 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
360 340 simprd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> k || ( # ` B ) )
361 360 adantr 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> k || ( # ` B ) )
362 simpr 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
363 361 362 jca 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
364 breq1 
 |-  ( m = k -> ( m || ( # ` B ) <-> k || ( # ` B ) ) )
365 eqeq2 
 |-  ( m = k -> ( ( ( od ` G ) ` x ) = m <-> ( ( od ` G ) ` x ) = k ) )
366 365 rabbidv 
 |-  ( m = k -> { x e. B | ( ( od ` G ) ` x ) = m } = { x e. B | ( ( od ` G ) ` x ) = k } )
367 366 neeq1d 
 |-  ( m = k -> ( { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
368 364 367 anbi12d 
 |-  ( m = k -> ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) <-> ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) ) )
369 366 fveq2d 
 |-  ( m = k -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
370 fveq2 
 |-  ( m = k -> ( phi ` m ) = ( phi ` k ) )
371 369 370 eqeq12d 
 |-  ( m = k -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
372 368 371 imbi12d 
 |-  ( m = k -> ( ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) ) <-> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) ) )
373 29 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> A. m e. NN ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) ) )
374 372 373 349 rspcdva 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
375 374 adantr 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
376 363 375 mpd 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) )
377 359 376 syl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) )
378 357 377 eqled 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
379 id 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
380 379 necon1bi 
 |-  ( -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = k } = (/) )
381 380 adantl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = k } = (/) )
382 381 fveq2d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` (/) ) )
383 223 a1i 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` (/) ) = 0 )
384 382 383 eqtrd 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = 0 )
385 346 adantr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> k e. NN )
386 385 phicld 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( phi ` k ) e. NN )
387 386 nnnn0d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( phi ` k ) e. NN0 )
388 387 nn0ge0d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> 0 <_ ( phi ` k ) )
389 384 388 eqbrtrd 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
390 378 389 pm2.61dan 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
391 390 ex 
 |-  ( ph -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) ) )
392 391 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) ) )
393 340 392 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
394 332 337 351 393 fsumle 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( phi ` k ) )
395 327 sumeq1d 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) = sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( phi ` k ) )
396 395 eqcomd 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( phi ` k ) = sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) )
397 394 396 breqtrd 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) )
398 328 397 eqbrtrd 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) )
399 398 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) )
400 113 121 123 140 227 399 ltleaddd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) + sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) ) < ( ( phi ` ( # ` B ) ) + sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) ) )
401 nfcv 
 |-  F/_ k ( phi ` ( # ` B ) )
402 simpll 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ph )
403 127 adantl 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) )
404 402 403 jca 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) )
405 131 adantl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
406 405 adantl 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) /\ ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
407 406 135 sylibr 
 |-  ( ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) /\ ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) ) -> k e. NN )
408 407 ex 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) -> k e. NN ) )
409 404 408 mpd 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> k e. NN )
410 409 phicld 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. NN )
411 410 nncnd 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. CC )
412 fveq2 
 |-  ( k = ( # ` B ) -> ( phi ` k ) = ( phi ` ( # ` B ) ) )
413 81 401 86 411 103 412 fsumsplit1 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( phi ` k ) = ( ( phi ` ( # ` B ) ) + sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( phi ` k ) ) )
414 400 413 breqtrrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) + sum_ k e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) ) < sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( phi ` k ) )
415 107 414 eqbrtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) < sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( phi ` k ) )
416 elfzelz 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> a e. ZZ )
417 elfzle1 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> 1 <_ a )
418 416 417 jca 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> ( a e. ZZ /\ 1 <_ a ) )
419 418 adantr 
 |-  ( ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) -> ( a e. ZZ /\ 1 <_ a ) )
420 419 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) ) -> ( a e. ZZ /\ 1 <_ a ) )
421 elnnz1 
 |-  ( a e. NN <-> ( a e. ZZ /\ 1 <_ a ) )
422 420 421 sylibr 
 |-  ( ( ph /\ ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) ) -> a e. NN )
423 422 rabss3d 
 |-  ( ph -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } C_ { a e. NN | a || ( # ` B ) } )
424 simpl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ph )
425 simprl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a e. NN )
426 424 425 jca 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ( ph /\ a e. NN ) )
427 simprr 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a || ( # ` B ) )
428 426 427 jca 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) )
429 1zzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> 1 e. ZZ )
430 280 adantr 
 |-  ( ( ph /\ a e. NN ) -> ( # ` B ) e. ZZ )
431 430 adantr 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> ( # ` B ) e. ZZ )
432 425 anassrs 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. NN )
433 432 nnzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. ZZ )
434 432 nnge1d 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> 1 <_ a )
435 nnz 
 |-  ( a e. NN -> a e. ZZ )
436 435 adantl 
 |-  ( ( ph /\ a e. NN ) -> a e. ZZ )
437 1 3 4 hashfingrpnn 
 |-  ( ph -> ( # ` B ) e. NN )
438 437 adantr 
 |-  ( ( ph /\ a e. NN ) -> ( # ` B ) e. NN )
439 dvdsle 
 |-  ( ( a e. ZZ /\ ( # ` B ) e. NN ) -> ( a || ( # ` B ) -> a <_ ( # ` B ) ) )
440 436 438 439 syl2anc 
 |-  ( ( ph /\ a e. NN ) -> ( a || ( # ` B ) -> a <_ ( # ` B ) ) )
441 440 imp 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a <_ ( # ` B ) )
442 429 431 433 434 441 elfzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. ( 1 ... ( # ` B ) ) )
443 428 442 syl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a e. ( 1 ... ( # ` B ) ) )
444 443 rabss3d 
 |-  ( ph -> { a e. NN | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
445 423 444 eqssd 
 |-  ( ph -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } = { a e. NN | a || ( # ` B ) } )
446 445 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } = { a e. NN | a || ( # ` B ) } )
447 446 sumeq1d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( phi ` k ) = sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) )
448 415 447 breqtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) < sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) )
449 phisum 
 |-  ( ( # ` B ) e. NN -> sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) = ( # ` B ) )
450 39 449 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) = ( # ` B ) )
451 448 450 breqtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) < ( # ` B ) )
452 80 451 eqbrtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) < ( # ` B ) )
453 170 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. NN0 )
454 453 nn0red 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. RR )
455 454 ltnrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> -. ( # ` B ) < ( # ` B ) )
456 452 455 pm2.21dd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )
457 456 ex 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } = (/) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) ) )
458 457 adantr 
 |-  ( ( ph /\ -. { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( { x e. B | ( ( od ` G ) ` x ) = D } = (/) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) ) )
459 36 458 mpd 
 |-  ( ( ph /\ -. { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )
460 33 459 pm2.61dan 
 |-  ( ph -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )