Step | Hyp | Ref
| Expression |
1 | | simpl1 1011 |
. . . . 5
      RegUSGrph
FriendGrph  
       RegUSGrph   |
2 | | simpr3 1016 |
. . . . 5
      RegUSGrph
FriendGrph  
   
    |
3 | | simpr1 1014 |
. . . . 5
      RegUSGrph
FriendGrph  
   
  |
4 | | numclwwlk.c |
. . . . . 6
   ClWWalksN       |
5 | | numclwwlk.f |
. . . . . 6
 

           |
6 | 4, 5 | numclwwlk5lem 25839 |
. . . . 5
     RegUSGrph
 
             |
7 | 1, 2, 3, 6 | syl3anc 1268 |
. . . 4
      RegUSGrph
FriendGrph  
                |
8 | 7 | a1i 11 |
. . 3
       RegUSGrph FriendGrph
 
   
             |
9 | | eleq1 2517 |
. . . . 5
 
   |
10 | | breq1 4405 |
. . . . 5
   

    |
11 | 9, 10 | 3anbi23d 1342 |
. . . 4
  
   
      |
12 | 11 | anbi2d 710 |
. . 3
       RegUSGrph FriendGrph
 
       
 RegUSGrph
FriendGrph  
       |
13 | | oveq2 6298 |
. . . . . 6
           |
14 | 13 | fveq2d 5869 |
. . . . 5
                   |
15 | | id 22 |
. . . . 5
   |
16 | 14, 15 | oveq12d 6308 |
. . . 4
                       |
17 | 16 | eqeq1d 2453 |
. . 3
                         |
18 | 8, 12, 17 | 3imtr4d 272 |
. 2
       RegUSGrph FriendGrph
 
   
             |
19 | | 3simpa 1005 |
. . . . . . . 8
     RegUSGrph
FriendGrph      RegUSGrph
FriendGrph    |
20 | 19 | adantr 467 |
. . . . . . 7
      RegUSGrph
FriendGrph  
        RegUSGrph
FriendGrph    |
21 | 20 | adantl 468 |
. . . . . 6
       RegUSGrph FriendGrph
 
         RegUSGrph
FriendGrph    |
22 | | simprl3 1055 |
. . . . . 6
       RegUSGrph FriendGrph
 
       |
23 | | simprr1 1056 |
. . . . . 6
       RegUSGrph FriendGrph
 
       |
24 | | prmn2uzge3 14644 |
. . . . . . . . . 10
         |
25 | 24 | ex 436 |
. . . . . . . . 9

        |
26 | 25 | 3ad2ant2 1030 |
. . . . . . . 8
 
           |
27 | 26 | adantl 468 |
. . . . . . 7
      RegUSGrph
FriendGrph  
            |
28 | 27 | impcom 432 |
. . . . . 6
       RegUSGrph FriendGrph
 
           |
29 | | fveq1 5864 |
. . . . . . . . . . . 12
           |
30 | 29 | eqeq1d 2453 |
. . . . . . . . . . 11
     
       |
31 | | fveq1 5864 |
. . . . . . . . . . . 12
          
    |
32 | 31, 29 | eqeq12d 2466 |
. . . . . . . . . . 11
           
             |
33 | 30, 32 | anbi12d 717 |
. . . . . . . . . 10
          
                          |
34 | 33 | cbvrabv 3044 |
. . . . . . . . 9
                                             |
35 | 34 | a1i 11 |
. . . . . . . 8
 
     
                     
                       |
36 | 35 | mpt2eq3ia 6356 |
. . . . . . 7
                                                           |
37 | | fveq2 5865 |
. . . . . . . . . . . 12
 lastS   lastS     |
38 | 37 | neeq1d 2683 |
. . . . . . . . . . 11
  lastS  
lastS      |
39 | 30, 38 | anbi12d 717 |
. . . . . . . . . 10
       lastS         lastS       |
40 | 39 | cbvrabv 3044 |
. . . . . . . . 9
   WWalksN          lastS        WWalksN          lastS      |
41 | 40 | a1i 11 |
. . . . . . . 8
 
 
  WWalksN
         lastS     
  WWalksN
         lastS       |
42 | 41 | mpt2eq3ia 6356 |
. . . . . . 7
     WWalksN          lastS       
   WWalksN          lastS       |
43 | | eqeq2 2462 |
. . . . . . . . . 10
     
       |
44 | 43 | anbi1d 711 |
. . . . . . . . 9
          
                          |
45 | 44 | rabbidv 3036 |
. . . . . . . 8
                                               |
46 | | fveq2 5865 |
. . . . . . . . . 10
           |
47 | | oveq1 6297 |
. . . . . . . . . . . . 13
       |
48 | 47 | fveq2d 5869 |
. . . . . . . . . . . 12
          
    |
49 | 48 | neeq1d 2683 |
. . . . . . . . . . 11
           
             |
50 | 49 | anbi2d 710 |
. . . . . . . . . 10
          
                          |
51 | 46, 50 | rabeqbidv 3040 |
. . . . . . . . 9
                                               |
52 | 31, 29 | neeq12d 2685 |
. . . . . . . . . . 11
           
             |
53 | 30, 52 | anbi12d 717 |
. . . . . . . . . 10
          
                          |
54 | 53 | cbvrabv 3044 |
. . . . . . . . 9
                                             |
55 | 51, 54 | syl6eq 2501 |
. . . . . . . 8
                                               |
56 | 45, 55 | cbvmpt2v 6371 |
. . . . . . 7
                                                   |
57 | 4, 5, 36, 42, 56 | numclwwlk3 25837 |
. . . . . 6
      RegUSGrph
FriendGrph  
                                      |
58 | 21, 22, 23, 28, 57 | syl13anc 1270 |
. . . . 5
       RegUSGrph FriendGrph
 
                                     |
59 | 58 | oveq1d 6305 |
. . . 4
       RegUSGrph FriendGrph
 
                                         |
60 | | rusgraprop 25657 |
. . . . . . . . . . . . 13
  
 RegUSGrph  USGrph

  VDeg
       |
61 | | nn0z 10960 |
. . . . . . . . . . . . . 14

  |
62 | 61 | 3ad2ant2 1030 |
. . . . . . . . . . . . 13
  USGrph

  VDeg        |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . 12
  
 RegUSGrph   |
64 | 63 | zred 11040 |
. . . . . . . . . . 11
  
 RegUSGrph   |
65 | | peano2rem 9941 |
. . . . . . . . . . 11
 
   |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
  
 RegUSGrph     |
67 | 66 | 3ad2ant1 1029 |
. . . . . . . . 9
     RegUSGrph
FriendGrph  
   |
68 | 67 | adantr 467 |
. . . . . . . 8
      RegUSGrph
FriendGrph  
        |
69 | | rusisusgra 25659 |
. . . . . . . . . . . . . . 15
  
 RegUSGrph USGrph   |
70 | | usgrav 25065 |
. . . . . . . . . . . . . . . 16
 USGrph 
   |
71 | 70 | simprd 465 |
. . . . . . . . . . . . . . 15
 USGrph   |
72 | 69, 71 | syl 17 |
. . . . . . . . . . . . . 14
  
 RegUSGrph   |
73 | 72 | anim1i 572 |
. . . . . . . . . . . . 13
     RegUSGrph
 
   |
74 | 73 | ancomd 453 |
. . . . . . . . . . . 12
     RegUSGrph
 
   |
75 | 74 | 3adant2 1027 |
. . . . . . . . . . 11
     RegUSGrph
FriendGrph  
   |
76 | | prmm2nn0 14645 |
. . . . . . . . . . . . 13

    |
77 | 76 | anim2i 573 |
. . . . . . . . . . . 12
 
       |
78 | 77 | 3adant3 1028 |
. . . . . . . . . . 11
 
   

    |
79 | 4, 5 | numclwwlkffin 25810 |
. . . . . . . . . . 11
        
        |
80 | 75, 78, 79 | syl2an 480 |
. . . . . . . . . 10
      RegUSGrph
FriendGrph  
            |
81 | | hashcl 12538 |
. . . . . . . . . 10
                   |
82 | 80, 81 | syl 17 |
. . . . . . . . 9
      RegUSGrph
FriendGrph  
                |
83 | 82 | nn0red 10926 |
. . . . . . . 8
      RegUSGrph
FriendGrph  
                |
84 | 68, 83 | remulcld 9671 |
. . . . . . 7
      RegUSGrph
FriendGrph  
                    |
85 | 64 | 3ad2ant1 1029 |
. . . . . . . 8
     RegUSGrph
FriendGrph    |
86 | 76 | 3ad2ant2 1030 |
. . . . . . . 8
 
   
   |
87 | | reexpcl 12289 |
. . . . . . . 8
  
     
    |
88 | 85, 86, 87 | syl2an 480 |
. . . . . . 7
      RegUSGrph
FriendGrph  
       
    |
89 | | prmnn 14625 |
. . . . . . . . . 10

  |
90 | 89 | nnrpd 11339 |
. . . . . . . . 9

  |
91 | 90 | 3ad2ant2 1030 |
. . . . . . . 8
 
     |
92 | 91 | adantl 468 |
. . . . . . 7
      RegUSGrph
FriendGrph  
   
  |
93 | 84, 88, 92 | 3jca 1188 |
. . . . . 6
      RegUSGrph
FriendGrph  
                            |
94 | 93 | adantl 468 |
. . . . 5
       RegUSGrph FriendGrph
 
                             |
95 | | modaddabs 12135 |
. . . . . 6
                      
                                                      |
96 | 95 | eqcomd 2457 |
. . . . 5
                      
                                                      |
97 | 94, 96 | syl 17 |
. . . 4
       RegUSGrph FriendGrph
 
                                                   
       |
98 | 89 | 3ad2ant2 1030 |
. . . . . . . . . . 11
 
     |
99 | 98 | adantl 468 |
. . . . . . . . . 10
      RegUSGrph
FriendGrph  
   
  |
100 | | peano2zm 10980 |
. . . . . . . . . . . . 13
 
   |
101 | 63, 100 | syl 17 |
. . . . . . . . . . . 12
  
 RegUSGrph     |
102 | 101 | 3ad2ant1 1029 |
. . . . . . . . . . 11
     RegUSGrph
FriendGrph  
   |
103 | 102 | adantr 467 |
. . . . . . . . . 10
      RegUSGrph
FriendGrph  
        |
104 | 82 | nn0zd 11038 |
. . . . . . . . . 10
      RegUSGrph
FriendGrph  
                |
105 | 99, 103, 104 | 3jca 1188 |
. . . . . . . . 9
      RegUSGrph
FriendGrph  
                    |
106 | | simpr3 1016 |
. . . . . . . . 9
      RegUSGrph
FriendGrph  
        |
107 | | mulmoddvds 14363 |
. . . . . . . . 9
  
             
                    |
108 | 105, 106,
107 | sylc 62 |
. . . . . . . 8
      RegUSGrph
FriendGrph  
                      |
109 | 63 | 3ad2ant1 1029 |
. . . . . . . . . 10
     RegUSGrph
FriendGrph    |
110 | | simp2 1009 |
. . . . . . . . . 10
 
     |
111 | 109, 110 | anim12ci 571 |
. . . . . . . . 9
      RegUSGrph
FriendGrph  
        |
112 | | powm2modprm 14754 |
. . . . . . . . 9
          
      |
113 | 111, 106,
112 | sylc 62 |
. . . . . . . 8
      RegUSGrph
FriendGrph  
              |
114 | 108, 113 | oveq12d 6308 |
. . . . . . 7
      RegUSGrph
FriendGrph  
                                  |
115 | 114 | oveq1d 6305 |
. . . . . 6
      RegUSGrph
FriendGrph  
                          
           |
116 | | 0p1e1 10721 |
. . . . . . . . . 10
   |
117 | 116 | oveq1i 6300 |
. . . . . . . . 9
       |
118 | 89 | nnred 10624 |
. . . . . . . . . 10

  |
119 | | prmgt1 14643 |
. . . . . . . . . 10

  |
120 | | 1mod 12129 |
. . . . . . . . . 10
       |
121 | 118, 119,
120 | syl2anc 667 |
. . . . . . . . 9

    |
122 | 117, 121 | syl5eq 2497 |
. . . . . . . 8

      |
123 | 122 | 3ad2ant2 1030 |
. . . . . . 7
 
         |
124 | 123 | adantl 468 |
. . . . . 6
      RegUSGrph
FriendGrph  
          |
125 | 115, 124 | eqtrd 2485 |
. . . . 5
      RegUSGrph
FriendGrph  
                          
       |
126 | 125 | adantl 468 |
. . . 4
       RegUSGrph FriendGrph
 
                                   |
127 | 59, 97, 126 | 3eqtrd 2489 |
. . 3
       RegUSGrph FriendGrph
 
                 |
128 | 127 | ex 436 |
. 2
       RegUSGrph FriendGrph
 
   
             |
129 | 18, 128 | pm2.61ine 2707 |
1
      RegUSGrph
FriendGrph  
                |