faclbnd4lem4 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem faclbnd4lem4 6965

Description: Lemma for faclbnd4 6966. Prove the 0 < N case by induction on K.

**Assertion**
Ref	Expression
faclbnd4lem4	⊢ ((N ∈ ℕ ⋀ K ∈ ℕ₀ ⋀ M ∈ ℕ₀) → ((N↑K) · (M↑N)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N)))

**Proof of Theorem faclbnd4lem4**
Step	Hyp	Ref	Expression
1		opreq1 3982	. . . . . 6 ⊢ (n = N → (n↑K) = (N↑K))
2		opreq2 3983	. . . . . 6 ⊢ (n = N → (M↑n) = (M↑N))
3	1, 2	opreq12d 3992	. . . . 5 ⊢ (n = N → ((n↑K) · (M↑n)) = ((N↑K) · (M↑N)))
4		fveq2 3738	. . . . . 6 ⊢ (n = N → (! ‘n) = (! ‘N))
5	4	opreq2d 3990	. . . . 5 ⊢ (n = N → (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n)) = (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N)))
6	3, 5	breq12d 2644	. . . 4 ⊢ (n = N → (((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n)) ↔ ((N↑K) · (M↑N)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N))))
7	6	rcla4va 1882	. . 3 ⊢ ((N ∈ ℕ ⋀ ∀n ∈ ℕ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n))) → ((N↑K) · (M↑N)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N)))
8		faclbnd4lem3 6964	. . . . . . . . . . . . . 14 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ (n − 1) = 0) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1))))
9		nnge1t 5949	. . . . . . . . . . . . . . . . 17 ⊢ (n ∈ ℕ → 1 ≤ n)
10	9	adantr 391	. . . . . . . . . . . . . . . 16 ⊢ ((n ∈ ℕ ⋀ n ≤ 1) → 1 ≤ n)
11		nnret 5935	. . . . . . . . . . . . . . . . . . 19 ⊢ (n ∈ ℕ → n ∈ ℝ)
12		1re 5448	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ
13		letri3t 5530	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((n ∈ ℝ ⋀ 1 ∈ ℝ) → (n = 1 ↔ (n ≤ 1 ⋀ 1 ≤ n)))
14	12, 13	mpan2 700	. . . . . . . . . . . . . . . . . . 19 ⊢ (n ∈ ℝ → (n = 1 ↔ (n ≤ 1 ⋀ 1 ≤ n)))
15	11, 14	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ (n ∈ ℕ → (n = 1 ↔ (n ≤ 1 ⋀ 1 ≤ n)))
16	15	biimpar 419	. . . . . . . . . . . . . . . . 17 ⊢ ((n ∈ ℕ ⋀ (n ≤ 1 ⋀ 1 ≤ n)) → n = 1)
17	16	anassrs 444	. . . . . . . . . . . . . . . 16 ⊢ (((n ∈ ℕ ⋀ n ≤ 1) ⋀ 1 ≤ n) → n = 1)
18	10, 17	mpdan 708	. . . . . . . . . . . . . . 15 ⊢ ((n ∈ ℕ ⋀ n ≤ 1) → n = 1)
19		opreq1 3982	. . . . . . . . . . . . . . . 16 ⊢ (n = 1 → (n − 1) = (1 − 1))
20		ax1cn 5282	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
21	20	subid 5404	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
22	19, 21	syl6eq 1530	. . . . . . . . . . . . . . 15 ⊢ (n = 1 → (n − 1) = 0)
23	18, 22	syl 10	. . . . . . . . . . . . . 14 ⊢ ((n ∈ ℕ ⋀ n ≤ 1) → (n − 1) = 0)
24	8, 23	sylan2 454	. . . . . . . . . . . . 13 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ (n ∈ ℕ ⋀ n ≤ 1)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1))))
25	24	a1d 12	. . . . . . . . . . . 12 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ (n ∈ ℕ ⋀ n ≤ 1)) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
26		1nn 5940	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ
27		nnsubt 5963	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℕ ⋀ n ∈ ℕ) → (1 < n ↔ (n − 1) ∈ ℕ))
28	26, 27	mpan 699	. . . . . . . . . . . . . . 15 ⊢ (n ∈ ℕ → (1 < n ↔ (n − 1) ∈ ℕ))
29	28	biimpa 418	. . . . . . . . . . . . . 14 ⊢ ((n ∈ ℕ ⋀ 1 < n) → (n − 1) ∈ ℕ)
30		opreq1 3982	. . . . . . . . . . . . . . . . 17 ⊢ (m = (n − 1) → (m↑j) = ((n − 1)↑j))
31		opreq2 3983	. . . . . . . . . . . . . . . . 17 ⊢ (m = (n − 1) → (M↑m) = (M↑(n − 1)))
32	30, 31	opreq12d 3992	. . . . . . . . . . . . . . . 16 ⊢ (m = (n − 1) → ((m↑j) · (M↑m)) = (((n − 1)↑j) · (M↑(n − 1))))
33		fveq2 3738	. . . . . . . . . . . . . . . . 17 ⊢ (m = (n − 1) → (! ‘m) = (! ‘(n − 1)))
34	33	opreq2d 3990	. . . . . . . . . . . . . . . 16 ⊢ (m = (n − 1) → (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) = (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1))))
35	32, 34	breq12d 2644	. . . . . . . . . . . . . . 15 ⊢ (m = (n − 1) → (((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) ↔ (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
36	35	rcla4v 1880	. . . . . . . . . . . . . 14 ⊢ ((n − 1) ∈ ℕ → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
37	29, 36	syl 10	. . . . . . . . . . . . 13 ⊢ ((n ∈ ℕ ⋀ 1 < n) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
38	37	adantl 390	. . . . . . . . . . . 12 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ (n ∈ ℕ ⋀ 1 < n)) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
39	25, 38	jaodan 428	. . . . . . . . . . 11 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ ((n ∈ ℕ ⋀ n ≤ 1) ⋁ (n ∈ ℕ ⋀ 1 < n))) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
40		lelttrit 5635	. . . . . . . . . . . . . . 15 ⊢ ((n ∈ ℝ ⋀ 1 ∈ ℝ) → (n ≤ 1 ⋁ 1 < n))
41	12, 40	mpan2 700	. . . . . . . . . . . . . 14 ⊢ (n ∈ ℝ → (n ≤ 1 ⋁ 1 < n))
42	11, 41	syl 10	. . . . . . . . . . . . 13 ⊢ (n ∈ ℕ → (n ≤ 1 ⋁ 1 < n))
43	42	ancli 296	. . . . . . . . . . . 12 ⊢ (n ∈ ℕ → (n ∈ ℕ ⋀ (n ≤ 1 ⋁ 1 < n)))
44		andi 607	. . . . . . . . . . . 12 ⊢ ((n ∈ ℕ ⋀ (n ≤ 1 ⋁ 1 < n)) ↔ ((n ∈ ℕ ⋀ n ≤ 1) ⋁ (n ∈ ℕ ⋀ 1 < n)))
45	43, 44	sylib 198	. . . . . . . . . . 11 ⊢ (n ∈ ℕ → ((n ∈ ℕ ⋀ n ≤ 1) ⋁ (n ∈ ℕ ⋀ 1 < n)))
46	39, 45	sylan2 454	. . . . . . . . . 10 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ n ∈ ℕ) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → (((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1)))))
47		faclbnd4lem2 6963	. . . . . . . . . . 11 ⊢ ((M ∈ ℕ₀ ⋀ j ∈ ℕ₀ ⋀ n ∈ ℕ) → ((((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1))) → ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
48	47	3expa 837	. . . . . . . . . 10 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ n ∈ ℕ) → ((((n − 1)↑j) · (M↑(n − 1))) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘(n − 1))) → ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
49	46, 48	syld 27	. . . . . . . . 9 ⊢ (((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) ⋀ n ∈ ℕ) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
50	49	r19.21adva 1726	. . . . . . . 8 ⊢ ((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) → (∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)) → ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
51		opreq1 3982	. . . . . . . . . . 11 ⊢ (n = m → (n↑j) = (m↑j))
52		opreq2 3983	. . . . . . . . . . 11 ⊢ (n = m → (M↑n) = (M↑m))
53	51, 52	opreq12d 3992	. . . . . . . . . 10 ⊢ (n = m → ((n↑j) · (M↑n)) = ((m↑j) · (M↑m)))
54		fveq2 3738	. . . . . . . . . . 11 ⊢ (n = m → (! ‘n) = (! ‘m))
55	54	opreq2d 3990	. . . . . . . . . 10 ⊢ (n = m → (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)) = (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)))
56	53, 55	breq12d 2644	. . . . . . . . 9 ⊢ (n = m → (((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)) ↔ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m))))
57	56	cbvralv 1807	. . . . . . . 8 ⊢ (∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)) ↔ ∀m ∈ ℕ ((m↑j) · (M↑m)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘m)))
58	50, 57	syl5ib 206	. . . . . . 7 ⊢ ((M ∈ ℕ₀ ⋀ j ∈ ℕ₀) → (∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)) → ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
59	58	expcom 374	. . . . . 6 ⊢ (j ∈ ℕ₀ → (M ∈ ℕ₀ → (∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)) → ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n)))))
60	59	a2d 13	. . . . 5 ⊢ (j ∈ ℕ₀ → ((M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n))) → (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n)))))
61		faclbnd3 6961	. . . . . . . 8 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ₀) → (M↑n) ≤ ((M↑M) · (! ‘n)))
62		nnnn0t 6112	. . . . . . . 8 ⊢ (n ∈ ℕ → n ∈ ℕ₀)
63	61, 62	sylan2 454	. . . . . . 7 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → (M↑n) ≤ ((M↑M) · (! ‘n)))
64		nncnt 5936	. . . . . . . . . . 11 ⊢ (n ∈ ℕ → n ∈ ℂ)
65		exp0t 6584	. . . . . . . . . . 11 ⊢ (n ∈ ℂ → (n↑0) = 1)
66	64, 65	syl 10	. . . . . . . . . 10 ⊢ (n ∈ ℕ → (n↑0) = 1)
67	66	opreq1d 3989	. . . . . . . . 9 ⊢ (n ∈ ℕ → ((n↑0) · (M↑n)) = (1 · (M↑n)))
68	67	adantl 390	. . . . . . . 8 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → ((n↑0) · (M↑n)) = (1 · (M↑n)))
69		expclt 6594	. . . . . . . . . 10 ⊢ ((M ∈ ℂ ⋀ n ∈ ℕ₀) → (M↑n) ∈ ℂ)
70		nn0cnt 6115	. . . . . . . . . 10 ⊢ (M ∈ ℕ₀ → M ∈ ℂ)
71	69, 70, 62	syl2an 457	. . . . . . . . 9 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → (M↑n) ∈ ℂ)
72		mulid2t 5430	. . . . . . . . 9 ⊢ ((M↑n) ∈ ℂ → (1 · (M↑n)) = (M↑n))
73	71, 72	syl 10	. . . . . . . 8 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → (1 · (M↑n)) = (M↑n))
74	68, 73	eqtrd 1514	. . . . . . 7 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → ((n↑0) · (M↑n)) = (M↑n))
75		sq0 6648	. . . . . . . . . . . . . 14 ⊢ (0↑2) = 0
76	75	opreq2i 3986	. . . . . . . . . . . . 13 ⊢ (2↑(0↑2)) = (2↑0)
77		2cn 5986	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
78		exp0t 6584	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ → (2↑0) = 1)
79	77, 78	ax-mp 7	. . . . . . . . . . . . 13 ⊢ (2↑0) = 1
80	76, 79	eqtr 1502	. . . . . . . . . . . 12 ⊢ (2↑(0↑2)) = 1
81	80	a1i 8	. . . . . . . . . . 11 ⊢ (M ∈ ℕ₀ → (2↑(0↑2)) = 1)
82		ax0id 5294	. . . . . . . . . . . . 13 ⊢ (M ∈ ℂ → (M + 0) = M)
83	70, 82	syl 10	. . . . . . . . . . . 12 ⊢ (M ∈ ℕ₀ → (M + 0) = M)
84	83	opreq2d 3990	. . . . . . . . . . 11 ⊢ (M ∈ ℕ₀ → (M↑(M + 0)) = (M↑M))
85	81, 84	opreq12d 3992	. . . . . . . . . 10 ⊢ (M ∈ ℕ₀ → ((2↑(0↑2)) · (M↑(M + 0))) = (1 · (M↑M)))
86		expclt 6594	. . . . . . . . . . . 12 ⊢ ((M ∈ ℂ ⋀ M ∈ ℕ₀) → (M↑M) ∈ ℂ)
87	70, 86	mpancom 709	. . . . . . . . . . 11 ⊢ (M ∈ ℕ₀ → (M↑M) ∈ ℂ)
88		mulid2t 5430	. . . . . . . . . . 11 ⊢ ((M↑M) ∈ ℂ → (1 · (M↑M)) = (M↑M))
89	87, 88	syl 10	. . . . . . . . . 10 ⊢ (M ∈ ℕ₀ → (1 · (M↑M)) = (M↑M))
90	85, 89	eqtrd 1514	. . . . . . . . 9 ⊢ (M ∈ ℕ₀ → ((2↑(0↑2)) · (M↑(M + 0))) = (M↑M))
91	90	opreq1d 3989	. . . . . . . 8 ⊢ (M ∈ ℕ₀ → (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)) = ((M↑M) · (! ‘n)))
92	91	adantr 391	. . . . . . 7 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)) = ((M↑M) · (! ‘n)))
93	63, 74, 92	3brtr4d 2658	. . . . . 6 ⊢ ((M ∈ ℕ₀ ⋀ n ∈ ℕ) → ((n↑0) · (M↑n)) ≤ (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)))
94	93	r19.21aiva 1721	. . . . 5 ⊢ (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑0) · (M↑n)) ≤ (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)))
95		opreq2 3983	. . . . . . . . 9 ⊢ (m = 0 → (n↑m) = (n↑0))
96	95	opreq1d 3989	. . . . . . . 8 ⊢ (m = 0 → ((n↑m) · (M↑n)) = ((n↑0) · (M↑n)))
97		opreq1 3982	. . . . . . . . . . 11 ⊢ (m = 0 → (m↑2) = (0↑2))
98	97	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = 0 → (2↑(m↑2)) = (2↑(0↑2)))
99		opreq2 3983	. . . . . . . . . . 11 ⊢ (m = 0 → (M + m) = (M + 0))
100	99	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = 0 → (M↑(M + m)) = (M↑(M + 0)))
101	98, 100	opreq12d 3992	. . . . . . . . 9 ⊢ (m = 0 → ((2↑(m↑2)) · (M↑(M + m))) = ((2↑(0↑2)) · (M↑(M + 0))))
102	101	opreq1d 3989	. . . . . . . 8 ⊢ (m = 0 → (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) = (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)))
103	96, 102	breq12d 2644	. . . . . . 7 ⊢ (m = 0 → (((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ((n↑0) · (M↑n)) ≤ (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n))))
104	103	ralbidv 1670	. . . . . 6 ⊢ (m = 0 → (∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ∀n ∈ ℕ ((n↑0) · (M↑n)) ≤ (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n))))
105	104	imbi2d 615	. . . . 5 ⊢ (m = 0 → ((M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n))) ↔ (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑0) · (M↑n)) ≤ (((2↑(0↑2)) · (M↑(M + 0))) · (! ‘n)))))
106		opreq2 3983	. . . . . . . . 9 ⊢ (m = j → (n↑m) = (n↑j))
107	106	opreq1d 3989	. . . . . . . 8 ⊢ (m = j → ((n↑m) · (M↑n)) = ((n↑j) · (M↑n)))
108		opreq1 3982	. . . . . . . . . . 11 ⊢ (m = j → (m↑2) = (j↑2))
109	108	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = j → (2↑(m↑2)) = (2↑(j↑2)))
110		opreq2 3983	. . . . . . . . . . 11 ⊢ (m = j → (M + m) = (M + j))
111	110	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = j → (M↑(M + m)) = (M↑(M + j)))
112	109, 111	opreq12d 3992	. . . . . . . . 9 ⊢ (m = j → ((2↑(m↑2)) · (M↑(M + m))) = ((2↑(j↑2)) · (M↑(M + j))))
113	112	opreq1d 3989	. . . . . . . 8 ⊢ (m = j → (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) = (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)))
114	107, 113	breq12d 2644	. . . . . . 7 ⊢ (m = j → (((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n))))
115	114	ralbidv 1670	. . . . . 6 ⊢ (m = j → (∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n))))
116	115	imbi2d 615	. . . . 5 ⊢ (m = j → ((M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n))) ↔ (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑j) · (M↑n)) ≤ (((2↑(j↑2)) · (M↑(M + j))) · (! ‘n)))))
117		opreq2 3983	. . . . . . . . 9 ⊢ (m = (j + 1) → (n↑m) = (n↑(j + 1)))
118	117	opreq1d 3989	. . . . . . . 8 ⊢ (m = (j + 1) → ((n↑m) · (M↑n)) = ((n↑(j + 1)) · (M↑n)))
119		opreq1 3982	. . . . . . . . . . 11 ⊢ (m = (j + 1) → (m↑2) = ((j + 1)↑2))
120	119	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = (j + 1) → (2↑(m↑2)) = (2↑((j + 1)↑2)))
121		opreq2 3983	. . . . . . . . . . 11 ⊢ (m = (j + 1) → (M + m) = (M + (j + 1)))
122	121	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = (j + 1) → (M↑(M + m)) = (M↑(M + (j + 1))))
123	120, 122	opreq12d 3992	. . . . . . . . 9 ⊢ (m = (j + 1) → ((2↑(m↑2)) · (M↑(M + m))) = ((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))))
124	123	opreq1d 3989	. . . . . . . 8 ⊢ (m = (j + 1) → (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) = (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n)))
125	118, 124	breq12d 2644	. . . . . . 7 ⊢ (m = (j + 1) → (((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
126	125	ralbidv 1670	. . . . . 6 ⊢ (m = (j + 1) → (∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n))))
127	126	imbi2d 615	. . . . 5 ⊢ (m = (j + 1) → ((M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n))) ↔ (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑(j + 1)) · (M↑n)) ≤ (((2↑((j + 1)↑2)) · (M↑(M + (j + 1)))) · (! ‘n)))))
128		opreq2 3983	. . . . . . . . 9 ⊢ (m = K → (n↑m) = (n↑K))
129	128	opreq1d 3989	. . . . . . . 8 ⊢ (m = K → ((n↑m) · (M↑n)) = ((n↑K) · (M↑n)))
130		opreq1 3982	. . . . . . . . . . 11 ⊢ (m = K → (m↑2) = (K↑2))
131	130	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = K → (2↑(m↑2)) = (2↑(K↑2)))
132		opreq2 3983	. . . . . . . . . . 11 ⊢ (m = K → (M + m) = (M + K))
133	132	opreq2d 3990	. . . . . . . . . 10 ⊢ (m = K → (M↑(M + m)) = (M↑(M + K)))
134	131, 133	opreq12d 3992	. . . . . . . . 9 ⊢ (m = K → ((2↑(m↑2)) · (M↑(M + m))) = ((2↑(K↑2)) · (M↑(M + K))))
135	134	opreq1d 3989	. . . . . . . 8 ⊢ (m = K → (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) = (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n)))
136	129, 135	breq12d 2644	. . . . . . 7 ⊢ (m = K → (((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n))))
137	136	ralbidv 1670	. . . . . 6 ⊢ (m = K → (∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n)) ↔ ∀n ∈ ℕ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n))))
138	137	imbi2d 615	. . . . 5 ⊢ (m = K → ((M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑m) · (M↑n)) ≤ (((2↑(m↑2)) · (M↑(M + m))) · (! ‘n))) ↔ (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n)))))
139	60, 94, 105, 116, 127, 138	nn0indALT 6222	. . . 4 ⊢ (K ∈ ℕ₀ → (M ∈ ℕ₀ → ∀n ∈ ℕ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n))))
140	139	imp 350	. . 3 ⊢ ((K ∈ ℕ₀ ⋀ M ∈ ℕ₀) → ∀n ∈ ℕ ((n↑K) · (M↑n)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘n)))
141	7, 140	sylan2 454	. 2 ⊢ ((N ∈ ℕ ⋀ (K ∈ ℕ₀ ⋀ M ∈ ℕ₀)) → ((N↑K) · (M↑N)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N)))
142	141	3impb 833	1 ⊢ ((N ∈ ℕ ⋀ K ∈ ℕ₀ ⋀ M ∈ ℕ₀) → ((N↑K) · (M↑N)) ≤ (((2↑(K↑2)) · (M↑(M + K))) · (! ‘N)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋁ wo 222 ⋀ wa 223 ⋀ w3a 779 = wceq 960 ∈ wcel 962 ∀wral 1652 class class class wbr 2632 ‘cfv 3196 (class class class)co 3977 ℂcc 5245 ℝcr 5246 0cc0 5247 1c1 5248 + caddc 5250 · cmul 5252 − cmin 5305 ≤ cle 5308 ℕcn 5309 ℕ₀cn0 5310 < clt 5499 2c2 5967 ↑cexp 6581 !cfa 6945

This theorem is referenced by: faclbnd4 6966

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 966 ax-gen 967 ax-8 968 ax-9 969 ax-10 970 ax-11 971 ax-12 972 ax-13 973 ax-14 974 ax-17 975 ax-4 977 ax-5o 979 ax-6o 982 ax-9o 1129 ax-10o 1146 ax-16 1216 ax-11o 1224 ax-ext 1466 ax-rep 2706 ax-sep 2716 ax-nul 2723 ax-pow 2756 ax-pr 2793 ax-un 2880 ax-inf2 4637

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 780 df-3an 781 df-ex 985 df-sb 1178 df-eu 1388 df-mo 1389 df-clab 1471 df-cleq 1476 df-clel&