Step | Hyp | Ref
| Expression |
1 | | nnnninfeq2.p |
. 2
ℕ∞ |
2 | | nnnninfeq2.n |
. 2
|
3 | | nnnninfeq2.1 |
. . 3
|
4 | 2 | adantr 274 |
. . . 4
|
5 | | unieq 3782 |
. . . . . . . 8
|
6 | 5 | fveqeq2d 5477 |
. . . . . . 7
|
7 | 6 | anbi2d 460 |
. . . . . 6
|
8 | | raleq 2652 |
. . . . . 6
|
9 | 7, 8 | imbi12d 233 |
. . . . 5
|
10 | | unieq 3782 |
. . . . . . . 8
|
11 | 10 | fveqeq2d 5477 |
. . . . . . 7
|
12 | 11 | anbi2d 460 |
. . . . . 6
|
13 | | raleq 2652 |
. . . . . 6
|
14 | 12, 13 | imbi12d 233 |
. . . . 5
|
15 | | unieq 3782 |
. . . . . . . 8
|
16 | 15 | fveqeq2d 5477 |
. . . . . . 7
|
17 | 16 | anbi2d 460 |
. . . . . 6
|
18 | | raleq 2652 |
. . . . . 6
|
19 | 17, 18 | imbi12d 233 |
. . . . 5
|
20 | | unieq 3782 |
. . . . . . . 8
|
21 | 20 | fveqeq2d 5477 |
. . . . . . 7
|
22 | 21 | anbi2d 460 |
. . . . . 6
|
23 | | raleq 2652 |
. . . . . 6
|
24 | 22, 23 | imbi12d 233 |
. . . . 5
|
25 | | ral0 3495 |
. . . . . 6
|
26 | 25 | a1i 9 |
. . . . 5
|
27 | | uni0 3800 |
. . . . . . . . . . . . . . . 16
|
28 | | unieq 3782 |
. . . . . . . . . . . . . . . 16
|
29 | | id 19 |
. . . . . . . . . . . . . . . 16
|
30 | 27, 28, 29 | 3eqtr4a 2216 |
. . . . . . . . . . . . . . 15
|
31 | 30 | fveq2d 5473 |
. . . . . . . . . . . . . 14
|
32 | | nnord 4572 |
. . . . . . . . . . . . . . . . . . 19
|
33 | | ordtr 4339 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 32, 33 | syl 14 |
. . . . . . . . . . . . . . . . . 18
|
35 | 34 | ad3antlr 485 |
. . . . . . . . . . . . . . . . 17
|
36 | | unisucg 4375 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | ad3antlr 485 |
. . . . . . . . . . . . . . . . 17
|
38 | 35, 37 | mpbid 146 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | fveq2d 5473 |
. . . . . . . . . . . . . . 15
|
40 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
41 | 39, 40 | eqtr3d 2192 |
. . . . . . . . . . . . . 14
|
42 | 31, 41 | sylan9eqr 2212 |
. . . . . . . . . . . . 13
|
43 | | nninff 7067 |
. . . . . . . . . . . . . . . . . . 19
ℕ∞ |
44 | 1, 43 | syl 14 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | adantr 274 |
. . . . . . . . . . . . . . . . 17
|
46 | | nnpredcl 4583 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | adantl 275 |
. . . . . . . . . . . . . . . . 17
|
48 | 45, 47 | ffvelrnd 5604 |
. . . . . . . . . . . . . . . 16
|
49 | | el2oss1o 6391 |
. . . . . . . . . . . . . . . 16
|
50 | 48, 49 | syl 14 |
. . . . . . . . . . . . . . 15
|
51 | 50 | ad3antrrr 484 |
. . . . . . . . . . . . . 14
|
52 | | simp-4r 532 |
. . . . . . . . . . . . . . . . . 18
|
53 | | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 53 | neqned 2334 |
. . . . . . . . . . . . . . . . . 18
|
55 | | nnsucpred 4577 |
. . . . . . . . . . . . . . . . . 18
|
56 | 52, 54, 55 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | fveq2d 5473 |
. . . . . . . . . . . . . . . 16
|
58 | 41 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
59 | 57, 58 | eqtrd 2190 |
. . . . . . . . . . . . . . 15
|
60 | | suceq 4363 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 60 | fveq2d 5473 |
. . . . . . . . . . . . . . . . . 18
|
62 | | fveq2 5469 |
. . . . . . . . . . . . . . . . . 18
|
63 | 61, 62 | sseq12d 3159 |
. . . . . . . . . . . . . . . . 17
|
64 | | fveq1 5468 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | | fveq1 5468 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | 64, 65 | sseq12d 3159 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 66 | ralbidv 2457 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | | df-nninf 7065 |
. . . . . . . . . . . . . . . . . . . . 21
ℕ∞
|
69 | 67, 68 | elrab2 2871 |
. . . . . . . . . . . . . . . . . . . 20
ℕ∞
|
70 | 1, 69 | sylib 121 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 70 | simprd 113 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | ad3antrrr 484 |
. . . . . . . . . . . . . . . . 17
|
73 | 46 | ad3antlr 485 |
. . . . . . . . . . . . . . . . 17
|
74 | 63, 72, 73 | rspcdva 2821 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | adantr 274 |
. . . . . . . . . . . . . . 15
|
76 | 59, 75 | eqsstrrd 3165 |
. . . . . . . . . . . . . 14
|
77 | 51, 76 | eqssd 3145 |
. . . . . . . . . . . . 13
|
78 | | nndceq0 4578 |
. . . . . . . . . . . . . . 15
DECID
|
79 | | exmiddc 822 |
. . . . . . . . . . . . . . 15
DECID |
80 | 78, 79 | syl 14 |
. . . . . . . . . . . . . 14
|
81 | 80 | ad3antlr 485 |
. . . . . . . . . . . . 13
|
82 | 42, 77, 81 | mpjaodan 788 |
. . . . . . . . . . . 12
|
83 | | simplr 520 |
. . . . . . . . . . . 12
|
84 | 82, 83 | mpd 13 |
. . . . . . . . . . 11
|
85 | | fveqeq2 5478 |
. . . . . . . . . . . . 13
|
86 | 85 | ralunsn 3761 |
. . . . . . . . . . . 12
|
87 | 86 | ad3antlr 485 |
. . . . . . . . . . 11
|
88 | 84, 41, 87 | mpbir2and 929 |
. . . . . . . . . 10
|
89 | | df-suc 4332 |
. . . . . . . . . . 11
|
90 | 89 | raleqi 2656 |
. . . . . . . . . 10
|
91 | 88, 90 | sylibr 133 |
. . . . . . . . 9
|
92 | 91 | exp31 362 |
. . . . . . . 8
|
93 | 92 | expcom 115 |
. . . . . . 7
|
94 | 93 | a2d 26 |
. . . . . 6
|
95 | | impexp 261 |
. . . . . 6
|
96 | | impexp 261 |
. . . . . 6
|
97 | 94, 95, 96 | 3imtr4g 204 |
. . . . 5
|
98 | 9, 14, 19, 24, 26, 97 | finds 4560 |
. . . 4
|
99 | 4, 98 | mpcom 36 |
. . 3
|
100 | 3, 99 | mpdan 418 |
. 2
|
101 | | nnnninfeq2.0 |
. 2
|
102 | 1, 2, 100, 101 | nnnninfeq 7072 |
1
|