Step | Hyp | Ref
| Expression |
1 | | elmapi 7879 |
. . . . . . . . . 10
|
2 | 1 | adantr 481 |
. . . . . . . . 9
|
3 | | c0ex 10034 |
. . . . . . . . . . 11
|
4 | 3 | fconst 6091 |
. . . . . . . . . 10
|
5 | 4 | a1i 11 |
. . . . . . . . 9
|
6 | | disjdif 4040 |
. . . . . . . . . 10
|
7 | 6 | a1i 11 |
. . . . . . . . 9
|
8 | | fun 6066 |
. . . . . . . . 9
|
9 | 2, 5, 7, 8 | syl21anc 1325 |
. . . . . . . 8
|
10 | | eulerpart.j |
. . . . . . . . . . 11
|
11 | | ssrab2 3687 |
. . . . . . . . . . 11
|
12 | 10, 11 | eqsstri 3635 |
. . . . . . . . . 10
|
13 | | undif 4049 |
. . . . . . . . . 10
|
14 | 12, 13 | mpbi 220 |
. . . . . . . . 9
|
15 | | 0nn0 11307 |
. . . . . . . . . . 11
|
16 | | snssi 4339 |
. . . . . . . . . . 11
|
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
|
18 | | ssequn2 3786 |
. . . . . . . . . 10
|
19 | 17, 18 | mpbi 220 |
. . . . . . . . 9
|
20 | 14, 19 | feq23i 6039 |
. . . . . . . 8
|
21 | 9, 20 | sylib 208 |
. . . . . . 7
|
22 | | nn0ex 11298 |
. . . . . . . 8
|
23 | | nnex 11026 |
. . . . . . . 8
|
24 | 22, 23 | elmap 7886 |
. . . . . . 7
|
25 | 21, 24 | sylibr 224 |
. . . . . 6
|
26 | | cnvun 5538 |
. . . . . . . . 9
|
27 | 26 | imaeq1i 5463 |
. . . . . . . 8
|
28 | | imaundir 5546 |
. . . . . . . 8
|
29 | 27, 28 | eqtri 2644 |
. . . . . . 7
|
30 | | vex 3203 |
. . . . . . . . . . 11
|
31 | | cnveq 5296 |
. . . . . . . . . . . . 13
|
32 | 31 | imaeq1d 5465 |
. . . . . . . . . . . 12
|
33 | 32 | eleq1d 2686 |
. . . . . . . . . . 11
|
34 | | eulerpart.r |
. . . . . . . . . . 11
|
35 | 30, 33, 34 | elab2 3354 |
. . . . . . . . . 10
|
36 | 35 | biimpi 206 |
. . . . . . . . 9
|
37 | 36 | adantl 482 |
. . . . . . . 8
|
38 | | cnvxp 5551 |
. . . . . . . . . . . . . 14
|
39 | 38 | dmeqi 5325 |
. . . . . . . . . . . . 13
|
40 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
|
41 | | 2z 11409 |
. . . . . . . . . . . . . . . . 17
|
42 | | iddvds 14995 |
. . . . . . . . . . . . . . . . 17
|
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
44 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 44 | notbid 308 |
. . . . . . . . . . . . . . . . . 18
|
46 | 45, 10 | elrab2 3366 |
. . . . . . . . . . . . . . . . 17
|
47 | 46 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
48 | 43, 47 | mt2 191 |
. . . . . . . . . . . . . . 15
|
49 | | eldif 3584 |
. . . . . . . . . . . . . . 15
|
50 | 40, 48, 49 | mpbir2an 955 |
. . . . . . . . . . . . . 14
|
51 | | ne0i 3921 |
. . . . . . . . . . . . . 14
|
52 | | dmxp 5344 |
. . . . . . . . . . . . . 14
|
53 | 50, 51, 52 | mp2b 10 |
. . . . . . . . . . . . 13
|
54 | 39, 53 | eqtri 2644 |
. . . . . . . . . . . 12
|
55 | 54 | ineq1i 3810 |
. . . . . . . . . . 11
|
56 | | incom 3805 |
. . . . . . . . . . 11
|
57 | | 0nnn 11052 |
. . . . . . . . . . . 12
|
58 | | disjsn 4246 |
. . . . . . . . . . . 12
|
59 | 57, 58 | mpbir 221 |
. . . . . . . . . . 11
|
60 | 55, 56, 59 | 3eqtr2i 2650 |
. . . . . . . . . 10
|
61 | | imadisj 5484 |
. . . . . . . . . 10
|
62 | 60, 61 | mpbir 221 |
. . . . . . . . 9
|
63 | | 0fin 8188 |
. . . . . . . . 9
|
64 | 62, 63 | eqeltri 2697 |
. . . . . . . 8
|
65 | | unfi 8227 |
. . . . . . . 8
|
66 | 37, 64, 65 | sylancl 694 |
. . . . . . 7
|
67 | 29, 66 | syl5eqel 2705 |
. . . . . 6
|
68 | | cnvimass 5485 |
. . . . . . . . 9
|
69 | | fdm 6051 |
. . . . . . . . . 10
|
70 | 2, 69 | syl 17 |
. . . . . . . . 9
|
71 | 68, 70 | syl5sseq 3653 |
. . . . . . . 8
|
72 | | 0ss 3972 |
. . . . . . . . . 10
|
73 | 62, 72 | eqsstri 3635 |
. . . . . . . . 9
|
74 | 73 | a1i 11 |
. . . . . . . 8
|
75 | 71, 74 | unssd 3789 |
. . . . . . 7
|
76 | 29, 75 | syl5eqss 3649 |
. . . . . 6
|
77 | | eulerpart.p |
. . . . . . 7
|
78 | | eulerpart.o |
. . . . . . 7
|
79 | | eulerpart.d |
. . . . . . 7
|
80 | | eulerpart.f |
. . . . . . 7
|
81 | | eulerpart.h |
. . . . . . 7
supp |
82 | | eulerpart.m |
. . . . . . 7
|
83 | | eulerpart.t |
. . . . . . 7
|
84 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 30431 |
. . . . . 6
|
85 | 25, 67, 76, 84 | syl3anbrc 1246 |
. . . . 5
|
86 | | resundir 5411 |
. . . . . 6
|
87 | | ffn 6045 |
. . . . . . . 8
|
88 | | fnresdm 6000 |
. . . . . . . . 9
|
89 | | incom 3805 |
. . . . . . . . . . . 12
|
90 | 89, 6 | eqtri 2644 |
. . . . . . . . . . 11
|
91 | | fnconstg 6093 |
. . . . . . . . . . . 12
|
92 | | fnresdisj 6001 |
. . . . . . . . . . . 12
|
93 | 15, 91, 92 | mp2b 10 |
. . . . . . . . . . 11
|
94 | 90, 93 | mpbi 220 |
. . . . . . . . . 10
|
95 | 94 | a1i 11 |
. . . . . . . . 9
|
96 | 88, 95 | uneq12d 3768 |
. . . . . . . 8
|
97 | 2, 87, 96 | 3syl 18 |
. . . . . . 7
|
98 | | un0 3967 |
. . . . . . 7
|
99 | 97, 98 | syl6eq 2672 |
. . . . . 6
|
100 | 86, 99 | syl5req 2669 |
. . . . 5
|
101 | | reseq1 5390 |
. . . . . . 7
|
102 | 101 | eqeq2d 2632 |
. . . . . 6
|
103 | 102 | rspcev 3309 |
. . . . 5
|
104 | 85, 100, 103 | syl2anc 693 |
. . . 4
|
105 | | simpr 477 |
. . . . . . 7
|
106 | | simpl 473 |
. . . . . . . . . . . 12
|
107 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 30431 |
. . . . . . . . . . . 12
|
108 | 106, 107 | sylib 208 |
. . . . . . . . . . 11
|
109 | 108 | simp1d 1073 |
. . . . . . . . . 10
|
110 | 22, 23 | elmap 7886 |
. . . . . . . . . 10
|
111 | 109, 110 | sylib 208 |
. . . . . . . . 9
|
112 | | fssres 6070 |
. . . . . . . . 9
|
113 | 111, 12, 112 | sylancl 694 |
. . . . . . . 8
|
114 | 10, 23 | rabex2 4815 |
. . . . . . . . 9
|
115 | 22, 114 | elmap 7886 |
. . . . . . . 8
|
116 | 113, 115 | sylibr 224 |
. . . . . . 7
|
117 | 105, 116 | eqeltrd 2701 |
. . . . . 6
|
118 | | ffun 6048 |
. . . . . . . . . 10
|
119 | | respreima 6344 |
. . . . . . . . . 10
|
120 | 111, 118,
119 | 3syl 18 |
. . . . . . . . 9
|
121 | 108 | simp2d 1074 |
. . . . . . . . . 10
|
122 | | infi 8184 |
. . . . . . . . . 10
|
123 | 121, 122 | syl 17 |
. . . . . . . . 9
|
124 | 120, 123 | eqeltrd 2701 |
. . . . . . . 8
|
125 | | vex 3203 |
. . . . . . . . . 10
|
126 | 125 | resex 5443 |
. . . . . . . . 9
|
127 | | cnveq 5296 |
. . . . . . . . . . 11
|
128 | 127 | imaeq1d 5465 |
. . . . . . . . . 10
|
129 | 128 | eleq1d 2686 |
. . . . . . . . 9
|
130 | 126, 129,
34 | elab2 3354 |
. . . . . . . 8
|
131 | 124, 130 | sylibr 224 |
. . . . . . 7
|
132 | 105, 131 | eqeltrd 2701 |
. . . . . 6
|
133 | 117, 132 | jca 554 |
. . . . 5
|
134 | 133 | rexlimiva 3028 |
. . . 4
|
135 | 104, 134 | impbii 199 |
. . 3
|
136 | 135 | abbii 2739 |
. 2
|
137 | | df-in 3581 |
. 2
|
138 | | eqid 2622 |
. . 3
|
139 | 138 | rnmpt 5371 |
. 2
|
140 | 136, 137,
139 | 3eqtr4i 2654 |
1
|