Metamath Proof Explorer


Theorem expubnd

Description: An upper bound on A ^ N when 2 <_ A . (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion expubnd A N 0 2 A A N 2 N A 1 N

Proof

Step Hyp Ref Expression
1 simp1 A N 0 2 A A
2 2re 2
3 peano2rem A A 1
4 remulcl 2 A 1 2 A 1
5 2 3 4 sylancr A 2 A 1
6 5 3ad2ant1 A N 0 2 A 2 A 1
7 simp2 A N 0 2 A N 0
8 0le2 0 2
9 0re 0
10 letr 0 2 A 0 2 2 A 0 A
11 9 2 10 mp3an12 A 0 2 2 A 0 A
12 8 11 mpani A 2 A 0 A
13 12 imp A 2 A 0 A
14 resubcl A 2 A 2
15 2 14 mpan2 A A 2
16 leadd2 2 A A 2 2 A A - 2 + 2 A - 2 + A
17 2 16 mp3an1 A A 2 2 A A - 2 + 2 A - 2 + A
18 15 17 mpdan A 2 A A - 2 + 2 A - 2 + A
19 18 biimpa A 2 A A - 2 + 2 A - 2 + A
20 recn A A
21 2cn 2
22 npcan A 2 A - 2 + 2 = A
23 20 21 22 sylancl A A - 2 + 2 = A
24 23 adantr A 2 A A - 2 + 2 = A
25 ax-1cn 1
26 subdi 2 A 1 2 A 1 = 2 A 2 1
27 21 25 26 mp3an13 A 2 A 1 = 2 A 2 1
28 2times A 2 A = A + A
29 2t1e2 2 1 = 2
30 29 a1i A 2 1 = 2
31 28 30 oveq12d A 2 A 2 1 = A + A - 2
32 addsub A A 2 A + A - 2 = A - 2 + A
33 21 32 mp3an3 A A A + A - 2 = A - 2 + A
34 33 anidms A A + A - 2 = A - 2 + A
35 27 31 34 3eqtrrd A A - 2 + A = 2 A 1
36 20 35 syl A A - 2 + A = 2 A 1
37 36 adantr A 2 A A - 2 + A = 2 A 1
38 19 24 37 3brtr3d A 2 A A 2 A 1
39 13 38 jca A 2 A 0 A A 2 A 1
40 39 3adant2 A N 0 2 A 0 A A 2 A 1
41 leexp1a A 2 A 1 N 0 0 A A 2 A 1 A N 2 A 1 N
42 1 6 7 40 41 syl31anc A N 0 2 A A N 2 A 1 N
43 3 recnd A A 1
44 mulexp 2 A 1 N 0 2 A 1 N = 2 N A 1 N
45 21 44 mp3an1 A 1 N 0 2 A 1 N = 2 N A 1 N
46 43 45 sylan A N 0 2 A 1 N = 2 N A 1 N
47 46 3adant3 A N 0 2 A 2 A 1 N = 2 N A 1 N
48 42 47 breqtrd A N 0 2 A A N 2 N A 1 N