Theorem metakunt29 40150

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)

Hypotheses

Ref	Expression
metakunt29.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt29.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt29.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)
metakunt29.4	⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
metakunt29.5	⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
metakunt29.6	⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
metakunt29.7	⊢ (𝜑 → ¬ 𝑋 = 𝐼)
metakunt29.8	⊢ (𝜑 → 𝑋 < 𝐼)
metakunt29.9	⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
metakunt29.10	⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)

Assertion

Ref	Expression
metakunt29	⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Distinct variable groups:   𝑦,𝐻   𝑦,𝐼   𝑧,𝐼   𝑥,𝑀   𝑦,𝑀   𝑧,𝑀   𝑥,𝑋   𝑦,𝑋   𝑧,𝑋   𝜑,𝑥   𝜑,𝑦   𝜑,𝑧

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑧)   𝐶(𝑥,𝑦,𝑧)   𝐻(𝑥,𝑧)   𝐼(𝑥)

Proof of Theorem metakunt29

Step	Hyp	Ref	Expression
1		metakunt29.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
2		metakunt29.2	. . . 4 ⊢ (𝜑 → 𝐼 ∈ ℕ)
3		metakunt29.3	. . . 4 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
4		metakunt29.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (1...𝑀))
5		metakunt29.5	. . . 4 ⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))
6		metakunt29.6	. . . 4 ⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼)))))
7		metakunt29.7	. . . 4 ⊢ (𝜑 → ¬ 𝑋 = 𝐼)
8		metakunt29.8	. . . 4 ⊢ (𝜑 → 𝑋 < 𝐼)
9	1, 2, 3, 4, 5, 6, 7, 8	metakunt27 40148	. . 3 ⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼)))
10	9	fveq2d 6775	. 2 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼))))
11		metakunt29.9	. . . 4 ⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))
12	11	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))))
13		elfznn 13284	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ)
14	4, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℕ)
15		nnre 11980	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℕ → 𝑋 ∈ ℝ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
17	1	nnred 11988	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
18	2	nnred 11988	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
19	17, 18	resubcld 11403	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ)
20	16, 19	readdcld 11005	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
21	16	recnd 11004	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
22	17	recnd 11004	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
23	18	recnd 11004	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
24	21, 22, 23	addsub12d 11355	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼)))
25	22, 23, 21	subsub2d 11361	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼)))
26	18, 16	resubcld 11403	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ)
27	16, 18	posdifd 11562	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋)))
28	8, 27	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐼 − 𝑋))
29	26, 28	elrpd 12768	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ+)
30	17, 29	ltsubrpd 12803	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀)
31	25, 30	eqbrtrrd 5103	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀)
32	24, 31	eqbrtrd 5101	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀)
33	20, 32	ltned 11111	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
34	33	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)
35		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
36	35	neeq1d 3005	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀))
37	34, 36	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀)
38	37	neneqd 2950	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀)
39	38	iffalsed 4476	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))
40		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
41	18	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ)
42	16	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ)
43	17	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ)
44	43, 41	resubcld 11403	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ)
45	42, 44	readdcld 11005	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ)
46	41, 45	lenltd 11121	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
47	40, 46	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
48	47	3adant2 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)
49		simp2 1136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
50	49	breq1d 5089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
51	50	notbid 318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
52	48, 51	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼)
53	52	iffalsed 4476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
54	49	oveq1d 7286	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1))
55	53, 54	eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1))
56		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
57	56	iftrued 4473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1)
58	57	eqcomd 2746	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
59		metakunt29.10	. . . . . . . . 9 ⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)
60	58, 59	eqtr4di 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻)
61	60	oveq2d 7287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
62	55, 61	eqtrd 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
63	62	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
64	20, 18	ltnled 11122	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))))
65	64	biimprd 247	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼))
66	65	imp 407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
67	66	3adant2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)
68		simp2 1136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼)))
69	68	breq1d 5089	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼))
70	67, 69	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼)
71	70	iftrued 4473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦)
72	21	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ)
73	22	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ)
74	23	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ)
75	73, 74	subcld 11332	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ)
76	72, 75	addcld 10995	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ)
77	76	addid1d 11175	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼)))
78	77	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0))
79	64	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))
80	79	iffalsed 4476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0)
81	80	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
82	59	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
83	82	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻)
84	81, 83	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻)
85	84	oveq2d 7287	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
86	78, 85	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
87	86	ex 413	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
88	65, 87	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)))
89	88	imp 407	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
90	89	3adant2 1130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
91	68, 90	eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
92	71, 91	eqtrd 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
93	92	3expa 1117	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
94	63, 93	pm2.61dan 810	. . . 4 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
95	39, 94	eqtrd 2780	. . 3 ⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
96		1zzd 12351	. . . 4 ⊢ (𝜑 → 1 ∈ ℤ)
97	1	nnzd 12424	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98	14	nnzd 12424	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℤ)
99	2	nnzd 12424	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
100	97, 99	zsubcld 12430	. . . . 5 ⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ)
101	98, 100	zaddcld 12429	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
102		1p0e1 12097	. . . . 5 ⊢ (1 + 0) = 1
103		1red 10977	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
104		0red 10979	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
105	14	nnge1d 12021	. . . . . 6 ⊢ (𝜑 → 1 ≤ 𝑋)
106	17, 18	subge0d 11565	. . . . . . 7 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀))
107	3, 106	mpbird 256	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼))
108	103, 104, 16, 19, 105, 107	le2addd 11594	. . . . 5 ⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼)))
109	102, 108	eqbrtrrid 5115	. . . 4 ⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼)))
110	20, 17, 32	ltled 11123	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀)
111	96, 97, 101, 109, 110	elfzd 13246	. . 3 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀))
112	111	elfzelzd 13256	. . . 4 ⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ)
113		0zd 12331	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
114	96, 113	ifcld 4511	. . . . 5 ⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)
115	59	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))
116	115	eleq1d 2825	. . . . 5 ⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ))
117	114, 116	mpbird 256	. . . 4 ⊢ (𝜑 → 𝐻 ∈ ℤ)
118	112, 117	zaddcld 12429	. . 3 ⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ)
119	12, 95, 111, 118	fvmptd 6879	. 2 ⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))
120	10, 119	eqtrd 2780	1 ⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1542   ∈ wcel 2110   ≠ wne 2945  ifcif 4465   class class class wbr 5079   ↦ cmpt 5162  ‘cfv 6432  (class class class)co 7271  ℂcc 10870  ℝcr 10871  0cc0 10872  1c1 10873   + caddc 10875   < clt 11010   ≤ cle 11011   − cmin 11205  ℕcn 11973  ℤcz 12319  ...cfz 13238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-om 7707  df-1st 7824  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12582  df-rp 12730  df-fz 13239

This theorem is referenced by:  metakunt31  40152