Step | Hyp | Ref
| Expression |
1 | | fzf 8878 |
. . . . 5
|
2 | | ffn 5046 |
. . . . 5
|
3 | 1, 2 | ax-mp 7 |
. . . 4
|
4 | | fnovex 5538 |
. . . 4
|
5 | 3, 4 | mp3an1 1219 |
. . 3
|
6 | 5 | 3adant3 924 |
. 2
|
7 | | simp1 904 |
. . . 4
|
8 | | simp3 906 |
. . . 4
|
9 | 7, 8 | zaddcld 8364 |
. . 3
|
10 | | simp2 905 |
. . . 4
|
11 | 10, 8 | zaddcld 8364 |
. . 3
|
12 | | fnovex 5538 |
. . . 4
|
13 | 3, 12 | mp3an1 1219 |
. . 3
|
14 | 9, 11, 13 | syl2anc 391 |
. 2
|
15 | | elfz1 8879 |
. . . . 5
|
16 | 15 | biimpd 132 |
. . . 4
|
17 | 16 | 3adant3 924 |
. . 3
|
18 | | zaddcl 8285 |
. . . . . . . . . . 11
|
19 | 18 | expcom 109 |
. . . . . . . . . 10
|
20 | 19 | 3ad2ant3 927 |
. . . . . . . . 9
|
21 | 20 | adantrd 264 |
. . . . . . . 8
|
22 | | zre 8249 |
. . . . . . . . . . . . . . 15
|
23 | | zre 8249 |
. . . . . . . . . . . . . . 15
|
24 | | zre 8249 |
. . . . . . . . . . . . . . 15
|
25 | | leadd1 7425 |
. . . . . . . . . . . . . . 15
|
26 | 22, 23, 24, 25 | syl3an 1177 |
. . . . . . . . . . . . . 14
|
27 | 26 | biimpd 132 |
. . . . . . . . . . . . 13
|
28 | 27 | adantrd 264 |
. . . . . . . . . . . 12
|
29 | 28 | 3com23 1110 |
. . . . . . . . . . 11
|
30 | 29 | 3expia 1106 |
. . . . . . . . . 10
|
31 | 30 | impd 242 |
. . . . . . . . 9
|
32 | 31 | 3adant2 923 |
. . . . . . . 8
|
33 | | zre 8249 |
. . . . . . . . . . . . . . 15
|
34 | | leadd1 7425 |
. . . . . . . . . . . . . . 15
|
35 | 23, 33, 24, 34 | syl3an 1177 |
. . . . . . . . . . . . . 14
|
36 | 35 | biimpd 132 |
. . . . . . . . . . . . 13
|
37 | 36 | adantld 263 |
. . . . . . . . . . . 12
|
38 | 37 | 3coml 1111 |
. . . . . . . . . . 11
|
39 | 38 | 3expia 1106 |
. . . . . . . . . 10
|
40 | 39 | impd 242 |
. . . . . . . . 9
|
41 | 40 | 3adant1 922 |
. . . . . . . 8
|
42 | 21, 32, 41 | 3jcad 1085 |
. . . . . . 7
|
43 | | zaddcl 8285 |
. . . . . . . . . 10
|
44 | 43 | 3adant2 923 |
. . . . . . . . 9
|
45 | | zaddcl 8285 |
. . . . . . . . . 10
|
46 | 45 | 3adant1 922 |
. . . . . . . . 9
|
47 | | elfz1 8879 |
. . . . . . . . 9
|
48 | 44, 46, 47 | syl2anc 391 |
. . . . . . . 8
|
49 | 48 | biimprd 147 |
. . . . . . 7
|
50 | 42, 49 | syld 40 |
. . . . . 6
|
51 | 50 | com12 27 |
. . . . 5
|
52 | 51 | 3impb 1100 |
. . . 4
|
53 | 52 | com12 27 |
. . 3
|
54 | 17, 53 | syld 40 |
. 2
|
55 | | elfz1 8879 |
. . . . 5
|
56 | 44, 46, 55 | syl2anc 391 |
. . . 4
|
57 | 56 | biimpd 132 |
. . 3
|
58 | | zsubcl 8286 |
. . . . . . . . . . 11
|
59 | 58 | expcom 109 |
. . . . . . . . . 10
|
60 | 59 | 3ad2ant3 927 |
. . . . . . . . 9
|
61 | 60 | adantrd 264 |
. . . . . . . 8
|
62 | | zre 8249 |
. . . . . . . . . . . . . 14
|
63 | | leaddsub 7433 |
. . . . . . . . . . . . . 14
|
64 | 22, 24, 62, 63 | syl3an 1177 |
. . . . . . . . . . . . 13
|
65 | 64 | biimpd 132 |
. . . . . . . . . . . 12
|
66 | 65 | adantrd 264 |
. . . . . . . . . . 11
|
67 | 66 | 3expia 1106 |
. . . . . . . . . 10
|
68 | 67 | impd 242 |
. . . . . . . . 9
|
69 | 68 | 3adant2 923 |
. . . . . . . 8
|
70 | | lesubadd 7429 |
. . . . . . . . . . . . . . . 16
|
71 | 62, 24, 33, 70 | syl3an 1177 |
. . . . . . . . . . . . . . 15
|
72 | 71 | biimprd 147 |
. . . . . . . . . . . . . 14
|
73 | 72 | adantld 263 |
. . . . . . . . . . . . 13
|
74 | 73 | 3coml 1111 |
. . . . . . . . . . . 12
|
75 | 74 | 3expia 1106 |
. . . . . . . . . . 11
|
76 | 75 | impd 242 |
. . . . . . . . . 10
|
77 | 76 | ancoms 255 |
. . . . . . . . 9
|
78 | 77 | 3adant1 922 |
. . . . . . . 8
|
79 | 61, 69, 78 | 3jcad 1085 |
. . . . . . 7
|
80 | | elfz1 8879 |
. . . . . . . . 9
|
81 | 80 | biimprd 147 |
. . . . . . . 8
|
82 | 81 | 3adant3 924 |
. . . . . . 7
|
83 | 79, 82 | syld 40 |
. . . . . 6
|
84 | 83 | com12 27 |
. . . . 5
|
85 | 84 | 3impb 1100 |
. . . 4
|
86 | 85 | com12 27 |
. . 3
|
87 | 57, 86 | syld 40 |
. 2
|
88 | 17 | imp 115 |
. . . . 5
|
89 | 88 | simp1d 916 |
. . . 4
|
90 | 89 | ex 108 |
. . 3
|
91 | 57 | imp 115 |
. . . . 5
|
92 | 91 | simp1d 916 |
. . . 4
|
93 | 92 | ex 108 |
. . 3
|
94 | | zcn 8250 |
. . . . . . 7
|
95 | | zcn 8250 |
. . . . . . 7
|
96 | | zcn 8250 |
. . . . . . 7
|
97 | | subadd 7214 |
. . . . . . . . 9
|
98 | | eqcom 2042 |
. . . . . . . . 9
|
99 | | eqcom 2042 |
. . . . . . . . 9
|
100 | 97, 98, 99 | 3bitr3g 211 |
. . . . . . . 8
|
101 | | addcom 7150 |
. . . . . . . . . 10
|
102 | 101 | 3adant1 922 |
. . . . . . . . 9
|
103 | 102 | eqeq2d 2051 |
. . . . . . . 8
|
104 | 100, 103 | bitrd 177 |
. . . . . . 7
|
105 | 94, 95, 96, 104 | syl3an 1177 |
. . . . . 6
|
106 | 105 | 3coml 1111 |
. . . . 5
|
107 | 106 | 3expib 1107 |
. . . 4
|
108 | 107 | 3ad2ant3 927 |
. . 3
|
109 | 90, 93, 108 | syl2and 279 |
. 2
|
110 | 6, 14, 54, 87, 109 | en3d 6249 |
1
|