Proof of Theorem fzoopth
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . . . 9
..^ ..^
|
2 | | fzolb 12476 |
. . . . . . . . 9
..^ |
3 | 1, 2 | sylibr 224 |
. . . . . . . 8
..^ ..^
..^ |
4 | | simpr 477 |
. . . . . . . 8
..^ ..^
..^ ..^ |
5 | 3, 4 | eleqtrd 2703 |
. . . . . . 7
..^ ..^
..^ |
6 | | elfzouz 12474 |
. . . . . . 7
..^
|
7 | | uzss 11708 |
. . . . . . 7
|
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
..^ ..^
|
9 | 2 | biimpri 218 |
. . . . . . . . . . 11
..^ |
10 | 9 | adantr 481 |
. . . . . . . . . 10
..^ ..^
..^ |
11 | | eleq2 2690 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^ |
12 | 11 | adantl 482 |
. . . . . . . . . 10
..^ ..^
..^ ..^ |
13 | 10, 12 | mpbid 222 |
. . . . . . . . 9
..^ ..^
..^ |
14 | | elfzolt3b 12482 |
. . . . . . . . 9
..^
..^ |
15 | 13, 14 | syl 17 |
. . . . . . . 8
..^ ..^
..^ |
16 | 15, 4 | eleqtrrd 2704 |
. . . . . . 7
..^ ..^
..^ |
17 | | elfzouz 12474 |
. . . . . . 7
..^
|
18 | | uzss 11708 |
. . . . . . 7
|
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
..^ ..^
|
20 | 8, 19 | eqssd 3620 |
. . . . 5
..^ ..^
|
21 | | simpl1 1064 |
. . . . . 6
..^ ..^
|
22 | | uz11 11710 |
. . . . . 6
|
23 | 21, 22 | syl 17 |
. . . . 5
..^ ..^
|
24 | 20, 23 | mpbid 222 |
. . . 4
..^ ..^
|
25 | | fzoend 12559 |
. . . . . . . . 9
..^
..^ |
26 | | elfzoel2 12469 |
. . . . . . . . . 10
..^
|
27 | | eleq2 2690 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ ..^ |
28 | 27 | eqcoms 2630 |
. . . . . . . . . . . . . 14
..^ ..^ ..^ ..^ |
29 | | elfzo2 12473 |
. . . . . . . . . . . . . . 15
..^
|
30 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
31 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | zlem1lt 11429 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
33 | 32 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | 33 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | 34 | impancom 456 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | impcom 446 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 30, 31, 36 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | expcom 451 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | 3adant1 1079 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | a1d 25 |
. . . . . . . . . . . . . . 15
|
41 | 29, 40 | sylbi 207 |
. . . . . . . . . . . . . 14
..^
|
42 | 28, 41 | syl6bi 243 |
. . . . . . . . . . . . 13
..^ ..^ ..^
|
43 | 42 | com23 86 |
. . . . . . . . . . . 12
..^ ..^ ..^
|
44 | 43 | impcom 446 |
. . . . . . . . . . 11
..^ ..^
..^
|
45 | 44 | com13 88 |
. . . . . . . . . 10
..^ ..^ ..^ |
46 | 26, 45 | mpcom 38 |
. . . . . . . . 9
..^
..^ ..^
|
47 | 25, 46 | syl 17 |
. . . . . . . 8
..^
..^ ..^
|
48 | 15, 47 | mpcom 38 |
. . . . . . 7
..^ ..^
|
49 | | eluz2 11693 |
. . . . . . . 8
|
50 | 49 | biimpri 218 |
. . . . . . 7
|
51 | | uzss 11708 |
. . . . . . 7
|
52 | 48, 50, 51 | 3syl 18 |
. . . . . 6
..^ ..^
|
53 | | fzoend 12559 |
. . . . . . . . . 10
..^
..^ |
54 | | eleq2 2690 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
55 | | elfzo2 12473 |
. . . . . . . . . . . . 13
..^
|
56 | | pm3.2 463 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
58 | 57 | com12 32 |
. . . . . . . . . . . . . 14
|
59 | 58 | 3adant1 1079 |
. . . . . . . . . . . . 13
|
60 | 55, 59 | sylbi 207 |
. . . . . . . . . . . 12
..^
|
61 | 54, 60 | syl6bi 243 |
. . . . . . . . . . 11
..^ ..^ ..^
|
62 | 61 | com3l 89 |
. . . . . . . . . 10
..^
..^ ..^
|
63 | 53, 62 | syl 17 |
. . . . . . . . 9
..^
..^ ..^
|
64 | 9, 63 | mpcom 38 |
. . . . . . . 8
..^ ..^
|
65 | 64 | imp 445 |
. . . . . . 7
..^ ..^
|
66 | | simpl 473 |
. . . . . . . 8
|
67 | | simprl 794 |
. . . . . . . 8
|
68 | | zlem1lt 11429 |
. . . . . . . . . . . 12
|
69 | 68 | ancoms 469 |
. . . . . . . . . . 11
|
70 | 69 | biimprd 238 |
. . . . . . . . . 10
|
71 | 70 | impancom 456 |
. . . . . . . . 9
|
72 | 71 | impcom 446 |
. . . . . . . 8
|
73 | | eluz2 11693 |
. . . . . . . 8
|
74 | 66, 67, 72, 73 | syl3anbrc 1246 |
. . . . . . 7
|
75 | | uzss 11708 |
. . . . . . 7
|
76 | 65, 74, 75 | 3syl 18 |
. . . . . 6
..^ ..^
|
77 | 52, 76 | eqssd 3620 |
. . . . 5
..^ ..^
|
78 | | simpl2 1065 |
. . . . . 6
..^ ..^
|
79 | | uz11 11710 |
. . . . . 6
|
80 | 78, 79 | syl 17 |
. . . . 5
..^ ..^
|
81 | 77, 80 | mpbid 222 |
. . . 4
..^ ..^
|
82 | 24, 81 | jca 554 |
. . 3
..^ ..^
|
83 | 82 | ex 450 |
. 2
..^ ..^
|
84 | | oveq12 6659 |
. 2
..^ ..^ |
85 | 83, 84 | impbid1 215 |
1
..^ ..^ |