Step | Hyp | Ref
| Expression |
1 | | peano2nn0 11333 |
. . . . 5
|
2 | | vdwapval 15677 |
. . . . 5
AP
|
3 | 1, 2 | syl3an1 1359 |
. . . 4
AP
|
4 | | simp1 1061 |
. . . . . . . . . . . . 13
|
5 | 4 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
6 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
7 | | pncan 10287 |
. . . . . . . . . . . 12
|
8 | 5, 6, 7 | sylancl 694 |
. . . . . . . . . . 11
|
9 | 8 | oveq2d 6666 |
. . . . . . . . . 10
|
10 | 9 | eleq2d 2687 |
. . . . . . . . 9
|
11 | | nn0uz 11722 |
. . . . . . . . . . 11
|
12 | 4, 11 | syl6eleq 2711 |
. . . . . . . . . 10
|
13 | | elfzp12 12419 |
. . . . . . . . . 10
|
14 | 12, 13 | syl 17 |
. . . . . . . . 9
|
15 | 10, 14 | bitrd 268 |
. . . . . . . 8
|
16 | 15 | anbi1d 741 |
. . . . . . 7
|
17 | | andir 912 |
. . . . . . 7
|
18 | 16, 17 | syl6bb 276 |
. . . . . 6
|
19 | 18 | exbidv 1850 |
. . . . 5
|
20 | | df-rex 2918 |
. . . . 5
|
21 | | 19.43 1810 |
. . . . . 6
|
22 | 21 | bicomi 214 |
. . . . 5
|
23 | 19, 20, 22 | 3bitr4g 303 |
. . . 4
|
24 | 3, 23 | bitrd 268 |
. . 3
AP
|
25 | | nncn 11028 |
. . . . . . . . . . 11
|
26 | 25 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
27 | 26 | mul02d 10234 |
. . . . . . . . 9
|
28 | 27 | oveq2d 6666 |
. . . . . . . 8
|
29 | | nncn 11028 |
. . . . . . . . . 10
|
30 | 29 | 3ad2ant2 1083 |
. . . . . . . . 9
|
31 | 30 | addid1d 10236 |
. . . . . . . 8
|
32 | 28, 31 | eqtrd 2656 |
. . . . . . 7
|
33 | 32 | eqeq2d 2632 |
. . . . . 6
|
34 | | c0ex 10034 |
. . . . . . 7
|
35 | | oveq1 6657 |
. . . . . . . . 9
|
36 | 35 | oveq2d 6666 |
. . . . . . . 8
|
37 | 36 | eqeq2d 2632 |
. . . . . . 7
|
38 | 34, 37 | ceqsexv 3242 |
. . . . . 6
|
39 | | velsn 4193 |
. . . . . 6
|
40 | 33, 38, 39 | 3bitr4g 303 |
. . . . 5
|
41 | | simpr 477 |
. . . . . . . . . . . . . 14
|
42 | | 0p1e1 11132 |
. . . . . . . . . . . . . . 15
|
43 | 42 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
44 | 41, 43 | syl6eleq 2711 |
. . . . . . . . . . . . 13
|
45 | | 1zzd 11408 |
. . . . . . . . . . . . . 14
|
46 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
|
47 | 46 | nn0zd 11480 |
. . . . . . . . . . . . . 14
|
48 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . 14
|
50 | | fzsubel 12377 |
. . . . . . . . . . . . . 14
|
51 | 45, 47, 49, 45, 50 | syl22anc 1327 |
. . . . . . . . . . . . 13
|
52 | 44, 51 | mpbid 222 |
. . . . . . . . . . . 12
|
53 | | 1m1e0 11089 |
. . . . . . . . . . . . 13
|
54 | 53 | oveq1i 6660 |
. . . . . . . . . . . 12
|
55 | 52, 54 | syl6eleq 2711 |
. . . . . . . . . . 11
|
56 | 49 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
57 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
58 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
59 | 56, 57, 58 | subdird 10487 |
. . . . . . . . . . . . . . . 16
|
60 | 58 | mulid2d 10058 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
62 | 59, 61 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
63 | 62 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
64 | 56, 58 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
65 | 58, 64 | pncan3d 10395 |
. . . . . . . . . . . . . 14
|
66 | 63, 65 | eqtr2d 2657 |
. . . . . . . . . . . . 13
|
67 | 66 | oveq2d 6666 |
. . . . . . . . . . . 12
|
68 | 30 | adantr 481 |
. . . . . . . . . . . . 13
|
69 | | subcl 10280 |
. . . . . . . . . . . . . . 15
|
70 | 56, 6, 69 | sylancl 694 |
. . . . . . . . . . . . . 14
|
71 | 70, 58 | mulcld 10060 |
. . . . . . . . . . . . 13
|
72 | 68, 58, 71 | addassd 10062 |
. . . . . . . . . . . 12
|
73 | 67, 72 | eqtr4d 2659 |
. . . . . . . . . . 11
|
74 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
75 | 74 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
76 | 75 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
77 | 76 | rspcev 3309 |
. . . . . . . . . . 11
|
78 | 55, 73, 77 | syl2anc 693 |
. . . . . . . . . 10
|
79 | | eqeq1 2626 |
. . . . . . . . . . 11
|
80 | 79 | rexbidv 3052 |
. . . . . . . . . 10
|
81 | 78, 80 | syl5ibrcom 237 |
. . . . . . . . 9
|
82 | 81 | expimpd 629 |
. . . . . . . 8
|
83 | 82 | exlimdv 1861 |
. . . . . . 7
|
84 | | simpr 477 |
. . . . . . . . . . . 12
|
85 | | 0zd 11389 |
. . . . . . . . . . . . 13
|
86 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
|
87 | 86 | nn0zd 11480 |
. . . . . . . . . . . . . 14
|
88 | | peano2zm 11420 |
. . . . . . . . . . . . . 14
|
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . 13
|
90 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
91 | 90 | adantl 482 |
. . . . . . . . . . . . 13
|
92 | | 1zzd 11408 |
. . . . . . . . . . . . 13
|
93 | | fzaddel 12375 |
. . . . . . . . . . . . 13
|
94 | 85, 89, 91, 92, 93 | syl22anc 1327 |
. . . . . . . . . . . 12
|
95 | 84, 94 | mpbid 222 |
. . . . . . . . . . 11
|
96 | 86 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
97 | | npcan 10290 |
. . . . . . . . . . . . 13
|
98 | 96, 6, 97 | sylancl 694 |
. . . . . . . . . . . 12
|
99 | 98 | oveq2d 6666 |
. . . . . . . . . . 11
|
100 | 95, 99 | eleqtrd 2703 |
. . . . . . . . . 10
|
101 | 30 | adantr 481 |
. . . . . . . . . . . 12
|
102 | 26 | adantr 481 |
. . . . . . . . . . . 12
|
103 | 91 | zcnd 11483 |
. . . . . . . . . . . . 13
|
104 | 103, 102 | mulcld 10060 |
. . . . . . . . . . . 12
|
105 | 101, 102,
104 | addassd 10062 |
. . . . . . . . . . 11
|
106 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
107 | 103, 106,
102 | adddird 10065 |
. . . . . . . . . . . . 13
|
108 | 102, 104 | addcomd 10238 |
. . . . . . . . . . . . . 14
|
109 | 102 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
111 | 108, 110 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
112 | 107, 111 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
113 | 112 | oveq2d 6666 |
. . . . . . . . . . 11
|
114 | 105, 113 | eqtr4d 2659 |
. . . . . . . . . 10
|
115 | | ovex 6678 |
. . . . . . . . . . 11
|
116 | | eleq1 2689 |
. . . . . . . . . . . 12
|
117 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
118 | 117 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
119 | 118 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
120 | 116, 119 | anbi12d 747 |
. . . . . . . . . . 11
|
121 | 115, 120 | spcev 3300 |
. . . . . . . . . 10
|
122 | 100, 114,
121 | syl2anc 693 |
. . . . . . . . 9
|
123 | | eqeq1 2626 |
. . . . . . . . . . 11
|
124 | 123 | anbi2d 740 |
. . . . . . . . . 10
|
125 | 124 | exbidv 1850 |
. . . . . . . . 9
|
126 | 122, 125 | syl5ibrcom 237 |
. . . . . . . 8
|
127 | 126 | rexlimdva 3031 |
. . . . . . 7
|
128 | 83, 127 | impbid 202 |
. . . . . 6
|
129 | | nnaddcl 11042 |
. . . . . . . 8
|
130 | 129 | 3adant1 1079 |
. . . . . . 7
|
131 | | vdwapval 15677 |
. . . . . . 7
AP
|
132 | 130, 131 | syld3an2 1373 |
. . . . . 6
AP
|
133 | 128, 132 | bitr4d 271 |
. . . . 5
AP |
134 | 40, 133 | orbi12d 746 |
. . . 4
AP |
135 | | elun 3753 |
. . . 4
AP
AP |
136 | 134, 135 | syl6bbr 278 |
. . 3
AP |
137 | 24, 136 | bitrd 268 |
. 2
AP
AP |
138 | 137 | eqrdv 2620 |
1
AP AP |