Proof of Theorem 2ffzoeq
Step | Hyp | Ref
| Expression |
1 | | eqeq1 2454 |
. . . . . . . . . . . 12
 
   |
2 | 1 | anbi1d 710 |
. . . . . . . . . . 11
      ..^        ..^       |
3 | | f0bi 5764 |
. . . . . . . . . . . . 13
    
  |
4 | | ffn 5726 |
. . . . . . . . . . . . . 14
       |
5 | | ffn 5726 |
. . . . . . . . . . . . . . 15
    ..^    ..^   |
6 | | fndmu 5675 |
. . . . . . . . . . . . . . . . 17
   ..^   ..^   |
7 | | 0z 10945 |
. . . . . . . . . . . . . . . . . . 19
 |
8 | | nn0z 10957 |
. . . . . . . . . . . . . . . . . . . 20

  |
9 | 8 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 

  |
10 | | fzon 11936 |
. . . . . . . . . . . . . . . . . . 19
 
   ..^    |
11 | 7, 9, 10 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18
 
   ..^    |
12 | | nn0ge0 10892 |
. . . . . . . . . . . . . . . . . . . 20

  |
13 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
14 | | nn0re 10875 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
15 | 13, 14 | letri3d 9774 |
. . . . . . . . . . . . . . . . . . . . 21


     |
16 | 15 | biimprd 227 |
. . . . . . . . . . . . . . . . . . . 20

 
    |
17 | 12, 16 | mpand 680 |
. . . . . . . . . . . . . . . . . . 19

    |
18 | 17 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
     |
19 | 11, 18 | sylbird 239 |
. . . . . . . . . . . . . . . . 17
 
   ..^    |
20 | 6, 19 | syl5com 31 |
. . . . . . . . . . . . . . . 16
   ..^        |
21 | 20 | ex 436 |
. . . . . . . . . . . . . . 15
  ..^

 
     |
22 | 5, 21 | syl 17 |
. . . . . . . . . . . . . 14
    ..^   
       |
23 | 4, 22 | syl5com 31 |
. . . . . . . . . . . . 13
         ..^          |
24 | 3, 23 | sylbir 217 |
. . . . . . . . . . . 12

    ..^          |
25 | 24 | imp 431 |
. . . . . . . . . . 11
     ..^     

   |
26 | 2, 25 | syl6bi 232 |
. . . . . . . . . 10
      ..^     
     |
27 | 26 | com3l 84 |
. . . . . . . . 9
     ..^     


    |
28 | 27 | a1i 11 |
. . . . . . . 8
      ..^     
 
     |
29 | | oveq2 6296 |
. . . . . . . . . . . 12
  ..^  ..^   |
30 | | fzo0 11939 |
. . . . . . . . . . . 12
 ..^  |
31 | 29, 30 | syl6eq 2500 |
. . . . . . . . . . 11
  ..^   |
32 | 31 | feq2d 5713 |
. . . . . . . . . 10
     ..^  
       |
33 | | f0bi 5764 |
. . . . . . . . . 10
    
  |
34 | 32, 33 | syl6bb 265 |
. . . . . . . . 9
     ..^  
   |
35 | 34 | anbi1d 710 |
. . . . . . . 8
      ..^      ..^        ..^       |
36 | | eqeq1 2454 |
. . . . . . . . . 10
 
   |
37 | 36 | imbi2d 318 |
. . . . . . . . 9
    
    |
38 | 37 | imbi2d 318 |
. . . . . . . 8
   


 
 
 
     |
39 | 28, 35, 38 | 3imtr4d 272 |
. . . . . . 7
      ..^      ..^   
 
 
     |
40 | 39 | com3l 84 |
. . . . . 6
     ..^      ..^     

 
     |
41 | 40 | impcom 432 |
. . . . 5
        ..^      ..^     

    |
42 | 41 | impcom 432 |
. . . 4
   
     ..^      ..^     

   |
43 | 29 | feq2d 5713 |
. . . . . . . . . . . 12
     ..^  
   ..^      |
44 | 30 | feq2i 5719 |
. . . . . . . . . . . . 13
    ..^  
      |
45 | 44, 33 | bitri 253 |
. . . . . . . . . . . 12
    ..^  
  |
46 | 43, 45 | syl6bb 265 |
. . . . . . . . . . 11
     ..^  
   |
47 | 46 | adantr 467 |
. . . . . . . . . 10
       ..^  
   |
48 | | eqeq1 2454 |
. . . . . . . . . . . 12
 
   |
49 | 48 | biimpac 489 |
. . . . . . . . . . 11
     |
50 | | oveq2 6296 |
. . . . . . . . . . . . 13
  ..^  ..^   |
51 | 50 | feq2d 5713 |
. . . . . . . . . . . 12
     ..^  
   ..^      |
52 | 30 | feq2i 5719 |
. . . . . . . . . . . . 13
    ..^  
      |
53 | 52, 3 | bitri 253 |
. . . . . . . . . . . 12
    ..^  
  |
54 | 51, 53 | syl6bb 265 |
. . . . . . . . . . 11
     ..^  
   |
55 | 49, 54 | syl 17 |
. . . . . . . . . 10
       ..^  
   |
56 | 47, 55 | anbi12d 716 |
. . . . . . . . 9
        ..^      ..^   
     |
57 | | eqtr3 2471 |
. . . . . . . . 9
     |
58 | 56, 57 | syl6bi 232 |
. . . . . . . 8
        ..^      ..^   
   |
59 | 58 | com12 32 |
. . . . . . 7
     ..^      ..^          |
60 | 59 | expd 438 |
. . . . . 6
     ..^      ..^     
    |
61 | 60 | adantl 468 |
. . . . 5
        ..^      ..^     

    |
62 | 61 | impcom 432 |
. . . 4
   
     ..^      ..^     

   |
63 | 42, 62 | impbid 194 |
. . 3
   
     ..^      ..^     

   |
64 | | ral0 3873 |
. . . . . 6
          |
65 | 31 | raleqdv 2992 |
. . . . . 6
  
 ..^         
            |
66 | 64, 65 | mpbiri 237 |
. . . . 5
   ..^            |
67 | 66 | biantrud 510 |
. . . 4
 

  ..^              |
68 | 67 | adantr 467 |
. . 3
   
     ..^      ..^     

   ..^              |
69 | 63, 68 | bitrd 257 |
. 2
   
     ..^      ..^     

   ..^              |
70 | | ffn 5726 |
. . . . . . 7
    ..^    ..^   |
71 | 70, 5 | anim12i 569 |
. . . . . 6
     ..^      ..^      ..^
 ..^    |
72 | 71 | adantl 468 |
. . . . 5
        ..^      ..^     
 ..^  ..^    |
73 | 72 | adantl 468 |
. . . 4
   
     ..^      ..^     
  ..^  ..^    |
74 | | eqfnfv2 5975 |
. . . 4
   ..^  ..^ 

  ..^  ..^   ..^              |
75 | 73, 74 | syl 17 |
. . 3
   
     ..^      ..^     

  ..^  ..^   ..^              |
76 | | df-ne 2623 |
. . . . . 6

  |
77 | | elnnne0 10880 |
. . . . . . . 8

    |
78 | | 0zd 10946 |
. . . . . . . . . . . . . . 15
   |
79 | | nnz 10956 |
. . . . . . . . . . . . . . 15
   |
80 | | nngt0 10635 |
. . . . . . . . . . . . . . 15
   |
81 | 78, 79, 80 | 3jca 1187 |
. . . . . . . . . . . . . 14
 
   |
82 | 81 | adantr 467 |
. . . . . . . . . . . . 13
 
     |
83 | | fzoopth 39050 |
. . . . . . . . . . . . 13
 
   ..^  ..^      |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . 12
 
   ..^  ..^
     |
85 | | simpr 463 |
. . . . . . . . . . . 12
     |
86 | 84, 85 | syl6bi 232 |
. . . . . . . . . . 11
 
   ..^  ..^    |
87 | 86 | anim1d 567 |
. . . . . . . . . 10
 
    ..^  ..^   ..^           
  ..^              |
88 | | oveq2 6296 |
. . . . . . . . . . 11
  ..^  ..^   |
89 | 88 | anim1i 571 |
. . . . . . . . . 10
    ..^             ..^  ..^   ..^             |
90 | 87, 89 | impbid1 207 |
. . . . . . . . 9
 
    ..^  ..^   ..^          

  ..^              |
91 | 90 | ex 436 |
. . . . . . . 8
 
   ..^  ..^ 
 ..^          

  ..^               |
92 | 77, 91 | sylbir 217 |
. . . . . . 7
       ..^  ..^   ..^          

  ..^               |
93 | 92 | impancom 442 |
. . . . . 6
 
     ..^  ..^   ..^          

  ..^               |
94 | 76, 93 | syl5bir 222 |
. . . . 5
 
 
   ..^  ..^   ..^              ..^               |
95 | 94 | adantr 467 |
. . . 4
        ..^      ..^     
   ..^  ..^   ..^          

  ..^               |
96 | 95 | impcom 432 |
. . 3
   
     ..^      ..^     
   ..^  ..^   ..^              ..^              |
97 | 75, 96 | bitrd 257 |
. 2
   
     ..^      ..^     

   ..^              |
98 | 69, 97 | pm2.61ian 798 |
1
        ..^      ..^     

  ..^              |