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 bilani 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) -> E. z e. B ( ( od ` G ) ` z ) = ( # ` B ) )
217 209 216 r19.29a 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) )
218 217 ex 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) )
219 218 necon4d 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } = (/) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } = (/) ) )
220 219 imp 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } = (/) )
221 220 fveq2d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) = ( # ` (/) ) )
222 hash0 
 |-  ( # ` (/) ) = 0
223 222 a1i 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` (/) ) = 0 )
224 221 223 eqtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) = 0 )
225 122 nngt0d 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> 0 < ( phi ` ( # ` B ) ) )
226 224 225 eqbrtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = ( # ` B ) } ) < ( phi ` ( # ` B ) ) )
227 eldif 
 |-  ( z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) <-> ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) )
228 227 bilani 
 |-  ( ( ph /\ z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) )
229 breq1 
 |-  ( a = z -> ( a || ( # ` B ) <-> z || ( # ` B ) ) )
230 229 elrab 
 |-  ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } <-> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
231 230 biimpi 
 |-  ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } -> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
232 231 adantr 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) )
233 velsn 
 |-  ( z e. { ( # ` B ) } <-> z = ( # ` B ) )
234 233 bicomi 
 |-  ( z = ( # ` B ) <-> z e. { ( # ` B ) } )
235 234 biimpi 
 |-  ( z = ( # ` B ) -> z e. { ( # ` B ) } )
236 235 necon3bi 
 |-  ( -. z e. { ( # ` B ) } -> z =/= ( # ` B ) )
237 236 adantl 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> z =/= ( # ` B ) )
238 232 237 jca 
 |-  ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) )
239 238 adantl 
 |-  ( ( ph /\ ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) ) -> ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) )
240 1zzd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> 1 e. ZZ )
241 4 adantr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> B e. Fin )
242 241 70 syl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. NN0 )
243 242 nn0zd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. ZZ )
244 243 240 zsubcld 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( ( # ` B ) - 1 ) e. ZZ )
245 elfzelz 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> z e. ZZ )
246 245 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> z e. ZZ )
247 246 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z e. ZZ )
248 247 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. ZZ )
249 elfzle1 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> 1 <_ z )
250 249 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> 1 <_ z )
251 250 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> 1 <_ z )
252 251 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> 1 <_ z )
253 elfzle2 
 |-  ( z e. ( 1 ... ( # ` B ) ) -> z <_ ( # ` B ) )
254 253 adantr 
 |-  ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) -> z <_ ( # ` B ) )
255 254 adantr 
 |-  ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z <_ ( # ` B ) )
256 255 adantl 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z <_ ( # ` B ) )
257 simprr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z =/= ( # ` B ) )
258 257 necomd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) =/= z )
259 256 258 jca 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z <_ ( # ` B ) /\ ( # ` B ) =/= z ) )
260 248 zred 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. RR )
261 242 nn0red 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( # ` B ) e. RR )
262 260 261 ltlend 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z < ( # ` B ) <-> ( z <_ ( # ` B ) /\ ( # ` B ) =/= z ) ) )
263 259 262 mpbird 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z < ( # ` B ) )
264 248 243 zltlem1d 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> ( z < ( # ` B ) <-> z <_ ( ( # ` B ) - 1 ) ) )
265 263 264 mpbid 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
266 240 244 248 252 265 elfzd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. ( 1 ... ( ( # ` B ) - 1 ) ) )
267 simprlr 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z || ( # ` B ) )
268 229 266 267 elrabd 
 |-  ( ( ph /\ ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
269 268 ex 
 |-  ( ph -> ( ( ( z e. ( 1 ... ( # ` B ) ) /\ z || ( # ` B ) ) /\ z =/= ( # ` B ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
270 269 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 ) } ) )
271 239 270 mpd 
 |-  ( ( ph /\ ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
272 271 ex 
 |-  ( ph -> ( ( z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } /\ -. z e. { ( # ` B ) } ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
273 272 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 ) } ) )
274 228 273 mpd 
 |-  ( ( ph /\ z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
275 274 ex 
 |-  ( ph -> ( z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) -> z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) )
276 275 ssrdv 
 |-  ( ph -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) C_ { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
277 1zzd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 e. ZZ )
278 170 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
279 278 adantr 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( # ` B ) e. ZZ )
280 elfzelz 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z e. ZZ )
281 280 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. ZZ )
282 elfzle1 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> 1 <_ z )
283 282 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 <_ z )
284 281 zred 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. RR )
285 279 zred 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( # ` B ) e. RR )
286 1red 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> 1 e. RR )
287 285 286 resubcld 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( ( # ` B ) - 1 ) e. RR )
288 elfzle2 
 |-  ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z <_ ( ( # ` B ) - 1 ) )
289 288 adantl 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
290 285 lem1d 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> ( ( # ` B ) - 1 ) <_ ( # ` B ) )
291 284 287 285 289 290 letrd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z <_ ( # ` B ) )
292 277 279 281 283 291 elfzd 
 |-  ( ( ph /\ z e. ( 1 ... ( ( # ` B ) - 1 ) ) ) -> z e. ( 1 ... ( # ` B ) ) )
293 292 ex 
 |-  ( ph -> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) -> z e. ( 1 ... ( # ` B ) ) ) )
294 293 ssrdv 
 |-  ( ph -> ( 1 ... ( ( # ` B ) - 1 ) ) C_ ( 1 ... ( # ` B ) ) )
295 rabss2 
 |-  ( ( 1 ... ( ( # ` B ) - 1 ) ) C_ ( 1 ... ( # ` B ) ) -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
296 294 295 syl 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
297 296 sseld 
 |-  ( ph -> ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) )
298 297 imp 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
299 170 ad2antrr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) e. NN0 )
300 299 nn0red 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) e. RR )
301 300 leidd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) <_ ( # ` B ) )
302 simpr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z = ( # ` B ) )
303 302 eqcomd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) = z )
304 229 elrab 
 |-  ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } <-> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) )
305 304 bilani 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) )
306 289 adantrr 
 |-  ( ( ph /\ ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) ) -> z <_ ( ( # ` B ) - 1 ) )
307 306 ex 
 |-  ( ph -> ( ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) -> z <_ ( ( # ` B ) - 1 ) ) )
308 307 adantr 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( z e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ z || ( # ` B ) ) -> z <_ ( ( # ` B ) - 1 ) ) )
309 305 308 mpd 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z <_ ( ( # ` B ) - 1 ) )
310 298 231 246 3syl 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. ZZ )
311 278 adantr 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` B ) e. ZZ )
312 310 311 zltlem1d 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( z < ( # ` B ) <-> z <_ ( ( # ` B ) - 1 ) ) )
313 309 312 mpbird 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z < ( # ` B ) )
314 313 adantr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z < ( # ` B ) )
315 303 314 eqbrtrd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( # ` B ) < ( # ` B ) )
316 300 300 ltnled 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> ( ( # ` B ) < ( # ` B ) <-> -. ( # ` B ) <_ ( # ` B ) ) )
317 315 316 mpbid 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> -. ( # ` B ) <_ ( # ` B ) )
318 301 317 pm2.21dd 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z = ( # ` B ) ) -> z =/= ( # ` B ) )
319 simpr 
 |-  ( ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ z =/= ( # ` B ) ) -> z =/= ( # ` B ) )
320 318 319 pm2.61dane 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z =/= ( # ` B ) )
321 298 320 eldifsnd 
 |-  ( ( ph /\ z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) )
322 321 ex 
 |-  ( ph -> ( z e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } -> z e. ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) ) )
323 322 ssrdv 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) )
324 276 323 eqssd 
 |-  ( ph -> ( { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } \ { ( # ` B ) } ) = { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
325 324 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 } ) )
326 fzfid 
 |-  ( ph -> ( 1 ... ( ( # ` B ) - 1 ) ) e. Fin )
327 ssrab2 
 |-  { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( 1 ... ( ( # ` B ) - 1 ) )
328 327 a1i 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } C_ ( 1 ... ( ( # ` B ) - 1 ) ) )
329 326 328 ssfid 
 |-  ( ph -> { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } e. Fin )
330 4 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> B e. Fin )
331 88 a1i 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
332 330 331 ssfid 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
333 332 91 syl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
334 333 nn0red 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. RR )
335 125 elrab 
 |-  ( k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } <-> ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) )
336 335 bilani 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) )
337 elfzelz 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> k e. ZZ )
338 elfzle1 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> 1 <_ k )
339 337 338 jca 
 |-  ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) -> ( k e. ZZ /\ 1 <_ k ) )
340 339 adantr 
 |-  ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> ( k e. ZZ /\ 1 <_ k ) )
341 340 adantl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
342 341 135 sylibr 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> k e. NN )
343 342 ex 
 |-  ( ph -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> k e. NN ) )
344 343 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> k e. NN ) )
345 336 344 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> k e. NN )
346 345 phicld 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. NN )
347 346 nnred 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. RR )
348 simpll 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ph )
349 335 bilanri 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } )
350 349 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 ) } )
351 348 350 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 ) } ) )
352 351 334 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 )
353 simpr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
354 351 353 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 } =/= (/) ) )
355 336 simprd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> k || ( # ` B ) )
356 355 adantr 
 |-  ( ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> k || ( # ` B ) )
357 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 } =/= (/) )
358 356 357 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 } =/= (/) ) )
359 breq1 
 |-  ( m = k -> ( m || ( # ` B ) <-> k || ( # ` B ) ) )
360 eqeq2 
 |-  ( m = k -> ( ( ( od ` G ) ` x ) = m <-> ( ( od ` G ) ` x ) = k ) )
361 360 rabbidv 
 |-  ( m = k -> { x e. B | ( ( od ` G ) ` x ) = m } = { x e. B | ( ( od ` G ) ` x ) = k } )
362 361 neeq1d 
 |-  ( m = k -> ( { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
363 359 362 anbi12d 
 |-  ( m = k -> ( ( m || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = m } =/= (/) ) <-> ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) ) )
364 361 fveq2d 
 |-  ( m = k -> ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
365 fveq2 
 |-  ( m = k -> ( phi ` m ) = ( phi ` k ) )
366 364 365 eqeq12d 
 |-  ( m = k -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = m } ) = ( phi ` m ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
367 363 366 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 ) ) ) )
368 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 ) ) )
369 367 368 345 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 ) ) )
370 369 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 ) ) )
371 358 370 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 ) )
372 354 371 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 ) )
373 352 372 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 ) )
374 id 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
375 374 necon1bi 
 |-  ( -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) -> { x e. B | ( ( od ` G ) ` x ) = k } = (/) )
376 375 adantl 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> { x e. B | ( ( od ` G ) ` x ) = k } = (/) )
377 376 fveq2d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` (/) ) )
378 222 a1i 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` (/) ) = 0 )
379 377 378 eqtrd 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = 0 )
380 342 adantr 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> k e. NN )
381 380 phicld 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( phi ` k ) e. NN )
382 381 nnnn0d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( phi ` k ) e. NN0 )
383 382 nn0ge0d 
 |-  ( ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) /\ -. { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> 0 <_ ( phi ` k ) )
384 379 383 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 ) )
385 373 384 pm2.61dan 
 |-  ( ( ph /\ ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
386 385 ex 
 |-  ( ph -> ( ( k e. ( 1 ... ( ( # ` B ) - 1 ) ) /\ k || ( # ` B ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) ) )
387 386 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 ) ) )
388 336 387 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( ( # ` B ) - 1 ) ) | a || ( # ` B ) } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) <_ ( phi ` k ) )
389 329 334 347 388 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 ) )
390 324 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 ) )
391 390 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 ) )
392 389 391 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 ) )
393 325 392 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 ) )
394 393 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 ) )
395 113 121 123 140 226 394 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 ) ) )
396 nfcv 
 |-  F/_ k ( phi ` ( # ` B ) )
397 simpll 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ph )
398 126 bilani 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) )
399 397 398 jca 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) )
400 131 adantl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( # ` B ) ) /\ k || ( # ` B ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
401 400 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 ) )
402 401 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 )
403 402 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 ) )
404 399 403 mpd 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> k e. NN )
405 404 phicld 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. NN )
406 405 nncnd 
 |-  ( ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) /\ k e. { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } ) -> ( phi ` k ) e. CC )
407 fveq2 
 |-  ( k = ( # ` B ) -> ( phi ` k ) = ( phi ` ( # ` B ) ) )
408 81 396 86 406 103 407 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 ) ) )
409 395 408 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 ) )
410 107 409 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 ) )
411 elfzelz 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> a e. ZZ )
412 elfzle1 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> 1 <_ a )
413 411 412 jca 
 |-  ( a e. ( 1 ... ( # ` B ) ) -> ( a e. ZZ /\ 1 <_ a ) )
414 413 adantr 
 |-  ( ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) -> ( a e. ZZ /\ 1 <_ a ) )
415 414 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) ) -> ( a e. ZZ /\ 1 <_ a ) )
416 elnnz1 
 |-  ( a e. NN <-> ( a e. ZZ /\ 1 <_ a ) )
417 415 416 sylibr 
 |-  ( ( ph /\ ( a e. ( 1 ... ( # ` B ) ) /\ a || ( # ` B ) ) ) -> a e. NN )
418 417 rabss3d 
 |-  ( ph -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } C_ { a e. NN | a || ( # ` B ) } )
419 simpl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ph )
420 simprl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a e. NN )
421 419 420 jca 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ( ph /\ a e. NN ) )
422 simprr 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a || ( # ` B ) )
423 421 422 jca 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) )
424 1zzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> 1 e. ZZ )
425 278 adantr 
 |-  ( ( ph /\ a e. NN ) -> ( # ` B ) e. ZZ )
426 425 adantr 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> ( # ` B ) e. ZZ )
427 420 anassrs 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. NN )
428 427 nnzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. ZZ )
429 427 nnge1d 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> 1 <_ a )
430 nnz 
 |-  ( a e. NN -> a e. ZZ )
431 430 adantl 
 |-  ( ( ph /\ a e. NN ) -> a e. ZZ )
432 1 3 4 hashfingrpnn 
 |-  ( ph -> ( # ` B ) e. NN )
433 432 adantr 
 |-  ( ( ph /\ a e. NN ) -> ( # ` B ) e. NN )
434 dvdsle 
 |-  ( ( a e. ZZ /\ ( # ` B ) e. NN ) -> ( a || ( # ` B ) -> a <_ ( # ` B ) ) )
435 431 433 434 syl2anc 
 |-  ( ( ph /\ a e. NN ) -> ( a || ( # ` B ) -> a <_ ( # ` B ) ) )
436 435 imp 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a <_ ( # ` B ) )
437 424 426 428 429 436 elfzd 
 |-  ( ( ( ph /\ a e. NN ) /\ a || ( # ` B ) ) -> a e. ( 1 ... ( # ` B ) ) )
438 423 437 syl 
 |-  ( ( ph /\ ( a e. NN /\ a || ( # ` B ) ) ) -> a e. ( 1 ... ( # ` B ) ) )
439 438 rabss3d 
 |-  ( ph -> { a e. NN | a || ( # ` B ) } C_ { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } )
440 418 439 eqssd 
 |-  ( ph -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } = { a e. NN | a || ( # ` B ) } )
441 440 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> { a e. ( 1 ... ( # ` B ) ) | a || ( # ` B ) } = { a e. NN | a || ( # ` B ) } )
442 441 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 ) )
443 410 442 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 ) )
444 phisum 
 |-  ( ( # ` B ) e. NN -> sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) = ( # ` B ) )
445 39 444 syl 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> sum_ k e. { a e. NN | a || ( # ` B ) } ( phi ` k ) = ( # ` B ) )
446 443 445 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 ) )
447 80 446 eqbrtrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) < ( # ` B ) )
448 170 adantr 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. NN0 )
449 448 nn0red 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` B ) e. RR )
450 449 ltnrd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> -. ( # ` B ) < ( # ` B ) )
451 447 450 pm2.21dd 
 |-  ( ( ph /\ { x e. B | ( ( od ` G ) ` x ) = D } = (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )
452 451 ex 
 |-  ( ph -> ( { x e. B | ( ( od ` G ) ` x ) = D } = (/) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) ) )
453 452 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 ) ) )
454 36 453 mpd 
 |-  ( ( ph /\ -. { x e. B | ( ( od ` G ) ` x ) = D } =/= (/) ) -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )
455 33 454 pm2.61dan 
 |-  ( ph -> ( # ` { y e. B | ( ( od ` G ) ` y ) = D } ) = ( phi ` D ) )