Proof of Theorem tz7.44-2
Step | Hyp | Ref
| Expression |
1 | | fveq2 5865 |
. . . 4
       
   |
2 | | reseq2 5100 |
. . . . 5
       |
3 | 2 | fveq2d 5869 |
. . . 4
          
    |
4 | 1, 3 | eqeq12d 2466 |
. . 3
           
             |
5 | | tz7.44.2 |
. . 3
        
    |
6 | 4, 5 | vtoclga 3113 |
. 2
             |
7 | 2 | eleq1d 2513 |
. . . 4
    
    |
8 | | tz7.44.3 |
. . . 4
     |
9 | 7, 8 | vtoclga 3113 |
. . 3
     |
10 | | noel 3735 |
. . . . . . 7
 |
11 | | dmeq 5035 |
. . . . . . . . 9
 

    |
12 | | dm0 5048 |
. . . . . . . . 9
 |
13 | 11, 12 | syl6eq 2501 |
. . . . . . . 8
 

    |
14 | | tz7.44.5 |
. . . . . . . . . . . . 13
 |
15 | | ordsson 6616 |
. . . . . . . . . . . . 13

  |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . 12
 |
17 | | ordtr 5437 |
. . . . . . . . . . . . . 14

  |
18 | 14, 17 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
19 | | trsuc 5507 |
. . . . . . . . . . . . 13
  
  |
20 | 18, 19 | mpan 676 |
. . . . . . . . . . . 12

  |
21 | 16, 20 | sseldi 3430 |
. . . . . . . . . . 11

  |
22 | | sucidg 5501 |
. . . . . . . . . . 11
   |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10

  |
24 | | dmres 5125 |
. . . . . . . . . . 11
     |
25 | | ordelss 5439 |
. . . . . . . . . . . . . 14
  
  |
26 | 14, 25 | mpan 676 |
. . . . . . . . . . . . 13

  |
27 | | tz7.44.4 |
. . . . . . . . . . . . . 14
 |
28 | | fndm 5675 |
. . . . . . . . . . . . . 14
   |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
30 | 26, 29 | syl6sseqr 3479 |
. . . . . . . . . . . 12

  |
31 | | df-ss 3418 |
. . . . . . . . . . . 12


   |
32 | 30, 31 | sylib 200 |
. . . . . . . . . . 11
 
   |
33 | 24, 32 | syl5eq 2497 |
. . . . . . . . . 10
     |
34 | 23, 33 | eleqtrrd 2532 |
. . . . . . . . 9

    |
35 | | eleq2 2518 |
. . . . . . . . 9
   
 
   |
36 | 34, 35 | syl5ibcom 224 |
. . . . . . . 8
 
     |
37 | 13, 36 | syl5 33 |
. . . . . . 7
       |
38 | 10, 37 | mtoi 182 |
. . . . . 6
     |
39 | 38 | iffalsed 3892 |
. . . . 5
        
   
                                           |
40 | | nlimsucg 6669 |
. . . . . . . 8
   |
41 | 21, 40 | syl 17 |
. . . . . . 7

  |
42 | | limeq 5435 |
. . . . . . . 8
         |
43 | 33, 42 | syl 17 |
. . . . . . 7
 
 
   |
44 | 41, 43 | mtbird 303 |
. . . . . 6

    |
45 | 44 | iffalsed 3892 |
. . . . 5
                                       |
46 | 33 | unieqd 4208 |
. . . . . . . . 9
       |
47 | | eloni 5433 |
. . . . . . . . . . 11
   |
48 | | ordunisuc 6659 |
. . . . . . . . . . 11

   |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
    |
50 | 21, 49 | syl 17 |
. . . . . . . . 9
    |
51 | 46, 50 | eqtrd 2485 |
. . . . . . . 8
      |
52 | 51 | fveq2d 5869 |
. . . . . . 7
                  |
53 | | fvres 5879 |
. . . . . . . 8
             |
54 | 23, 53 | syl 17 |
. . . . . . 7
             |
55 | 52, 54 | eqtrd 2485 |
. . . . . 6
                |
56 | 55 | fveq2d 5869 |
. . . . 5
                        |
57 | 39, 45, 56 | 3eqtrd 2489 |
. . . 4
        
   
                            |
58 | | fvex 5875 |
. . . 4
         |
59 | 57, 58 | syl6eqel 2537 |
. . 3
        
   
                    |
60 | | eqeq1 2455 |
. . . . 5
   
     |
61 | | dmeq 5035 |
. . . . . . 7
  
    |
62 | | limeq 5435 |
. . . . . . 7
   
     |
63 | 61, 62 | syl 17 |
. . . . . 6
   
     |
64 | | rneq 5060 |
. . . . . . 7
  
    |
65 | 64 | unieqd 4208 |
. . . . . 6
   
     |
66 | | fveq1 5864 |
. . . . . . . 8
         
       |
67 | 61 | unieqd 4208 |
. . . . . . . . 9
   
     |
68 | 67 | fveq2d 5869 |
. . . . . . . 8
           
         |
69 | 66, 68 | eqtrd 2485 |
. . . . . . 7
         
         |
70 | 69 | fveq2d 5869 |
. . . . . 6
                           |
71 | 63, 65, 70 | ifbieq12d 3908 |
. . . . 5
    
               
   
                  |
72 | 60, 71 | ifbieq2d 3906 |
. . . 4
    
    
                     
   
                   |
73 | | tz7.44.1 |
. . . 4
      
                |
74 | 72, 73 | fvmptg 5946 |
. . 3
           
   
                                 
   
                   |
75 | 9, 59, 74 | syl2anc 667 |
. 2
               
   
                   |
76 | 6, 75, 57 | 3eqtrd 2489 |
1
               |