Proof of Theorem fmtnorec2lem
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 11333 |
. . . . . 6
|
2 | | peano2nn0 11333 |
. . . . . 6
|
3 | | fmtno 41441 |
. . . . . 6
FermatNo |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
FermatNo |
5 | | 2cnd 11093 |
. . . . . . . . 9
|
6 | 5, 1 | expp1d 13009 |
. . . . . . . 8
|
7 | 6 | oveq2d 6666 |
. . . . . . 7
|
8 | | 2nn0 11309 |
. . . . . . . . . . . 12
|
9 | 8 | a1i 11 |
. . . . . . . . . . 11
|
10 | 9, 1 | nn0expcld 13031 |
. . . . . . . . . . 11
|
11 | 9, 10 | nn0expcld 13031 |
. . . . . . . . . 10
|
12 | 11 | nn0cnd 11353 |
. . . . . . . . 9
|
13 | 12 | sqvald 13005 |
. . . . . . . 8
|
14 | 5, 9, 10 | expmuld 13011 |
. . . . . . . 8
|
15 | | fmtnom1nn 41444 |
. . . . . . . . . 10
FermatNo |
16 | 1, 15 | syl 17 |
. . . . . . . . 9
FermatNo |
17 | 16, 16 | oveq12d 6668 |
. . . . . . . 8
FermatNo FermatNo |
18 | 13, 14, 17 | 3eqtr4d 2666 |
. . . . . . 7
FermatNo FermatNo |
19 | 7, 18 | eqtrd 2656 |
. . . . . 6
FermatNo FermatNo |
20 | 19 | oveq1d 6665 |
. . . . 5
FermatNo FermatNo |
21 | 4, 20 | eqtrd 2656 |
. . . 4
FermatNo FermatNo FermatNo |
22 | 21 | adantr 481 |
. . 3
FermatNo FermatNo FermatNo FermatNo FermatNo |
23 | | oveq1 6657 |
. . . . . 6
FermatNo
FermatNo
FermatNo
FermatNo |
24 | 23 | oveq1d 6665 |
. . . . 5
FermatNo
FermatNo
FermatNo FermatNo FermatNo FermatNo |
25 | 24 | oveq1d 6665 |
. . . 4
FermatNo
FermatNo
FermatNo FermatNo FermatNo FermatNo |
26 | 25 | adantl 482 |
. . 3
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
27 | | fzfid 12772 |
. . . . . . . . . . 11
|
28 | | elfznn0 12433 |
. . . . . . . . . . . . 13
|
29 | | fmtnonn 41443 |
. . . . . . . . . . . . . 14
FermatNo |
30 | 29 | nncnd 11036 |
. . . . . . . . . . . . 13
FermatNo |
31 | 28, 30 | syl 17 |
. . . . . . . . . . . 12
FermatNo |
32 | 31 | adantl 482 |
. . . . . . . . . . 11
FermatNo |
33 | 27, 32 | fprodcl 14682 |
. . . . . . . . . 10
FermatNo |
34 | | 1cnd 10056 |
. . . . . . . . . 10
|
35 | 33, 5, 34 | addsubassd 10412 |
. . . . . . . . 9
FermatNo FermatNo |
36 | | 2m1e1 11135 |
. . . . . . . . . 10
|
37 | 36 | oveq2i 6661 |
. . . . . . . . 9
FermatNo FermatNo |
38 | 35, 37 | syl6eq 2672 |
. . . . . . . 8
FermatNo FermatNo |
39 | 38 | oveq1d 6665 |
. . . . . . 7
FermatNo FermatNo FermatNo FermatNo |
40 | | fmtnonn 41443 |
. . . . . . . . . . 11
FermatNo |
41 | 1, 40 | syl 17 |
. . . . . . . . . 10
FermatNo |
42 | 41 | nncnd 11036 |
. . . . . . . . 9
FermatNo |
43 | 42, 34 | subcld 10392 |
. . . . . . . 8
FermatNo |
44 | 33, 42 | muls1d 10491 |
. . . . . . . . 9
FermatNo FermatNo FermatNo FermatNo FermatNo |
45 | 43 | mulid2d 10058 |
. . . . . . . . 9
FermatNo FermatNo |
46 | 44, 45 | oveq12d 6668 |
. . . . . . . 8
FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo FermatNo |
47 | 33, 43, 34, 46 | joinlmuladdmuld 10067 |
. . . . . . 7
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
48 | 39, 47 | eqtrd 2656 |
. . . . . 6
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
49 | 48 | adantr 481 |
. . . . 5
FermatNo FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
50 | 49 | oveq1d 6665 |
. . . 4
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
51 | 42, 5, 33 | subadd2d 10411 |
. . . . . . 7
FermatNo
FermatNo
FermatNo FermatNo |
52 | | eqcom 2629 |
. . . . . . 7
FermatNo
FermatNo FermatNo FermatNo |
53 | 51, 52 | syl6rbbr 279 |
. . . . . 6
FermatNo
FermatNo FermatNo FermatNo |
54 | | oveq2 6658 |
. . . . . . . . . . 11
FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo |
55 | 54 | oveq1d 6665 |
. . . . . . . . . 10
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
56 | 55 | oveq1d 6665 |
. . . . . . . . 9
FermatNo FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
57 | 56 | eqcoms 2630 |
. . . . . . . 8
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
58 | 33, 42 | mulcld 10060 |
. . . . . . . . . . 11
FermatNo FermatNo |
59 | 42, 5 | subcld 10392 |
. . . . . . . . . . 11
FermatNo |
60 | 58, 59 | subcld 10392 |
. . . . . . . . . 10
FermatNo FermatNo FermatNo |
61 | 60, 43, 34 | addassd 10062 |
. . . . . . . . 9
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
62 | | elnn0uz 11725 |
. . . . . . . . . . . . . . 15
|
63 | 62 | biimpi 206 |
. . . . . . . . . . . . . 14
|
64 | | elfznn0 12433 |
. . . . . . . . . . . . . . . 16
|
65 | 64, 30 | syl 17 |
. . . . . . . . . . . . . . 15
FermatNo |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . 14
FermatNo |
67 | | fveq2 6191 |
. . . . . . . . . . . . . 14
FermatNo FermatNo |
68 | 63, 66, 67 | fprodp1 14699 |
. . . . . . . . . . . . 13
FermatNo FermatNo FermatNo |
69 | 68 | eqcomd 2628 |
. . . . . . . . . . . 12
FermatNo FermatNo
FermatNo |
70 | 69 | oveq1d 6665 |
. . . . . . . . . . 11
FermatNo FermatNo FermatNo FermatNo FermatNo |
71 | | npcan1 10455 |
. . . . . . . . . . . 12
FermatNo FermatNo FermatNo |
72 | 42, 71 | syl 17 |
. . . . . . . . . . 11
FermatNo FermatNo |
73 | 70, 72 | oveq12d 6668 |
. . . . . . . . . 10
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
74 | | fzfid 12772 |
. . . . . . . . . . . 12
|
75 | 74, 66 | fprodcl 14682 |
. . . . . . . . . . 11
FermatNo |
76 | 75, 59, 42 | subadd23d 10414 |
. . . . . . . . . 10
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
77 | 73, 76 | eqtrd 2656 |
. . . . . . . . 9
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
78 | 42, 5 | nncand 10397 |
. . . . . . . . . 10
FermatNo FermatNo |
79 | 78 | oveq2d 6666 |
. . . . . . . . 9
FermatNo FermatNo FermatNo
FermatNo |
80 | 61, 77, 79 | 3eqtrd 2660 |
. . . . . . . 8
FermatNo FermatNo FermatNo FermatNo FermatNo |
81 | 57, 80 | sylan9eqr 2678 |
. . . . . . 7
FermatNo
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo |
82 | 81 | ex 450 |
. . . . . 6
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
83 | 53, 82 | sylbid 230 |
. . . . 5
FermatNo
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo |
84 | 83 | imp 445 |
. . . 4
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
85 | 50, 84 | eqtrd 2656 |
. . 3
FermatNo FermatNo FermatNo FermatNo
FermatNo |
86 | 22, 26, 85 | 3eqtrd 2660 |
. 2
FermatNo FermatNo FermatNo FermatNo |
87 | 86 | ex 450 |
1
FermatNo
FermatNo
FermatNo FermatNo |