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

Theorem binom 15862
Description: The binomial theorem: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴𝑘) · (𝐵↑(𝑁𝑘)). Theorem 15-2.8 of [Gleason] p. 296. This part of the proof sets up the induction and does the base case, with the bulk of the work (the induction step) in binomlem 15861. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)
Assertion
Ref Expression
binom ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝑁

Proof of Theorem binom
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7437 . . . . . 6 (𝑥 = 0 → ((𝐴 + 𝐵)↑𝑥) = ((𝐴 + 𝐵)↑0))
2 oveq2 7437 . . . . . . 7 (𝑥 = 0 → (0...𝑥) = (0...0))
3 oveq1 7436 . . . . . . . . 9 (𝑥 = 0 → (𝑥C𝑘) = (0C𝑘))
4 oveq1 7436 . . . . . . . . . . 11 (𝑥 = 0 → (𝑥𝑘) = (0 − 𝑘))
54oveq2d 7445 . . . . . . . . . 10 (𝑥 = 0 → (𝐴↑(𝑥𝑘)) = (𝐴↑(0 − 𝑘)))
65oveq1d 7444 . . . . . . . . 9 (𝑥 = 0 → ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)) = ((𝐴↑(0 − 𝑘)) · (𝐵𝑘)))
73, 6oveq12d 7447 . . . . . . . 8 (𝑥 = 0 → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))))
87adantr 480 . . . . . . 7 ((𝑥 = 0 ∧ 𝑘 ∈ (0...𝑥)) → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))))
92, 8sumeq12dv 15738 . . . . . 6 (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))))
101, 9eqeq12d 2752 . . . . 5 (𝑥 = 0 → (((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) ↔ ((𝐴 + 𝐵)↑0) = Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘)))))
1110imbi2d 340 . . . 4 (𝑥 = 0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑0) = Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))))))
12 oveq2 7437 . . . . . 6 (𝑥 = 𝑛 → ((𝐴 + 𝐵)↑𝑥) = ((𝐴 + 𝐵)↑𝑛))
13 oveq2 7437 . . . . . . 7 (𝑥 = 𝑛 → (0...𝑥) = (0...𝑛))
14 oveq1 7436 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑥C𝑘) = (𝑛C𝑘))
15 oveq1 7436 . . . . . . . . . . 11 (𝑥 = 𝑛 → (𝑥𝑘) = (𝑛𝑘))
1615oveq2d 7445 . . . . . . . . . 10 (𝑥 = 𝑛 → (𝐴↑(𝑥𝑘)) = (𝐴↑(𝑛𝑘)))
1716oveq1d 7444 . . . . . . . . 9 (𝑥 = 𝑛 → ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)) = ((𝐴↑(𝑛𝑘)) · (𝐵𝑘)))
1814, 17oveq12d 7447 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))))
1918adantr 480 . . . . . . 7 ((𝑥 = 𝑛𝑘 ∈ (0...𝑥)) → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))))
2013, 19sumeq12dv 15738 . . . . . 6 (𝑥 = 𝑛 → Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))))
2112, 20eqeq12d 2752 . . . . 5 (𝑥 = 𝑛 → (((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) ↔ ((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘)))))
2221imbi2d 340 . . . 4 (𝑥 = 𝑛 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))))))
23 oveq2 7437 . . . . . 6 (𝑥 = (𝑛 + 1) → ((𝐴 + 𝐵)↑𝑥) = ((𝐴 + 𝐵)↑(𝑛 + 1)))
24 oveq2 7437 . . . . . . 7 (𝑥 = (𝑛 + 1) → (0...𝑥) = (0...(𝑛 + 1)))
25 oveq1 7436 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑥C𝑘) = ((𝑛 + 1)C𝑘))
26 oveq1 7436 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝑥𝑘) = ((𝑛 + 1) − 𝑘))
2726oveq2d 7445 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → (𝐴↑(𝑥𝑘)) = (𝐴↑((𝑛 + 1) − 𝑘)))
2827oveq1d 7444 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)) = ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘)))
2925, 28oveq12d 7447 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))
3029adantr 480 . . . . . . 7 ((𝑥 = (𝑛 + 1) ∧ 𝑘 ∈ (0...𝑥)) → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))
3124, 30sumeq12dv 15738 . . . . . 6 (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))
3223, 31eqeq12d 2752 . . . . 5 (𝑥 = (𝑛 + 1) → (((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) ↔ ((𝐴 + 𝐵)↑(𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘)))))
3332imbi2d 340 . . . 4 (𝑥 = (𝑛 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))))
34 oveq2 7437 . . . . . 6 (𝑥 = 𝑁 → ((𝐴 + 𝐵)↑𝑥) = ((𝐴 + 𝐵)↑𝑁))
35 oveq2 7437 . . . . . . 7 (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
36 oveq1 7436 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑥C𝑘) = (𝑁C𝑘))
37 oveq1 7436 . . . . . . . . . . 11 (𝑥 = 𝑁 → (𝑥𝑘) = (𝑁𝑘))
3837oveq2d 7445 . . . . . . . . . 10 (𝑥 = 𝑁 → (𝐴↑(𝑥𝑘)) = (𝐴↑(𝑁𝑘)))
3938oveq1d 7444 . . . . . . . . 9 (𝑥 = 𝑁 → ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)) = ((𝐴↑(𝑁𝑘)) · (𝐵𝑘)))
4036, 39oveq12d 7447 . . . . . . . 8 (𝑥 = 𝑁 → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
4140adantr 480 . . . . . . 7 ((𝑥 = 𝑁𝑘 ∈ (0...𝑥)) → ((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = ((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
4235, 41sumeq12dv 15738 . . . . . 6 (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
4334, 42eqeq12d 2752 . . . . 5 (𝑥 = 𝑁 → (((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘))) ↔ ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘)))))
4443imbi2d 340 . . . 4 (𝑥 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑥) = Σ𝑘 ∈ (0...𝑥)((𝑥C𝑘) · ((𝐴↑(𝑥𝑘)) · (𝐵𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))))
45 exp0 14102 . . . . . . . . 9 (𝐴 ∈ ℂ → (𝐴↑0) = 1)
46 exp0 14102 . . . . . . . . 9 (𝐵 ∈ ℂ → (𝐵↑0) = 1)
4745, 46oveqan12d 7448 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑0)) = (1 · 1))
48 1t1e1 12424 . . . . . . . 8 (1 · 1) = 1
4947, 48eqtrdi 2792 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑0) · (𝐵↑0)) = 1)
5049oveq2d 7445 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑0) · (𝐵↑0))) = (1 · 1))
5150, 48eqtrdi 2792 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑0) · (𝐵↑0))) = 1)
52 0z 12620 . . . . . 6 0 ∈ ℤ
53 ax-1cn 11209 . . . . . . 7 1 ∈ ℂ
5451, 53eqeltrdi 2848 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑0) · (𝐵↑0))) ∈ ℂ)
55 oveq2 7437 . . . . . . . . 9 (𝑘 = 0 → (0C𝑘) = (0C0))
56 0nn0 12537 . . . . . . . . . 10 0 ∈ ℕ0
57 bcn0 14345 . . . . . . . . . 10 (0 ∈ ℕ0 → (0C0) = 1)
5856, 57ax-mp 5 . . . . . . . . 9 (0C0) = 1
5955, 58eqtrdi 2792 . . . . . . . 8 (𝑘 = 0 → (0C𝑘) = 1)
60 oveq2 7437 . . . . . . . . . . 11 (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
61 0m0e0 12382 . . . . . . . . . . 11 (0 − 0) = 0
6260, 61eqtrdi 2792 . . . . . . . . . 10 (𝑘 = 0 → (0 − 𝑘) = 0)
6362oveq2d 7445 . . . . . . . . 9 (𝑘 = 0 → (𝐴↑(0 − 𝑘)) = (𝐴↑0))
64 oveq2 7437 . . . . . . . . 9 (𝑘 = 0 → (𝐵𝑘) = (𝐵↑0))
6563, 64oveq12d 7447 . . . . . . . 8 (𝑘 = 0 → ((𝐴↑(0 − 𝑘)) · (𝐵𝑘)) = ((𝐴↑0) · (𝐵↑0)))
6659, 65oveq12d 7447 . . . . . . 7 (𝑘 = 0 → ((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))) = (1 · ((𝐴↑0) · (𝐵↑0))))
6766fsum1 15779 . . . . . 6 ((0 ∈ ℤ ∧ (1 · ((𝐴↑0) · (𝐵↑0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))) = (1 · ((𝐴↑0) · (𝐵↑0))))
6852, 54, 67sylancr 587 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))) = (1 · ((𝐴↑0) · (𝐵↑0))))
69 addcl 11233 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
7069exp0d 14176 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑0) = 1)
7151, 68, 703eqtr4rd 2787 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑0) = Σ𝑘 ∈ (0...0)((0C𝑘) · ((𝐴↑(0 − 𝑘)) · (𝐵𝑘))))
72 simprl 771 . . . . . . 7 ((𝑛 ∈ ℕ0 ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝐴 ∈ ℂ)
73 simprr 773 . . . . . . 7 ((𝑛 ∈ ℕ0 ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝐵 ∈ ℂ)
74 simpl 482 . . . . . . 7 ((𝑛 ∈ ℕ0 ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝑛 ∈ ℕ0)
75 id 22 . . . . . . 7 (((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))) → ((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))))
7672, 73, 74, 75binomlem 15861 . . . . . 6 (((𝑛 ∈ ℕ0 ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘)))) → ((𝐴 + 𝐵)↑(𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))
7776exp31 419 . . . . 5 (𝑛 ∈ ℕ0 → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘))) → ((𝐴 + 𝐵)↑(𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))))
7877a2d 29 . . . 4 (𝑛 ∈ ℕ0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴↑(𝑛𝑘)) · (𝐵𝑘)))) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴↑((𝑛 + 1) − 𝑘)) · (𝐵𝑘))))))
7911, 22, 33, 44, 71, 78nn0ind 12709 . . 3 (𝑁 ∈ ℕ0 → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘)))))
8079impcom 407 . 2 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
81803impa 1110 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁𝑘)) · (𝐵𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  (class class class)co 7429  cc 11149  0cc0 11151  1c1 11152   + caddc 11154   · cmul 11156  cmin 11488  0cn0 12522  cz 12609  ...cfz 13543  cexp 14098  Ccbc 14337  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-inf2 9677  ax-cnex 11207  ax-resscn 11208  ax-1cn 11209  ax-icn 11210  ax-addcl 11211  ax-addrcl 11212  ax-mulcl 11213  ax-mulrcl 11214  ax-mulcom 11215  ax-addass 11216  ax-mulass 11217  ax-distr 11218  ax-i2m1 11219  ax-1ne0 11220  ax-1rid 11221  ax-rnegex 11222  ax-rrecex 11223  ax-cnre 11224  ax-pre-lttri 11225  ax-pre-lttrn 11226  ax-pre-ltadd 11227  ax-pre-mulgt0 11228  ax-pre-sup 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-int 4945  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-se 5636  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-om 7884  df-1st 8010  df-2nd 8011  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-er 8741  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-sup 9478  df-oi 9546  df-card 9975  df-pnf 11293  df-mnf 11294  df-xr 11295  df-ltxr 11296  df-le 11297  df-sub 11490  df-neg 11491  df-div 11917  df-nn 12263  df-2 12325  df-3 12326  df-n0 12523  df-z 12610  df-uz 12875  df-rp 13031  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  binom1p  15863  efaddlem  16125  basellem3  27116  lcmineqlem1  42008  jm2.22  42985  binomcxplemnn0  44346  altgsumbc  48241
  Copyright terms: Public domain W3C validator