Theorem ostth2lem4

Description: Lemma for ostth2 . (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
	padic.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
	ostth.k	$$⊢K=\left(x\in \mathbb{Q}⟼if\left(x=0,0,1\right)\right)$$
	ostth.1	$$⊢\phi \to F\in A$$
	ostth2.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
	ostth2.3	$$⊢\phi \to 1<F\left(N\right)$$
	ostth2.4	$$⊢R=\frac{\log F\left(N\right)}{\log N}$$
	ostth2.5	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge 2}$$
	ostth2.6	$$⊢S=\frac{\log F\left(M\right)}{\log M}$$
	ostth2.7	$$⊢T=if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)$$
	ostth2.8	$$⊢U=\frac{\log N}{\log M}$$
Assertion	ostth2lem4	$$⊢\phi \to \left(1<F\left(M\right)\wedge R\le S\right)$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
3		padic.j	$$⊢J=\left(q\in \mathbb{P}⟼\left(x\in \mathbb{Q}⟼if\left(x=0,0,q^{-\left(q\mathrm{pCnt}x\right)}\right)\right)\right)$$
4		ostth.k	$$⊢K=\left(x\in \mathbb{Q}⟼if\left(x=0,0,1\right)\right)$$
5		ostth.1	$$⊢\phi \to F\in A$$
6		ostth2.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
7		ostth2.3	$$⊢\phi \to 1<F\left(N\right)$$
8		ostth2.4	$$⊢R=\frac{\log F\left(N\right)}{\log N}$$
9		ostth2.5	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge 2}$$
10		ostth2.6	$$⊢S=\frac{\log F\left(M\right)}{\log M}$$
11		ostth2.7	$$⊢T=if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)$$
12		ostth2.8	$$⊢U=\frac{\log N}{\log M}$$
13		1re	$$⊢1\in ℝ$$
14		eluz2b2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{N}\wedge 1<N\right)$$
15	6 14	sylib	$$⊢\phi \to \left(N\in \mathbb{N}\wedge 1<N\right)$$
16	15	simpld	$$⊢\phi \to N\in \mathbb{N}$$
17		nnq	$$⊢N\in \mathbb{N}\to N\in \mathbb{Q}$$
18	16 17	syl	$$⊢\phi \to N\in \mathbb{Q}$$
19	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
20	2 19	abvcl	$$⊢\left(F\in A\wedge N\in \mathbb{Q}\right)\to F\left(N\right)\in ℝ$$
21	5 18 20	syl2anc	$$⊢\phi \to F\left(N\right)\in ℝ$$
22		ltnle	$$⊢\left(1\in ℝ\wedge F\left(N\right)\in ℝ\right)\to \left(1<F\left(N\right)\leftrightarrow \neg F\left(N\right)\le 1\right)$$
23	13 21 22	sylancr	$$⊢\phi \to \left(1<F\left(N\right)\leftrightarrow \neg F\left(N\right)\le 1\right)$$
24	7 23	mpbid	$$⊢\phi \to \neg F\left(N\right)\le 1$$
25		eluz2b2	$$⊢M\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(M\in \mathbb{N}\wedge 1<M\right)$$
26	9 25	sylib	$$⊢\phi \to \left(M\in \mathbb{N}\wedge 1<M\right)$$
27	26	simpld	$$⊢\phi \to M\in \mathbb{N}$$
28		nnq	$$⊢M\in \mathbb{N}\to M\in \mathbb{Q}$$
29	27 28	syl	$$⊢\phi \to M\in \mathbb{Q}$$
30	2 19	abvcl	$$⊢\left(F\in A\wedge M\in \mathbb{Q}\right)\to F\left(M\right)\in ℝ$$
31	5 29 30	syl2anc	$$⊢\phi \to F\left(M\right)\in ℝ$$
32		ifcl	$$⊢\left(1\in ℝ\wedge F\left(M\right)\in ℝ\right)\to if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)\in ℝ$$
33	13 31 32	sylancr	$$⊢\phi \to if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)\in ℝ$$
34	11 33	eqeltrid	$$⊢\phi \to T\in ℝ$$
35		0red	$$⊢\phi \to 0\in ℝ$$
36	13	a1i	$$⊢\phi \to 1\in ℝ$$
37		0lt1	$$⊢0<1$$
38	37	a1i	$$⊢\phi \to 0<1$$
39		max2	$$⊢\left(F\left(M\right)\in ℝ\wedge 1\in ℝ\right)\to 1\le if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)$$
40	31 13 39	sylancl	$$⊢\phi \to 1\le if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)$$
41	40 11	breqtrrdi	$$⊢\phi \to 1\le T$$
42	35 36 34 38 41	ltletrd	$$⊢\phi \to 0<T$$
43	34 42	elrpd	$$⊢\phi \to T\in {ℝ}^{+}$$
44	16	nnrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
45	44	relogcld	$$⊢\phi \to \log N\in ℝ$$
46	27	nnred	$$⊢\phi \to M\in ℝ$$
47	26	simprd	$$⊢\phi \to 1<M$$
48	46 47	rplogcld	$$⊢\phi \to \log M\in {ℝ}^{+}$$
49	45 48	rerpdivcld	$$⊢\phi \to \frac{\log N}{\log M}\in ℝ$$
50	12 49	eqeltrid	$$⊢\phi \to U\in ℝ$$
51	43 50	rpcxpcld	$$⊢\phi \to T^U\in {ℝ}^{+}$$
52	21 51	rerpdivcld	$$⊢\phi \to \frac{F\left(N\right)}{T^U}\in ℝ$$
53	46 34	remulcld	$$⊢\phi \to MT\in ℝ$$
54		peano2re	$$⊢U\in ℝ\to U+1\in ℝ$$
55	50 54	syl	$$⊢\phi \to U+1\in ℝ$$
56	53 55	remulcld	$$⊢\phi \to MT\left(U+1\right)\in ℝ$$
57	1 2 3 4 5 6 7 8 9 10 11 12	ostth2lem3	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to {\left(\frac{F\left(N\right)}{T^U}\right)}^n\le nMT\left(U+1\right)$$
58	52 56 57	ostth2lem1	$$⊢\phi \to \frac{F\left(N\right)}{T^U}\le 1$$
59	21 36 51	ledivmuld	$$⊢\phi \to \left(\frac{F\left(N\right)}{T^U}\le 1\leftrightarrow F\left(N\right)\le T^U\cdot 1\right)$$
60	58 59	mpbid	$$⊢\phi \to F\left(N\right)\le T^U\cdot 1$$
61	51	rpcnd	$$⊢\phi \to T^U\in ℂ$$
62	61	mulridd	$$⊢\phi \to T^U\cdot 1=T^U$$
63	60 62	breqtrd	$$⊢\phi \to F\left(N\right)\le T^U$$
64	63	adantr	$$⊢\left(\phi \wedge F\left(M\right)\le 1\right)\to F\left(N\right)\le T^U$$
65		iftrue	$$⊢F\left(M\right)\le 1\to if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)=1$$
66	11 65	eqtrid	$$⊢F\left(M\right)\le 1\to T=1$$
67	66	oveq1d	$$⊢F\left(M\right)\le 1\to T^U=1^U$$
68	50	recnd	$$⊢\phi \to U\in ℂ$$
69	68	1cxpd	$$⊢\phi \to 1^U=1$$
70	67 69	sylan9eqr	$$⊢\left(\phi \wedge F\left(M\right)\le 1\right)\to T^U=1$$
71	64 70	breqtrd	$$⊢\left(\phi \wedge F\left(M\right)\le 1\right)\to F\left(N\right)\le 1$$
72	24 71	mtand	$$⊢\phi \to \neg F\left(M\right)\le 1$$
73		ltnle	$$⊢\left(1\in ℝ\wedge F\left(M\right)\in ℝ\right)\to \left(1<F\left(M\right)\leftrightarrow \neg F\left(M\right)\le 1\right)$$
74	13 31 73	sylancr	$$⊢\phi \to \left(1<F\left(M\right)\leftrightarrow \neg F\left(M\right)\le 1\right)$$
75	72 74	mpbird	$$⊢\phi \to 1<F\left(M\right)$$
76	35 36 21 38 7	lttrd	$$⊢\phi \to 0<F\left(N\right)$$
77	21 76	elrpd	$$⊢\phi \to F\left(N\right)\in {ℝ}^{+}$$
78	77	reeflogd	$$⊢\phi \to {\mathrm{e}}^{\log F\left(N\right)}=F\left(N\right)$$
79		iffalse	$$⊢\neg F\left(M\right)\le 1\to if\left(F\left(M\right)\le 1,1,F\left(M\right)\right)=F\left(M\right)$$
80	11 79	eqtrid	$$⊢\neg F\left(M\right)\le 1\to T=F\left(M\right)$$
81	72 80	syl	$$⊢\phi \to T=F\left(M\right)$$
82	81	oveq1d	$$⊢\phi \to T^U={F\left(M\right)}^U$$
83	31	recnd	$$⊢\phi \to F\left(M\right)\in ℂ$$
84	35 36 31 38 75	lttrd	$$⊢\phi \to 0<F\left(M\right)$$
85	31 84	elrpd	$$⊢\phi \to F\left(M\right)\in {ℝ}^{+}$$
86	85	rpne0d	$$⊢\phi \to F\left(M\right)\ne 0$$
87	83 86 68	cxpefd	$$⊢\phi \to {F\left(M\right)}^U={\mathrm{e}}^{U\log F\left(M\right)}$$
88	82 87	eqtr2d	$$⊢\phi \to {\mathrm{e}}^{U\log F\left(M\right)}=T^U$$
89	63 78 88	3brtr4d	$$⊢\phi \to {\mathrm{e}}^{\log F\left(N\right)}\le {\mathrm{e}}^{U\log F\left(M\right)}$$
90	77	relogcld	$$⊢\phi \to \log F\left(N\right)\in ℝ$$
91	85	relogcld	$$⊢\phi \to \log F\left(M\right)\in ℝ$$
92	50 91	remulcld	$$⊢\phi \to U\log F\left(M\right)\in ℝ$$
93		efle	$$⊢\left(\log F\left(N\right)\in ℝ\wedge U\log F\left(M\right)\in ℝ\right)\to \left(\log F\left(N\right)\le U\log F\left(M\right)\leftrightarrow {\mathrm{e}}^{\log F\left(N\right)}\le {\mathrm{e}}^{U\log F\left(M\right)}\right)$$
94	90 92 93	syl2anc	$$⊢\phi \to \left(\log F\left(N\right)\le U\log F\left(M\right)\leftrightarrow {\mathrm{e}}^{\log F\left(N\right)}\le {\mathrm{e}}^{U\log F\left(M\right)}\right)$$
95	89 94	mpbird	$$⊢\phi \to \log F\left(N\right)\le U\log F\left(M\right)$$
96	45	recnd	$$⊢\phi \to \log N\in ℂ$$
97	91	recnd	$$⊢\phi \to \log F\left(M\right)\in ℂ$$
98	48	rpcnd	$$⊢\phi \to \log M\in ℂ$$
99	48	rpne0d	$$⊢\phi \to \log M\ne 0$$
100	96 97 98 99	div12d	$$⊢\phi \to \log N\left(\frac{\log F\left(M\right)}{\log M}\right)=\log F\left(M\right)\left(\frac{\log N}{\log M}\right)$$
101	12	oveq2i	$$⊢\log F\left(M\right)U=\log F\left(M\right)\left(\frac{\log N}{\log M}\right)$$
102	100 101	eqtr4di	$$⊢\phi \to \log N\left(\frac{\log F\left(M\right)}{\log M}\right)=\log F\left(M\right)U$$
103	97 68	mulcomd	$$⊢\phi \to \log F\left(M\right)U=U\log F\left(M\right)$$
104	102 103	eqtrd	$$⊢\phi \to \log N\left(\frac{\log F\left(M\right)}{\log M}\right)=U\log F\left(M\right)$$
105	95 104	breqtrrd	$$⊢\phi \to \log F\left(N\right)\le \log N\left(\frac{\log F\left(M\right)}{\log M}\right)$$
106	91 48	rerpdivcld	$$⊢\phi \to \frac{\log F\left(M\right)}{\log M}\in ℝ$$
107	16	nnred	$$⊢\phi \to N\in ℝ$$
108	15	simprd	$$⊢\phi \to 1<N$$
109	107 108	rplogcld	$$⊢\phi \to \log N\in {ℝ}^{+}$$
110	90 106 109	ledivmuld	$$⊢\phi \to \left(\frac{\log F\left(N\right)}{\log N}\le \frac{\log F\left(M\right)}{\log M}\leftrightarrow \log F\left(N\right)\le \log N\left(\frac{\log F\left(M\right)}{\log M}\right)\right)$$
111	105 110	mpbird	$$⊢\phi \to \frac{\log F\left(N\right)}{\log N}\le \frac{\log F\left(M\right)}{\log M}$$
112	111 8 10	3brtr4g	$$⊢\phi \to R\le S$$
113	75 112	jca	$$⊢\phi \to \left(1<F\left(M\right)\wedge R\le S\right)$$