MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  faclbnd6 Structured version   Visualization version   GIF version

Theorem faclbnd6 13509
Description: Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.)
Assertion
Ref Expression
faclbnd6 ((𝑁 ∈ ℕ0𝑀 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))

Proof of Theorem faclbnd6
Dummy variables 𝑚 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7024 . . . 4 (𝑚 = 0 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑0))
21oveq2d 7032 . . 3 (𝑚 = 0 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑0)))
3 oveq2 7024 . . . 4 (𝑚 = 0 → (𝑁 + 𝑚) = (𝑁 + 0))
43fveq2d 6542 . . 3 (𝑚 = 0 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 0)))
52, 4breq12d 4975 . 2 (𝑚 = 0 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑0)) ≤ (!‘(𝑁 + 0))))
6 oveq2 7024 . . . 4 (𝑚 = 𝑘 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑘))
76oveq2d 7032 . . 3 (𝑚 = 𝑘 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑘)))
8 oveq2 7024 . . . 4 (𝑚 = 𝑘 → (𝑁 + 𝑚) = (𝑁 + 𝑘))
98fveq2d 6542 . . 3 (𝑚 = 𝑘 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑘)))
107, 9breq12d 4975 . 2 (𝑚 = 𝑘 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))))
11 oveq2 7024 . . . 4 (𝑚 = (𝑘 + 1) → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑(𝑘 + 1)))
1211oveq2d 7032 . . 3 (𝑚 = (𝑘 + 1) → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))))
13 oveq2 7024 . . . 4 (𝑚 = (𝑘 + 1) → (𝑁 + 𝑚) = (𝑁 + (𝑘 + 1)))
1413fveq2d 6542 . . 3 (𝑚 = (𝑘 + 1) → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + (𝑘 + 1))))
1512, 14breq12d 4975 . 2 (𝑚 = (𝑘 + 1) → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1)))))
16 oveq2 7024 . . . 4 (𝑚 = 𝑀 → ((𝑁 + 1)↑𝑚) = ((𝑁 + 1)↑𝑀))
1716oveq2d 7032 . . 3 (𝑚 = 𝑀 → ((!‘𝑁) · ((𝑁 + 1)↑𝑚)) = ((!‘𝑁) · ((𝑁 + 1)↑𝑀)))
18 oveq2 7024 . . . 4 (𝑚 = 𝑀 → (𝑁 + 𝑚) = (𝑁 + 𝑀))
1918fveq2d 6542 . . 3 (𝑚 = 𝑀 → (!‘(𝑁 + 𝑚)) = (!‘(𝑁 + 𝑀)))
2017, 19breq12d 4975 . 2 (𝑚 = 𝑀 → (((!‘𝑁) · ((𝑁 + 1)↑𝑚)) ≤ (!‘(𝑁 + 𝑚)) ↔ ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))))
21 faccl 13493 . . . . 5 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
2221nnred 11501 . . . 4 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℝ)
2322leidd 11054 . . 3 (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (!‘𝑁))
24 nn0cn 11755 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
25 peano2cn 10659 . . . . . . 7 (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
2624, 25syl 17 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
2726exp0d 13354 . . . . 5 (𝑁 ∈ ℕ0 → ((𝑁 + 1)↑0) = 1)
2827oveq2d 7032 . . . 4 (𝑁 ∈ ℕ0 → ((!‘𝑁) · ((𝑁 + 1)↑0)) = ((!‘𝑁) · 1))
2921nncnd 11502 . . . . 5 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℂ)
3029mulid1d 10504 . . . 4 (𝑁 ∈ ℕ0 → ((!‘𝑁) · 1) = (!‘𝑁))
3128, 30eqtrd 2831 . . 3 (𝑁 ∈ ℕ0 → ((!‘𝑁) · ((𝑁 + 1)↑0)) = (!‘𝑁))
3224addid1d 10687 . . . 4 (𝑁 ∈ ℕ0 → (𝑁 + 0) = 𝑁)
3332fveq2d 6542 . . 3 (𝑁 ∈ ℕ0 → (!‘(𝑁 + 0)) = (!‘𝑁))
3423, 31, 333brtr4d 4994 . 2 (𝑁 ∈ ℕ0 → ((!‘𝑁) · ((𝑁 + 1)↑0)) ≤ (!‘(𝑁 + 0)))
3522adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘𝑁) ∈ ℝ)
36 peano2nn0 11785 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
3736nn0red 11804 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℝ)
38 reexpcl 13296 . . . . . . . . 9 (((𝑁 + 1) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℝ)
3937, 38sylan 580 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℝ)
4035, 39remulcld 10517 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ)
41 nnnn0 11752 . . . . . . . . . . 11 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℕ0)
4241nn0ge0d 11806 . . . . . . . . . 10 ((!‘𝑁) ∈ ℕ → 0 ≤ (!‘𝑁))
4321, 42syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ0 → 0 ≤ (!‘𝑁))
4443adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 0 ≤ (!‘𝑁))
4537adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 1) ∈ ℝ)
46 simpr 485 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
4736nn0ge0d 11806 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 0 ≤ (𝑁 + 1))
4847adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 0 ≤ (𝑁 + 1))
4945, 46, 48expge0d 13378 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 0 ≤ ((𝑁 + 1)↑𝑘))
5035, 39, 44, 49mulge0d 11065 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)))
5140, 50jca 512 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))))
52 nn0addcl 11780 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 𝑘) ∈ ℕ0)
5352faccld 13494 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℕ)
5453nnred 11501 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘(𝑁 + 𝑘)) ∈ ℝ)
55 nn0re 11754 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
56 peano2nn0 11785 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
5756nn0red 11804 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℝ)
58 readdcl 10466 . . . . . . . 8 ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → (𝑁 + (𝑘 + 1)) ∈ ℝ)
5955, 57, 58syl2an 595 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + (𝑘 + 1)) ∈ ℝ)
6045, 48, 59jca31 515 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ))
6151, 54, 60jca31 515 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)))
6261adantr 481 . . . 4 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)))
6332adantr 481 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 0) = 𝑁)
64 nn0ge0 11770 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
6564adantl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 0 ≤ 𝑘)
66 0re 10489 . . . . . . . . . 10 0 ∈ ℝ
67 nn0re 11754 . . . . . . . . . . 11 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
6867adantl 482 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 𝑘 ∈ ℝ)
6955adantr 481 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 𝑁 ∈ ℝ)
70 leadd2 10957 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘)))
7166, 68, 69, 70mp3an2i 1458 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (0 ≤ 𝑘 ↔ (𝑁 + 0) ≤ (𝑁 + 𝑘)))
7265, 71mpbid 233 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 0) ≤ (𝑁 + 𝑘))
7363, 72eqbrtrrd 4986 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → 𝑁 ≤ (𝑁 + 𝑘))
7452nn0red 11804 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 𝑘) ∈ ℝ)
75 1re 10487 . . . . . . . . 9 1 ∈ ℝ
76 leadd1 10956 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)))
7775, 76mp3an3 1442 . . . . . . . 8 ((𝑁 ∈ ℝ ∧ (𝑁 + 𝑘) ∈ ℝ) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)))
7869, 74, 77syl2anc 584 . . . . . . 7 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 ≤ (𝑁 + 𝑘) ↔ (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1)))
7973, 78mpbid 233 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 𝑘) + 1))
80 nn0cn 11755 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
81 ax-1cn 10441 . . . . . . . 8 1 ∈ ℂ
82 addass 10470 . . . . . . . 8 ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1)))
8381, 82mp3an3 1442 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1)))
8424, 80, 83syl2an 595 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((𝑁 + 𝑘) + 1) = (𝑁 + (𝑘 + 1)))
8579, 84breqtrd 4988 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1)))
8685anim1ci 615 . . . 4 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))))
87 lemul12a 11346 . . . 4 ((((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ∈ ℝ ∧ 0 ≤ ((!‘𝑁) · ((𝑁 + 1)↑𝑘))) ∧ (!‘(𝑁 + 𝑘)) ∈ ℝ) ∧ (((𝑁 + 1) ∈ ℝ ∧ 0 ≤ (𝑁 + 1)) ∧ (𝑁 + (𝑘 + 1)) ∈ ℝ)) → ((((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘)) ∧ (𝑁 + 1) ≤ (𝑁 + (𝑘 + 1))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1)))))
8862, 86, 87sylc 65 . . 3 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) ≤ ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))
89 expp1 13286 . . . . . . 7 (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))
9026, 89sylan 580 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((𝑁 + 1)↑(𝑘 + 1)) = (((𝑁 + 1)↑𝑘) · (𝑁 + 1)))
9190oveq2d 7032 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1))))
9229adantr 481 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘𝑁) ∈ ℂ)
93 expcl 13297 . . . . . . 7 (((𝑁 + 1) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℂ)
9426, 93sylan 580 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((𝑁 + 1)↑𝑘) ∈ ℂ)
9526adantr 481 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (𝑁 + 1) ∈ ℂ)
9692, 94, 95mulassd 10510 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)) = ((!‘𝑁) · (((𝑁 + 1)↑𝑘) · (𝑁 + 1))))
9791, 96eqtr4d 2834 . . . 4 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)))
9897adantr 481 . . 3 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) = (((!‘𝑁) · ((𝑁 + 1)↑𝑘)) · (𝑁 + 1)))
99 facp1 13488 . . . . . 6 ((𝑁 + 𝑘) ∈ ℕ0 → (!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)))
10052, 99syl 17 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)))
10184fveq2d 6542 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘((𝑁 + 𝑘) + 1)) = (!‘(𝑁 + (𝑘 + 1))))
10284oveq2d 7032 . . . . 5 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → ((!‘(𝑁 + 𝑘)) · ((𝑁 + 𝑘) + 1)) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))
103100, 101, 1023eqtr3d 2839 . . . 4 ((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))
104103adantr 481 . . 3 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → (!‘(𝑁 + (𝑘 + 1))) = ((!‘(𝑁 + 𝑘)) · (𝑁 + (𝑘 + 1))))
10588, 98, 1043brtr4d 4994 . 2 (((𝑁 ∈ ℕ0𝑘 ∈ ℕ0) ∧ ((!‘𝑁) · ((𝑁 + 1)↑𝑘)) ≤ (!‘(𝑁 + 𝑘))) → ((!‘𝑁) · ((𝑁 + 1)↑(𝑘 + 1))) ≤ (!‘(𝑁 + (𝑘 + 1))))
1065, 10, 15, 20, 34, 105nn0indd 11928 1 ((𝑁 ∈ ℕ0𝑀 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wcel 2081   class class class wbr 4962  cfv 6225  (class class class)co 7016  cc 10381  cr 10382  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388  cle 10522  cn 11486  0cn0 11745  cexp 13279  !cfa 13483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-n0 11746  df-z 11830  df-uz 12094  df-seq 13220  df-exp 13280  df-fac 13484
This theorem is referenced by:  eftlub  15295
  Copyright terms: Public domain W3C validator