Metamath Proof Explorer


Theorem expcllem

Description: Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005)

Ref Expression
Hypotheses expcllem.1 F
expcllem.2 x F y F x y F
expcllem.3 1 F
Assertion expcllem A F B 0 A B F

Proof

Step Hyp Ref Expression
1 expcllem.1 F
2 expcllem.2 x F y F x y F
3 expcllem.3 1 F
4 elnn0 B 0 B B = 0
5 oveq2 z = 1 A z = A 1
6 5 eleq1d z = 1 A z F A 1 F
7 6 imbi2d z = 1 A F A z F A F A 1 F
8 oveq2 z = w A z = A w
9 8 eleq1d z = w A z F A w F
10 9 imbi2d z = w A F A z F A F A w F
11 oveq2 z = w + 1 A z = A w + 1
12 11 eleq1d z = w + 1 A z F A w + 1 F
13 12 imbi2d z = w + 1 A F A z F A F A w + 1 F
14 oveq2 z = B A z = A B
15 14 eleq1d z = B A z F A B F
16 15 imbi2d z = B A F A z F A F A B F
17 1 sseli A F A
18 exp1 A A 1 = A
19 17 18 syl A F A 1 = A
20 19 eleq1d A F A 1 F A F
21 20 ibir A F A 1 F
22 2 caovcl A w F A F A w A F
23 22 ancoms A F A w F A w A F
24 23 adantlr A F w A w F A w A F
25 nnnn0 w w 0
26 expp1 A w 0 A w + 1 = A w A
27 17 25 26 syl2an A F w A w + 1 = A w A
28 27 eleq1d A F w A w + 1 F A w A F
29 28 adantr A F w A w F A w + 1 F A w A F
30 24 29 mpbird A F w A w F A w + 1 F
31 30 exp31 A F w A w F A w + 1 F
32 31 com12 w A F A w F A w + 1 F
33 32 a2d w A F A w F A F A w + 1 F
34 7 10 13 16 21 33 nnind B A F A B F
35 34 impcom A F B A B F
36 oveq2 B = 0 A B = A 0
37 exp0 A A 0 = 1
38 17 37 syl A F A 0 = 1
39 36 38 sylan9eqr A F B = 0 A B = 1
40 39 3 syl6eqel A F B = 0 A B F
41 35 40 jaodan A F B B = 0 A B F
42 4 41 sylan2b A F B 0 A B F