Step | Hyp | Ref
| Expression |
1 | | elfznelfzo 11915 |
. . . . . . 7
|
2 | | ffn 5736 |
. . . . . . . . . . . . . . . . . 18
|
3 | 2 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
4 | | 0elfz 11802 |
. . . . . . . . . . . . . . . . . 18
|
5 | 4 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
6 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
7 | | nn0re 10829 |
. . . . . . . . . . . . . . . . . . . 20
|
8 | 7 | leidd 10144 |
. . . . . . . . . . . . . . . . . . 19
|
9 | | elfz2nn0 11798 |
. . . . . . . . . . . . . . . . . . 19
|
10 | 6, 6, 8, 9 | syl3anbrc 1180 |
. . . . . . . . . . . . . . . . . 18
|
11 | 10 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
12 | | fnimapr 5937 |
. . . . . . . . . . . . . . . . 17
|
13 | 3, 5, 11, 12 | syl3anc 1228 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | ineq1d 3698 |
. . . . . . . . . . . . . . 15
|
15 | 14 | eqeq1d 2459 |
. . . . . . . . . . . . . 14
|
16 | | disj 3867 |
. . . . . . . . . . . . . 14
|
17 | 15, 16 | syl6bb 261 |
. . . . . . . . . . . . 13
|
18 | | fvex 5881 |
. . . . . . . . . . . . . . . 16
|
19 | | fvex 5881 |
. . . . . . . . . . . . . . . 16
|
20 | 18, 19 | pm3.2i 455 |
. . . . . . . . . . . . . . 15
|
21 | | eleq1 2529 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | notbid 294 |
. . . . . . . . . . . . . . . 16
|
23 | | eleq1 2529 |
. . . . . . . . . . . . . . . . 17
|
24 | 23 | notbid 294 |
. . . . . . . . . . . . . . . 16
|
25 | 22, 24 | ralprg 4078 |
. . . . . . . . . . . . . . 15
|
26 | 20, 25 | mp1i 12 |
. . . . . . . . . . . . . 14
|
27 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | eqcoms 2469 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 28 | eleq1d 2526 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | notbid 294 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | biimpd 207 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | 1eluzge0 11153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
33 | | fzoss1 11852 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
34 | 32, 33 | mp1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | | fzossfz 11846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
36 | 34, 35 | syl6ss 3515 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
37 | | fvelimab 5929 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 2, 36, 37 | syl2an 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 38 | notbid 294 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | | ralnex 2903 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
42 | 41 | eqeq1d 2459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
43 | 42 | notbid 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
44 | 43 | rspcva 3208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
45 | | pm2.21 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
46 | 45 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
47 | 46 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
48 | 47 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
49 | 44, 48 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
50 | 49 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | 50 | com24 87 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
52 | 40, 51 | sylbir 213 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | 52 | com12 31 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 39, 53 | sylbid 215 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | com12 31 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 31, 55 | syl6com 35 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | com12 31 |
. . . . . . . . . . . . . . . 16
|
59 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
60 | 59 | eqcoms 2469 |
. . . . . . . . . . . . . . . . . . . . . 22
|
61 | 60 | eleq1d 2526 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 61 | notbid 294 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 62 | biimpd 207 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63, 55 | syl6com 35 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | com12 31 |
. . . . . . . . . . . . . . . 16
|
67 | 58, 66 | jaoi 379 |
. . . . . . . . . . . . . . 15
|
68 | 67 | com13 80 |
. . . . . . . . . . . . . 14
|
69 | 26, 68 | sylbid 215 |
. . . . . . . . . . . . 13
|
70 | 17, 69 | sylbid 215 |
. . . . . . . . . . . 12
|
71 | 70 | com14 88 |
. . . . . . . . . . 11
|
72 | 71 | com12 31 |
. . . . . . . . . 10
|
73 | 72 | com15 93 |
. . . . . . . . 9
|
74 | | elfznelfzo 11915 |
. . . . . . . . . . 11
|
75 | | eqtr3 2485 |
. . . . . . . . . . . . . 14
|
76 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | a1d 25 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | a1d 25 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | a1d 25 |
. . . . . . . . . . . . . . 15
|
80 | 79 | a1d 25 |
. . . . . . . . . . . . . 14
|
81 | 75, 80 | syl 16 |
. . . . . . . . . . . . 13
|
82 | 28 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
83 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 83 | eqcoms 2469 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
86 | 82, 85 | neeq12d 2736 |
. . . . . . . . . . . . . . . 16
|
87 | | df-ne 2654 |
. . . . . . . . . . . . . . . . 17
|
88 | | pm2.24 109 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 88 | eqcoms 2469 |
. . . . . . . . . . . . . . . . . 18
|
90 | 89 | com12 31 |
. . . . . . . . . . . . . . . . 17
|
91 | 87, 90 | sylbi 195 |
. . . . . . . . . . . . . . . 16
|
92 | 86, 91 | syl6bi 228 |
. . . . . . . . . . . . . . 15
|
93 | 92 | a1d 25 |
. . . . . . . . . . . . . 14
|
94 | 93 | a1d 25 |
. . . . . . . . . . . . 13
|
95 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 95 | eqcoms 2469 |
. . . . . . . . . . . . . . . . . 18
|
97 | 96 | adantr 465 |
. . . . . . . . . . . . . . . . 17
|
98 | 60 | adantl 466 |
. . . . . . . . . . . . . . . . 17
|
99 | 97, 98 | neeq12d 2736 |
. . . . . . . . . . . . . . . 16
|
100 | | df-ne 2654 |
. . . . . . . . . . . . . . . . 17
|
101 | 100, 45 | sylbi 195 |
. . . . . . . . . . . . . . . 16
|
102 | 99, 101 | syl6bi 228 |
. . . . . . . . . . . . . . 15
|
103 | 102 | a1d 25 |
. . . . . . . . . . . . . 14
|
104 | 103 | a1d 25 |
. . . . . . . . . . . . 13
|
105 | | eqtr3 2485 |
. . . . . . . . . . . . . 14
|
106 | 105, 80 | syl 16 |
. . . . . . . . . . . . 13
|
107 | 81, 94, 104, 106 | ccase 946 |
. . . . . . . . . . . 12
|
108 | 107 | ex 434 |
. . . . . . . . . . 11
|
109 | 74, 108 | syl 16 |
. . . . . . . . . 10
|
110 | 109 | expcom 435 |
. . . . . . . . 9
|
111 | 73, 110 | pm2.61i 164 |
. . . . . . . 8
|
112 | 111 | com12 31 |
. . . . . . 7
|
113 | 1, 112 | syl 16 |
. . . . . 6
|
114 | 113 | ex 434 |
. . . . 5
|
115 | 114 | com23 78 |
. . . 4
|
116 | 115 | impcom 430 |
. . 3
|
117 | 116 | com12 31 |
. 2
|
118 | 117 | com25 91 |
1
|