Proof of Theorem tz7.44-3
Step | Hyp | Ref
| Expression |
1 | | fveq2 5863 |
. . . . . 6
           |
2 | | reseq2 5099 |
. . . . . . 7
       |
3 | 2 | fveq2d 5867 |
. . . . . 6
               |
4 | 1, 3 | eqeq12d 2465 |
. . . . 5
           
             |
5 | | tz7.44.2 |
. . . . 5
        
    |
6 | 4, 5 | vtoclga 3112 |
. . . 4
        
    |
7 | 6 | adantr 467 |
. . 3
          
    |
8 | 2 | eleq1d 2512 |
. . . . . . 7
   
     |
9 | | tz7.44.3 |
. . . . . . 7
     |
10 | 8, 9 | vtoclga 3112 |
. . . . . 6
     |
11 | 10 | adantr 467 |
. . . . 5
       |
12 | | simpr 463 |
. . . . . . . . 9
     |
13 | | nlim0 5480 |
. . . . . . . . . . 11
 |
14 | | dmres 5124 |
. . . . . . . . . . . . . 14
     |
15 | | tz7.44.5 |
. . . . . . . . . . . . . . . . . 18
 |
16 | | ordelss 5438 |
. . . . . . . . . . . . . . . . . 18
     |
17 | 15, 16 | mpan 675 |
. . . . . . . . . . . . . . . . 17
   |
18 | 17 | adantr 467 |
. . . . . . . . . . . . . . . 16
     |
19 | | tz7.44.4 |
. . . . . . . . . . . . . . . . 17
 |
20 | | fndm 5673 |
. . . . . . . . . . . . . . . . 17
   |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
22 | 18, 21 | syl6sseqr 3478 |
. . . . . . . . . . . . . . 15
     |
23 | | df-ss 3417 |
. . . . . . . . . . . . . . 15

    |
24 | 22, 23 | sylib 200 |
. . . . . . . . . . . . . 14
   
   |
25 | 14, 24 | syl5eq 2496 |
. . . . . . . . . . . . 13
   
   |
26 | | dmeq 5034 |
. . . . . . . . . . . . . 14
 

    |
27 | | dm0 5047 |
. . . . . . . . . . . . . 14
 |
28 | 26, 27 | syl6eq 2500 |
. . . . . . . . . . . . 13
 

    |
29 | 25, 28 | sylan9req 2505 |
. . . . . . . . . . . 12
    
    |
30 | | limeq 5434 |
. . . . . . . . . . . 12

    |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
    
      |
32 | 13, 31 | mtbiri 305 |
. . . . . . . . . 10
    
    |
33 | 32 | ex 436 |
. . . . . . . . 9
     
   |
34 | 12, 33 | mt2d 121 |
. . . . . . . 8
   
   |
35 | 34 | iffalsed 3891 |
. . . . . . 7
          
                                               |
36 | | limeq 5434 |
. . . . . . . . . 10
     
   |
37 | 25, 36 | syl 17 |
. . . . . . . . 9
     
   |
38 | 12, 37 | mpbird 236 |
. . . . . . . 8
       |
39 | 38 | iftrued 3888 |
. . . . . . 7
    
                     
    |
40 | 35, 39 | eqtrd 2484 |
. . . . . 6
          
                           |
41 | | rnexg 6722 |
. . . . . . 7
 

    |
42 | | uniexg 6585 |
. . . . . . 7
    
   |
43 | 11, 41, 42 | 3syl 18 |
. . . . . 6
    
   |
44 | 40, 43 | eqeltrd 2528 |
. . . . 5
          
                        |
45 | | eqeq1 2454 |
. . . . . . 7
   
     |
46 | | dmeq 5034 |
. . . . . . . . 9
  
    |
47 | | limeq 5434 |
. . . . . . . . 9
   
     |
48 | 46, 47 | syl 17 |
. . . . . . . 8
   
     |
49 | | rneq 5059 |
. . . . . . . . 9
  
    |
50 | 49 | unieqd 4207 |
. . . . . . . 8
   
     |
51 | | fveq1 5862 |
. . . . . . . . . 10
         
       |
52 | 46 | unieqd 4207 |
. . . . . . . . . . 11
   
     |
53 | 52 | fveq2d 5867 |
. . . . . . . . . 10
           
         |
54 | 51, 53 | eqtrd 2484 |
. . . . . . . . 9
         
         |
55 | 54 | fveq2d 5867 |
. . . . . . . 8
                           |
56 | 48, 50, 55 | ifbieq12d 3907 |
. . . . . . 7
    
               
                      |
57 | 45, 56 | ifbieq2d 3905 |
. . . . . 6
    
    
                        
       
            |
58 | | tz7.44.1 |
. . . . . 6
      
                |
59 | 57, 58 | fvmptg 5944 |
. . . . 5
           
                               
        
       
            |
60 | 11, 44, 59 | syl2anc 666 |
. . . 4
                
                        |
61 | 60, 40 | eqtrd 2484 |
. . 3
         
    |
62 | 7, 61 | eqtrd 2484 |
. 2
            |
63 | | df-ima 4846 |
. . 3
       |
64 | 63 | unieqi 4206 |
. 2
     
   |
65 | 62, 64 | syl6eqr 2502 |
1
              |