Proof of Theorem pellfund14
Step | Hyp | Ref
| Expression |
1 | | pell14qrrp 37424 |
. . . 4
◻NN Pell14QR
|
2 | | pellfundrp 37452 |
. . . . 5
◻NN PellFund |
3 | 2 | adantr 481 |
. . . 4
◻NN Pell14QR PellFund |
4 | | pellfundne1 37453 |
. . . . 5
◻NN PellFund |
5 | 4 | adantr 481 |
. . . 4
◻NN Pell14QR PellFund |
6 | | reglogcl 37454 |
. . . 4
PellFund PellFund PellFund |
7 | 1, 3, 5, 6 | syl3anc 1326 |
. . 3
◻NN Pell14QR PellFund |
8 | 7 | flcld 12599 |
. 2
◻NN Pell14QR PellFund |
9 | | pell14qrre 37421 |
. . . 4
◻NN Pell14QR
|
10 | 9 | recnd 10068 |
. . 3
◻NN Pell14QR
|
11 | 3, 8 | rpexpcld 13032 |
. . . 4
◻NN Pell14QR PellFund PellFund |
12 | 11 | rpcnd 11874 |
. . 3
◻NN Pell14QR PellFund PellFund |
13 | 8 | znegcld 11484 |
. . . . 5
◻NN Pell14QR PellFund |
14 | 3, 13 | rpexpcld 13032 |
. . . 4
◻NN Pell14QR PellFund PellFund |
15 | 14 | rpcnd 11874 |
. . 3
◻NN Pell14QR PellFund PellFund |
16 | 14 | rpne0d 11877 |
. . 3
◻NN Pell14QR PellFund PellFund |
17 | | simpl 473 |
. . . . 5
◻NN Pell14QR
◻NN |
18 | | pell1qrss14 37432 |
. . . . . . . . 9
◻NN Pell1QR Pell14QR |
19 | | pellfundex 37450 |
. . . . . . . . 9
◻NN PellFund Pell1QR |
20 | 18, 19 | sseldd 3604 |
. . . . . . . 8
◻NN PellFund Pell14QR |
21 | 20 | adantr 481 |
. . . . . . 7
◻NN Pell14QR PellFund Pell14QR |
22 | | pell14qrexpcl 37431 |
. . . . . . 7
◻NN PellFund Pell14QR
PellFund PellFund PellFund Pell14QR |
23 | 17, 21, 13, 22 | syl3anc 1326 |
. . . . . 6
◻NN Pell14QR PellFund PellFund Pell14QR |
24 | | pell14qrmulcl 37427 |
. . . . . 6
◻NN Pell14QR PellFund PellFund Pell14QR
PellFund PellFund Pell14QR |
25 | 23, 24 | mpd3an3 1425 |
. . . . 5
◻NN Pell14QR PellFund PellFund Pell14QR |
26 | | 1rp 11836 |
. . . . . . . . . 10
|
27 | 26 | a1i 11 |
. . . . . . . . 9
◻NN Pell14QR |
28 | | modge0 12678 |
. . . . . . . . 9
PellFund
PellFund |
29 | 7, 27, 28 | syl2anc 693 |
. . . . . . . 8
◻NN Pell14QR
PellFund |
30 | 7 | recnd 10068 |
. . . . . . . . . 10
◻NN Pell14QR PellFund |
31 | 8 | zcnd 11483 |
. . . . . . . . . 10
◻NN Pell14QR PellFund |
32 | 30, 31 | negsubd 10398 |
. . . . . . . . 9
◻NN Pell14QR PellFund PellFund PellFund PellFund |
33 | | modfrac 12683 |
. . . . . . . . . 10
PellFund PellFund PellFund PellFund |
34 | 7, 33 | syl 17 |
. . . . . . . . 9
◻NN Pell14QR PellFund PellFund PellFund |
35 | 32, 34 | eqtr4d 2659 |
. . . . . . . 8
◻NN Pell14QR PellFund PellFund PellFund |
36 | 29, 35 | breqtrrd 4681 |
. . . . . . 7
◻NN Pell14QR
PellFund PellFund |
37 | | reglog1 37460 |
. . . . . . . 8
PellFund PellFund PellFund |
38 | 3, 5, 37 | syl2anc 693 |
. . . . . . 7
◻NN Pell14QR PellFund |
39 | | reglogmul 37457 |
. . . . . . . . 9
PellFund PellFund
PellFund PellFund
PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
40 | 1, 14, 3, 5, 39 | syl112anc 1330 |
. . . . . . . 8
◻NN Pell14QR
PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
41 | | reglogexpbas 37461 |
. . . . . . . . . 10
PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
42 | 13, 3, 5, 41 | syl12anc 1324 |
. . . . . . . . 9
◻NN Pell14QR PellFund PellFund PellFund PellFund |
43 | 42 | oveq2d 6666 |
. . . . . . . 8
◻NN Pell14QR PellFund PellFund PellFund PellFund PellFund PellFund |
44 | 40, 43 | eqtrd 2656 |
. . . . . . 7
◻NN Pell14QR
PellFund PellFund PellFund PellFund PellFund |
45 | 36, 38, 44 | 3brtr4d 4685 |
. . . . . 6
◻NN Pell14QR PellFund
PellFund PellFund PellFund |
46 | 1, 14 | rpmulcld 11888 |
. . . . . . 7
◻NN Pell14QR PellFund PellFund |
47 | | pellfundgt1 37447 |
. . . . . . . 8
◻NN
PellFund |
48 | 47 | adantr 481 |
. . . . . . 7
◻NN Pell14QR
PellFund |
49 | | reglogleb 37456 |
. . . . . . 7
PellFund PellFund PellFund PellFund
PellFund PellFund
PellFund PellFund PellFund PellFund |
50 | 27, 46, 3, 48, 49 | syl22anc 1327 |
. . . . . 6
◻NN Pell14QR
PellFund PellFund
PellFund PellFund PellFund PellFund |
51 | 45, 50 | mpbird 247 |
. . . . 5
◻NN Pell14QR
PellFund PellFund |
52 | | modlt 12679 |
. . . . . . . . 9
PellFund PellFund |
53 | 7, 27, 52 | syl2anc 693 |
. . . . . . . 8
◻NN Pell14QR PellFund |
54 | 35, 53 | eqbrtrd 4675 |
. . . . . . 7
◻NN Pell14QR PellFund PellFund |
55 | | reglogbas 37459 |
. . . . . . . 8
PellFund PellFund PellFund PellFund |
56 | 3, 5, 55 | syl2anc 693 |
. . . . . . 7
◻NN Pell14QR PellFund PellFund |
57 | 54, 44, 56 | 3brtr4d 4685 |
. . . . . 6
◻NN Pell14QR
PellFund PellFund PellFund PellFund PellFund |
58 | | reglogltb 37455 |
. . . . . . 7
PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
59 | 46, 3, 3, 48, 58 | syl22anc 1327 |
. . . . . 6
◻NN Pell14QR PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
60 | 57, 59 | mpbird 247 |
. . . . 5
◻NN Pell14QR PellFund PellFund PellFund |
61 | | pellfund14gap 37451 |
. . . . 5
◻NN PellFund PellFund Pell14QR
PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
62 | 17, 25, 51, 60, 61 | syl112anc 1330 |
. . . 4
◻NN Pell14QR PellFund PellFund |
63 | 31 | negidd 10382 |
. . . . . 6
◻NN Pell14QR PellFund PellFund |
64 | 63 | oveq2d 6666 |
. . . . 5
◻NN Pell14QR PellFund PellFund PellFund PellFund |
65 | 3 | rpcnd 11874 |
. . . . . 6
◻NN Pell14QR PellFund |
66 | 3 | rpne0d 11877 |
. . . . . 6
◻NN Pell14QR PellFund |
67 | | expaddz 12904 |
. . . . . 6
PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
68 | 65, 66, 8, 13, 67 | syl22anc 1327 |
. . . . 5
◻NN Pell14QR PellFund PellFund PellFund PellFund PellFund PellFund PellFund |
69 | 65 | exp0d 13002 |
. . . . 5
◻NN Pell14QR PellFund |
70 | 64, 68, 69 | 3eqtr3rd 2665 |
. . . 4
◻NN Pell14QR PellFund PellFund PellFund PellFund |
71 | 62, 70 | eqtrd 2656 |
. . 3
◻NN Pell14QR PellFund PellFund PellFund PellFund PellFund PellFund |
72 | 10, 12, 15, 16, 71 | mulcan2ad 10663 |
. 2
◻NN Pell14QR
PellFund PellFund |
73 | | oveq2 6658 |
. . . 4
PellFund PellFund PellFund PellFund |
74 | 73 | eqeq2d 2632 |
. . 3
PellFund PellFund
PellFund PellFund |
75 | 74 | rspcev 3309 |
. 2
PellFund PellFund PellFund PellFund |
76 | 8, 72, 75 | syl2anc 693 |
1
◻NN Pell14QR
PellFund |